New Polynomial Classes for #2SAT Established Via Graph-Topological Structure
Guillermo De Ita Luna, Pedro Bello, Meliza Contreras González · Engineering letters · 2007
We address the problem of designing ef- ficient procedures for counting models of Boolean formulas and, in this task, we establish new classes of instances where #2SAT is solved in polynomial time. Those instances are recognized by the topo- logical structure of the underlying graph of the in- stances. We show that, if the depth-search over the constrained graph of a formula generates a tree where the set of fundamental cycles are disjointed (there are not common edges between any pair of fundamental cycles), then #2SAT is tractable. This class of in- stances do not set restrictions on the number of oc- currences of a variable in a Boolean formula. Our proposal can be applied to impact directly in the re- duction of the complexity time of the algorithms for