Nothing Special   »   [go: up one dir, main page]
Skip to main content
SpringerLink
Log in

A New Probabilistic Algorithm for Approximate Model Counting

  • Conference paper
  • First Online:
Automated Reasoning (IJCAR 2018)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 10900))

Included in the following conference series:

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.

This work has been supported by the National 973 Program of China under Grant 2014CB340701, Key Research Program of Frontier Sciences, Chinese Academy of Sciences (CAS) under Grant QYZDJ-SSW-JSC036, and the National Natural Science Foundation of China under Grant 61100064. Feifei Ma is also supported by the Youth Innovation Promotion Association, CAS.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    Our tools STAC_CNF and STAC_BV and the suite of benchmarks are available at

    https://github.com/bearben/STAC.

References

  1. Achlioptas, D., Theodoropoulos, P.: Probabilistic model counting with short XORs. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 3–19. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66263-3_1

    Chapter  Google Scholar 

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

    Google Scholar 

  3. Bellare, M., Goldreich, O., Petrank, E.: Uniform generation of NP-witnesses using an NP-oracle. Inf. Comput. 163(2), 510–526 (2000)

    Article  MathSciNet  Google Scholar 

  4. Belle, V., Broeck, G.V., Passerini, A.: Hashing-based approximate probabilistic inference in hybrid domains. In: Proceedings of UAI, pp. 141–150 (2015)

    Google Scholar 

  5. Brown, L.D., Cai, T.T., Dasgupta, A.: Interval estimation for a binomial proportion. Stat. Sci. 16(2), 101–133 (2001)

    MathSciNet  MATH  Google Scholar 

  6. Brummayer, R., Biere, A.: Boolector: an efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 174–177. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00768-2_16

    Chapter  MATH  Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  9. Chakraborty, S., Meel, K.S., Vardi, M.Y.: A scalable and nearly uniform generator of SAT witnesses. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 608–623. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_40

    Chapter  Google Scholar 

  10. Chakraborty, S., Meel, K.S., Vardi, M.Y.: A scalable approximate model counter. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 200–216. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40627-0_18

    Chapter  Google Scholar 

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

    Google Scholar 

  12. Chavira, M., Darwiche, A.: On probabilistic inference by weighted model counting. Artif. Intell. 172(6–7), 772–799 (2008)

    Article  MathSciNet  Google Scholar 

  13. Chistikov, D., Dimitrova, R., Majumdar, R.: Approximate counting in SMT and value estimation for probabilistic programs. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 320–334. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_26

    Chapter  Google Scholar 

  14. Domshlak, C., Hoffmann, J.: Probabilistic planning via heuristic forward search and weighted model counting. J. Artif. Intell. Res. (JAIR) 30, 565–620 (2007)

    MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  17. Filieri, A., Pasareanu, C.S., Visser, W.: Reliability analysis in symbolic pathfinder: a brief summary. In: Proceedings of ICSE, pp. 39–40 (2014)

    Google Scholar 

  18. Filieri, A., Pasareanu, C.S., Yang, G.: Quantification of software changes through probabilistic symbolic execution (N). In: Proceedings of ASE, pp. 703–708 (2015)

    Google Scholar 

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

    Google Scholar 

  20. Geldenhuys, J., Dwyer, M.B., Visser, W.: Probabilistic symbolic execution. In: Proceedings of ISSTA, pp. 166–176 (2012)

    Google Scholar 

  21. von Gleissenthall, K., Köpf, B., Rybalchenko, A.: Symbolic polytopes for quantitative interpolation and verification. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 178–194. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_11

    Chapter  MATH  Google Scholar 

  22. Gomes, C.P., Hoffmann, J., Sabharwal, A., Selman, B.: From sampling to model counting. In: Proceedings of IJCAI, pp. 2293–2299 (2007)

    Google Scholar 

  23. Gomes, C.P., Sabharwal, A., Selman, B.: Model counting: a new strategy for obtaining good bounds. In: Proceedings of AAAI, pp. 54–61 (2006)

    Google Scholar 

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

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  26. Karp, R.M., Luby, M., Madras, N.: Monte-carlo approximation algorithms for enumeration problems. J. Algorithms 10(3), 429–448 (1989)

    Article  MathSciNet  Google Scholar 

  27. Kroc, L., Sabharwal, A., Selman, B.: Leveraging belief propagation, backtrack search, and statistics for model counting. Ann. OR 184(1), 209–231 (2011)

    Article  MathSciNet  Google Scholar 

  28. Liu, S., Zhang, J.: Program analysis: from qualitative analysis to quantitative analysis. In: Proceedings of ICSE, pp. 956–959 (2011)

    Google Scholar 

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

    Google Scholar 

  30. Phan, Q., Malacaria, P., Pasareanu, C.S., d’Amorim, M.: Quantifying information leaks using reliability analysis. In: Proceedings of SPIN, pp. 105–108 (2014)

    Google Scholar 

  31. Roth, D.: On the hardness of approximate reasoning. Artif. Intell. 82(1–2), 273–302 (1996)

    Article  MathSciNet  Google Scholar 

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

    Google Scholar 

  33. Sang, T., Beame, P., Kautz, H.A.: Performing bayesian inference by weighted model counting. In: Proceedings of AAAI, pp. 475–482 (2005)

    Google Scholar 

  34. Sipser, M.: A complexity theoretic approach to randomness. In: Proceedings of the 15th Annual ACM Symposium on Theory of Computing, pp. 330–335 (1983)

    Google Scholar 

  35. Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 244–257. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02777-2_24

    Chapter  Google Scholar 

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

    Google Scholar 

  37. Valiant, L.G.: The complexity of enumeration and reliability problems. SIAM J. Comput. 8(3), 410–421 (1979)

    Article  MathSciNet  Google Scholar 

  38. Wallis, S.: Binomial confidence intervals and contingency tests: mathematical fundamentals and the evaluation of alternative methods. J. Quant. Linguist. 20(3), 178–208 (2013)

    Article  Google Scholar 

  39. Wei, W., Selman, B.: A new approach to model counting. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 324–339. Springer, Heidelberg (2005). https://doi.org/10.1007/11499107_24

    Chapter  Google Scholar 

  40. Wilson, E.B.: Probable inference, the law of succession and statistical inference. J. Am. Stat. Assoc. 22(158), 209–212 (1927)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China

    Cunjing Ge, Feifei Ma & Jian Zhang

  2. Laboratory of Parallel Software and Computational Science, Institute of Software, Chinese Academy of Sciences, Beijing, China

    Feifei Ma

  3. University of Chinese Academy of Sciences, Beijing, China

    Cunjing Ge, Feifei Ma, Jian Zhang & Xutong Ma

  4. School of Electronics Engineering and Computer Science, Peking University, Beijing, China

    Tian Liu

  5. Technology Center of Software Engineering, Institute of Software, Chinese Academy of Sciences, Beijing, China

    Xutong Ma

Authors
  1. Cunjing Ge
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Feifei Ma
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Tian Liu
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Jian Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Xutong Ma
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Feifei Ma .

Editor information

Editors and Affiliations

  1. Université de Lorraine, Vandoeuvre-lès-Nancy, France

    Didier Galmiche

  2. Baden-Wuerttemberg Cooperative State University, Stuttgart, Germany

    Stephan Schulz

  3. University of Trento, Trento, Italy

    Roberto Sebastiani

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Ge, C., Ma, F., Liu, T., Zhang, J., Ma, X. (2018). A New Probabilistic Algorithm for Approximate Model Counting. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds) Automated Reasoning. IJCAR 2018. Lecture Notes in Computer Science(), vol 10900. Springer, Cham. https://doi.org/10.1007/978-3-319-94205-6_21

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-94205-6_21

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-94204-9

  • Online ISBN: 978-3-319-94205-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation