Skip to main content
Top

2018 | OriginalPaper | Chapter

A New Probabilistic Algorithm for Approximate Model Counting

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

Published in: Automated Reasoning

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Footnotes
1
Our tools STAC_CNF and STAC_BV and the suite of benchmarks are available at
 
Literature
2.
go back to reference Bayardo, Jr, R.J., Schrag, R.: Using CSP look-back techniques to solve real-world SAT instances. In: Proceedings of AAAI, pp. 203–208 (1997) Bayardo, Jr, R.J., Schrag, R.: Using CSP look-back techniques to solve real-world SAT instances. In: Proceedings of AAAI, pp. 203–208 (1997)
3.
go back to reference Bellare, M., Goldreich, O., Petrank, E.: Uniform generation of NP-witnesses using an NP-oracle. Inf. Comput. 163(2), 510–526 (2000)MathSciNetCrossRef Bellare, M., Goldreich, O., Petrank, E.: Uniform generation of NP-witnesses using an NP-oracle. Inf. Comput. 163(2), 510–526 (2000)MathSciNetCrossRef
4.
go back to reference Belle, V., Broeck, G.V., Passerini, A.: Hashing-based approximate probabilistic inference in hybrid domains. In: Proceedings of UAI, pp. 141–150 (2015) Belle, V., Broeck, G.V., Passerini, A.: Hashing-based approximate probabilistic inference in hybrid domains. In: Proceedings of UAI, pp. 141–150 (2015)
5.
go back to reference Brown, L.D., Cai, T.T., Dasgupta, A.: Interval estimation for a binomial proportion. Stat. Sci. 16(2), 101–133 (2001)MathSciNetMATH Brown, L.D., Cai, T.T., Dasgupta, A.: Interval estimation for a binomial proportion. Stat. Sci. 16(2), 101–133 (2001)MathSciNetMATH
7.
go back to reference Chakraborty, S., Fremont, D.J., Meel, K.S., Seshia, S.A., Vardi, M.Y.: Distribution-aware sampling and weighted model counting for SAT. In: Proceedings of AAAI, pp. 1722–1730 (2014) Chakraborty, S., Fremont, D.J., Meel, K.S., Seshia, S.A., Vardi, M.Y.: Distribution-aware sampling and weighted model counting for SAT. In: Proceedings of AAAI, pp. 1722–1730 (2014)
8.
go back to reference Chakraborty, S., Meel, K.S., Mistry, R., Vardi, M.Y.: Approximate probabilistic inference via word-level counting. In: Proceedings of AAAI, pp. 3218–3224 (2016) Chakraborty, S., Meel, K.S., Mistry, R., Vardi, M.Y.: Approximate probabilistic inference via word-level counting. In: Proceedings of AAAI, pp. 3218–3224 (2016)
11.
go back to reference Chakraborty, S., Meel, K.S., Vardi, M.Y.: Algorithmic improvements in approximate counting for probabilistic inference: from linear to logarithmic SAT calls. In: Proceedings of IJCAI, pp. 3569–3576 (2016) Chakraborty, S., Meel, K.S., Vardi, M.Y.: Algorithmic improvements in approximate counting for probabilistic inference: from linear to logarithmic SAT calls. In: Proceedings of IJCAI, pp. 3569–3576 (2016)
12.
go back to reference Chavira, M., Darwiche, A.: On probabilistic inference by weighted model counting. Artif. Intell. 172(6–7), 772–799 (2008)MathSciNetCrossRef Chavira, M., Darwiche, A.: On probabilistic inference by weighted model counting. Artif. Intell. 172(6–7), 772–799 (2008)MathSciNetCrossRef
14.
go back to reference Domshlak, C., Hoffmann, J.: Probabilistic planning via heuristic forward search and weighted model counting. J. Artif. Intell. Res. (JAIR) 30, 565–620 (2007)MathSciNetMATH Domshlak, C., Hoffmann, J.: Probabilistic planning via heuristic forward search and weighted model counting. J. Artif. Intell. Res. (JAIR) 30, 565–620 (2007)MathSciNetMATH
15.
go back to reference Ermon, S., Gomes, C.P., Sabharwal, A., Selman, B.: Embed and project: discrete sampling with universal hashing. Adv. Neural Inf. Process. Syst. 26, 2085–2093 (2013) Ermon, S., Gomes, C.P., Sabharwal, A., Selman, B.: Embed and project: discrete sampling with universal hashing. Adv. Neural Inf. Process. Syst. 26, 2085–2093 (2013)
16.
go back to reference Ermon, S., Gomes, C.P., Selman, B.: Uniform solution sampling using a constraint solver as an oracle. In: Proceedings of UAI, pp. 255–264 (2012) Ermon, S., Gomes, C.P., Selman, B.: Uniform solution sampling using a constraint solver as an oracle. In: Proceedings of UAI, pp. 255–264 (2012)
17.
go back to reference Filieri, A., Pasareanu, C.S., Visser, W.: Reliability analysis in symbolic pathfinder: a brief summary. In: Proceedings of ICSE, pp. 39–40 (2014) Filieri, A., Pasareanu, C.S., Visser, W.: Reliability analysis in symbolic pathfinder: a brief summary. In: Proceedings of ICSE, pp. 39–40 (2014)
18.
go back to reference Filieri, A., Pasareanu, C.S., Yang, G.: Quantification of software changes through probabilistic symbolic execution (N). In: Proceedings of ASE, pp. 703–708 (2015) Filieri, A., Pasareanu, C.S., Yang, G.: Quantification of software changes through probabilistic symbolic execution (N). In: Proceedings of ASE, pp. 703–708 (2015)
19.
go back to reference Fredrikson, M., Jha, S.: Satisfiability modulo counting: a new approach for analyzing privacy properties. In: Proceedings of CSL-LICS, pp. 42:1–42:10 (2014) Fredrikson, M., Jha, S.: Satisfiability modulo counting: a new approach for analyzing privacy properties. In: Proceedings of CSL-LICS, pp. 42:1–42:10 (2014)
20.
go back to reference Geldenhuys, J., Dwyer, M.B., Visser, W.: Probabilistic symbolic execution. In: Proceedings of ISSTA, pp. 166–176 (2012) Geldenhuys, J., Dwyer, M.B., Visser, W.: Probabilistic symbolic execution. In: Proceedings of ISSTA, pp. 166–176 (2012)
22.
go back to reference Gomes, C.P., Hoffmann, J., Sabharwal, A., Selman, B.: From sampling to model counting. In: Proceedings of IJCAI, pp. 2293–2299 (2007) Gomes, C.P., Hoffmann, J., Sabharwal, A., Selman, B.: From sampling to model counting. In: Proceedings of IJCAI, pp. 2293–2299 (2007)
23.
go back to reference Gomes, C.P., Sabharwal, A., Selman, B.: Model counting: a new strategy for obtaining good bounds. In: Proceedings of AAAI, pp. 54–61 (2006) Gomes, C.P., Sabharwal, A., Selman, B.: Model counting: a new strategy for obtaining good bounds. In: Proceedings of AAAI, pp. 54–61 (2006)
24.
go back to reference Gomes, C.P., Sabharwal, A., Selman, B.: Near-uniform sampling of combinatorial spaces using XOR constraints. Adv. Neural Inf. Process. Syst. 19, 481–488 (2006) Gomes, C.P., Sabharwal, A., Selman, B.: Near-uniform sampling of combinatorial spaces using XOR constraints. Adv. Neural Inf. Process. Syst. 19, 481–488 (2006)
25.
go back to reference Ivrii, A., Malik, S., Meel, K.S., Vardi, M.Y.: On computing minimal independent support and its applications to sampling and counting. Constraints 21(1), 41–58 (2016)MathSciNetCrossRef Ivrii, A., Malik, S., Meel, K.S., Vardi, M.Y.: On computing minimal independent support and its applications to sampling and counting. Constraints 21(1), 41–58 (2016)MathSciNetCrossRef
26.
go back to reference Karp, R.M., Luby, M., Madras, N.: Monte-carlo approximation algorithms for enumeration problems. J. Algorithms 10(3), 429–448 (1989)MathSciNetCrossRef Karp, R.M., Luby, M., Madras, N.: Monte-carlo approximation algorithms for enumeration problems. J. Algorithms 10(3), 429–448 (1989)MathSciNetCrossRef
27.
go back to reference Kroc, L., Sabharwal, A., Selman, B.: Leveraging belief propagation, backtrack search, and statistics for model counting. Ann. OR 184(1), 209–231 (2011)MathSciNetCrossRef Kroc, L., Sabharwal, A., Selman, B.: Leveraging belief propagation, backtrack search, and statistics for model counting. Ann. OR 184(1), 209–231 (2011)MathSciNetCrossRef
28.
go back to reference Liu, S., Zhang, J.: Program analysis: from qualitative analysis to quantitative analysis. In: Proceedings of ICSE, pp. 956–959 (2011) Liu, S., Zhang, J.: Program analysis: from qualitative analysis to quantitative analysis. In: Proceedings of ICSE, pp. 956–959 (2011)
29.
go back to reference Meel, K.S., Vardi, M.Y., Chakraborty, S., Fremont, D.J., Seshia, S.A., Fried, D., Ivrii, A., Malik, S.: Constrained sampling and counting: universal hashing meets SAT solving. In: Proceedings of Workshop on Beyond NP (BNP) (2016) Meel, K.S., Vardi, M.Y., Chakraborty, S., Fremont, D.J., Seshia, S.A., Fried, D., Ivrii, A., Malik, S.: Constrained sampling and counting: universal hashing meets SAT solving. In: Proceedings of Workshop on Beyond NP (BNP) (2016)
30.
go back to reference Phan, Q., Malacaria, P., Pasareanu, C.S., d’Amorim, M.: Quantifying information leaks using reliability analysis. In: Proceedings of SPIN, pp. 105–108 (2014) Phan, Q., Malacaria, P., Pasareanu, C.S., d’Amorim, M.: Quantifying information leaks using reliability analysis. In: Proceedings of SPIN, pp. 105–108 (2014)
32.
go back to reference Sang, T., Bacchus, F., Beame, P., Kautz, H.A., Pitassi, T.: Combining component caching and clause learning for effective model counting. In: Proceedings of SAT (2004) Sang, T., Bacchus, F., Beame, P., Kautz, H.A., Pitassi, T.: Combining component caching and clause learning for effective model counting. In: Proceedings of SAT (2004)
33.
go back to reference Sang, T., Beame, P., Kautz, H.A.: Performing bayesian inference by weighted model counting. In: Proceedings of AAAI, pp. 475–482 (2005) Sang, T., Beame, P., Kautz, H.A.: Performing bayesian inference by weighted model counting. In: Proceedings of AAAI, pp. 475–482 (2005)
34.
go back to reference Sipser, M.: A complexity theoretic approach to randomness. In: Proceedings of the 15th Annual ACM Symposium on Theory of Computing, pp. 330–335 (1983) Sipser, M.: A complexity theoretic approach to randomness. In: Proceedings of the 15th Annual ACM Symposium on Theory of Computing, pp. 330–335 (1983)
36.
go back to reference Stockmeyer, L.J.: The complexity of approximate counting (preliminary version). In: Proceedings of the 15th Annual ACM Symposium on Theory of Computing, pp. 118–126 (1983) Stockmeyer, L.J.: The complexity of approximate counting (preliminary version). In: Proceedings of the 15th Annual ACM Symposium on Theory of Computing, pp. 118–126 (1983)
37.
38.
go back to reference Wallis, S.: Binomial confidence intervals and contingency tests: mathematical fundamentals and the evaluation of alternative methods. J. Quant. Linguist. 20(3), 178–208 (2013)CrossRef Wallis, S.: Binomial confidence intervals and contingency tests: mathematical fundamentals and the evaluation of alternative methods. J. Quant. Linguist. 20(3), 178–208 (2013)CrossRef
40.
go back to reference Wilson, E.B.: Probable inference, the law of succession and statistical inference. J. Am. Stat. Assoc. 22(158), 209–212 (1927)CrossRef Wilson, E.B.: Probable inference, the law of succession and statistical inference. J. Am. Stat. Assoc. 22(158), 209–212 (1927)CrossRef
Metadata
Title
A New Probabilistic Algorithm for Approximate Model Counting
Authors
Cunjing Ge
Feifei Ma
Tian Liu
Jian Zhang
Xutong Ma
Copyright Year
2018
DOI
https://doi.org/10.1007/978-3-319-94205-6_21

Premium Partner