Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Revision(s):

Revision #1 to TR13-070 | 25th February 2014 17:42

On Sparser Random 3-SAT Refutation Algorithms and the Interpolation Problem

RSS-Feed

Abstract:

We formalize a combinatorial principle, called the 3XOR principle, due to Feige, Kim and Ofek (2006), 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 3-SAT with $n$ variables and $\Omega(n^{1.4})$ clauses. Such small size refutations would improve the state of the art (with respect to the clause density) efficient refutation algorithm, which works only for $\Omega(n^{1.5})$ many clauses (Feige and Ofek (2007)).

We demonstrate polynomial-size refutations of the 3XOR principle in resolution operating with disjunctions of quadratic equations with small integer coefficients, denoted R(quad); this is a weak extension of cutting planes with small coefficients. We show that R(quad) is weakly automatizable iff R(line) is weakly automatizable, where R(lin) is similar to R(quad) but with linear instead of quadratic equations (introduced in Raz and Tzameret (2008)). This reduces the problem of refuting random 3CNF with $n$ variables and $\Omega(n^{1.4})$ clauses to the interpolation problem of R(quad) and to the weak automatizability of R(lin).



Changes to previous version:

Improved exposition. Minor corrections.


Paper:

TR13-070 | 4th May 2013 20:56

On Sparser Random 3SAT Refutation Algorithms and Feasible Interpolation


Abstract:

We formalize a combinatorial principle, called the 3XOR principle, due to Feige, Kim and Ofek (2006), 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 $\Omega(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 $\Omega(n^{1.5})$ many clauses (Feige and Ofek 2007).

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 (Raz and Tzameret 2008). This reduces the question of the existence of efficient deterministic refutation algorithms for random 3SAT with $n$ variables and $\Omega(n^{1.4})$ clauses to the question of feasible interpolation of R(quad) and to the weak automatizability of R(lin).



ISSN 1433-8092 | Imprint