#∃SAT: projected model counting

Rehan Abdul Aziz, Geoffrey Chu, Christian Muise, Peter Stuckey

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

15 Citations (Scopus)


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.

Original languageEnglish
Title of host publicationTheory and Applications of Satisfiability Testing – SAT 2015
Subtitle of host publication18th International Conference Austin, TX, USA, September 24–27, 2015 Proceedings
EditorsMarijn Heule, Sean Weaver
Place of PublicationCham Switzerland
Number of pages17
ISBN (Electronic)9783319243184
ISBN (Print)9783319243177
Publication statusPublished - 2015
Externally publishedYes
EventInternational Conference on Theory and Applications of Satisfiability Testing 2015 - Austin, United States of America
Duration: 24 Sep 201527 Sep 2015
Conference number: 18th

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceInternational Conference on Theory and Applications of Satisfiability Testing 2015
Abbreviated titleSAT 2015
CountryUnited States of America
Internet address

Cite this