Just like the title says. I need to use a SAT solver on a series of CNF formulas
ID: 647676 • Letter: J
Question
Just like the title says. I need to use a SAT solver on a series of CNF formulas but not only do I need an answer of the type satisfiable/unsatisfiable but also some subset of clauses whose conjunction is still unsatisfiable (the unsatisfiability core).
I have read somewhere that it is possible to hack the code of some SAT solver (like MiniSAT) to produce UNSAT core, but I don't feel competent enough to actually do it. I was hoping that somebody else have already done it and have uploaded the code somewhere, but either that is not the case or I suck at Googling.
Explanation / Answer
MUSer2 is probably the tool for extracting minimal unsatisfiable cores (MUS) currently. It treats the SAT solver as a black box, so you can plug in any solver you want.
If you want a solver with MUS extraction capability, the newest version of PicoSAT comes with a utility tool PicoMUS that does the job
Related Questions
Navigate
Integrity-first tutoring: explanations and feedback only — we do not complete graded work. Learn more.