• Funding : Artois
  • PhD defended on :
  • 2019-12-11
  • 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é