On the Use of Partially Ordered Decision Graphs for Knowledge Compilation and Quantified Boolean Formulae

Hélène Fargier (1, 2) , Pierre Marquis (3)

1 IRIT-ADRIA - Argumentation, Décision, Raisonnement, Incertitude et Apprentissage
2 CNRS - Centre National de la Recherche Scientifique
3 CRIL - Centre de Recherche en Informatique de Lens

Decomposable Negation Normal Form formulae DNNFs form an interesting propositional fragment, both for efficiency and succinctness reasons. A famous subclass of the DNNF fragment is the OBDD fragment which offers many polytime queries and transformations, including quantifier eliminations (under some ordering restrictions). Nevertheless, the decomposable AND nodes at work in OBDDs enable only sequential decisions: clusters of variables are never assigned "in parallel" like in full DNNFs. This is an serious drawback since succinctness for the full t DNNF fragment relies on such a "parallelization property". This is why we suggest to go a step further, from (sequentially) ordered decision diagrams to (partially) ordered, decomposable decision graphs, in which any decomposable AND node is allowed, and not only assignment ones. We show that, like the OBDD fragment, such a new class offers many tractable queries and transformations, including quantifier eliminations under some ordering restrictions. Furthermore, we show that this class is strictly more succinct than OBDD.

Mots clés: Knowledge Representation; Computational Complexity

Domaines: Intelligence artificielle [cs.AI]

Hélène Fargier, Pierre Marquis. On the Use of Partially Ordered Decision Graphs for Knowledge Compilation and Quantified Boolean Formulae. 21st National Conference on Artificial Intelligence (AAAI 2006), AAAI: Association for the Advancement of Artificial Intelligence, Jul 2006, Boston, Massachusetts, United States. pp.42-47. ⟨hal-03300967⟩