50 Years of Satisfiability: The Centrality of SAT in the Theory of Computing
2021-02-11..2021-05-13
-- online --
[Satisfiability: Theory, Practice, and Beyond 2023, Proof Complexity and Meta-Mathematics 2023, Fine-Grained Complexity and Algorithm Design Boot Camp 2015, Satisfiability Lower Bounds and Tight Results for Parameterized and Exponential-Time Algorithms, Symmetry, Logic, Computation 2016, Connections Between Algorithm Design and Complexity Theory]
who it's for
complexity theorists, proof complexity researchers, theoretical computer scientists, sat solver developers, automated reasoning engineers, formal verification engineers, constraint satisfaction researchers
topics
strong exponential time hypothesis; exponential-time reductions; proof systems and automatizability; cdcl and resolution connections; symbolic satisfiability with bdd/add; belief and survey propagation; knowledge compilation and treewidth; interpolation and lifting techniques; total function problems in polynomial hierarchy; quantified invariants and symmetry (ic3po)
| title | author | length |
|---|---|---|
| Existentially Polytime Theorems | Jack Edmonds | 55m |
Defines an EP theorem as “for every x there exists y” with |y| poly(|x|) and claims NP∩coNP theorems should have polytime witnesses (conjectures factoring fits… | ||
| Hypotheses about Satisfiability and their Consequences | Russell Impagliazzo | 01h 23m |
Proposes the Exponential Time Hypothesis (3‑SAT needs 2^{c n} time for some c>0) and the Strong ETH (limiting exponent →1), proves a sparsification lemma that… | ||
| Total Function Problems in the Polynomial Hierarchy | Christos Papadimitriou | 51m |
Defines total search problems beyond NP, locates a new union‑bound class (PEP/APEP) and proposes the circuit‑complexity construction "complexity" as the… | ||
| On the Usefulness of the Strong Exponential Time Hypothesis | Ryan Williams | 01h 07m |
Argues Strong Exponential Time Hypothesis is likely false while conceding uncertainty, and shows that chasing that refutation yields concrete results… | ||
| On Symmetry and Quantification: A New Approach to Verify Distributed Protocols | Karem Sakallah | 56m |
Claims that symmetry→quantification yields compact, automatically derived inductive invariants for unbounded parameterized protocols, implemented as an IC3… | ||
| Progress in Symbolic Satisfiability Solving | Moshe Vardi | 52m |
Field-wide claim: CDCL remains the single algorithmic backbone, tied to resolution (the weakest proof system) despite scaling SAT to industrial instances with… | ||
| The Dawn of Computational Complexity Theory | Dick Karp | 55m |
Starts from Cook 1971 proving satisfiability’s central role and shows a concrete method: polynomial-time reductions that tie many problems’ fate to SAT… | ||
| Are we aging well? | Avi Wigderson | 01h 00m |
Field argues it's aging brilliantly but uneasy; core technical claim is that a noncommutative/quantum variant of polynomial identity testing (PIT) admits a… | ||
| Belief and Survey Propagation | Amin Coja-Oghlan | 01h 18m |
Experimental survey propagation beats classic solvers on random 4‑SAT but later analysis shows the message‑passing decimation idea stalls roughly a factor K… | ||
| Information Efficiency of Proof Systems | Jan Krajicek | 51m |
Defines an instance measure using Levin time-bounded Kolmogorov complexity that assigns I(tau) to each tautology and proves two core facts: any proof search… | ||
| Proofs and Circuits: Connections via Interpolation and Lifting | Susanna de Rezende | 51m |
Proves equivalence between DAG-like communication for the Karchmer–Wigderson game and circuit size, extracts a protocol from a resolution refutation, and uses… | ||
| Short Proofs in Strong Proof Systems | Marijn Heule | 01h 00m |
Claims that stronger, interference-based clausal proof systems let SAT solvers produce exponentially shorter certificates than resolution, using techniques… | ||
| SAT for Optimization | Fahiem Bacchus | 57m |
SAT for optimization frames optimization as repeated SAT decision queries (encode feasibility plus objective ≤ Q) and shows MaxSAT as the practical formalism… | ||
| Branching on Formulas: A Perspective From Knowledge Compilation | Adnan Darwiche | 55m |
Claims that branching on formulas (not just variables) gives exponential savings and that knowledge compilation provides the right lens. Uses DNNF… | ||
| Classifying the Complexity of SAT and CSP: Are we there yet? | Andrei Krokhin | 01h 10m |
Classifies when finite-domain SAT/CSP are tractable versus NP-complete by pinning complexity to actual algebraic symmetries: polymorphisms control gadget… | ||
| Complexity and Diversity | Les Valiant | 45m |
Argues that modular counting for SAT resists one-shot determinant-style reductions by combining counting with linear algebra constraints: the Grassmann‑Plücker… | ||
| Where The Really Hard Problems Really Are? | Lenka Zdeborova | 01h 00m |
Random k‑SAT shows sharp satisfiability transitions at a clause‑to‑variable ratio α and statistical‑physics methods (notably survey propagation and belief… | ||
| Strict NP: Expressive Power, Structure, and Complexity | Phokion Kolaitis | 59m |
Defines Strict NP (SNP) as the fragment of existential second‑order logic with only universal first‑order quantifiers and shows SNP is a proper subset of ESO… | ||
| Constraint Satisfaction and Expansion | Irit Dveer Dinur | 01h 01m |
PCP-based reductions produce instances whose value is either 1 or bounded away from 1 (classically 7/8 for 3-SAT), using two routes: an algebraic encoding into… | ||
| Symmetric Properties and Boolean Complexity | Alasdair Urquhart | 01h 04m |
Claim: a proposed P≠NP proof uses solution-space fragmentation (statistical‑physics clustering results of Achlioptas and Ricci‑Tersenghi plus finite‑model… | ||
| Cooperative Competition: A New Way of Solving SAT and other NP-Hard Problems in AI and Beyond | Holger H. Hoos | 01h 07m |
Argues that competitions should reward contribution to team performance by automatically building per-instance selectors over submitted solvers; implements the… | ||
| On Time, and Space, and Width, and Depth | Sasha Razborov | 55m |
Asserts that many resolution measures collapse into a small structural picture: up to log and quasi‑polynomial factors, log of resolution size is bounded by… | ||
| A Personal History of Practical SAT Solving | Armin Biere | 58m |
A personal timeline shows concrete leaps: QSAT solved far more instances in SAT Comp 2020, driven by integrating local search plus target phases into a CDCL… | ||
| nothing matches | ||