Sparser Random 3SAT Refutation Algorithms and the Interpolation Problem: Extended Abstract

Iddo Tzameret

Research output: Chapter in Book/Report/Conference proceedingConference contribution

113 Downloads (Pure)

Abstract

We formalize a combinatorial principle, called the 3XOR principle, due to Feige, Kim and Ofek [14], 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 state of the art (with respect to the clause density) efficient refutation algorithm, which works only for (n^1.5) many
clauses [15].

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(lin) is weakly automatizable, where R(lin) is similar to R(quad) but with linear instead of quadratic equations (introduced in [28]). This reduces the problem of refuting random 3CNF with n variables and (n^1.4) clauses to the interpolation problem
of R(quad) and to the weak automatizability of R(lin).
Original languageEnglish
Title of host publicationAutomata, Languages, and Programming - 41st International Colloquium, (ICALP) 2014, Copenhagen, Denmark, July 8-11, 2014, Proceedings, Part {I}
Subtitle of host publication--
Pages1015-1026
Number of pages12
Publication statusPublished - 8 Jul 2014

Publication series

NameLNCS

Cite this