Abstract
Propositional model counting is a classic problem that has recently witnessed many technical advances and novel applications. While the basic model counting problem requires computing the number of all solutions to the given formula, in some important application scenarios, the desired count is not of all solutions, but instead, of all unique solutions up to isomorphism. In such a scenario, the user herself must try to either use the full count that the model counter returns to compute the count up to isomorphism, or ensure that the input formula to the model counter adequately captures the symmetry breaking predicates so it can directly report the count she desires.
We study the use of CNF-level and domain-level symmetry breaking predicates in the context of the state-of-the-art in model counting, specifically the leading approximate model counter ApproxMC and the recently introduced exact model counter ProjMC. As benchmarks, we use a range of problems, including structurally complex specifications of software systems and constraint satisfaction problems. The results show that while it is sometimes feasible to compute the model counts up to isomorphism using the full counts that are computed by the model counters, doing so suffers from poor scalability. The addition of symmetry breaking predicates substantially assists model counters. Domain-specific predicates are particularly useful, and in many cases can provide full symmetry breaking to enable highly efficient model counting up to isomorphism. We hope our study motivates new research on designing model counters that directly account for symmetries to facilitate further applications of model counting.
Chapter PDF
Similar content being viewed by others
References
Alloy GitHub repository, 2019. https://github.com/AlloyTools/org.alloytools.alloy.
Alloy models repository, 2019. https://github.com/AlloyTools/models.
BreakID BitBucket repository, 2019. https://bitbucket.org/krr/breakid/src/master/.
Kodkod examples repository, 2019. https://github.com/emina/kodkod/tree/master/examples.
Kodkod GitHub repository, 2019. https://github.com/emina/kodkod.
The on-line encyclopedia of integer sequences, 2019. https://oeis.org/.
Alyas Almaawi, Nima Dini, Cagdas Yelen, Milos Gligoric, Sasa Misailovic, and Sarfraz Khurshid. Predictive constraint solving and analysis. In International Conference on Software Engineering, New Ideas and Emerging Results (ICSE-NIER), 2020. To appear.
Fadi A. Aloul, Igor L. Markov, and Karem A. Sakallah. Shatter: Efficient symmetry-breaking for boolean satisfiability. In 40th Annual Design Automation Conference, pages 836–839, 2003.
Abdulbaki Aydin, Lucas Bang, and Tevfik Bultan. Automata-based model counting for string constraints. In CAV (1), volume 9206 of Lecture Notes in Computer Science, pages 255–272, 2015.
Rehan Abdul Aziz, Geoffrey Chu, Christian J. Muise, and Peter J. Stuckey. Projected model counting. CoRR, abs/1507.07648, 2015.
Hamid Bagheri, Eunsuk Kang, Sam Malek, and Daniel Jackson. A formal approach for detection of security flaws in the android permission system. Formal Asp. Comput., 30(5):525–544, 2018.
Roberto J. Bayardo, Jr., and J. D. Pehoushek. Counting models using connected components. In In AAAI, pages 157–162, 2000.
Mateus Borges, Antonio Filieri, Marcelo d’Amorim, Corina S. Păsăreanu, and Willem Visser. Compositional solution space quantification for probabilistic software analysis. SIGPLAN Not., 49(6):123–132, June 2014.
Chandrasekhar Boyapati, Sarfraz Khurshid, and Darko Marinov. Korat: Automated testing based on Java predicates. In ISSTA, pages 123–133, 2002.
Supratik Chakraborty, Kuldeep S. Meel, Rakesh Mistry, and Moshe Y. Vardi. Approximate probabilistic inference via word-level counting. In Proc. of AAAI, 2016.
Supratik Chakraborty, Kuldeep S. Meel, and Moshe Y. Vardi. A scalable approximate model counter. In Proc. of CP, pages 200–216, 2013.
Supratik Chakraborty, Kuldeep S. Meel, and Moshe Y. Vardi. Algorithmic improvements in approximate counting for probabilistic inference: From linear to logarithmic SAT calls. In Proc. of IJCAI, 2016.
Nathan Chong, Tyler Sorensen, and John Wickerson. The semantics of transactions and weak memory in x86, Power, ARM, and C++. SIGPLAN Not., 53(4):211–225, 2018.
David Clark, Sebastian Hunt, and Pasquale Malacaria. Quantitative analysis of the leakage of confidential data. Electr. Notes Theor. Comput. Sci., 59(3):238–251, 2001.
James Crawford. A theoretical analysis of reasoning by symmetry in first-order logic (extended abstract). In Workshop notes, AAAI-92 workshop on tractable reasoning, 1992.
James Crawford, Matthew Ginsberg, Eugene Luks, and Amitabha Roy. Symmetry-breaking predicates for search problems. KR, 96:148–159, 1996.
Adnan Darwiche and Pierre Marquis. A knowledge compilation map. J. Artif. Int. Res., 17(1):229–264, September 2002.
Jo Devriendt, Bart Bogaerts, Maurice Bruynooghe, and Marc Denecker. Improved static symmetry breaking for SAT. In TACAS, pages 104–122, 2016.
Jeffrey Dudek, Kuldeep S. Meel, and Moshe Y. Vardi. Combining the k-cnf and xor phase-transitions. In Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), 7 2016.
Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In Enrico Giunchiglia and Armando Tacchella, editors, Theory and Applications of Satisfiability Testing, pages 502–518, 2004.
Antonio Filieri, Corina S. Păsăreanu, and Willem Visser. Reliability analysis in symbolic pathfinder. In International Conference on Software Engineering, pages 622–631, 2013.
J. P. Galeotti, N. Rosner, C. G. López Pombo, and M. F. Frias. Taco: Efficient SAT-based bounded verification using symmetry breaking and tight bounds. Transactions on Software Engineering, 2013.
Jaco Geldenhuys, Matthew B. Dwyer, and Willem Visser. Probabilistic symbolic execution. In International Symposium on Software Testing and Analysis, pages 166–176, 2012.
Ian P. Gent, Karen E. Petrie, and Jean-François Puget. Symmetry in constraint programming. In Handbook of Constraint Programming, pages 329–376. 2006.
Carla P. Gomes, Jörg Hoffmann, Ashish Sabharwal, and Bart Selman. Short XORs for model counting: From theory to practice. In Theory and Applications of Satisfiability Testing (SAT), pages 100–106, 2007.
Carla P. Gomes, Ashish Sabharwal, and Bart Selman. Model counting: A new strategy for obtaining good bounds. In 21st National Conference on Artificial Intelligence - Volume 1, pages 54–61, 2006.
Divya Gopinath, Muhammad Zubair Malik, and Sarfraz Khurshid. Specification-based program repair using SAT. In TACAS, pages 173–188, 2011.
Jinbo Huang and Adnan Darwiche. Dpll with a trace: From sat to knowledge compilation. In IJCAI, volume 5, pages 156–162, 2005.
Daniel Jackson. Software Abstractions: Logic, Language, and Analysis. The MIT Press, 2006.
Daniel Jackson and Kevin J. Sullivan. COM revisited: Tool-assisted modelling of an architectural framework. In SIGSOFT FSE, pages 149–158, 2000.
Daniel Jackson and Mandana Vaziri. Finding bugs with a constraint solver. In ISSTA, August 2000.
Sarfraz Khurshid and Daniel Jackson. Exploring the design of an intentional naming scheme with an automatic constraint analyzer. In ASE, pages 13–22, 2000.
Sarfraz Khurshid, Darko Marinov, Ilya Shlyakhter, and Daniel Jackson. A case for efficient solution enumeration. In SAT, pages 272–286, 2003.
Seonmo Kim and Stephen McCamant. Bit-vector model counting using statistical estimation. In TACAS (1), pages 133–151, 2018.
Jean-Marie Lagniez and Pierre Marquis. A recursive algorithm for projected model counting. AAAI, 33:1536–1543, 2019.
Loi Luu, Shweta Shinde, Prateek Saxena, and Brian Demsky. A model counter for constraints over unbounded strings. SIGPLAN Not., 49(6):565–576, June 2014.
Darko Marinov and Sarfraz Khurshid. TestEra: A novel framework for automated testing of Java programs. In ASE, 2001.
Hakan Metin, Souheib Baarir, Maximilien Colange, and Fabrice Kordon. Cdclsym: Introducing effective symmetry breaking in sat solving. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 99–114. Springer, 2018.
Quoc-Sang Phan and Pasquale Malacaria. Abstract model counting: a novel approach for quantification of information leaks. In 9th ACM Symposium on Information, Computer and Communications Security, pages 283–292, 2014.
Stuart Russell and Peter Norvig. Artificial Intelligence: A Modern Approach. Prentice Hall Press, 2009.
Karem Sakallah. Symmetry and satisfiability. Frontiers in Artificial Intelligence and Applications, 185, 012009.
Marko Samer and Stefan Szeider. Algorithms for propositional model counting. Journal of Discrete Algorithms, 8(1):50–64, 2010.
Hesam Samimi, Ei Darli Aung, and Todd D. Millstein. Falling back on executable specifications. In ECOOP, pages 552–576, 2010.
Tian Sang, Fahiem Bacchus, Paul Beame, Henry A. Kautz, and Toniann Pitassi. Combining component caching and clause learning for effective model counting. In SAT, 2004.
Shubham Sharma, Subhajit Roy, Mate Soos, and Kuldeep S. Meel. GANAK: A scalable probabilistic exact model counter. In IJCAI, pages 1169–1176, 2019.
Ilya Shlyakhter. Generating effective symmetry-breaking predicates for search problems. In Proc. Workshop on Theory and Applications of Satisfiability Testing, June 2001.
Mate Soos and Kuldeep S. Meel. Bird: Engineering an efficient cnf-xor sat solver and its applications to approximate model counting. In Proceedings of AAAI Conference on Artificial Intelligence (AAAI), 1 2019.
Mate Soos, Karsten Nohl, and Claude Castelluccia. Extending SAT solvers to cryptographic problems. In Theory and Applications of Satisfiability Testing (SAT), pages 244–257, 2009.
Larry Stockmeyer. The complexity of approximate counting. In Proceedings of the Fifteenth Annual ACM Symposium on Theory of Computing, STOC ’83, pages 118–126, New York, NY, USA, 1983. ACM.
Allison Sullivan, Kaiyuan Wang, Razieh Nokhbeh Zaeem, and Sarfraz Khurshid. Automated test generation and mutation testing for Alloy. In ICST, 2017.
Marc Thurley. SharpSAT – Counting models with advanced component caching and implicit BCP. In Armin Biere and Carla P. Gomes, editors, Theory and Applications of Satisfiability Testing - SAT 2006, pages 424–429, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg.
Emina Torlak. A Constraint Solver for Software Engineering: Finding Models and Cores of Large Relational Specifications. PhD thesis, Cambridge, MA, USA, 2009. AAI0821754.
Emina Torlak and Daniel Jackson. Kodkod: A relational model finder. In TACAS, 2007.
Caroline Trippel, Daniel Lustig, and Margaret Martonosi. CheckMate: Automated synthesis of hardware exploits and security litmus tests. In MICRO, 2018.
G. S. Tseitin. On the Complexity of Derivation in Propositional Calculus, pages 466–483. 1983.
Alasdair Urquhart. The symmetry rule in propositional logic. Discrete Applied Mathematics, 96-97:177 – 193, 1999.
Muhammad Usman, Wenxi Wang, and Sarfraz Khurshid. TestMC: A framework for testing model counters. Under submission, 2020.
Leslie G. Valiant. The complexity of enumeration and reliability problems. SIAM J. Comput., 8:410–421, 1979.
Guy Van Den Broeck. First-order model counting in a nutshell. In Twenty-Fifth International Joint Conference on Artificial Intelligence, pages 4086–4089, 2016.
Marko Vasic, David Soloveichik, and Sarfraz Khurshid. CRNs exposed: Systematic exploration of chemical reaction networks. CoRR, abs/1912.06197, 2019.
E. J. Weyuker and T. J. Ostrand. Theories of program testing and the application of revealing subdomains. TSE, 6(3):236–246, May 1980.
John Wickerson, Mark Batty, Tyler Sorensen, and George A. Constantinides. Automatically comparing memory consistency models. In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), pages 190–204, 2017.
Tao Xie, Darko Marinov, Wolfram Schulte, and David Notkin. Symstra: A framework for generating object-oriented unit tests using symbolic execution. In 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 365–381, 2005.
Razieh Nokhbeh Zaeem and Sarfraz Khurshid. Contract-based data structure repair using Alloy. In ECOOP, pages 577–598, 2010.
Pamela Zave. How to make Chord correct (using a stable base). CoRR, abs/1502.06461, 2015.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Wang, W., Usman, M., Almaawi, A., Wang, K., Meel, K.S., Khurshid, S. (2020). A Study of Symmetry Breaking Predicates and Model Counting. In: Biere, A., Parker, D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2020. Lecture Notes in Computer Science(), vol 12078. Springer, Cham. https://doi.org/10.1007/978-3-030-45190-5_7
Download citation
DOI: https://doi.org/10.1007/978-3-030-45190-5_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45189-9
Online ISBN: 978-3-030-45190-5
eBook Packages: Computer ScienceComputer Science (R0)