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.593-614  - doi:10.3166/ria.28.593-614
TITRE
Améliorer SAT dans le cadre incrémental

TITLE
Improve engines in incremental SAT solving

RÉSUMÉ
Les avancées spectaculaires obtenues dans le cadre de la résolution pratique du problème SAT ont rejailli bien au-delà de ses frontières. Ainsi, à l’heure actuelle, de nombreux problèmes dont la classe de complexité est supérieure à NP peuvent être traités de manière pratique en se reposant sur l’utilisation de solveurs SAT. Dans un grand nombre de cas, la résolution de ces problèmes consiste à appeler un solveur SAT sur plusieurs instances analogues. Ce type de résolution, appelé résolution incrémentale de SAT, est en passe de devenir l’état de l’art dans bien des domaines. Dans cet article, nous proposons d’améliorer les moteurs SAT afin de les rendre plus efficaces dans le cadre incrémental. Afin de valider notre contribution, nous avons étudié travaillé avec une utilisation importante et typique des démonstrateurs SAT incrémentaux : la recherche de noyaux minimaux inconsistants.


ABSTRACT
The spectacular progresses obtained in the practical solving of SAT problems had a number of important impacts beyond its own frontiers. For instance, a number of recent applications explicitly rely on a new use of SAT solvers called incremental SAT. In this new mode of operation, the same solver can be called a thousand times on almost the same formula each time (with added/removed clauses between calls). This new framework allowed a number of new scale up in some critical applications beyond NP. In this paper, we focus on optimizing the SAT engine in order to make it more competitive in the incremental case. We show that our approach immediately and significantly improves an intensive assumption-based incremental SAT solving task: finding Minimal Unsatisfiable Set.


AUTEUR(S)
Gilles AUDEMARD, Armin BIERE, Jean-Marie LAGNIEZ, Laurent SIMON

MOTS-CLÉS
démonstrateur automatique, SAT incrémental.

KEYWORDS
theorem prover, SAT incremental.

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  (455 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

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

 English version >> 
Lavoisier