Read-Once Resolution for Unsatisfiability-Based Max-SAT Algorithms
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.
Cite
Text
Heras and Marques-Silva. "Read-Once Resolution for Unsatisfiability-Based Max-SAT Algorithms." International Joint Conference on Artificial Intelligence, 2011. doi:10.5591/978-1-57735-516-8/IJCAI11-103Markdown
[Heras and Marques-Silva. "Read-Once Resolution for Unsatisfiability-Based Max-SAT Algorithms." International Joint Conference on Artificial Intelligence, 2011.](https://mlanthology.org/ijcai/2011/heras2011ijcai-read/) doi:10.5591/978-1-57735-516-8/IJCAI11-103BibTeX
@inproceedings{heras2011ijcai-read,
title = {{Read-Once Resolution for Unsatisfiability-Based Max-SAT Algorithms}},
author = {Heras, Federico and Marques-Silva, João},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2011},
pages = {572-577},
doi = {10.5591/978-1-57735-516-8/IJCAI11-103},
url = {https://mlanthology.org/ijcai/2011/heras2011ijcai-read/}
}