Projet PHC Barrande France / République Tchèque KC4CP

Knowledge compilation for constraint programming

L’objectif principal de ce projet est d’utiliser les forces complémentaires des deux équipes de recherche pour obtenir de nouveaux résultats dans le domaine de recherche qui se situe à la frontière de la compilation de connaissances, du codage et de la résolution SAT, et de la programmation par contraintes. Dans ce projet, l’accent sera mis sur le format CNF, qui est le principal format d’entrée des solveurs et compilateurs existants. Notre objectif est d’identifier et d’étudier un certain nombre de fragments CNF qui peuvent servir de langages cibles de sortie utiles pour la compilation de connaissances. En effet, les formules CNF étant par essence conjonctives, les représentations compilées qui en résultent peuvent être interprétées facilement. Nous prévoyons d’aborder plusieurs questions qui sont à l’intersection des trois domaines de recherche (décrits ci-dessus) :

• Analyse des solveurs SAT CDCL (qui ajoutent des clauses apprises) en ce qui concerne la complétude de la réfutation unitaire et la complétude de la propagation.
• L’étude de plusieurs codages CNF différents de contraintes globales sélectionnées et la compilation de ces CNF en CNF plus grandes (par l’ajout de clauses), ce qui assurent la cohérence du domaine de la contrainte globale codée.
• Etudier les propriétés de la compilation des connaissances lorsque la sortie est dans un format CNF (pour différents formats d’entrée), en identifiant les stratégies d’encodage possibles pour ce processus.

Partenaires : Ondrej Cepek, Milos Chromy, Petr Kucera, Vorel Vojtech (Department of Theoretical Computer Science and Mathematical Logic, Université Charles de Prague).