constraint-programmingsatsat-solvers

Unsat core in Minisat


Is there any API call in minisat to extract unsat core or any other method for the same.

I want to extract the unsat core for every invocation of the solver and then work on the unsat core.


Solution

  • MiniSat is quite an old program at this point. At the very least, you should look into one of the solvers entered into a recent SAT competition, e.g. Glucose. The competitions have required SAT solvers to emit DRAT proofs of unsatisfiability since 2013. Run whichever solver you choose and have it dump its DRAT proof into proof.out. Feed proof.out into the drat-trim utility with the -c option, which will produce an UNSAT core in DIMACS format. I.e.

    drat-trim originalproblem.cnf proof.out -c core.cnf
    

    Note that you don't have to use a MiniSat clone; any modern solver that emits DRAT proofs can have its proof fed into drat-trim to yield an UNSAT core.