On tackling the limits of resolution in SAT solving

DOI10.1007/978-3-319-66263-3_11zbMATH Open1496.68368arXiv1705.01477OpenAlexW2963321374MaRDI QIDQ1680253FDOQ1680253

Authors: A. A. Ignatiev, Antonio Morgado, Joao Marques-Silva 

Publication date: 15 November 2017

Abstract: The practical success of Boolean Satisfiability (SAT) solvers stems from the CDCL (Conflict-Driven Clause Learning) approach to SAT solving. However, from a propositional proof complexity perspective, CDCL is no more powerful than the resolution proof system, for which many hard examples exist. This paper proposes a new problem transformation, which enables reducing the decision problem for formulas in conjunctive normal form (CNF) to the problem of solving maximum satisfiability over Horn formulas. Given the new transformation, the paper proves a polynomial bound on the number of MaxSAT resolution steps for pigeonhole formulas. This result is in clear contrast with earlier results on the length of proofs of MaxSAT resolution for pigeonhole formulas. The paper also establishes the same polynomial bound in the case of modern core-guided MaxSAT solvers. Experimental results, obtained on CNF formulas known to be hard for CDCL SAT solvers, show that these can be efficiently solved with modern MaxSAT solvers.

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

Recommendations

• Propositional SAT solving
• On the power of clause-learning SAT solvers as resolution engines
• Empirical study of the anatomy of modern SAT solvers
• Present and Future of Practical SAT Solving
• Anatomy and empirical evaluation of modern SAT solvers

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational aspects of satisfiability (68R07)

Cited In (15)

• Title not available (Why is that?)
• Bounds on the size of PC and URC formulas
• Propositional proof systems based on maximum satisfiability
• MaxSAT Resolution and Subcube Sums
• Theory and Applications of Satisfiability Testing
• Solving the resolution-free SAT problem by submodel propagation in linear time
• Learning a propagation complete formula
• NAE-resolution: A new resolution refutation technique to prove not-all-equal unsatisfiability
• Theory and Applications of Satisfiability Testing
• MaxSAT resolution for regular propositional logic
• Circular (Yet Sound) Proofs in Propositional Logic
• Polynomial calculus for optimization
• SAT-solving based on boundary point elimination
• SAT and SMT are still resolution: questions and challenges
• Long proofs of (seemingly) simple formulas

Uses Software

• CPLEX
• PicoSAT
• Sat4j
• QMaxSAT
• Open-WBO
• LMHS

This page was built for publication: On tackling the limits of resolution in SAT solving

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