| Title: |
Proofs and Certificates for Max-SAT (Extended Abstract) * |
| Authors: |
Py, Matthieu; Cherif, Mohamed, Sami; Habet, Djamal |
| Contributors: |
Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS); Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Centre National de la Recherche Scientifique (CNRS)-Université Clermont Auvergne (UCA)-Institut national polytechnique Clermont Auvergne (INP Clermont Auvergne); Université Clermont Auvergne (UCA)-Université Clermont Auvergne (UCA); COntraintes, ALgorithmes et Applications (COALA); Laboratoire d'Informatique et des Systèmes (LIS) (Marseille, Toulon) (LIS); Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS)-Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS) |
| Source: |
Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence ; International Joint Conference on Artificial Intelligence ; https://hal.science/hal-04318066 ; International Joint Conference on Artificial Intelligence, Aug 2023, Macao, China. ⟨10.24963/ijcai.2023/787⟩ |
| Publisher Information: |
CCSD |
| Publication Year: |
2023 |
| Collection: |
Université de Toulon: HAL |
| Subject Terms: |
[INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI] |
| Subject Geographic: |
Macao; China |
| Description: |
International audience ; 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. |
| Document Type: |
conference object |
| Language: |
English |
| DOI: |
10.24963/ijcai.2023/787 |
| Availability: |
https://hal.science/hal-04318066; https://hal.science/hal-04318066v1/document; https://hal.science/hal-04318066v1/file/IJCAI_2023___Proof_And_Certificates_for_Max_SAT__Extended_Abstract_.pdf; https://doi.org/10.24963/ijcai.2023/787 |
| Rights: |
info:eu-repo/semantics/OpenAccess |
| Accession Number: |
edsbas.6282977 |
| Database: |
BASE |