Summary: In this paper, symmetries are exploited for achieving significant space savings in a knowledge compilation perspective. More precisely, the languages FBDD and DDG of decision diagrams are extended to the languages Sym-FBDD\(_{X,Y}\) and Sym-DDG\(_{X,Y}\) of symmetry-driven decision diagrams, where \(X\) is a set of “symmetry-free” variables and \(Y\) is a set of “top” variables. Both the time efficiency and the space efficiency of Sym-FBDD\(_{X,Y}\) and Sym-DDG\(_{X,Y}\) are analyzed, in order to put those languages in the knowledge compilation map for propositional representations. It turns out that each of Sym-FBDD\(_{X,Y}\) and Sym-DDG\(_{X,Y}\) satisfies CT (the model counting query). We prove that no propositional language over a set \(X\cup Y\) of variables, satisfying both CO (the consistency query) and CD (the conditioning transformation), is at least as succinct as any of Sym-FBDD\(_{X,Y}\) and Sym-DDG\(_{X,Y}\) unless the polynomial hierarchy collapses. The price to be paid is that only a restricted form of conditioning and a restricted form of forgetting are offered by Sym-FBDD\(_{X,Y}\) and Sym-DDG\(_{X,Y}\). Nevertheless, this proves sufficient for a number of applications, including configuration and planning. We describe a compiler targeting Sym-FBDD\(_{X,Y}\) and Sym-DDG\(_{X,Y}\) and give some experimental results on planning domains, highlighting the practical significance of these languages.
For the entire collection see [Zbl 1296.68011].