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实例编译为简洁的表示形式，使得能够高效执行可满足性检测、计数或枚举所有解等操作。该领域研究的实用表示形式涵盖从有序二元决策图（OBDDs）到可分解否定规范形式（DNNFs）电路等多种类型。尽管已知存在需要指数级规模表示的CNF公式，但对于布尔析取子句之外的其他约束类型，相关研究尚不充分。约束满足问题（CSP）作为强大的理论框架，通过允许在任意有限域上定义约束集合，推广了CNF-SAT问题。本文的主要目标是探究何种类型的约束（即约束语言）能够被高效编译为多项式规模的表示形式。我们完整回答了该问题，并根据目标表示形式是否具有结构化特征，给出了可高效编译约束语言的两种严格特征刻画。首先，我们提出"强分块可分解性"的组合性质，证明若约束语言满足此性质，则可构造线性规模的DNNF表示。对于所有其他约束语言，我们构建了CSP实例族，严格证明其需要指数级规模的DNNF表示。针对"强均匀分块可分解"约束语言子类，我们在结构化DNNF表示上获得了类似的对偶性结果。实际上，强（均匀）分块可分解性甚至允许分别高效编译为OBDD和FBDD的多值泛化形式。因此，我们为O(B)DD至DNNF区间内所有知识编译类别提供了完整的特征刻画。