Mots clés de ma recherche :
Allocation de ressources, CSP, Heuristique, MaxSAT, NP-complet,
Placement d'objets, Recherche locale, SAT
Citation : google
scholar, citeseer,
ACM
Guide
Contenu de la présentation :
- Animation de recherche
- Rayonnement scientifique
- Valorisation
- Encadrement
doctoral
- Liste de
co-auteurs depuis 1997
- Liste de
publications depuis 1997
- Logiciels
- Contexte
scientifique en SAT
Animation de recherche :
Responsable d'équipe
Contraintes et Heuristiques du LaRIA
J'ai constitué une équipe dont je suis responsable au
sein du LaRIA pour travailler sur la résolution pratique de
problèmes NP-difficiles et plus généralement de
problèmes combinatoires en 2002 grâce à une action
JemSTIC du CNRS. Les problèmes que nous étudions et sur
lesquels nous avons fait au moins une publication comprennent
actuellement : SAT, MaxSAT, SAT multivalué, Problème de
Satisfaction de Contraintes, Placement d'objets, Allocation de
ressources. Mon équipe se compose actuellement d'un
professeur (moi-même, le responsable), trois maîtres de
conférences, trois doctorants, et deux doctorants
co-encadrés avec deux collègues étrangers.
D'autres responsabilités
scientifiques
- Je suis membre élu du Conseil Scientifique de mon
université (Université de Picardie Jules Verne) depuis
mai 2005, et représentant du Conseil Scientifique au
Comité de Direction Scientifique du pôle biomédical
régional de recherche et de développement technologique
depuis juillet 2005.
- Je suis membre titulaire de la commission de spécialistes
informatique de mon université depuis 1998 (2e
vice-président entre 2000 et 2002). J'ai été
membre de la Commission de Spécialistes 27ème section de
l'Université de Cergy-Pontoise de septembre 2001 à
septembre 2003.
- J'ai été responsable de locaux et de
matériels du LaRIA du 01/01/2001 au 31/07/2003. En absence de
secrétariat du LaRIA à cette époque qui
était jeune, cette responsabilité consiste à faire
remonter à l'université les besoins du LaRIA en locaux et
mobiliers, constater et surveiller l'état physique de
chaque bureau mis à la disposition du LaRIA et faire intervenir
des techniciens pour la réparation en cas de besoin, et à
recenser les besoins en matériels (mobiliers et fournitures) et
préparer les devis et les bons de commande.
- J'ai été responsable des publications internes du
LaRIA de 1996 à 1998
Rayonnement scientifique
- Titulaire d'une prime d'encadrement doctoral et de recherche
depuis 1998 (renouvelée en 2002) et professeur des
universités depuis septembre 2003
- Mon démonstrateur G2WSAT a remporté une
médaille d'argent (2e) dans la compétition 2005 des
démonstrateurs SAT catégorie problèmes
aléatoires satisfiables (Voir la page de la compétition
SAT2005 pour un résumé des résultats). Trente
démonstrateurs ont participé à la
compétition
- Membre de jury et de comité d'organisation du challenge
ROADEF'2005 sur le problème "Car sequencing" proposé
par Renault
- Membre des comités de programme des conférences
suivantes:
- Les 8èmes Journées Nationales sur la
Résolution Pratique de Problèmes NP-Complets (JNPC2002), Mai
2002, Nice, dont je suis également président d'une des
sessions,
- Les Premières Journées Francophones de
Programmation par Contraintes (JFPC05), Lens, juin
2005, dont je suis également président d'une des sessions,
- The Fifth International Symposium on Theory and
Applications of Satisfiability Testing (SAT2002),
Cincinnati, Ohio, USA, May 2002,
- The Seventh International Conference on Theory and Applications
of Satisfiability Testing (SAT2004), Mai 2004,
Vancouver, Canada,
- The Eighth International Conference on Theory and Applications
of Satisfiability Testing (SAT2005), Juin 2005,
St. Andrews, Scotland.
- Président du comité d'organisation des 9èmes
Journées Nationales sur la Résolution Pratique de
Problèmes NP-Complets (JNPC2003) et des
12èmes Journées Francophones de Programmation Logique et
Programmation par Contraintes (JFPLC2003), qui
ont eu lieu conjointement à Amiens au mois de Juin 2003. Une
centaine de participants ont assistés à ces
manifestations nationales majeures du domaine. Ceci indique une
reconnaissance des activités de recherche de notre équipe
dans la communauté nationale. J'ai demandé et obtenu des
subventions pour ces colloques de l'INRIA, Amiens métropole, le
conseil régional de Picardie, l'Université
d'Amiens, les sociétés Cosytec, ILOG,
Thalès, et le ministère de recherche.
- Membre du board éditorial de Journal on Satisfiability,
Boolean Modeling and Computation (JSAT)
- Referee pour les revues internationales suivantes : Journal of
Automated Reasoning; Journal of Artificial Intelligence; Discrete
Applied Mathematics; Journal of Artificial Intelligence Research;
Systems, Man and Cybernetics - Part B, The European Journal of
Operational Research (EJOR). Je suis également referee
pour des conférences internationales prestigieuses suivantes:
ECAI2002, IJCAI2003, IJCAI2005
- Membre du jury de la thèse de
- Gilles Audemard (octobre 2001, Marseille)
- Alain Sidaner, soutenue le 16 décembre 2003
à Dijon. Je suis également rapporteur et
président du jury;
- Abdelkader Sbihi, soutenue le 18 décembre 2003
à Paris;
- Carlos Ansotegui, soutenue le 9 juillet 2004 à
Lleida, Espagne;
- Frédéric Lardeux, soutenue le 25
novembre 2005 à Angers.
- Edition et maintenance de ma page web
où je distribue mes papiers et les codes sources de mes
programmes suivants : Satz214 et Satz215, un des meilleurs
démonstrateurs SAT; EqSatz, Satz spécialisé pour
une classe de problèmes SAT; PSatz, la version parallèle
de Satz; G2WSAT, le démonstrateur incomplet qui a
remporté une médaille d'argent dans la compétition
SAT 2005
- Séjours scientifiques en Canada, Chine et Espagne.
- Dans le cadre du projet franco-chinois PRA SI02-04 (Programme
de Recherches Avancées, voir ci-dessous), j'ai été
invité pour un séjour scientifique d'un mois chaque
été de 2002 à 2004, puis de trois semaines au mois
d'Avril 2005;
- J'ai été invité pour un séjour
scientifique d'une semaine au mois de février 2002 à
University of Lleida à l'Espagne pour travailler avec Dr.
Felip Manya sur la version multi-valuée de mon
démonstrateur SAT Satz;
- J'ai été invité à l'University of
New Brunswick au Canada du 15 juillet au 15 août 2005 pour
travailler avec Professeur Huajie Zhang et notre doctorante Wanxia Wei
sur l'exploitation de machine learning dans les recherches locales.
Valorisation et Vulgarisation
- Porteur du projet JemSTIC (Jeune équipe, Mobilité
et Jeune chercheur) du CNRS: intégration des raisonnements
spéciaux dans les démonstrateurs SAT pour résoudre
des problèmes combinatoires (85KF HT, 2002)
- Responsable du projet Franco-Chinois PRA SI02-04 (Programme de
Recherches Avancées soutenu par les ministères de
recherche des deux pays): Algorithmes inspirés de
phénomènes naturels et sociaux pour résoudre les
problèmes NP-difficiles (15000 euros HT, 2002-2004)
- Participation au projet ``tolérant" dans l'axe
mobilisateur ``Homme, Technologie et Systèmes Complexes'' du
contrat de plan Etat/Région Picardie 2000-2006 (22000 euros TTC,
2003-2005).
- Participation au sous-projet ``Algorithms d'allocation de
ressources et leur complexité" au titre de la coopération
internationale dans le projet chinois intitulé ``Theory and
practice of coordination and survivability of massive information",
National 973 Program of China, Grant No. 2005CB321900
- J'ai co-animé une action de formation de l'académie
d'Amiens (5ème cycle de rencontres avec les acteurs de la
science contemporaine) sur la calculabilité et la
NP-Complétude aux professeurs des lycées et des
collèges de l'académie du 14/02/2003 (9H30-17h30). Il y a
eu une centaine de participants.
Encadrement
doctoral
Thèses soutenues
- Anbulagan, Boursier du gouvernement indonésien. Direction:
Chu Min Li (taux d'encadrement : 100%). Date de la première
inscription : septembre 1994, soutenue le 5 juin 1998. Sujet :
Hypothèse de contrainte: une explication de la réussite
de l'heuristique UP dans la résolution des problèmes de
satisfiabilité des expressions booléennes. Anbulagan est
actuellement chercheur du Canberra Research Laboratory, National ICT
Australia Limited. Il a remporté une médaille d'or dans
la compétition SAT 2005.
- Bernard Jurkowiak, allocataire de recherche ministère,
moniteur CIES. Direction: Chu Min Li (taux d'encadrement : 100%).
Date de la première inscription: octobre 2000, soutenue le 4
octobre 2004. Sujet : Programmation haute performance pour la
résolution des problèmes SAT et CSP. Bernard Jurkowiak
est actuellement ingénieur de recherche R&D dans la
société AerieLogic spécialisée dans la
vérification formelle des circuits électroniques
- Djamal Habet, boursier à l'Ecole des mines d'Alès
à Nîmes. Direction : Michel Vasquez, Chu Min Li (taux
d'encadrement : 33%, un tier). Date de la première inscription :
novembre 2001, soutenue le 14 décembre 2004, Sujet :
Coopération entre recherche locale et exhaustive pour
l'optimisation combinatoire. Djamal Habet est
actuellement maître de conférences à
l'Université Aix-Marseille (U3)
Thèses en cours
- Sylvain Darras, allocataire de recherche ministère et
moniteur. Direction : Gilles Dequen, Laure Devendeville, Chu Min LI}
(taux d'encadrement : 10%). Date de la première inscription :
septembre 2004, date de soutenance prévue : décembre
2007. Sujet : Intégration de raisonnements spéciaux pour
la résolution de problèmes combinatoires.
- Xavier Domingo (Salarié de l'entreprise GPS microSAT
à Barcelone, Espagne), Direction : Felip Manya (Artificial
Intelligence Research Institute (IIIA-CSIC), Espagne), Chu Min LI, Date
de la première inscription : octobre 2005
Sujet : Design and implementation of exact Multi-Valued MaxSAT solvers.
- Abdellah Idrissi Direction: Chu Min LI (taux d'encadrement :
100%), Date de la première inscription : novembre 2004, date de
soutenance prévue : novembre 2007. Sujet : Techniques de
satisfaction de contraintes pour le problème d'allocation des
ressources
- Nouredine Ould Mohamedou, boursier du gouvernement Mouritanie.
Direction: Chu Min LI (taux d'encadrement : 100%). Date de la
première inscription : septembre 2005, date de soutenance
prévue : septembre 2008. Sujet : Etude de la programmation en
nombres entiers pour SAT et MaxSAT
- Jordi Planes, boursier du gouvernement espagnol. Direction : Felip Manya (Artificial
Intelligence Research Institute (IIIA-CSIC), Espagne), Chu Min LI
(taux d'encadrement : 40%). Date de la première
inscription : septembre 2003, date de soutenance prévue :
septembre 2006. Sujet : Design and implementation of exact MaxSAT
solvers.
- Wanxia Wei, boursier (Scholarship) of Natural Sciences and
Engineering Research Council of Canada, Direction : Huajie Zhang (University of New
brunswick, Canada), Chu Min LI (taux d'encadrement : 60%), sujet :
Exploiting machine learning in Local search for SAT. Date de la
première inscription : mai 2005, date de soutenance
prévue : septembre 2008.
Liste de co-auteurs depuis
1997 :
Je pense que la meilleure façon pour faire la
recherche est de coopérer. Ci-dessous est
la liste des collègues avec qui j'ai
publié au moins un papier depuis 1997
(voir la liste de
publications):
Kakim Akeb, Anbulagan, Carlos Ansotegui, Ramon
Bejar, Hachemi Bennaceur,
Marc-Antoine Boryczka, Alba Cabiscol, Laure
Devendeville, Sylvain Gérard,
Jean-Luc Guérin, Djamal Habet, Wenqi Huang,
Abdellah Idrissi, Bernard Jurkowiak,
J. Larrubia, Yu Li, Felip Manya, Jordi Planes, Paul
W. Purdom, Gil Utard,
Michel Vasquez,
RuChu Xu
Liste de publications
depuis 1997:
Papiers publiés ou acceptés dans une revue
d'audience internationale avec comité de lecture :
WenQi HUANG, Yu LI, ChuMin LI, RuChu XU, "New
Heuristics for Packing Unequal Circles into a Circular Container",
A paraître dans Computers & operations research (Vol 33,
Issue 8, August 2006, Pages 2125-2142).
Bernard Jurkowiak, Chu Min LI, and Gil Utard, "A
parallelization scheme based on work stealing for a class of SAT solvers",
in Journal of Automated Reasoning
(2005) 34:73-101.
WenQi Huang, Yu LI, Kakim Akeb, Chu Min LI, ``Greedy
algorithms
for packing unequal circles into a rectangular container''
in Journal of the
Operational Research Society (JORS), May 2005, Volume 56, Number
5,
Page 539-548.
Chu Min LI, Sylvain Gérard, ``On
the Limit of Branching Rules for Hard Random Unsatisfiable 3-SAT'',
dans Discrete Applied
Mathematics, Vol 130/2, pp 277-290, 2003.
Chu Min LI, ``Equivalent
literal propagation in Davis-Putnam procedure'', dans Discrete
Applied Mathematics, Vol 130/2 pp 251-276, 2003.
Chu Min LI, ``Equivalency
reasoning to solve a class of hard SAT problems'', Information
Processing Letters 76 (2000) pages 75-81.
Chu Min LI, ``A
constrained-based approach to narrow search trees for satisfiability'',
Information Processing Letters 71(1999) pages
75-80.
Papier court publié dans une revue d'audience nationale
avec comité de lecture :
Chu Min LI, ``La
Propagation de Contraintes et la Procédure DPLL pour le
Raisonnement Propositionnel'', Compte rendu d'habilitation,
Technique et Science Informatique, volume 20-N°6/2001, pages
821-823.
Papiers publiés dans une conférence d'audience
internationale avec actes et comité de lecture :
Chu Min LI, Felip Manya and Jordi Planes, "Exploiting
unit propagation to compute lower bounds in branch and bound MaxSAT
solvers", in proceedings of 11th
international conference on Principles and Practice of Constraint
Programming (CP 2005), LNCS 3709 Springer,
Sitges, Spain, October 2005, Pages 403-414, (Taux de sélection :
48 sur 164, 29%).
Chu Min LI and Wenqi Huang, "Diversification
and Determinism in Local search for Satisfiability", in proceedings
of 8th international conference
on the Theory and Applications of Satisfiability Testing (SAT2005),
LNCS 3569 Springer, St Andrews,
UK, June 2005, Pages 158-172 (taux de sélection : 26 sur 73, 35%)
Wen Qi Huang, Yu LI, Bernard Jurkowiak, Chu Min LI and Ru Chu Xu, ``A
Two-Level Search Strategy for Packing Unequal Circles into a Circle
Container''.
dans les actes de the 9th International Conference on Principles and
Practice of
Constraint Programming (CP 2003), Springer-Verlag, Kinsale, Ireland,
September 29-October 3,
2003, pp. 868-872.
Ansótegui C., Larrubia J., Chu Min LI, Manyà F. "Mv-Satz: A SAT
Solver for Many-valued Clausal forms", dans les actes de the Fourth
International
Conference Journées de l'Informatique Messine(JIM'2003),
September 3-6,
2003, Metz, France.
Bennaceur H., Chu Min LI, ``Characterizing
SAT Problems with the Row Convexity Property", dans les actes de
Eighth International Conference on
Principles and Practice of Constraint Programming (CP2002), Cornell
University, Ithaca, NY, USA,
Pages 720-725, septembre 2002.
Habet D., Chu Min LI, Devendeville L., Vasquez M., ``A
Hybrid Approach for SAT", dans les actes de Eighth International
Conference on Principles and Practice
of Constraint Programming (CP2002), Cornell University, Ithaca, NY,
USA, Pages
172-184, septembre 2002. Taux de sélection : 44 sur 146 (30%).
Carlos Ansotegui, Ramon Bejar, Alba Cabiscol, Chu Min LI et Felip
Manya, ``Resolution
Methods for Many-Valued CNF Formulas", dans les actes du Fifth
International Symposium on the Theory and Applications of
Satisfiability Testing (SAT'2002),
pages 156-163, Cincinnati, Ohio, USA, 6-9 mai 2002.
Chu Min LI, Bernard Jurkowiak, Paul W. Purdom Jr, ``Integrating
symmetry breaking into a DLL procedure", dans les actes du Fifth
International Symposium
on the Theory and Applications of Satisfiability Testing (SAT'2002),
pages 149-155,
Cincinnati, Ohio, USA, 6-9 mai 2002.
Hachemi Bennaceur, Chu Min LI, ``An
Empirical Measure for Characterizing 3-SAT", dans les actes du
Fifth International Symposium on the Theory and
Applications of Satisfiability Testing (SAT'2002), pages 201-205,
Cincinnati, Ohio,
USA, 6-9 mai 2002.
Chu Min LI, ``Integrating
Equivalency reasoning into Davis-Putnam procedure", in proceedings
of the 17th National Conference on
Artificial Intelligence (AAAI-2000), Pages 291-296, Austin Texas, USA,
2000. Taux de sélection : 141 sur 430 (32%).
Chu Min LI, Sylvain Gérard, ``On
the Limit
of Branching Rules for Hard Random Unsatisfiable 3-SAT'', in
proceedings of the 14th European Conference
on Artificial Intelligence (ECAI-2000), IOS Press, Pages 98-102,
Berlin, 2000. Taux de
sélection : 140 sur 443 (31%).
Chu Min LI, Anbulagan, ``Look-ahead
versus look-back for satisfiability problems", in proceedings
of the third international conference on Principles and
Practice of Constraint Programming--CP97, Springer-Verlag, LNCS 1330,
Pages 342-356, Autriche,
1997. Taux de sélection : 37 sur 132 (28%).
Chu Min LI, Anbulagan, ``Heuristics
based on unit propagation for satisfiability problems", Proceedings
of the 15th International Joint Conference on Artificial
Intelligence (IJCAI'97), Morgan Kaufmann Publishers, ISBN
1-55860-480-4, Pages 366-371, Japon,
1997. Taux de sélection : 216 sur 882 (24%).
Papiers publiés ou acceptés dans un workshop
d'audience internationale avec actes et
comité de lecture :
Marc-Antoine Boryczka, Yu LI, Wenqi Huang, Chu Min LI, ``A
Generator of Instances for Circle Packing Problems", dans
les actes de International Workshop on Heuristics, 24-27 July 2002,
Beijing, China.
WenQi Huang, Yu LI, Sylvain Gérard, Chu Min LI, Xu RuChu, ``A
learning from human heuristic for solving unequal disks packing problem",
dans les
actes de International Workshop on Heuristics, 24-27 July 2002,
Beijing, China.
Bernard Jurkowiak, Chu Min LI, Gil Utard, ``Parallelizing
Satz Using Dynamic Workload Balancing''. Dans les actes du Workshop
on Theory and Applications of Satisfiability Testing (SAT'2001), pages
205--211, Boston, 14-15 juin 2001.
Papiers publiés dans une conférence d'audience
nationale avec actes et comité de lecture :
Abdellah Idrissi, Chu Min LI, ``Modélisation et Optimisation des
Problèmes d'Allocation de Capacités des Fixes d'un
Aéroport". A paraître dans les actes de
Modélisation et Simulation des Systèmes (MOSIM-06),
ISBN, Rabat, April, 2006.
Abdellah Idrissi, Chu Min LI, ``CSPAC : Modèle de
Résolution du Problème d'Allocation de Capacités",
in proceedings de Manifestation des jeunes
chercheurs en STIC (MajecStic-2005), INRIA, Rennes, France,
Novembre 2005, pp. 172-179.
Djamal Habet, Chu Min LI, Laure Devendeville, Michel Vasquez,
Jean-Luc Guérin, ``Une Approche Hybride pour
SAT", dans
les actes des 8èmes journées nationales en
résolution pratique de problèmes NP-Complets (JNPC'02),
Nice, mai 2002, pages 115-126.
Hachemi Bennaceur, Chu Min LI, ``Caractériser les
problèmes SAT avec la convexité par ligne", dans les
actes des 8èmes journées nationales
en résolution pratique de problèmes NP-Complets
(JNPC'02), Nice, mai 2002, pages 31-41.
Bernard Jurkowiak, Chu Min LI, Gil Utard, ``Parallélisation
d'une recherche arborescente pour les problèmes de
satisfiabilité'', dans les actes
des 13ième Rencontres Francophones du Parallélisme des
Architectures et des Systèmes
(RenPar01), Paris, avril 2001, pages 121-126.
Chu Min LI, ``Integration d'un raisonnement d'équivalence dans
la procédure Davis-Putnam'', dans les actes des 6èmes
journées nationales en
résolution pratique de problèmes NP-Complets (JNPC'00),
Marseille, juin 2000, pp. 167-178.
Chu Min LI, Sylvain Gérard, ``A propos des règles de
branchement pour les problèmes 3-SAT aléatoires
insatisfiables et difficiles'', dans les actes
des 6èmes journées nationales en résolution
pratique de problèmes NP-Complets (JNPC'00),
Marseille, 2000, pp. 179-190.
Chu Min LI, Anbulagan, ``Why a
random 3-SAT problem is harder than another", dans les actes
des 3èmes journées nationales en
résolution pratique de problèmes NP-Complets (JNPC'97),
pages 49-54, Rennes, 1997.
Logiciels :
Pour avoir les codes sources de différents logiciels, il suffit
de cliquer sur leur nom.
Pour les codes sources de Walksatz, envoyer-moi un e-mail. Voir ma
page en anglais pour plus de détails de ces logiciels.
Chu Min LI & Wenqi HUANG, "G2WSAT",
une méthode de recherche locale qui a gagné une
médaille d'argent dans la compétition SAT2005,
catégorie formules aléatoires satisfiables
Chu Min LI, Anbulagan, "Satz214",
un des meilleurs solveurs des problèmes SAT.
Chu Min LI, Daniel Leberre, "Satz215",
un des meilleurs solveurs des problèmes SAT.
Chu Min LI, "EqSatz",
Satz spécialisé dans la résolution des
problèmes SAT contenant de nombreuses equivalences de
littéraux.
Chu Min LI, "Compactor",
pour simplifier un problème SAT avant de le résoudre.
Bernard Jurkowiak, Chu Min LI, Gil Utard, "ParaSatz",
la version parallèle et distribuée de Satz fonctionnant
sur un cluster PC sous unix/linux.
Habet D., Chu Min LI, Devendeville L., Vasquez M., "Walksatz", une
méthode hybride pour SAT.
Contexte scientifique en SAT :
Le problème SAT peut être défini comme suit. Soit
un ensemble de variables booléennes
x1, x2, ..., xn, un littéral
est une variable (littéral positif) ou sa négation
(littéral négatif).
Un littéral positif (négatif) est satisfait si la
variable
est affectée à la valeur de vérité vraie
(fausse). Une clause est un ou logique de littéraux, qui
est satisfaite s'il y a au moins un littéral
satisfait dans la clause. Une formule CNF est une conjonction de
clauses. Le problème SAT
consiste à tester si toutes les clauses dans une formule CNF
peuvent être satisfaites par une
affectation de valeur de vérité aux variables. Le
problème SAT offre une puissance
d'expression suffisante pour de nombreuses applications.
Malgré la NP-complétude du problème SAT, on est
aujourd'hui capable de résoudre des
problèmes réels intéressants comme la
planification et le VLSI en les modélisant par la
logique propositionnelle.
Le regain d'intérêt observé est dû à
plusieurs facteurs. Premièrement, de nouveaux
algorithmes ont été découverts et sont capables de
résoudre les problèmes SAT de grande
taille. En l'espace de 10 ans, la taille des problèmes SAT
difficiles pouvant être résolus en
un temps raisonnable est passé de 100 variables à plus de
100 000 variables. Deuxièmement,
les machines sont de plus en plus performantes tant en vitesse qu'en
mémoire. Troisièmement,
les chercheurs modélisent mieux les problèmes
réels en logique propositionnelle, les codages
propositionnels étant plus sophistiqués et capturant
mieux la structure des problèmes codés.
De plus, les problèmes réels sont loin de constituer le
pire cas pour les algorithmes de
résolution.
Il existe deux principales familles d'algorithmes pour résoudre
SAT :
- Les algorithmes incomplets qui ne parcourent pas
tout l'espace de recherche et ne peuvent
prouver l'inconsistance.
- Les algorithmes complets basés sur la
procédure de Davis et Putnam (DPLL), qui
parcourent tout l'arbre de recherche.
Le problème SAT peut être appliqué dans de nombreux
domaines :
- La planification : étant données
une configuration initiale et une configuration finale d'un
système et un ensemble
d'opérations légales, trouver une suite
d'opérations permettant
d'obtenir la configuration finale en
appliquant successivement la suite d'opérations.
- L'ordonnancement : étant donné un
ensemble de tâches à accomplir, ordonner ces tâches
en obéissant à certaines
contraintes sous un objectif qui est souvent le temps minimum
d'exécution.
- La cryptographie à clé publique : on
attaque un système cryptographique soit en essayant
de trouver la clé secrète soit
en essayant de la contourner.
- Le problème de diagnostic des circuits
logiques.
- Démonstration automatique de
théorèmes. Par exemple, beaucoup de
théorèmes
concernant les Quasi-Groupes ont
été démontrés à l'aide de SAT.
- ...
On trouve facilement dans la littérature des exemples
d'application réussie de SAT dans ces
domaine.
Coder un problème réel en SAT puis résoudre la
formule CNF obtenue par un solveur
SAT existant est souvent plus facile de concevoir un algorithme
spécifique pour résoudre
directement le problème. De plus, certains problèmes
codés sous forme CNF et résolus
grâce à un algorithme dédié à SAT
trouvent une solution (ou simplement l'existence de
celle-ci) plus rapidement que par des outils spécifiques dans
leur codage d'origine. La raison
est que ces solveurs SAT sont issus de quarante ans de recherche
intensive.