A Study of Symmetry Breaking Predicates and
Model Counting
Wenxi Wang
1 , Muhammad Usman
1 , Alyas Almaawi
1 , Kaiyuan Wang
2 ,
Kuldeep S. Meel
3 , and Sarfraz Khurshid
1
1 University of Texas at Austin, Austin, TX, USA
2 Google Inc., Sunnyvale, CA, USA
3 National University of Singapore, Singapore
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.
1 Introduction
Propositional model counting is the classic problem of counting the number of
all solutions for the given formula in propositional logic. While the core problem
is an integral part of complexity theory literature, advances in propositional
satisfiability (SAT) solvers and other decision procedures in the last decade have
led to much progress in tackling this problem in innovative ways [7, 9, 10, 15, 17,
31, 39, 40, 47, 49, 50, 56, 64]. These advances have fueled the application of model
counters in various software verification and reliability domains, e.g., to perform
© The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 115–134, 2020.
https://doi.org/10.1007/978-3-030-45190-5_7
Model Counting
Wenxi Wang
1 , Muhammad Usman
1 , Alyas Almaawi
1 , Kaiyuan Wang
2 ,
Kuldeep S. Meel
3 , and Sarfraz Khurshid
1
1 University of Texas at Austin, Austin, TX, USA
2 Google Inc., Sunnyvale, CA, USA
3 National University of Singapore, Singapore
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.
1 Introduction
Propositional model counting is the classic problem of counting the number of
all solutions for the given formula in propositional logic. While the core problem
is an integral part of complexity theory literature, advances in propositional
satisfiability (SAT) solvers and other decision procedures in the last decade have
led to much progress in tackling this problem in innovative ways [7, 9, 10, 15, 17,
31, 39, 40, 47, 49, 50, 56, 64]. These advances have fueled the application of model
counters in various software verification and reliability domains, e.g., to perform
© The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 115–134, 2020.
https://doi.org/10.1007/978-3-030-45190-5_7