Open Collections

Algorithms beyond Resolution using MaxSAT

Banff International Research Station for Mathematical Innovation and Discovery

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 dual-rail 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 neither $AC_0$-Frege+PHP nor the cutting planes proof system.

Mathematics; Computer science; Mathematical logic and foundations; Theoretical computer science

video/mp4

Author affiliation: Universitat Politècnica de Catalunya

2019-04-05

Attribution-NonCommercial-NoDerivatives 4.0 International

http://hdl.handle.net/2429/69480

Unreviewed

http://creativecommons.org/licenses/by-nc-nd/4.0/