logo spi

Les contraintes pseudo-booléennes [1] constituent un formalisme attractif pour la représentation d’informations de nature propositionnelle, interprétée classiquement. Aussi le raisonnement déductif à partir de contraintes pseudo-booléennes se réduit-il au test de cohérence d’un ensemble de contraintes. Pour ce faire, plusieurs approches peuvent être utilisées, par exemple des approches qui opèrent directement à partir de l’ensemble de contraintes en appliquant des règles qui visent à mettre en évidence une contradiction quand il en existe une et des approches qui consistent à réduire l’ensemble de contraintes à une formule propositionnelle qui est cohérente précisément quand l’ensemble des contraintes de départ l’est lui aussi [1].

D’un point de vue théorique, plusieurs systèmes de preuve opérant directement sur l’ensemble de contraintes et réfutationnellement complets ont été mis en évidence, étudiés et comparés [2]. Parmi eux figurent des systèmes à base de résolution [3] et d’autres à base de génération de plans coupes [4]. Le concept de p-simulation joue un rôle clé pour comparer l’efficacité de deux systèmes de preuve en comparant la taille des preuves qui peuvent être obtenues dans chacun d’eux. Un système de preuve A p-simule un second B lorsqu’il existe un polynôme p tel que pour toute formule F ayant une réfutation de longueur LA dans A, il existe une réfutation de F de longueur LB dans B telle que LB ≤ p(LA). En théorie, il est connu que les systèmes de preuve à base de génération de plans coupes sont plus puissants que ceux à base de résolution (les premiers p-simulent les seconds, mais la réciproque est fausse). Toutefois, cette supériorité en théorie n’a pas été jusqu’ici clairement mise en évidence en pratique.

Par ailleurs, la compilation de contraintes pseudo-booléennes est un sujet qui reste également à défricher. Compiler de l’information consiste à la pré-traiter de façon à rendre son exploitation plus efficace du point de vue calculatoire [5]. Ce type d’approche peut se révéler particulièrement utile lorsque des garanties de temps de réponse sont attendues, ce qui est le cas d’applications en ligne nécessitant une interaction avec un utilisateur. Alors que diverses approches ont été proposées depuis plus de vingt ans pour compiler des formules propositionnelles en vue de faciliter certains traitements, comme l’implication clausale ou le comptage de modèles [6], définir des pré-traitements de contraintes pseudo-booléennes pour rendre le raisonnement plus efficace reste essentiellement à réaliser. Or, la construction de représentations compilées est typiquement obtenue en suivant la trace d’un algorithme de recherche de preuve [7]. L’utilisation de systèmes de preuve plus puissants devrait donc permettre la construction de représentations compilées plus succinctes, mais le gain en espace obtenu en pratique reste également à évaluer.

Le travail à réaliser comporte un volet théorique et un volet pratique. D’un point de vue théorique, il s’agira d’une part de définir formellement les langages cibles correspondant aux deux familles de systèmes de preuve considérées, puis d’étudier ces langages en s’appuyant sur les critères d’efficacité temporelle et spatiale utilisés dans les cartes de compilation propositionnelle.

D’un point de vue pratique, l’objectif sera de développer et d’évaluer des compilateurs vers les langages cibles possibles et comparer leur efficacité pratique avec celle d’une approche directe, sans compilation, et une approche passant par une traduction en CNF, suivie d’une compilation en Decision-DNNF [8].

Quelques références

[1] Olivier Roussel, Vasco M. Manquinho: Pseudo-Boolean and Cardinality Constraints. Handbook of Satisfiability 2009: 695-733

[2] Jakob Nordström: On the interplay between proof complexity and SAT solving. SIGLOG News 2(3): 19-44

[3] Archie Blake. 1937. Canonical Expressions in Boolean Algebra. Ph.D. Dissertation. University of Chicago.

[4] William Cook, Collette Rene Coullard, and Gyorgy Turan. 1987. On the Complexity of Cutting-Plane Proofs. Discrete Applied Mathematics 18, 1 (Nov. 1987), 25–38.

[5] Pierre Marquis: Compile! AAAI 2015: 4112-4118.

[6] Adnan Darwiche, Pierre Marquis: A Knowledge Compilation Map. J. Artif. Intell. Res. (JAIR) 17: 229-264 (2002).

[7] Jinbo Huang, Adnan Darwiche: DPLL with a Trace: From SAT to Knowledge Compilation. IJCAI 2005: 156-162.

[8] Adnan Darwiche: Decomposable negation normal form. J. ACM 48(4): 608-647 (2001).