A characterization of efficiently compilable constraint languages
Symposium on Theoretical Aspects of Computer Science(2023)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要