Information Efficiency of Proof Systems
Talkat 50 Years of Satisfiability: The Centrality of SAT in the Theory of Computing · 2021-02-11..05-13
summary
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 needs time Omega(2^{I(tau)}) and a universal universal search procedure finds a proof in time polynomially above 2^{I(tau)} (this is called information automatizability). Gives a reduction linking P-optimal proof systems to time-optimal proof search under mild closure assumptions, constructs candidate hard families from one‑way permutations and PRGs (hypothesis‑based), and poses proving unconditional information lower bounds for specific formulas.
AI-written summary · about
chapters (15)
- 0:00Intro
- 2:12basics 1
- 6:52proof search alg's
- 9:36no new problem A natural quasi ordering
- 14:00doubts about
- 17:16information efficiency
- 19:30information and time
- 21:55information vs. size
- 23:29calculation 2
- 26:59example
- 29:08uses of size lower bounds
- 37:03non-uniform candidates Generators of proof complexity given
- 38:58references
- 43:11basics 3
- 45:14related topics in proof complexity