A New Probabilistic Algorithm for Approximate Model Counting

作者：Ge, Cunjing; Ma, Feifei^*; Liu, Tian; Zhang, Jian; Ma, Xutong

来源：9th International Joint Conference on Automated Reasoning, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018, 2018-07-14 To 2018-07-17.

DOI：10.1007/978-3-319-94205-6_21

• Approximate model
• Counting models
• Empirical evaluations
• Probabilistic algorithm
• Propositional logic
• Software analysis
• Stopping criteria
• Theoretical guarantees

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 success but still rely on solution enumeration. In this paper, a new probabilistic approximate model counter is proposed, which is also a hashing-based universal framework, but with only satisfiability queries. A dynamic stopping criteria, for the new algorithm, is presented, which has not been studied yet in previous works of hashing-based approaches. Although the new algorithm lacks theoretical guarantee, it works well in practice. Empirical evaluation over benchmarks on propositional logic formulas and SMT(BV) formulas shows that the approach is promising.

• 出版日期2018
• 单位中国科学院大学; 计算机科学国家重点实验室; 北京大学