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). © 2012 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
De Ita Luna, G., & Marcial-Romero, J. R. (2012). Computing #2SAT and #2UNSAT by binary patterns. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7329 LNCS, pp. 273–282). https://doi.org/10.1007/978-3-642-31149-9_28
Mendeley helps you to discover research relevant for your work.