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.


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.


For the Java world: Sat4j also has a MUS extraction tool, buried in the org.sat4j.tools package.

AllMUSes musFinder = new AllMUSes(SolverFactory.instance());
ISolver solver = musFinder.getSolverInstance();

// add clauses to solver . . .

List<IVecInt> muses = musFinder.computeAllMUSes();

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.