Satisfiability Algorithms Based on Concentrated Shrinkage
summary
Shows how concentrated shrinkage and a greedy restriction that repeatedly fixes the most frequent variable turn worstcase formula lower bound analyses into faster SAT solvers. Claims that after n − p n greedy steps most branches shrink by a factor near the shrinkage exponent (close to 2 for De Morgan formulas) so only a tiny fraction need brute force. Implements branching plus lookup-table memoization for sublinear residues to get improved running times (works up to formula sizes like n^{2.49}, with extensions to Max‑SAT and depth reductions).
AI-written summary · about
chapters (7)
- 0:00Intro
- 0:17Formula Lower Bound
- 1:22Shrinkage Exponenti
- 6:28Algorithmic Template
- 7:51Sparse MAX-SAT
- 13:09Sparse Depth-2 TC
- 15:19Other Examples
related talks
29mImproved Deterministic Algorithms for Sparse Max-SAT
27mProducing Shorter Congruence Closure Proofs in a State-of-the-Art SMT Solver
56mSatisfiability Algorithms II
01h 07mSatisfiability Algorithms I
13mProgram Analysis via Efficient Symbolic Abstraction
35mA Peek Inside SAT Solvers
19mAlgorithms and Lower Bounds for Comparator Circuits from Shrinkage
18mScalable Floating-Point Satisfiability via Staged Optimization