[Proof Complexity] Preprint

[Neil Thapen]

Dear colleagues,

A new paper "Random resolution refutations" by Pavel Pudlak and myself is 
available on ECCC:
http://eccc.hpi-web.de/report/2016/175/

Abstract: We study the random resolution refutation system defined in
[Buss et al. 2014]. This attempts to capture the notion of a resolution 
refutation that may make mistakes but is correct most of the time. By 
proving the equivalence of several different definitions, we show that 
this concept is robust. On the other hand, if P!=NP, then random 
resolution cannot be polynomially simulated by any proof system in which 
correctness of proofs is checkable in polynomial time.

We prove several upper and lower bounds on the width and size of random 
resolution refutations of explicit and random unsatisfiable CNF formulas. 
Our main result is a separation between polylogarithmic width random 
resolution and quasipolynomial size resolution, which solves the problem 
stated in [Buss et al. 2014]. We also prove exponential size lower bounds 
on random resolution refutations of the pigeonhole principle CNFs, and of 
a family of CNFs which have polynomial size refutations in constant depth 
Frege.

Regards,

Neil Thapen