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

Original language | English |
---|---|

Title of host publication | Theory and Applications of Satisfiability Testing – SAT 2015 |

Subtitle of host publication | 18th International Conference Austin, TX, USA, September 24–27, 2015 Proceedings |

Editors | Marijn Heule, Sean Weaver |

Place of Publication | Cham Switzerland |

Publisher | Springer |

Pages | 121-137 |

Number of pages | 17 |

ISBN (Electronic) | 9783319243184 |

ISBN (Print) | 9783319243177 |

DOIs | |

Publication status | Published - 2015 |

Externally published | Yes |

Event | International Conference on Theory and Applications of Satisfiability Testing 2015 - Austin, United States of America Duration: 24 Sep 2015 → 27 Sep 2015 Conference number: 18th https://www.cs.utexas.edu/~marijn/sat15/ |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer |

Volume | 9340 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Conference

Conference | International Conference on Theory and Applications of Satisfiability Testing 2015 |
---|---|

Abbreviated title | SAT 2015 |

Country | United States of America |

City | Austin |

Period | 24/09/15 → 27/09/15 |

Internet address |