The Hitting Proof System
summary
A hitting refutation is a partition of 0/1^n into subcubes where each subcube’s assignments all falsify a single clause; disjointness is certified by variable disagreements and coverage by summing subcube sizes to 2^n (muddle accounting). Verification reduces to checking a polynomial identity obtained by summing indicator monomials, certified using Raz–Shpilka PIT. Tree-like resolution quasi-polynomially simulates hitting (argument: a large subcube has ≤ log m fixed vars and eliminates many others), yielding a quasi-polynomial separation from tree-like resolution; whether full resolution simulates hitting remains open.
AI-written summary · about
chapters (9)
- 0:00Hitting proof system intro
- 2:45Hitting refutations
- 7:58Hitting vs tree-like resolution
- 11:49Separation from tree-like
- 15:02Relation to resolution
- 20:53Hitting simulation by EF
- 24:57Other similar systems
- 27:45Hitting plus variants
- 28:49Summary & Q&A
related talks
01h 17mInapproximability of Constraint Satisfaction Problems V
18mOn the Verification of a Subgraph Construction Algorithm
01h 00mThe Classification Program for Counting Problems I
01h 01mThe Gospel According to TCS
56mApproximate Counting II
55mThe Classification Program for Counting Problems III
01h 02mApproximate Counting I
01h 03mThe Classification Program for Counting Problems II