Page précédente LERIA Faculté des Sciences Université d'Angers
English version


Qu'est-ce que le problème SAT?


Le problème de satisfiabilité (SAT)[9] consiste à trouver une affectation booléenne validant une formule en logique propositionnelle. Une instance de ce problème est définie par un ensemble de variables booléennes (aussi appelées atomes) ${\cal X}=\{x_1,\dots,x_n\}$ et une formule booléenne $\phi:\{0,1\}^n\rightarrow\{0,1\}$. Un littéral est une variable ou sa négation; une clause est une disjonction de littéraux. Une formule est en forme normale conjonctive (CNF) si c'est une conjonction de clauses. Une affectation est une fonction $v:{\cal X}\rightarrow\{0,1\}$. La formule est dite satisfiable s'il existe une affectation rendant $\phi$ vraie et est non satisfiable s'il n'en existe pas. Une formule est vraie si et seulement si toutes ses clauses sont vraies.
SAT est un des six principaux problèmes NP-complet et a de nombreuses applications telles que les tests et vérifications de circuits intégrés (VLSI), le diagnostic de pannes, les emplois du temps ... Sa résolution est généralement considéré comme un problème de décision mais il peut aussi être abordé comme :

Les algorithmes dédiés au problème SAT se divisent en deux classes : les algorithmes complets et les algorithmes incomplets.

Les algorithmes complets répondent au problème de décision et sont principalement basés sur la procédure Davis-Putnam-Loveland [3]. Ils diffèrent essentiellement dans la règle de branchement utilisée pour explorer l'arbre de recherche [2,5,17,22,18]. Des techniques spécifiques telles que la détection de symétries, de backbones ou encore d'équivalences permettent de renforcer quelques algorithmes [1,16,6].

Les algorithmes incomplets sont généralement basés sur la recherche locale [12,21,14] et sur les algorithmes évolutionnaires ou hybrides [4,13,8,15,7,10,11]. GSAT [20], le premier algorithme de descente, et Walksat [19], sa version améliorée, sont les exemples les plus connus d'algorithmes incomplets. Bien que les algorithmes incomplets ne soient pas d'un grand secours pour le problème de décision dans le cas des instances insatisfiables, ils sont très utiles pour le problème MAX-SAT. De plus, les algorithmes incomplets sont les seuls à pouvoir trouver des solutions pour les très grandes instances.

Bibliographie

1
Belaid Benhamou and Lakhdar Sais.
Theoretical study of symmetries in propositional calculus and applications.
In CADE'92, pages 281-294, 1992.

2
Thierry Castell, Claudette Cayrol, Michel Cayrol, and Daniel Le Berre.
Using the davis and putnam procedure for an efficient computation of preferred models.
In ECAI '96; 12th European Conference on Artificial Intelligence, pages 350-354, August 1996.

3
Martin Davis, George Logemann, and Donald Loveland.
A machine program for theorem-proving.
Communications of the ACM, 5(7):394-397, Jul 1962.

4
Kenneth A. De Jong and William M. Spears.
Using genetic algorithm to solve NP-complete problems.
In Proc. of the Third Int. Conf. on Genetic Algorithms, pages 124-132, San Mateo, CA, 1989.

5
Olivier Dubois, Pascal André, Yacine Boufkhad, and Jacques Carlier.
SAT versus UNSAT.
In Second DIMACS implementation challenge : cliques, coloring and satisfiability, volume 26 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 415-436, 1996.

6
Olivier Dubois and Gilles Dequen.
A backbone-search heuristic for efficient solving of hard 3-SAT formulae.
In Bernhard Nebel, editor, Proc. of the IJCAI'01, pages 248-253, San Francisco, CA, 2001.

7
Agoston E. Eiben, Jan K. van der Hauw, and Jano I. van Hemert.
Graph coloring with adaptive evolutionary algorithms.
Journal of Heuristics, 4(1):25-46, 1998.

8
Charles Fleurent and Jacques A. Ferland.
Object-oriented implementation of heuristic search methods for graph coloring, maximum clique, and satisfiability.
In Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge, volume 26 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 619-652, 1994.

9
Michael R. Garey and David S. Johnson.
Computers and Intractability , A Guide to the Theory of NP-Completeness.
W.H. Freeman & Company, San Francisco, 1978.

10
Jens Gottlieb, Elena Marchiori, and Claudio Rossi.
Evolutionary algorithms for the satisfiability problem.
Evolutionary Computation, 10(1):35-50, 2002.

11
Djamal Habet, Chu Min Li, Laure Devendeville, and Michel Vasquez.
A Hybrid Approach for SAT.
In ICCP; International Conference on Constraint Programming (CP), LNCS, 2002.

12
Pierre Hansen and Brigitte Jaumard.
Algorithms for the maximum satisfiability problem.
Computing, 44(4):279-303, 1990.

13
Jin-Kao Hao and Raphael Dorne.
A new population-based method for satisfiability problems.
In Proc. of the 11th European Conf. on Artificial Intelligence, pages 135-139, Amsterdam, 1994.

14
Wengi Huang and Renchao Jin.
Solar, a quasi physical algorithm for sat.
Science in China (Series E), 2(27):179-186, 1997.

15
Brigitte Jaumard, Mihnea Stan, and Jacques Desrosiers.
Tabu search and a quadratic relaxation for the satisfiability problem.
In Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge, volume 26 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 457-478, 1994.

16
Chu Min Li.
Integrating equivalency reasoning into davis-putnam procedure.
In Proc. of the AAAI'00, pages 291-296, 2000.

17
Chu Min Li and Anbulagan.
Heuristics based on unit propagation for satisfiability problems.
In Proc. of the IJCAI'97, pages 366-371, 1997.

18
Bertrand Mazure, Lakhdar Saïs, and Eric Grégoire.
Boosting complete techniques thanks to local search methods.
Annals of Mathematics and Artificial Intelligence, 22:319-331, 1998.

19
Bart Selman, Henry A. Kautz, and Bram Cohen.
Noise strategies for improving local search.
In Proc. of the AAAI, Vol. 1, pages 337-343, 1994.

20
Bart Selman, Hector J. Levesque, and David G. Mitchell.
A new method for solving hard satisfiability problems.
In Proc. of the AAAI'92, pages 440-446, San Jose, CA, 1992.

21
William M. Spears.
Simulated annealing for hard satisfiability problems.
In Second DIMACS implementation challenge : cliques, coloring and satisfiability, volume 26 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 533-558, 1996.

22
Hantao Zhang.
SATO: An efficient propositional prover.
In Proc. of the 14th International Conference on Automated deduction, volume 1249 of LNAI, pages 272-275, Berlin, 1997.