CS 172: Computability and ComplexitySAT: Typical-Case ComplexitySanjit A. SeshiaEECS, UC BerkeleyS. A. Seshia 2k-SAT• A SAT problem with input in CNF with at most k literals in each clause• Complexity for non-trivial values of k:– 2-SAT: in P– 3-SAT: NP-complete– > 3-SAT: ?S. A. Seshia 33-SAT: Complexity Bounds (circa 2006/07)• Obvious upper bound on run-time?– In terms of n, the number of Boolean variables• Best known deterministic upper bound1.473n• Best known randomized upper bound1.324n• Best known lower boundn1.801– If limited to sub poly spaceS. A. Seshia 4Worst-Case ComplexityS. A. Seshia 5Beyond Worst-Case Complexity• What we really care about is “typical-case”complexity• But how can one measure “typical-case”?• Two approaches:– Is your problem a restricted form of 3-SAT? That might be polynomial-time solvable– Experiment with (random) SAT instances and see how the solver run-time varies with formula parameters (#vars, #clauses, … )S. A. Seshia 6Special Cases of 3-SAT• You already know two poly-time solvable cases: – 2-SAT– Horn-SATS. A. Seshia 7Phase Transitions in k-SAT• Consider a fixed-length clause model– k-SAT means that each clause contains exactly k literals • Let SAT problem comprise m clauses and n variables– Randomly generate the problem for fixed k and varying m and n• Question: How does the problem hardness vary with m/n ?– Why is m/n interesting?S. A. Seshia 83-SAT HardnessAs n increases hardness transition grows sharperm / nS. A. Seshia 9Transition from SAT to UNSAT at m/n  4.3m / nS. A. Seshia 10Threshold Conjecture• For every k, there exists a c* such that– For m/n < c*, as n  ∞∞∞∞ , problem is satisfiablewith probability 1– For m/n > c*, as n  ∞∞∞∞ , problem is unsatisfiable with probability 1• Conjecture proved true for k=2 and c*=1• For k=3, current status is that c* is in the range 3.42 – 4.51S. A. Seshia 11The (2+p)-SAT Model• We know:– 2-SAT is in P– 3-SAT is NP-complete• Problems are (typically) a mix of binary and ternary clauses– Let p ∈ {0,1}– Let problem comprise (1-p) fraction of binary clauses and p of ternary– So-called (2+p)-SAT problemS. A. Seshia 12Experimentation with random (2+p)-SAT• When p < ~0.41– Problem behaves like 2-SAT– Linear scaling• When p > ~0.42– Problem behaves like 3-SAT– Exponential scalingS. A. Seshia 13Backbones and Backdoors• Backbone [Parkes; Monasson et al.]– Subset of literals that must be true in every satisfying assignment (if one exists)– Empirically related to hardness of problems• Backdoor [Williams, Gomes, Selman]– Subset of variables such that once you’ve given those a suitable assignment (if one exists), the rest of the problem is poly-time solvable– Also empirically related to hardness• But no easy way to find such backbones / backdoors! S. A. Seshia 14A Classification of SAT Algorithms• Davis-Putnam (DP)– Based on resolution• Davis-Logemann-Loveland (DLL/DPLL)– Search-based– Basis for current most successful solvers• Stalmarck’s algorithm– “Different” kind of search, proprietary algorithm• Stochastic search– Local search, hill climbing, etc.– Unable to prove unsatisfiability (incomplete)S. A. Seshia 15Resolution• Two CNF clauses that contain a variable x in opposite phases (polarities) imply a new CNF clause that contains all literals except x and x’• (a + b) (a’ + c) = (a + b)(a’ + c)(b + c)• Why is this true?S. A. Seshia 16The Davis-Putnam Algorithm• Iteratively select a variable x to perform resolution on• Retain only the newly added clauses and the ones not containing x• Termination: You either– Derive the empty clause (conclude UNSAT)– Or all variables have been selectedS. A. Seshia 17Resolution ExampleHow many clauses can you end up with?(at any iteration)S. A. Seshia 18Further Reading• Handbook of Satisfiability, IOS Press, published 2009.• Article on Phase Transitions in SAT (linked on