A central task in knowledge compilation is to compile a CNF-SAT instance into a succinct representation format that allows efficient operations such as testing satisfiability, counting, or enumerating all solutions. Useful representation formats studied in this area range from ordered binary decision diagrams (OBDDs) to circuits in decomposable negation normal form (DNNFs). While it is known that there exist CNF formulas that require exponential size representations, the situation is less well studied for other types of constraints than Boolean disjunctive clauses. The constraint satisfaction problem (CSP) is a powerful framework that generalizes CNF-SAT by allowing arbitrary sets of constraints over any finite domain. The main goal of our work is to understand for which type of constraints (also called the constraint language) it is possible to efficiently compute representations of polynomial size. We answer this question completely and prove two tight characterizations of efficiently compilable constraint languages, depending on whether target format is structured. We first identify the combinatorial property of ``strong blockwise decomposability'' and show that if a constraint language has this property, we can compute DNNF representations of linear size. For all other constraint languages we construct families of CSP-instances that provably require DNNFs of exponential size. For a subclass of ``strong uniformly blockwise decomposable'' constraint languages we obtain a similar dichotomy for structured DNNFs. In fact, strong (uniform) blockwise decomposability even allows efficient compilation into multi-valued analogs of OBDDs and FBDDs, respectively. Thus, we get complete characterizations for all knowledge compilation classes between O(B)DDs and DNNFs.

翻译：知识编译的核心任务是将CNF-SAT实例编译为简洁的表示形式，从而支持诸如可满足性测试、计数或枚举所有解等高效操作。该领域研究的有效表示形式包括有序二叉决策图（OBDD）以及可分解否定范式（DNNF）电路等。尽管已知存在需要指数级规模表示的CNF公式，但对于布尔析取子句之外的其他约束类型，情况的研究尚不充分。约束满足问题（CSP）是一个强大的框架，它允许在任意有限域上使用任意约束集，从而推广了CNF-SAT。我们工作的主要目标是理解对于何种类型的约束（也称为约束语言），能够高效计算多项式规模的表示。我们彻底回答了这个问题，并针对目标格式是否有结构，分别证明了两个紧致的可高效编译约束语言的刻画。我们首先识别出“强块状可分解性”这一组合性质，并证明若约束语言具有该性质，则可计算线性规模的DNNF表示。对于所有其他约束语言，我们构造了必然需要指数规模DNNF的CSP实例族。对于一类“强一致块状可分解”约束语言的子类，我们获得了类似的结构化DNNF二分性。实际上，强（一致）块状可分解性甚至允许分别高效编译为OBDD和FBDD的多值对应的形式。因此，我们得到了介于O(B)DD与DNNF之间的所有知识编译类的完整刻画。