MaxSat resolution with the dual rail encoding

Maria Luisa Bonet, Sam Buss, Alexey Ignatiev, Joao Marques-Silva, Antonio Morgado

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

31 Citations (Scopus)

Abstract

Conflict-driven clause learning (CDCL) is at the core of the success of modern SAT solvers. In terms of propositional proof complexity, CDCL has been shown as strong as general resolution. Improvements to SAT solvers can be realized either by improving existing algorithms, or by exploiting proof systems stronger than CDCL. Recent work proposed an approach for solving SAT by reduction to Horn MaxSAT. The proposed reduction coupled with MaxSAT resolution represents a new proof system, DRMaxSAT, which was shown to enable polynomial time refutations of pigeonhole formulas, in contrast with either CDCL or general resolution. This paper investigates the DRMaxSAT proof system, and shows that DRMaxSAT p-simulates general resolution, that AC 0 -Frege+PHP p-simulates DRMaxSAT, and that DRMaxSAT can not p-simulate AC 0 -Frege+PHP or the cutting planes proof system.

Original languageEnglish
Title of host publicationThe Thirty-Second AAAI Conference on Artificial Intelligence
EditorsSheila McIlraith, Kilian Weinberger
Place of PublicationPalo Alto CA USA
PublisherAssociation for the Advancement of Artificial Intelligence (AAAI)
Pages6565-6572
Number of pages8
ISBN (Electronic)9781577358008
Publication statusPublished - 2018
Externally publishedYes
EventAAAI Conference on Artificial Intelligence 2018 - New Orleans, United States of America
Duration: 2 Feb 20187 Feb 2018
Conference number: 32nd
https://aaai.org/Conferences/AAAI-18/

Conference

ConferenceAAAI Conference on Artificial Intelligence 2018
Abbreviated titleAAAI 2018
Country/TerritoryUnited States of America
CityNew Orleans
Period2/02/187/02/18
Internet address

Keywords

  • Proof complexity
  • Proof system
  • Satisfiability
  • MaxSAT resolution
  • Dual rail encoding

Cite this