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 language | English |
---|---|
Title of host publication | The Thirty-Second AAAI Conference on Artificial Intelligence |
Editors | Sheila McIlraith, Kilian Weinberger |
Place of Publication | Palo Alto CA USA |
Publisher | Association for the Advancement of Artificial Intelligence (AAAI) |
Pages | 6565-6572 |
Number of pages | 8 |
ISBN (Electronic) | 9781577358008 |
Publication status | Published - 2018 |
Externally published | Yes |
Event | AAAI Conference on Artificial Intelligence 2018 - New Orleans, United States of America Duration: 2 Feb 2018 → 7 Feb 2018 Conference number: 32nd https://aaai.org/Conferences/AAAI-18/ |
Conference
Conference | AAAI Conference on Artificial Intelligence 2018 |
---|---|
Abbreviated title | AAAI 2018 |
Country/Territory | United States of America |
City | New Orleans |
Period | 2/02/18 → 7/02/18 |
Internet address |
Keywords
- Proof complexity
- Proof system
- Satisfiability
- MaxSAT resolution
- Dual rail encoding