Contraintes de cardinalité cachées dans les preuves d'insatisfaisabilité

Résumé : Les solveurs SAT sont utilisés avec succès dans de nombreuses applications combinatoires et du monde réel. Il n'est maintenant pas rare de lire qu'une preuve mathé-matique implique des centaines de gigaoctets de traces de solveur SAT. L'ampleur de la preuve commence à consti-tuer une véritable limite à l'approche globale. Dans ce travail, nous proposons de rechercher des contraintes de haut niveau dans les preuves UNSAT. Un travail similaire a été proposé il y a quelques annéespour les contraintes de cardinalité les plus simples. Nous étendons cette idée à un cas plus général (sans limitation sur les bornes des contraintes de cardinalité) en généralisant l'algorithme de Bron & Kerbosh (pour l'énumération de cliques dans les graphes) aux hypergraphes. Nous démontrons expéri-mentalement la capacité de notre approche à trouver des contraintes de cardinalité dans les grandes preuves, ou-vrant ainsi un nouveau moyen de générer des preuves plus courtes et compréhensibles pour les problèmes di ciles. Abstract SAT solvers are successfully used in many real-world and combinatoric applications. It is now not uncommon to read that a mathematical proof implied hundreds of gigabytes of SAT solver traces. The size of the proof by itself begins to be a real limit to the whole approach. In this work, we propose to search for higher-level constraints in UNSAT proofs. A similar work was proposed a few years ago, but only on the original formulafor the most simple cardinality constraints. We extend this idea to a more general case (with no limitations on the bounds of the cardinality constraints) by generalizing the Bron & Kerbosh algorithm (for clique enumeration in graphs) to hypergraphs. We experimentaly demonstrate the ability of our approach to find for cardinality constraints in large proofs, opening a new way of generating more shorter and human-understandable UNSAT proofs of hard problems.
Document type :
Conference papers
Complete list of metadatas

Cited literature [26 references]  Display  Hide  Download

https://hal.univ-cotedazur.fr/hal-02271389
Contributor : Valentin Montmirail <>
Submitted on : Monday, August 26, 2019 - 5:29:49 PM
Last modification on : Thursday, August 29, 2019 - 1:15:38 AM

File

JFPC-Nice.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02271389, version 1

Citation

Valentin Montmirail, Marie Pelleau, Jean-Charles Régin, Laurent Simon. Contraintes de cardinalité cachées dans les preuves d'insatisfaisabilité. 15es Journées Francophones de Programmation par Contraintes, Jun 2019, Albi, France. ⟨hal-02271389⟩

Share

Metrics

Record views

21

Files downloads

19