Projected Model Counting
  Model counting is the task of computing the number of assignments to
variables V that satisfy a given propositional theory F. Model counting is an
essential tool in probabilistic reasoning. In this paper, we introduce the
problem of model counting projected on a subset P of original variables that we
call 'priority' variables. 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. 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 projected model counting (two of which are novel), and compare their
performance on different benchmark problems.
  To appear in 18th International Conference on Theory and Applications of
Satisfiability Testing, September 24-27, 2015, Austin, Texas, USA
