5
$\begingroup$

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.

$\endgroup$
3

3 Answers 3

4
$\begingroup$

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.

$\endgroup$
0
$\begingroup$

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();
$\endgroup$
0
$\begingroup$

Minisat and Z3 have the same hack to extract unsat cores. I found the Z3 example easy to understand. The link is here:

https://github.com/Z3Prover/z3/blob/master/examples/c%2B%2B/example.cpp

There are about 4 examples on extracting unsat cores. You can use the code as is by modifying the assertions, if you like C++.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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