Model Counting in the 2mu-3MON Syntactic Class

Abstract

The counting model problem in Boolean formulas is #P-complete, i.e., there is no known deterministic algorithm in the classical computability model (Turing machine) that makes this count in polynomial time. The difficulty persists even imposing more restrictive conditions on the syntactic clases of Boolean formulas. In this paper we present a treatable family within the syntactical class 2_-3MON. The identification of this family is done by using the hypergraph associated with simple structures such as chains and cycles. Then, matrix operators acting over these structures are identified; these operators lead to efficient algorithms that perform the model counting on the identified family in linear time for the number of clauses in the instantiated formula; unlike hypergraphic invariant based methods (such as tree width), which perform the count in cubic time.