Satisfiability Algorithms I
summary
Shows that combinatorial facts about K-CNF drive both algorithms and lower bounds: the satisfiability decoding lemma proves any K-CNF has at most 2^{n(1-1/K)} isolated solutions, which forces sigma-pi-sigma_K circuits for parity to need ~2^{n/K} bottom gates. Algorithmically, the PPZ method (unit-propagation plus random guessing) and its refined PP S Z variant that uses S-bounded resolution and a critical clause tree give the best-known k-SAT runtimes, yielding nontrivial savings over 2^n — asymptotically about 2^{n(1−Θ(1/K))} with Θ(1)≈1.64 in the limit.
AI-written summary · about
chapters (12)
- 0:00Intro
- 1:52Outline
- 2:21Motivation
- 5:12Connections to Other Circuit Models
- 15:04Critical Clauses
- 23:08Satisfiability Coding Lemma
- 24:39Maximum Number of Isolated Solutions
- 27:42Parity Lower Bound for General Depth-3 Circuits
- 29:50Lower Bound Proof
- 41:49PPZ Analysis
- 52:36PPSZ Analysis
- 57:09Improved Lower Bounds for Depth-3 Circuits
related talks
29mImproved Deterministic Algorithms for Sparse Max-SAT
17mSatisfiability Algorithms Based on Concentrated Shrinkage
01h 21mComputational Complexity in Theory and in Practice
25mLower Bounds for Problems Parameterized by Clique-width
33mUnification of SAT, Constraint Programming, and Pseudo-Boolean Solving: A Personal Story
01h 03mTrustworthy Automated Reasoning
31mFaster Satisfiability Algorithms for Systems of Polynomial Equations over Finite Fields and ACC^0[p]
23mTowards General and Tight Hardness Results for Graph Problems