Computing #2SAT and #2UNSAT by Binary Patterns
We present some results about the parametric complexity of #2SAT and #2UNSAT, which consist on counting the number of models and falsifying assignments, respectively, for two Conjunctive Forms (2-CF’s) . Firstly, we show some cases where given a formula F, #2SAT(F) can be bounded above by considering a binary pattern analysis over its set of clauses. Secondly, since #2SAT(F) = 2 n -#2UNSAT(F) we show that, by considering the constrained graph G F of F, if G F represents an acyclic graph then, #UNSAT(F) can be computed in polynomial time. To the best of our knowledge, this is the first time where #2UNSAT is computed through its constrained graph, since the inclusion-exclusion formula has been commonly used for computing #UNSAT(F).
Keywords#SAT Binary Patterns Enumerative Combinatorics
- 11.Zhou, J., Yin, M., Zhou, C.: New Worts-Case Upper Bound for #2-SAT and #3-SAT with the Number of Clauses as the Parameter. In: Proc. of the AAAI, pp. 217–222 (2010)Google Scholar