FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
A New Probabilistic Algorithm for Approximate Model Counting

Authors: Cunjing Ge, Feifei Ma, Tian Liu, Jian Zhang and Xutong Ma

Paper Information

Title:A New Probabilistic Algorithm for Approximate Model Counting
Authors:Cunjing Ge, Feifei Ma, Tian Liu, Jian Zhang and Xutong Ma
Proceedings:IJCAR Proceedings 9th IJCAR, 2018
Editors: Stephan Schulz, Didier Galmiche and Roberto Sebastiani
Keywords:Model Counting, #SMT(BV), Probabilistic Algorithm
Abstract:

ABSTRACT. Constrained counting is important in domains ranging from artificial intelligence to software analysis. There are already a few approaches for counting models over various types of constraints. Recently, hashing-based approaches achieve both theoretical guarantees and scalability, but still rely on solution enumeration. In this paper, a correlation between the model count and the probability of the hashed formula being unsatisfiable is revealed. Despite it has not been proved, experimental results fit the analysis based on it well. With such correlation, a new probabilistic approximate model counter is proposed, which is also a hashing-based universal framework, but with only satisfiability queries. A variant with a dynamic stopping criterion is also presented. Empirical evaluation over benchmarks on propositional logic formulas and SMT(BV) formulas shows that the approach is promising.

Pages:16
Talk:Jul 14 15:00 (Session 96E: SAT Extensions & Applications)
Paper: