Sparser random 3-SAT refutation algorithms and the interpolation problem (extended abstract)

DOI10.1007/978-3-662-43948-7_84MaRDI QIDQ5167811zbMATH OpenOpenAlexFDO

Authors Iddo Tzameret

Publication date 1 July 2014

Published in Automata, Languages, and Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1305.0948

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25)

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 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(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 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).

Recommendations

• Short propositional refutations for dense random 3CNF formulas
• Automata, Languages and Programming
• Short propositional refutations for dense random 3CNF formulas
• Refuting random 3CNF formulas in propositional logic
• scientific article; zbMATH DE number 5899254

Cited in

(3)

• Refuting random 3CNF formulas in propositional logic
• A feasible interpolation for random resolution
• Short propositional refutations for dense random 3CNF formulas

This page was built for publication: Sparser random 3-SAT refutation algorithms and the interpolation problem (extended abstract)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5167811)