ML Anthology

A Clause Tableau Calculus for MaxSAT

Chu Min Li, Felip Manyà, Joan Ramon Soler
IJCAI 2016 pp. 766-772
/ijcai/2016/li2016ijcai-clause/

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. PDF

PDF IJCAI Semantic Scholar

Cite

Text

Li et al. "A Clause Tableau Calculus for MaxSAT." International Joint Conference on Artificial Intelligence, 2016.

Markdown

[Li et al. "A Clause Tableau Calculus for MaxSAT." International Joint Conference on Artificial Intelligence, 2016.](https://mlanthology.org/ijcai/2016/li2016ijcai-clause/)

BibTeX

@inproceedings{li2016ijcai-clause,
  title     = {{A Clause Tableau Calculus for MaxSAT}},
  author    = {Li, Chu Min and Manyà, Felip and Soler, Joan Ramon},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {2016},
  pages     = {766-772},
  url       = {https://mlanthology.org/ijcai/2016/li2016ijcai-clause/}
}