Hardness amplification in proof complexity
Hardness amplification in proof complexity
We present a general method for converting any family of unsatisfiable CNF formulas that is hard for one of the simplest proof systems -- tree resolution -- into formulas that require large rank in very strong proof systems, including any proof system that manipulates polynomials of degree at most k …