Conference Proceedings

#∃SAT: Projected Model Counting

RA Aziz, G Chu, C Muise, P Stuckey, M Heule (ed.), S Weaver (ed.)

Lecture Notes in Computer Science | Springer International Publishing | Published : 2015

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 prob..

View full abstract