[Proof Complexity] Preprint
Neil Thapen
thapen at math.cas.cz
Wed Nov 9 16:35:52 CET 2016
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
More information about the Proof-Complexity
mailing list