Non-Restarting SAT Solvers with Simple Preprocessing Can Efficiently Simulate Resolution

Authors

  • Paul Beame University of Washington
  • Ashish Sabharwal IBM Watson Research Center

DOI:

https://doi.org/10.1609/aaai.v28i1.9121

Keywords:

clause learning, restarts, preprocessing

Abstract

Propositional satisfiability (SAT) solvers based on conflict directed clause learning (CDCL) implicitly produce resolution refutations of unsatisfiable formulas. The precise class of formulas for which they can produce polynomial size refutations has been the subject of several studies, with special focus on the clause learning aspect of these solvers. The results, however, assume the use of non-standard and non-asserting learning schemes, or rely on polynomially many restarts for simulating individual steps of a resolution refutation, or work with a theoretical model that significantly deviates from certain key aspects of all modern CDCL solvers such as learning only one asserting clause from each conflict and other techniques such as conflict guided backjumping and phase saving. We study non-restarting CDCL solvers that learn only one asserting clause per conflict and show that, with simple preprocessing that depends only on the number of variables of the input formula, such solvers can polynomially simulate resolution. We show, moreover, that this preprocessing allows one to convert any CDCL solver to one that is non-restarting.

Downloads

Published

2014-06-21

How to Cite

Beame, P., & Sabharwal, A. (2014). Non-Restarting SAT Solvers with Simple Preprocessing Can Efficiently Simulate Resolution. Proceedings of the AAAI Conference on Artificial Intelligence, 28(1). https://doi.org/10.1609/aaai.v28i1.9121

Issue

Section

Main Track: Search and Constraint Satisfaction