Arrêt de service programmé du vendredi 10 juin 16h jusqu’au lundi 13 juin 9h. Pour en savoir plus
Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

From Declarative Set Constraint Models to “Good” SAT Instances

Abstract :

On the one hand, Constraint Satisfaction Problems allow one to declaratively model problems. On the other hand, propositional satisfiability problem (SAT) solvers can handle huge SAT instances. We thus present a technique to declaratively model set constraint problems, to reduce them, and to encode them into ”good” SAT instances. We illustrate our technique on the well-known nqueens problem. Our technique is simpler, more expressive, and less error-prone than direct hand modeling. The SAT instances that we automatically generate are rather small w.r.t. hand-written instances.

Type de document :
Communication dans un congrès
Liste complète des métadonnées

https://hal.univ-angers.fr/hal-03352573
Contributeur : Okina Univ Angers Connectez-vous pour contacter le contributeur
Soumis le : mercredi 13 octobre 2021 - 10:46:21
Dernière modification le : mercredi 20 octobre 2021 - 03:19:09
Archivage à long terme le : : vendredi 14 janvier 2022 - 18:41:21

Fichier

aisc2014.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Frédéric Lardeux, Eric Monfroy. From Declarative Set Constraint Models to “Good” SAT Instances. Artificial Intelligence and Symbolic Computation, 2014, Séville, Spain. pp.76-87, ⟨10.1007/978-3-319-13770-4_8⟩. ⟨hal-03352573⟩

Partager

Métriques

Consultations de la notice

30

Téléchargements de fichiers

8