ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique

APPEL À
CONTRIBUTION
Masses de données hétérogènes
En savoir plus >>
Autres revues >>

Revue d'Intelligence Artificielle

0992-499X
Revue des Sciences et Technologies de l'Information
 

 ARTICLE VOL 28/5 - 2014  - pp.615-636  - doi:10.3166/ria.28.615-636
TITRE
Réutiliser ou adapter les prouveurs SAT pour l’optimisation booléenne

TITLE
Reusing or adapting SAT solvers for boolean optimization

RÉSUMÉ
D’années en années, le succès des approches basées sur SAT dans de nombreux domaines a contribué à la création de solveurs SAT robustes, efficaces, et pensés pour être réutilisables dans des applications tierces. Dans le cadre des problèmes d’optimisation qui nous intéressent, on souhaite pouvoir créer de manière paresseuse des contraintes de borne, c’està-dire ajouter des contraintes de cardinalité ou des contraintes pseudo-booléennes pendant la recherche. Nous avons intégré cette fonctionnalité sur la plate-forme d’optimisation booléenne libre Sat4j, et intégré un algorithme d’optimisation par contraintes de borne paresseuses. Nous comparons l’approche boîte noire et l’approche paresseuse sur l’ensemble des problèmes d’optimisation issus des compétitions PB10 et MAXSAT10. Nous n’observons malheureusement pas de différences flagrantes de performance (en termes de nombre d’instances résolues et de temps d’exécution) entre les deux approches, malgré des comportements différents. Nous présentons quelques hypothèses pour expliquer cette observation.


ABSTRACT
The success of SAT technology in many areas has lead to the availability of robust, efficient, and easy to embed SAT solvers. The most effective approaches for solving Boolean optimization problems tend to reuse as much as possible existing SAT solvers as black boxes. A more intimate communication between the SAT solver and external programs is sometimes needed to build solvers based on lazy constraints generation. Such capability can also be used to implement optimization solvers based on bound conflicts. We extended the classical CDCL SAT architecture in Sat4j to allow the introduction of new constraints during the search: clauses, cardinality constraints and pseudo-Boolean constraints. We identify for each kind of constraints the requirements on the solver side to maintain the invariants of the CDCL architecture. We used that lazy constraint generation capability to build two optimization solvers for which a black box approach was previously used: pseudo-Boolean optimization and MAXSAT. We compare the two approaches on competition benchmarks. While no approach outperformed the other one, they behave quite differently in terms of intermediate solution found.


AUTEUR(S)
Daniel LE BERRE, Emmanuel LONCA

MOTS-CLÉS
SAT, satisfaction et optimisation booléenne.

KEYWORDS
SAT solving, Boolean satisfaction and optimization.

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 7.5 €
• Non abonné : 15.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (233 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier