On the Dominance-Based Strengthening Rule
summary
Introduces a formalization of the dominance-based strengthening rule and proves it simulates polynomial local search (PLS) by encoding neighbors, initial solution and lexicographic order with extension axioms and substitutions; uses bounded arithmetic (PV, S2,2/T1,2) and extended Frege translations to construct EF proofs that iterate the neighbor function and derive a contradiction. The result is an effective equivalence between the dominance system and G1, showing the rule yields a system plausibly stronger than extended Frege and the simulation indeed succeeds.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 1:06Follow-up to Jakob’s talk
- 7:04Dominance rule soundness
- 13:24Proof complexity
- 18:12Jakob’s system position
- 21:50Simulating G1
- 31:41Summary
- 32:22Q&A
related talks
01h 00mAverage-case Complexity for Polynomials, and All That
54mConstraints, Gadgets, and Invariants
18mOn the Verification of a Subgraph Construction Algorithm
28mPro-Aperiodic Monoids via Saturated Models
49mPerfection and Beyond
34mLogic in Computer Science, Engineering and Industry
23mExtending Symmetric Circuits
01h 17mInapproximability of Constraint Satisfaction Problems III