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-FBDDX,Y and Sym-DDGX,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-FBDDX,Y and Sym-DDGX,Y are analyzed, in order to put those languages in the knowledge compilation map for propositional representations. It turns out that each of Sym-FBDDX,Y and Sym-DDGX,Y satisfies CT (the model counting query). We prove that no propositional language over a set X∪Y of variables, satisfying both CO (the consistency query) and CD (the conditioning transformation), is at least as succinct as any of Sym-FBDDX,Y and Sym-DDGX,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-FBDDX,Y and Sym-DDGX,Y . Nevertheless, this proves sufficient for a number of applications, including configuration and planning. We describe a compiler targeting Sym-FBDDX,Y and Sym-DDGX,Y and give some experimental results on planning domains, highlighting the practical significance of these languages.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 firstname.lastname@example.org
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 email@example.com