Proofs and Certificates for Max-SAT (Extended Abstract)

Matthieu Py, Mohamed Sami Cherif, Djamal Habet

IJCAI 2023 pp. 6942-6947

doi:10.24963/IJCAI.2023/787 /ijcai/2023/py2023ijcai-proofs/

Abstract

In this paper, we present a tool, called MS-Builder, which generates certificates for the Max-SAT problem in the particular form of a sequence of equivalence-preserving transformations. To generate a certificate, MS-Builder iteratively calls a SAT oracle to get a SAT resolution refutation which is handled and adapted into a sound refutation for Max-SAT. In particular, the size of the computed Max-SAT refutation is linear with respect to the size of the initial refutation if it is semi-read-once, tree-like regular, tree-like or semi-tree-like. Additionally, we propose an extendable tool, called MS-Checker, able to verify the validity of any Max-SAT certificate using Max-SAT inference rules.

PDF IJCAI Semantic Scholar

Cite

Text

Py et al. "Proofs and Certificates for Max-SAT (Extended Abstract)." International Joint Conference on Artificial Intelligence, 2023. doi:10.24963/IJCAI.2023/787

Markdown

[Py et al. "Proofs and Certificates for Max-SAT (Extended Abstract)." International Joint Conference on Artificial Intelligence, 2023.](https://mlanthology.org/ijcai/2023/py2023ijcai-proofs/) doi:10.24963/IJCAI.2023/787

BibTeX

@inproceedings{py2023ijcai-proofs,
  title     = {{Proofs and Certificates for Max-SAT (Extended Abstract)}},
  author    = {Py, Matthieu and Cherif, Mohamed Sami and Habet, Djamal},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {2023},
  pages     = {6942-6947},
  doi       = {10.24963/IJCAI.2023/787},
  url       = {https://mlanthology.org/ijcai/2023/py2023ijcai-proofs/}
}