Hybridization of clauses learning techniques in constraint programming
- PhD Student:
- Gaël Glorian
- Co-Advisors :
- Christophe Lecoutre
- Bertrand Mazure
- Co-Supervisor :
- Frédéric Boussemart
- Funding : Artois
- PhD defended on :
- Dec 11, 2019 • faculté des sciences, salle des thèses
Abstract
This thesis belongs to the field of constraint programming (CP), one of the most efficient paradigms for solving many problems (of a combinatorial nature) in AI. We have been interested in improving the CSP (constraint satisfaction problem) solving techniques, especially in a hybrid context using the power of SAT (Boolean satisfaction problem) inference engines. We have developed several conflict analysis techniques to extract useful information for resolution, through fine analysis followed by a form of learning. To achieve this goal, we first strengthened the power of nogoods recorded by the resolution system by proposing several rules to combine them. In addition, we integrated a SAT resolution engine into a CP system based on the notion of lazy explanations. The use of a SAT engine is motivated by their high efficiency in producing and manipulating simple forms of nogoods in clausal form. The NACRE software, a generic reasoning engine, is the result of this work; In particular, it was designed to be a hybrid solver, solving constraint satisfaction problems using dedicated or SAT-inspired methods. Our generic (i.e., valid for any problem) approach has proved very effective in practice (NACRE has won 2 gold medals at the XCSP competitions 2018 and 2019). In order to enrich the SAT / CP hybridization, we conducted a study on the quality of clauses produced by the SAT engine. This allowed us to propose new methods for clauses database reduction, minimization and new search heuristics.
Defense Committee
- M. Christophe LECOUTRE Université d’Artois Directeur de thèse
- M. Laurent SIMON Université de Bordeaux Rapporteur
- M. Cyril TERRIOUX Aix-Marseille Université Rapporteur
- Mme Marie-José HUGUET INSA Toulouse Examinateur
- M. Bertrand MAZURE Université d’Artois Co-directeur de thèse
- M. Frédéric BOUSSEMART Université d’Artois Examinateur
- M. Jean-Marie LAGNIEZ Huawei Technologies Ltd Examinateur
- Mme Christine SOLNON INSA Lyon Examinateur
- M. Gilles AUDEMARD Université d’Artois Invité