Read-Once Resolution for Unsatisfiability-Based Max-SAT Algorithms

Heras, Federico; Silva, João P. Marques

doi:10.5591/978-1-57735-516-8/IJCAI11-103

Read-Once Resolution for Unsatisfiability-Based Max-SAT Algorithms

Federico Heras, João P. Marques Silva

Download BibTeX Cite

Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence. Pages 572-576.

https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-103

Abstract

This paper proposes the integration of the resolution rule for Max-SAT with unsatisfiability-based Max-SAT solvers. First, we show that the resolution rule for Max-SAT can be safely applied as dictated by the resolution proof associated with an unsatisfiable core when such proof is read-once, that is, each clause is used at most once in the resolution process. Second, we study how this property can be integrated in an unsatisfiability-based solver. In particular, the resolution rule for Max-SAT is applied to read-once proofs or to read-once subparts of a general proof. Finally, we perform an empirical investigation on structured instances from recent Max-SAT evaluations. Preliminary results show that the use of read-once resolution substantially improves the performance of the solver.

Federico Heras, and João P. Marques Silva. 2011. Read-Once Resolution for Unsatisfiability-Based Max-SAT Algorithms. In Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence, IJCAI-11. IJCAI, 572–576. https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-103

@inproceedings{ijcai2011p103,
  title     = {Read-Once Resolution for Unsatisfiability-Based Max-SAT Algorithms},
  author    = {Heras, Federico and Silva, João P. Marques},
  booktitle = {Proceedings of the Twenty-Second International Joint Conference on
               Artificial Intelligence, {IJCAI-11}},
  publisher = {AAAI Press/International Joint Conferences on Artificial Intelligence},
  editor    = {Toby Walsh},
  pages     = {572--576},
  year      = {2011},
  month     = {7},
  doi       = {10.5591/978-1-57735-516-8/IJCAI11-103},
  url       = {https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-103},
}

TY  - CPAPER
TI  - Read-Once Resolution for Unsatisfiability-Based Max-SAT Algorithms
AU  - Heras, Federico
AU  - Silva, João P. Marques
T2  - Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence, IJCAI-11
PB  - AAAI Press/International Joint Conferences on Artificial Intelligence
PY  - 2011
SP  - 572
EP  - 576
DO  - 10.5591/978-1-57735-516-8/IJCAI11-103
UR  - https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-103
ER  -