Understanding the complexity of #SAT using knowledge compilation
Two main techniques have been used so far to solve the #P-hard problem #SAT. The first one, used in practice, is based on an extension of DPLL for model counting called exhaustive DPLL. The second approach, more theoretical, exploits the structure of the input to compute the number of satisfying assignments by usually using a dynamic programming scheme on a decomposition of the formula. In this paper, we make a first step toward the separation of these two techniques by exhibiting a family of formulas that can be solved in polynomial time with the first technique but needs an exponential time with the second one. We show this by observing that both techniques implicitely construct a very specific boolean circuit equivalent to the input formula. We then show that every beta-acyclic formula can be represented by a polynomial size circuit corresponding to the first method and exhibit a family of beta-acyclic formulas which cannot be represented by polynomial size circuits corresponding to the second method. This result shed a new light on the complexity of #SAT and related problems on beta-acyclic formulas. As a byproduct, we give new handy tools to design algorithms on beta-acyclic hypergraphs.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Phase Transition Behavior in Knowledge Compilation
The study of phase transition behaviour in SAT has led to deeper understanding and algorithmic improvements of modern SAT solvers. Motivated by these prior studies of phase transitions in SAT, we seek to study the behavi…
On the Role of Canonicity in Bottom-up Knowledge Compilation
We consider the problem of bottom-up compilation of knowledge bases, which is usually predicated on the existence of a polytime function for combining compilations using Boolean operators (usually called an Apply functio…
Open-Ended Question AnsweringAn extended Knowledge Compilation Map for Conditional Preference Statements-based and Generalized Additive Utilities-based Languages
Conditional preference statements have been used to compactly represent preferences over combinatorial domains. They are at the core of CP-nets and their generalizations, and lexicographic preference trees. Several works…
New Limits for Knowledge Compilation and Applications to Exact Model Counting
We show new limits on the efficiency of using current techniques to make exact probabilistic inference for large classes of natural problems. In particular we show new lower bounds on knowledge compilation to SDD and DNN…
A Knowledge Compilation Map
We propose a perspective on knowledge compilation which calls for analyzing different compilation approaches according to two key dimensions: the succinctness of the target compilation language, and the class of queries …