Hypotheses about Satisfiability and their Consequences
Talkat 50 Years of Satisfiability: The Centrality of SAT in the Theory of Computing · 2021-02-11..05-13
summary
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 reduces k‑SAT to linear‑clause instances in 2^{ε n} time, and shows those hypotheses imply tight barriers: subexponential SAT would collapse exact complexities across CSPs, yield N^{Ω(k)} hardness for k‑SUM, tie to orthogonal‑vectors lower bounds, and give circuit lower bounds; also proves matching lower bounds for many proof systems (tree/regular resolution) though general resolution remains open.
AI-written summary · about
chapters (16)
- 0:00Introduction
- 1:05Motivation for SAT algorithms
- 13:52Resolution proofs bottlenecks
- 17:53Exponential Time Hypothesis
- 22:14Strong ETH defined
- 26:33Why ETH and Strong ETH matter
- 31:05k-SAT and NP-complete equivalence
- 35:05Sparsification lemma for SAT/CSPs
- 46:52Hard instances for CSPs
- 50:31ETH for unique satisfiability
- 53:03Fine-grained complexity
- 57:33ETH and algorithmic problems
- 1:01:09Worst-case vs average-case SAT
- 1:03:00Resolution lower bounds
- 1:06:55Value of ETH
- 1:13:38Q&A