118
W. Wang et al.
counters, doing so suffers from poor scalability. The addition of symmetry breaking predicates substantially assists model counters, although it is a well-known
feature in SAT solving supported by theory finding [46, 61]. Domain specific
predicates are particularly effective, and in many cases, can provide full symmetry breaking to enable highly efficient model counting up to isomorphism.
We were surprised by the extent of the impact. Since the addition of symmetry breaking predicates introduces new dependencies among the variables, we
expected these dependencies to make the formula more complex and perhaps
less amenable to efficient model counting. However, the sheer reduction in the
number of solutions caused by symmetry breaking more than compensates for
the additional logical complexity of the formula. In cases where it was possible
to create full symmetry breaking predicates, the model count for the formula
with the predicates was computed up to a few orders of magnitude faster than
the formula with no symmetry breaking predicates.
A key lesson of our study (in the context of the model counting problems
considered) is: if non-isomorphic solution counts are desired, use full symmetry
breaking predicates at the domain-level whenever feasible – even if it is straightforward to compute the number of non-isomorphic solutions from the number
of all solutions, or even if the symmetry breaking constraints have to be written
manually. This paper makes the following contributions:
– Study. To the best of our knowledge, we present the first study of symmetry
breaking in the context of model counting. As pointed out earlier, there is
a tradeoff between the reduction of solution space and the likely increase in
complexity due to added symmetry breaking predicates. In prior work, the
benefit of symmetry breaking in SAT solving were typically observed largely
for unsatisfiable problems [43], our study shows the importance of symmetry
breaking and its deep relation to problem formulation in the context of
satisfiable problems, albeit for model counting.
– Dataset. All CNF files we used for the experiments are being made publicly available: https://github.com/wenxiwang/TACAS2020. We expect the
dataset to be useful for future work on evaluating the performance of different model counters, and of the different strategies they employ, as well as
for evaluating model enumeration tools.
We believe there is an important bi-directional relation between symmetry
breaking and model counting whereas: 1) in one direction the model counters
directly support computing the counts for non-isomorphic solutions to facilitate
applications that so require; and 2) in the other direction symmetry breaking
helps model counters become more efficient. We hope our study motivates future
work that further investigates this relation.
2 Examples
This section provides two illustrative examples that require computing the number of unique solutions up to isomorphism. We specify the examples in the Alloy
W. Wang et al.
counters, doing so suffers from poor scalability. The addition of symmetry breaking predicates substantially assists model counters, although it is a well-known
feature in SAT solving supported by theory finding [46, 61]. Domain specific
predicates are particularly effective, and in many cases, can provide full symmetry breaking to enable highly efficient model counting up to isomorphism.
We were surprised by the extent of the impact. Since the addition of symmetry breaking predicates introduces new dependencies among the variables, we
expected these dependencies to make the formula more complex and perhaps
less amenable to efficient model counting. However, the sheer reduction in the
number of solutions caused by symmetry breaking more than compensates for
the additional logical complexity of the formula. In cases where it was possible
to create full symmetry breaking predicates, the model count for the formula
with the predicates was computed up to a few orders of magnitude faster than
the formula with no symmetry breaking predicates.
A key lesson of our study (in the context of the model counting problems
considered) is: if non-isomorphic solution counts are desired, use full symmetry
breaking predicates at the domain-level whenever feasible – even if it is straightforward to compute the number of non-isomorphic solutions from the number
of all solutions, or even if the symmetry breaking constraints have to be written
manually. This paper makes the following contributions:
– Study. To the best of our knowledge, we present the first study of symmetry
breaking in the context of model counting. As pointed out earlier, there is
a tradeoff between the reduction of solution space and the likely increase in
complexity due to added symmetry breaking predicates. In prior work, the
benefit of symmetry breaking in SAT solving were typically observed largely
for unsatisfiable problems [43], our study shows the importance of symmetry
breaking and its deep relation to problem formulation in the context of
satisfiable problems, albeit for model counting.
– Dataset. All CNF files we used for the experiments are being made publicly available: https://github.com/wenxiwang/TACAS2020. We expect the
dataset to be useful for future work on evaluating the performance of different model counters, and of the different strategies they employ, as well as
for evaluating model enumeration tools.
We believe there is an important bi-directional relation between symmetry
breaking and model counting whereas: 1) in one direction the model counters
directly support computing the counts for non-isomorphic solutions to facilitate
applications that so require; and 2) in the other direction symmetry breaking
helps model counters become more efficient. We hope our study motivates future
work that further investigates this relation.
2 Examples
This section provides two illustrative examples that require computing the number of unique solutions up to isomorphism. We specify the examples in the Alloy