[Proof Complexity] New preprint

[Iddo Tzameret]

Dear colleagues,

A new preprint of mine, titled
"On Sparser Random 3SAT Refutation Algorithms and Feasible Interpolation"
is available at: http://iiis.tsinghua.edu.cn/~tzameret/AutFKO.pdf
Comments, corrections, and suggestions are appreciated.


Best wishes,

Iddo Tzameret

--------------------------------------
Abstract: We formalize a combinatorial principle, called the 3XOR 
principle, due to Feige, Kim
and Ofek [FKO06], as a family of unsatisfiable propositional formulas 
for which refutations
of small size in any propositional proof system that possesses the 
feasible interpolation
property imply an efficient deterministic refutation algorithm for 
random 3SAT with n
variables and Ω(n^{1.4}) clauses. Such small size refutations would 
improve the current best
(with respect to the clause density) efficient refutation algorithm, 
which works only for
Ω(n^{1.5}) many clauses [FO07].

We then study the proof complexity of the above formulas in weak 
extensions of cutting
planes and resolution. Specifically, we show that there are 
polynomial-size refutations
of the 3XOR principle in resolution operating with disjunctions of 
quadratic equations
(with small integer coefficients), denoted R(quad). We show that R(quad) 
is weakly
automatizable iff R(lin) is weakly automatizable, where R(lin) is 
similar to R(quad) but with
linear instead of quadratic equations (introduced in [RT08]). This 
reduces the question of the
existence of efficient deterministic refutation algorithms for random 
3SAT with n variables
and Ω(n^{1.4}) clauses to the question of feasible interpolation of 
R(quad) and to the weak
automatizability of R(lin).