An Enumerative Algorithm for #2SAT

Counting models for two conjunctive forms (2-CF), problem known as #2SAT, is a classic #P-complete problem. We determine different discrete structures on the constrained graph of the 2-CF formula allowing the efficient computation of #2SAT.We show that if the constrained graph of a 2-CF F is acyclic or it has only cycles, which are independent each other, then #2SAT(F) is computed efficiently. On the other hand, we design a bottom-up procedure to compute #2SAT(F) in an incremental way. Given a formula F, our procedure begins with the maximum subformula which does not have intersecting cycles, let say F0. In each iteration of the procedure, a new clause Ci∈(F−F0) is considered in order to form Fi=(Fi−1∧Ci) and then to compute #2SAT(Fi) based on the computation of #2SAT(Fi−1).