The intersection of computation and logic is both intellecually interesting and of tremendous practical significance.
Some of the most valuable theoretical developments in computing have come from this intersection:
A preview:
Our presentation will pull together material from various sources - see the references below. But most of it will come from [Marq1999], [Gome2008] and [Zhan2003].
Consider math equations:
x | x' |
T | F |
F | T |
x1 | x2 | x1 AND x2 |
T | T | T |
T | F | F |
F | T | F |
F | F | F |
x1 | x2 | x1 OR x2 |
T | T | T |
T | F | T |
F | T | T |
F | F | F |
Exercise: How many possible binary operators are there?
Can we find a solution?
Answer: Yes: x1 = F,
x2 = T, x3 = T
Note: this equation has more than one solution: x1 = F, x2 = T, x3 = F
Turns out: this has no solution
What about Boolean equations using operators other than AND/OR?
Consider DNF: Disjunctive Normal Form
Exercise: Give a polynomial-time algorithm to test whether a DNF expression is satisfiable.
Exercise:
Consider the CNF expression
(xa1 + xb1)
(xa2 + xb2)
...
(xan + xbn)
Other types of operators:
Applications:
The Cook-Levin theorem:
2-SAT:
Exercise: What edges do we get for the second clause?
Let's examine what this means when x1=T
Exercise: Add some clauses to make the above 2-CNF formula unsatisfiable.
The Davis-Putnam algorithm [Davi1960].
Exercise: Why is this true?
Algorithm Davis-Putnam (F) Input: A formula (set of clauses) F 1. if F has a unit-clause contradiction 2. return false // It must be unsatisfiable 3. endif 4. if F has single-phase variables 5. remove their clauses from F // Because we can make those clauses true 6. endif // Now eliminate a variable and add its resolvents 7. Pick a variable x from those remaining 8. F' = empty-set 9. for each (x+Ai) and (x+Bj) in F 10. if (Ai + Bj) is not tautological 11. Add (Ai + Bj) to F' 12. endif 13. endfor 14. Remove all clauses containing x or x' from F 15. F = F AND all clauses in F' 16. return Davis-Putnam (F)
The Davis-Putnam-Logemann-Loveland (DPLL) algorithm: [Davi1962].
Algorithm DPLL (F) Input: A formula (set of clauses) F defined using variables in a set V 1. if F is empty 2. return current assignment // Found a satisfying assignment. 3. endif 4. if F contains an empty clause 5. return null // Unsatisfiable. 6. endif // One variable => no choice, really, for that variable. 7. if F contains a clause c with only one variable v 8. Set the value of v to make c true // One TRUE variable is enough to make c TRUE 9. F' = F - c // Call DP recursively on the remaining clauses. 10. return DPLL(F') 11. endif // Try both TRUE and FALSE for an unassigned variable. 12. v = variable in V which has not been assigned a value // Try TRUE first 13. v = TRUE 14. F' = simplify F accounting for v's new value 15. if DPLL(F') is satisfiable 16. return current assignment 17. endif // OK, that didn't work. So try FALSE next. 18. v = FALSE 19. F' = simplify F accounting for v's new value 20. if DPLL(F') is satisfiable 21. return current assignment 22. else // If it can't be done with either, it's unsatisfiable. 23. return null 24. endif
1. check for end-of-recursion 2. propagate unit-clauses 3. explore
Exercise: How how DPLL can be written iterative (non-recursive) form.
Consider this approach to generating a random graph:
(Reproduced from: D.G.Mitchell, B.Selman, H.J.Levesque. Hard and easy distributions for SAT problems. Proc. Nat.Conf.AI, 1992).
State-based local search is an idea that works well for many combinatorial optimization problems:
An example:
x1 | x2 | x3 | x4 | x5 | # unsatisfied clauses |
|
Step 1: | T | T | F | T | F | 4 |
x1 → F results in 2 fewer unsatisfied clauses. x2 → F results in 1 fewer unsatisfied clauses. x3 → T results in 1 fewer unsatisfied clauses. x4 → F results in 2 fewer unsatisfied clauses. x5 → T results in 2 fewer unsatisfied clauses.
x1 | x2 | x3 | x4 | x5 | # unsatisfied clauses |
|
Step 1: | T | T | F | T | F | 4 |
Step 2: | F | T | F | T | F | 2 |
x1 → T results in -2 fewer unsatisfied clauses. x2 → F results in 2 fewer unsatisfied clauses. x3 → T results in 0 fewer unsatisfied clauses. x4 → F results in 1 fewer unsatisfied clauses. x5 → T results in 1 fewer unsatisfied clauses.
x1 | x2 | x3 | x4 | x5 | # unsatisfied clauses |
|
Step 1: | T | T | F | T | F | 4 |
Step 2: | F | T | F | T | F | 2 |
Step 3: | F | F | F | T | F | 0 |
Exercise: In the above approach, when do we know that a formula is NOT satisfiable?
More details:
Algorithm: Greedy-SAT (F) Input: a CNF formula F 1. for i=1 to maxTries 2. A = a randomly generated assignment 3. for j=1 to maxFlips 4. if A satisfies F 5. return A // Done. 6. endif 7. A = Greedy-Flip (A, F) 8. endfor 9. endfor // Give up. 10. return "No satisfying assignment found"
Algorithm: Greedy-Flip (A, F) Input: an assignment A and a CNF formula F // See how much each variable-flip independently reduces # unsatisfied clauses. 1. for k=1 to n 2. βk = reduction in unsatisfied clauses by flipping variable xk 3. endfor 4. Let xm be the variable with the maximum β value. 5. if βm > 0 // Create a new assignment with variable m flipped. 6. A = flip (A, m) 7. endif 8. return A
Exercise: Notice the condition β>0 in line 5 of Greedy-Flip. What would be the implication of making this β≥0?
Some improvements:
Algorithm: Random-Walk-SAT (F) Input: a CNF formula F 1. for i=1 to maxTries 2. A = a randomly generated assignment 3. for j=1 to maxFlips 4. if A satisfies F 5. return A 6. endif 7. if uniform() < p // With probability p 8. xk = a randomly selected variable in a randomly selected unsatisfied clause 9. flip (A, k) 10. else // With probability 1-p 11. Greedy-Flip (A, F) 12. endif 13. endfor 14. endfor
Algorithm: Walk-SAT (F) Input: a CNF formula F 1. for i=1 to maxTries 2. A = a randomly generated assignment 3. for j=1 to maxFlips 4. if A satisfies F 5. return A 6. endif 7. C = a randomly selected unsatisfied clause. 8. xk = the variable in C with the smallest b(xk) 9. if b(xk) = 0 10. flip (A, k) // Greedy move. 11. else if uniform() < 1-p 12. flip (A, k) // Alternative greedy move. 13. else // With probability p 14. xm = a randomly selected variable in C 15. flip (A, m) // Random walk move. 16. endif 17. endfor 18. endfor
Experimental results: (reported in [Selm1995])
Other algorithms:
loop identify possible neighbor states (with one or more flips) Pick one of the flips flip the assignment endloop
The above raises interesting questions about SAT instances:
A study about the importance of "greed" and "randomness" [Gent1993]:
Tuning algorithm parameters [McAl1997]:
The backbone of an instance: [Mona1999]:
Although modern SAT solvers vastly outperform DPLL (million variables vs. a few hundred), they are all based on DPLL itself.
First, let's re-write DPLL iteratively:
DPLL (F) 1. See if recursion has bottomed out (determine satisfiability) 2. Pursue unit-propagation to see if a contradiction occurs 3. if not 4. find an unassigned variable x 5. recurse with x=TRUE 6. if that didn't work, recurse with x=FALSE 7. endif
Algorithm: DPLL-Iterative (F) Input: A formula (set of clauses) F defined using variables in a set V 1. formulaStack.push (F) 2. while formulaStack not empty 3. status = deduce () // Pursue unit-clauses, and see if there's a conflict. 4. if status = SATISFIABLE 5. return assignment 6. else if status = CONFLICT 7. backtrack () 8. else 9. decideNextBranch () // status=CONTINUE so continue trying variable values. 10. endif 11. endwhile 12. return null // Unsatisfiable. deduce () 1. F = formulaStack.peek () 2. while there is a unit-clause // Pursue the chain of unit clauses. 3. set the clause's variable to make the clause TRUE 4. if contradiction found 5. return CONFLICT 6. endif 7. endwhile 8. if no more clauses 9. return SATISFIABLE 10. else 11. F' = simplified formula after unit clauses 12. replace F with F' on top of formulaStack 13. return CONTINUE 14. endif backtrack () 1. while true 2. F = formulaStack.pop () 3. v = variableStack.pop () 4. if v = TRUE // We've tried v=TRUE, and next need to try v=FALSE. 5. v = FALSE 6. F' = F simplified with v = FALSE 7. formulaStack.push (F') 8. variableStack.push (v) 9. return 10. endif 11. endwhile decideNextBranch () 1. F = formulaStack.pop () 2. v = a randomly selected unassigned variable 3. v = TRUE 4. F' = F simplifed with v=TRUE 5. formulaStack.push (F') 6. variableStack.push (v)
Main ideas in improving DPLL:
Let's now look at conflicts and clause learning in more detail:
Exercise: Simplify the clauses after these assignments. What remains? Also, after the assignment X6=1, what other assignments are forced?
At d=1: X1 ← 0 At d=2: X2 ← 1 At d=3: X3 ← 0 At d=4: X4 ← 0 At d=5: X5 ← 1
d=6: X6 ← 1 d=6: This forces X7=1 and X8=1 d=6: This in turn forces X9=1 d=6: This forces X10=1 d=6: This forces both X11=1 and X11=0 → A conflict!
Next, we will build an associated directed graph called an implication graph:
At d=3: X3 ← 0 At d=4: X4 ← 0 At d=5: X5 ← 1
Next, what does one do with the implication graph?
Non-chronological backtracking:
At d=1: X1 ← 0 At d=3: X3 ← 0 At d=4: X4 ← 0 At d=6: X6 ← 1
We'll now examine some ideas related to:
Let's start with decision variables:
Next, let's examine data structures:
How are all these ideas worked into DPLL?
Algorithm: DPLL-Iterative (F) Input: A formula (set of clauses) F defined using variables in a set V 1. formulaStack.push (F) 2. while formulaStack not empty 3. status = deduce () 4. if status = SATISFIABLE 5. return assignment 6. else if status = CONFLICT 7. backtrack () 8. else 9. decideNextBranch () 10. endif 11. endwhile 12. return null // Unsatisfiable.
The Satisfiability (SAT) problem is one of the most important problems in computer science:
What we learned about SAT solvers:
[WP-1]
Wikipedia entry on SAT.
[Sat-comp]
SAT competition page.
[Aspv1979]
B.Aspvall, M.F.Plass and R.E.Tarjan
A linear-time algorithm for testing the truth of certain
quantified boolean formulas.
Inf. Proc. Lett, 8:3, 1979, pp.121�V123.
[Auda2009]
The
Glucose solver. See
Predicting learnt clauses quality in modern SAT solvers.
IJCAI, 2009, pp.399-404.
[Bier2010]
A.Biere et al.
The PrecoSAT project website.
See also:
M.Jarvisalo, A.Biere, and M.Heule.
Blocked Clause Elimination,
TACAS, 2010.
[Davi1960]
M.Davis and H.Putnam.
A computing procedure for quantification theory.
J.ACM, 7:3, 1960, pp.201-215.
[Davi1962]
M.Davis, G.Logemann and D.Loveland.
A machine program for theorem proving.
Comm. ACM, 5:7, 1962, pp.394-397.
[Dubo2001]
O.Dubois and G.Dequen.
A backbone-search heuristic for efficient solving of hard 3-SAT formulae.
IJCAI, 2001.
[Een2003]
N.Een and N.Sorensson.
An extensible SAT solver.
SAT, 2003.
See the MiniSAT and SatELite website.
[Gebs2007]
M.Gebser, B.Kaufmann, A.Neumann, and T.Schaub.
CLASP: A Conflict-Driven Answer Set Solver,
LPNMR,
2007, pp.260-265.
See the Clasp project website.
[Gent1993]
I.P.Gent and T.Walsh.
Towards an Understanding of Hill-climbing Procedures for SAT.
AAAI, 1993, pp.28-33.
[Gome2008]
C.P.Gomes, H.Kautz, A.Sabharwal and B.Selman.
Satisfiability Solvers.
Chapter 2, Handbook of Knowledge Representation,
Elsevier 2008.
[Gu1997]
J.Gu, P.W.Purdom, J.Franco and B.Wah
Algorithms for the Satisfiability (SAT) Problem: A Survey.
In: "Satisfiability Problem: Theory and Applications",
DIMACS Series in Discrete Mathematics and Theoretical
Computer Science, American Mathematical Society, pp. 19-152, 1997.
[Li2005]
C.M.Li and W.Huang.
Diversification and Determinism in Local search
for Satisfiability,
SAT2005, St Andrews, UK, June 2005, Pages 158-172.
See the TNM Solver website.
[Marq1999]
J.Marques-Silva and K.A.Sakallah.
GRASP: A search algorithm for propositional satisfiability.
IEEE Trans. Comput., 48:5, 1999, pp.506-521.
[Marq2008]
J.Marques-Silva.
Practical Applications of Boolean Satisfiability.
In: Workshop on Discrete Event Systems (WODES'08),
May 2008, Goteborg, Sweden.
[McAl1997]
D.McAllester, B.Selman, and H.Kautz.
Evidence for Invariants in Local Search
Proc. AAAI-97, Providence, RI, 1997.
[Mitc2005]
D.G.Mitchell.
A SAT Solver Primer.
EATCS Bulletin (The Logic in Computer Science Column),
Vol.85, February 2005, pages 112-133.
[Mona1999]
R.Monasson, R.Zecchina, S.Kirkpatrick, B.Selman and L.Troyansky.
Determining computational complexity from characteristic `phase transitions'.
Nature, Vol. 400(8), 1999, pp.133--137.
[Mosk2001]
M.Moskewicz, C.Madigan, Y.Zhao, L.Zhang and S.Malik.
Chaff: Engineering an Efficient SAT Solver.
39th Design Automation Conference (DAC 2001),
Las Vegas, June 2001.
See the Chaff project website.
[Nude2004]
E.Nudelman, A.Devkar, Y.Shoham , K.Leyton-Brown and H.Hoos.
SATzilla: An Algorithm Portfolio for SAT.
Int.Conf. Theory and App. of SAT, 2004.
See also the
project website.
[Pipa2008]
K.Pipatsrisawat and A.Darwiche
A New Clause Learning Scheme for Efficient Unsatisfiability Proofs.
AAAI, 2008.
See the RSat project website.
[Selm1992]
B.Selman, H.Levesque and D.Mitchell.
A New Method for Solving Hard Satisfiability Problems.
AAAI, 1992, pp.440-446.
[Selm1995]
B.Selman, H.Kautz and B.Cohen.
Algorithms for the Satisfiability (SAT) Problem: A Survey.
DIMACS Series in Discrete Mathematics and Theoretical
Computer Science, American Mathematical Society, pp.521-532, 1995.
[Will2003]
R.Williams, C.Gomes and B.Selman.
Backdoors To Typical Case Complexity.
Proc. IJCAI-03, Acapulco, Mexico, 2003.
[Zhan2003]
L.Zhang.
Searching for truth: techniques for satisfiability of
Boolean formulas.
PhD thesis, Princeton University, 2003.
See also his
set of slides.