MaxSAT Resolution With the Dual Rail Encoding


  • Maria Luisa Bonet Universidad Politécnica de Cataluña, Barcelona
  • Sam Buss University of California, San Diego
  • Alexey Ignatiev LASIGE, Faculty of Science, University of Lisbon
  • Joao Marques-Silva LASIGE, Faculty of Science, University of Lisbon
  • Antonio Morgado LASIGE, Faculty of Science, University of Lisbon



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


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 AC0-Frege+PHP p-simulates DRMaxSAT, and that DRMaxSAT can not p-simulate AC0-Frege+PHP or the cutting planes proof system.




How to Cite

Bonet, M. L., Buss, S., Ignatiev, A., Marques-Silva, J., & Morgado, A. (2018). MaxSAT Resolution With the Dual Rail Encoding. Proceedings of the AAAI Conference on Artificial Intelligence, 32(1).



Main Track: Search and Constraint Satisfaction