#∃sat: Projected model counting

Abstract

Model counting is the task of computing the number of assignments to variables V that satisfy a given propositional theory F. The model counting problem is denoted as #SAT. Model counting is an essential tool in probabilistic reasoning. In this paper, we introduce the problem of model counting projected on a subset of original variables that we call priority variables P ⊆ V. The task is to compute the number of assignments to P such that there exists an extension to non-priority variables V\P that satisfies F. We denote this as #∃SAT. Projected model counting arises when some parts of the model are irrelevant to the counts, in particular when we require additional variables to model the problem we are counting in SAT. We discuss three different approaches to #∃SAT (two of which are novel), and compare their performance on different benchmark problems.