A Polynomial Graphical Reduction to Speed Up

Workshop in Logic, Language and Computation

the Counting of Models for Boolean Formulas

PID  :  79566

来源: CEUR

【 摘 要 】

In this paper, we focus on exact, deterministic algorithms forcomputing the number of models in Boolean formulas in Two Conjuntive Form (2CF), denoted as #2SAT problem. We present a series of linear procedures which when they are integrated into a main program, allow us to compute in polynomial time the number of models of a formula F in 2CF when the constraint graph GF holds the following condition: GF can be reduced to one free tree joined with a set of fundamental cycles, and such that those cyles are nonintersected (any pair of cycles do not share edges) or, they are intersected in just one edge. The resulting method for counting models in a 2CF could be used to impact directly in the reduction of the complexity time of the algorithms for other counting problems.