arXiv Analytics

Sign in

arXiv:1701.01461 [cs.CC]AbstractReferencesReviewsResources

Understanding the complexity of #SAT using knowledge compilation

Florent Capelli

Published 2017-01-05Version 1

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.

Related articles: Most relevant | Search more
arXiv:1004.5329 [cs.CC] (Published 2010-04-29, updated 2011-06-24)
Settling the complexity of local max-cut (almost) completely
arXiv:1110.0693 [cs.CC] (Published 2011-10-04, updated 2011-11-23)
The Complexity of Rooted Phylogeny Problems
arXiv:cs/0301024 [cs.CC] (Published 2003-01-23)
Complexity and Completeness of Immanants