A Clause Tableau Calculus for MaxSAT
Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence. Pages 766-771.
Abstract
We define a clause tableau calculus for MaxSAT, prove its soundness and completeness, and describe a tableau-based algorithm for MaxSAT. Given a multiset of clauses C, the algorithm computes both the minimum number of clauses that can be falsified in C, and an optimal assignment. We also describe how the algorithm can be extended to solve weighted MaxSAT and weighted partial MaxSAT.
Chu-Min Li, Felip Manyà, and Joan Ramon Soler. 2016. A Clause Tableau Calculus for MaxSAT. In Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-16. IJCAI, 766–771. https://ijcai.org/proceedings/2016/114
Li, C., Manyà, F., & Soler, J. R. (2016). A Clause Tableau Calculus for MaxSAT. In Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-16 (pp. 766–771). IJCAI. https://ijcai.org/proceedings/2016/114
@inproceedings{ijcai2016p114,
title = {A Clause Tableau Calculus for MaxSAT},
author = {Li, Chu-Min and Manyà, Felip and Soler, Joan Ramon},
booktitle = {Proceedings of the Twenty-Fifth International Joint Conference on
Artificial Intelligence, {IJCAI-16}},
publisher = {AAAI Press / International Joint Conferences on Artificial Intelligence},
editor = {Subbarao Kambhampati},
pages = {766--771},
year = {2016},
month = {7},
url = {https://ijcai.org/proceedings/2016/114},
}
TY - CPAPER TI - A Clause Tableau Calculus for MaxSAT AU - Li, Chu-Min AU - Manyà, Felip AU - Soler, Joan Ramon T2 - Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-16 PB - AAAI Press / International Joint Conferences on Artificial Intelligence PY - 2016 SP - 766 EP - 771 UR - https://ijcai.org/proceedings/2016/114 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
