Computing #2SAT and #2UNSAT by Binary Patterns

  • Guillermo De Ita Luna
  • J. Raymundo Marcial-Romero
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7329)


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).


#SAT Binary Patterns Enumerative Combinatorics 


  1. 1.
    Dahllöf, V., Jonsson, P., Wahlström, M.: Counting models for 2SAT and 3SAT formulae. Theoretical Computer Sciences 332(1-3), 265–291 (2005)zbMATHCrossRefGoogle Scholar
  2. 2.
    De Ita, G., Marcial-Romero, R., Hernández, J.A.: A threshold for a Polynomial Solution of #2SAT. Fundamenta Informaticae 113(1), 63–77 (2011)MathSciNetzbMATHGoogle Scholar
  3. 3.
    De Ita, G., Bello, P., Contreras, M.: New Polynomial Classes for #2SAT Established Via Graph-Topological Structure. Engineering Letters 15(2), 250–258 (2007), Google Scholar
  4. 4.
    Olivier, D.: Counting the number of solutions for instances of satisfiability. Theor. Comp. Sc. 81, 49–64 (1991)zbMATHCrossRefGoogle Scholar
  5. 5.
    Gusfield, D., Pitt, L.: A bounded approximation for the minimum cost 2-Sat problem. Algorithmica 8, 103–117 (1992)MathSciNetzbMATHCrossRefGoogle Scholar
  6. 6.
    Linial, N., Nisan, N.: Approximate inclusion-exclusion. Combinatorica 10(4), 349–365 (1990)MathSciNetzbMATHCrossRefGoogle Scholar
  7. 7.
    Lozinskii, E.: Counting propositional models. Inf. Proc. Letters 41, 327–332 (1992)MathSciNetzbMATHCrossRefGoogle Scholar
  8. 8.
    Roth, D.: On the hardness of approximate reasoning. Artificial Intelligence 82, 273–302 (1996)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Vadhan Salil, P.: The Complexity of Counting in Sparse, Regular, and Planar Graphs. SIAM Journal on Computing 31(2), 398–427 (2001)MathSciNetzbMATHCrossRefGoogle Scholar
  10. 10.
    Wahlström, M.: A Tighter Bound for Counting Max-Weight Solutions to 2SAT Instances. In: Grohe, M., Niedermeier, R. (eds.) IWPEC 2008. LNCS, vol. 5018, pp. 202–213. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  11. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Guillermo De Ita Luna
    • 1
  • J. Raymundo Marcial-Romero
    • 2
  1. 1.Faculty of Computer SciencesBUAPMexico
  2. 2.Facultad de IngenieríaUAEMMexico

Personalised recommendations