On tackling the limits of resolution in SAT solving

Alexey Ignatiev, Antonio Morgado, Joao Marques-Silva

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

21 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationTheory and Applications of Satisfiability Testing – SAT 2017
Subtitle of host publication20th International Conference Melbourne, VIC, Australia, August 28 – September 1, 2017 Proceedings
EditorsSerge Gaspers, Toby Walsh
Place of PublicationCham Switzerland
PublisherSpringer
Pages164-183
Number of pages20
ISBN (Electronic)9783319662633
ISBN (Print)9783319662626
DOIs
Publication statusPublished - 2017
Externally publishedYes
EventInternational Conference on Theory and Applications of Satisfiability Testing 2017 - Melbourne, Australia
Duration: 28 Aug 20171 Sep 2017
Conference number: 20th
http://sat2017.gitlab.io/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume10491
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Conference on Theory and Applications of Satisfiability Testing 2017
Abbreviated titleSAT 2017
Country/TerritoryAustralia
CityMelbourne
Period28/08/171/09/17
Internet address

Cite this