Refutation of Products of Linear Polynomials

Authors: Jan Horacek and Martin Kreuzer

Paper Information

Title:Refutation of Products of Linear Polynomials
Authors:Jan Horacek and Martin Kreuzer
Proceedings:SCSC Papers
Editors: Anna Maria Bigatti and Martin Brain
Keywords:linear clauses, Boolean polynomials, algebraic proof systems, SAT solving

ABSTRACT. In this paper we consider formulas that are conjunctions of linear clauses, i.e., of linear equations. Such formulas are very interesting because they encode CNF constraints that are typically very hard for SAT solvers. We introduce a new proof system SRES that works with linear clauses and show that SRES is implicationally and refutationally complete. Algebraically speaking, linear clauses correspond to products of linear polynomials over a ring of Boolean polynomials. That is why SRES can certify if a product of linear polynomials lies in the ideal generated by some other such products, i.e., the SRES calculus decides the ideal membership problem. Furthermore, an algorithm for certifying inconsistent systems of the above shape is described. We also establish the connection with an another combined proof system R(lin).

Talk:Jul 11 16:00 (Session 67F: Research papers)