A Fast and Efficient Method for #2SAT via Graph Transformations

摘要

In this paper we present an implementation (markSAT) for computing #2SAT via graph transformations. For that, we transform the input formula into a graph and test whether it is which we call a cactus graph. If it is not the case, the formula is decomposed until cactus sub-formulas are obtained. We compare the efficiency of markSAT against sharpSAT which is the leading sequential algorithm in the literature for computing #SAT obtaining better results with our proposal.