Contraintes de cardinalité cachées dans les preuves d'insatisfaisabilité - Université Côte d'Azur
Conference Papers Year : 2019

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

Abstract

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.
Fichier principal
Vignette du fichier
JFPC-Nice.pdf (3.1 Mo) Télécharger le fichier
Origin Files produced by the author(s)
Loading...

Dates and versions

hal-02271389 , version 1 (26-08-2019)

Identifiers

  • HAL Id : hal-02271389 , version 1

Cite

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⟩
105 View
143 Download

Share

More