.png){kind=icon}
.png){kind=icon}
Return
Propositional proof systems based on maximum satisfiability
.png){kind=icon}
PRE
AI
DOI：10.1016/j.artint.2021.103552.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
The paper describes the use of dual-rail MaxSAT systems to solve Boolean satisfiability (SAT), namely to determine if a set of clauses is satisfiable. The MaxSAT problem is the problem of satisfying the maximum number of clauses in an instance of SAT. The dual-rail encoding adds extra variables for the complements of variables, and allows encoding an instance of SAT as a Horn MaxSAT problem. We discuss three implementations of dual-rail MaxSAT: core-guided systems, minimal hitting set (MaxHS) systems, and MaxSAT resolution inference systems. All three of these can be more efficient than resolution and thus than conflict-driven clause learning (CDCL). All three systems can give polynomial size refutations for the pigeonhole principle, the doubled pigeonhole principle and the mutilated chessboard principles. The dual-rail MaxHS MaxSat system can give polynomial size proofs of the parity principle. However, dual-rail MaxSAT resolution requires exponential size proofs for the parity principle; this is proved by showing that constant depth Frege augmented with the pigeonhole principle can polynomially simulate dual-rail MaxSAT resolution. Consequently, dual-rail MaxSAT resolution does not simulate cutting planes. We further show that core-guided dual-rail MaxSAT and weighted dual-rail MaxSAT resolution polynomially simulate resolution. Finally, we report the results of experiments with core-guided dual-rail MaxSAT and MaxHS dual-rail MaxSAT showing strong performance by these systems. (C) 2021 Published by Elsevier B.V.
Keywords:
Propositional proof systems
Maximum satisfiability
Clause learning
Resolution
AI Summary
Key information extracted from the uploaded paper, including a brief overview, abstract, background, key highlights, visual analysis, and future outlook.
Journal
IF:
13.9
Papers:
6.1K
Citations:
1.9W
View more organizations