Knowledge compilation for constraint programming

The principal aim of this joint project is to use the complementary strengths of both research teams to derive new results in the research area which lies on the borderline of knowledge compilation, SAT encoding and solving, and constraint programming. In this project, the focus will be laid on the CNF format, which is the main input format for existing solvers and compilers. Our objective is to identify and study a number of CNF fragments which can serve as useful output target languages for knowledge compilation. Indeed, since CNF formulae are conjunctive in essence, the resulting compiled representations can be interpreted easily. We plan to address several issues which are at the intersection of the three (above described) research areas: -Analyzing CDCL SAT solvers (that add learnt clauses) with respect to unit refutation completeness and propagation completeness. -Considering several different CNF encodings of selected global constraints and compiling these CNFs into larger CNFs (by adding clauses) that ensure domain consistency of the encoded global constraint. -Studying the properties of knowledge compilation where the output is in a CNF format (for different input formats), identifying possible encoding strategies for this process.

Partners: Ondrej Cepek, Milos Chromy, Petr Kucera, Vorel Vojtech (Department of Theoretical Computer Science and Mathematical Logic, Charles University in Prague)


Scientific Responsible for CRIL :
Pierre Marquis
Participants :
Gilles Audemard
Jean-Marie Lagniez
Stefan Mengel
Nicolas Szczepanski
Romain Wallon
Duration :
2017-2018