## 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: | 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). |

Pages: | 15 |

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

Paper: |