patternMinor
Are there any open source SAT solvers with UNSAT core extraction algorithm built in?
Viewed 0 times
satbuiltcoresolversaresourceopenanywithunsat
Problem
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.
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.
Solution
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.
If you want a solver with MUS extraction capability, the newest version of PicoSAT comes with a utility tool PicoMUS that does the job.
Context
StackExchange Computer Science Q#40276, answer score: 4
Revisions (0)
No revisions yet.