(The following text has been copypasted to the SAT/SMT by example book.)
Instead of epigraph: There is a 350+ book from 2015 by Donald Knuth in the art of programming series on SAT. So the nerdiness of SAT has highest blessing.
It's a bit frustrating to get a depressing 'UNSAT' message from a SAT solver, and nothing else. What can you do for diagnostics? What can you do to fix your SAT instance? What can you do to unclog your (overconstrained) instance?
In my book I used UNSAT core generation in Z3 to get a list of conflicting cells in spreadsheet. Here I'll see what can be done for a SAT instance.
I'll use this problem from D.Knuth's TAOCP:
I'm assiging 1..7 SAT variables to t,u,v,w,x,y,z variables and translating this to a CNF file (lines prefixed with "c " are comments, of course):
p cnf 7 16 c variables: c 1 t c 2 u c 3 v c 4 w c 5 x c 6 y c 7 z c clauses. c first line (commented) is clause number and variable names. c second line: CNF clause c #1 -t -w -1 -4 0 c #2 -u -z -2 -7 0 c #3 u y 2 -6 0 c #4 u z 2 7 0 c #5 -y z -6 7 0 c #6 t -x 1 -5 0 c #7 t z 1 7 0 c #8 -x z -5 7 0 c #9 -t -z -1 -7 0 c #10 -v y -3 6 0 c #11 v -w 3 -4 0 c #12 v -y 3 -6 0 c #13 -w -y -4 -6 0 c #14 y x 2 5 0 c #15 -u v -2 3 0 c #16 -v -x -3 -5 0
The instance is UNSAT, of course. Now I'm running PicoMUS utility from Picosat SAT solver, that extracts MUS (Minimal Unsatisfiable Subformula):
c [picomus] WARNING: no output file given c [picomus] WARNING: PicoSAT compiled without trace generation c [picomus] WARNING: core extraction disabled s UNSATISFIABLE c [picomus] computed MUS of size 8 out of 16 (50%) v 2 v 4 v 5 v 6 v 9 v 10 v 14 v 15 v 0
This is a list of clauses. If all of them are removed from your instances, it will be transformed from UNSAT to SAT. Let's see, what are these clauses?
-2 -7 0 # 2 -u -z 2 7 0 # 4 u z -6 7 0 # 5 -y z 1 -5 0 # 6 t -x -1 -7 0 # 9 -t -z -3 6 0 # 10 -v y -2 3 0 # 15 -u v
These are indeed clauses with variables that are in the vicious cycle according to D.Knuth.
Note that MUS is not the smallest possible (sub)set, but just a set that you can use for diagnostics. 'Minimal' in MUS means that is cannot be reduced in its form. However, smallest MUSes are still possible to exist, but PicoMUS isn't guaranteed to find a smallest MUS.
Now there is another tool in Picosat: PicoMCS, that extracts MCS (Minimal Correction Subset). What can it say?
s UNSATISFIABLE v 10 0 v 14 0 v 15 0 v 2 0 v 5 0 v 6 0 v 8 4 0 v 9 0
Each line in list is a list of clauses. If a list of clauses is removed from your instances, it transforms from UNSAT to SAT. Indeed, 10th clause is an element of 'viciuos cycle'. And so is 15th, etc. But 14th clause is not. But removing it from the instance will solve the problem. Also, if 8th and 4th clauses are both to be removed from the instance, it will be SAT, but not one-by-one.
Why not always using PicoMCS instead of PicoMUS? It's way slower. And in practice, you can be satisfied with larger MUS.
Now what if we can represent each clause as weighted and use MaxSAT solver? (The same Open-WBO, I use so often.)
I prepend each clause with '1', that is a (smallest) weight of each clause:
p wcnf 7 16 1000 1 -1 -4 0 1 -2 -7 0 1 2 -6 0 1 2 7 0 1 -6 7 0 1 1 -5 0 1 7 0 1 -5 7 0 1 -1 -7 0 1 -3 6 0 1 3 -4 0 1 3 -6 0 1 -4 -6 0 1 2 5 0 1 -2 3 0 1 -3 -5 0
... and asking Open-WBO MaxSAT solver to find such an assignment, that can satisfy as many clauses, as possible:
s OPTIMUM FOUND v -1 2 3 -4 -5 6 7
Let's see, which clauses gets satisfied with this assignment? I manually added comments to the WCNF instance:
p wcnf 7 16 1000 1 -1 -4 0 # -t -w OK 1 -2 -7 0 # -u -z UNSAT 1 2 -6 0 # u y OK 1 2 7 0 # u z OK 1 -6 7 0 # -y z OK 1 1 -5 0 # t -x OK 1 1 7 0 # t z OK 1 -5 7 0 # -x z OK 1 -1 -7 0 # -t -z OK 1 -3 6 0 # -v y OK 1 3 -4 0 # v -w OK 1 3 -6 0 # v -y OK 1 -4 -6 0 # -w -y OK 1 2 5 0 # y x OK 1 -2 3 0 # -u v OK 1 -3 -5 0 # -v -x OK
The only 2nd clause is to be removed to break the 'vicious cycle'.
Again, MaxSAT solvers are way slower than MUS extractors. So they cannot be always used in practice.
Yes, I know about these lousy Disqus ads. Please use adblocker. I would consider to subscribe to 'pro' version of Disqus if the signal/noise ratio in comments would be good enough.