A Study of Symmetry Breaking Predicates and Model Counting
129
Error. For the Alloy, Kodkod, and data structure benchmarks, we compute the
error in ApproxMC with respect to the counts reported by ProjMC for the cases
where ProjMC reported a count. The error ranges were: [0, 0.168] for the Alloy
benchmarks, [0, 0.168] for the Kodkod benchmarks, and [0, 0.165] for the data
structure benchmarks. Section 2.1 presented the error results for the n-Queens
benchmarks with respect to the number in OEIS [6].
5.2 Symmetry breaking and exact model counting
Time. Figures 5b, 5d, and 5f illustrate the time performance of ProjMC on the
benchmarks based on Alloy, Kodkod, and data structure invariants respectively.
With no symmetry breaking, ProjMC times out on 21 (of 47) Alloy benchmarks
(which is the same number as ApproxMC although the two sets of benchmarks
are not the same), 9 (of 13) Kodkod benchmarks (which is more that the number for ApproxMC), and 9 (of 24) data structure benchmarks (which is more
than ApproxMC). In all but 8 cases, formulas with Alloy’s default symmetry
breaking take less time than with CNF-level symmetry breaking. In all but 24
cases, formulas with CNF-level symmetry breaking take less time than with no
symmetry breaking. Moreover, for data structure benchmarks, in all but 2 cases,
formulas with manual symmetry breaking take less time than Alloy’s default
symmetry breaking. Among all the problems that time out with no symmetry
breaking, the smallest time taken by the corresponding problem with Alloy’s
default symmetry breaking was 3.12 seconds, and the smallest time taken by the
corresponding problem with manual symmetry breaking was 0.01 seconds.
Model counts. Figure 6b graphically illustrates how the model counts vary
under different symmetry breaking settings. For the Alloy and Kodkod benchmarks, in all but 9 cases the model count for the formula with Alloy’s default
symmetry breaking is less than the corresponding count with CNF-level symmetry breaking. For the data structures, the model count for the formula with
Alloy’s symmetry breaking is less than the corresponding count with CNF-level
symmetry breaking in all cases; moreover, in all cases, manual symmetry breaking gives the lowest count. Among all problems where ApproxMC reports a
count with no symmetry breaking, the largest ratio of count with no symmetry breaking to count with Alloy’s default symmetry breaking was 40320, and
the largest ratio of count with no symmetry breaking to count with manual
symmetry breaking was 362880.
Overall, the impact of symmetry breaking is significant for both ApproxMC
and ProjMC. In majority of the cases, Alloy’s default symmetry breaking is more
effective than CNF-level symmetry breaking using BreakID. For data structure
benchmarks, manual symmetry breaking is the most effective, and reports exactly the counts of the non-isomorphic solutions as desired; moreover, in cases
where Alloy’s default symmetry breaking provides full symmetry breaking, manual symmetry breaking provides much faster solving.
5.3 Discussion
The empirical evaluation in the preceding subsections clearly demonstrates the
significant impact of symmetry breaking on ApproxMC and ProjMC. While a
129
Error. For the Alloy, Kodkod, and data structure benchmarks, we compute the
error in ApproxMC with respect to the counts reported by ProjMC for the cases
where ProjMC reported a count. The error ranges were: [0, 0.168] for the Alloy
benchmarks, [0, 0.168] for the Kodkod benchmarks, and [0, 0.165] for the data
structure benchmarks. Section 2.1 presented the error results for the n-Queens
benchmarks with respect to the number in OEIS [6].
5.2 Symmetry breaking and exact model counting
Time. Figures 5b, 5d, and 5f illustrate the time performance of ProjMC on the
benchmarks based on Alloy, Kodkod, and data structure invariants respectively.
With no symmetry breaking, ProjMC times out on 21 (of 47) Alloy benchmarks
(which is the same number as ApproxMC although the two sets of benchmarks
are not the same), 9 (of 13) Kodkod benchmarks (which is more that the number for ApproxMC), and 9 (of 24) data structure benchmarks (which is more
than ApproxMC). In all but 8 cases, formulas with Alloy’s default symmetry
breaking take less time than with CNF-level symmetry breaking. In all but 24
cases, formulas with CNF-level symmetry breaking take less time than with no
symmetry breaking. Moreover, for data structure benchmarks, in all but 2 cases,
formulas with manual symmetry breaking take less time than Alloy’s default
symmetry breaking. Among all the problems that time out with no symmetry
breaking, the smallest time taken by the corresponding problem with Alloy’s
default symmetry breaking was 3.12 seconds, and the smallest time taken by the
corresponding problem with manual symmetry breaking was 0.01 seconds.
Model counts. Figure 6b graphically illustrates how the model counts vary
under different symmetry breaking settings. For the Alloy and Kodkod benchmarks, in all but 9 cases the model count for the formula with Alloy’s default
symmetry breaking is less than the corresponding count with CNF-level symmetry breaking. For the data structures, the model count for the formula with
Alloy’s symmetry breaking is less than the corresponding count with CNF-level
symmetry breaking in all cases; moreover, in all cases, manual symmetry breaking gives the lowest count. Among all problems where ApproxMC reports a
count with no symmetry breaking, the largest ratio of count with no symmetry breaking to count with Alloy’s default symmetry breaking was 40320, and
the largest ratio of count with no symmetry breaking to count with manual
symmetry breaking was 362880.
Overall, the impact of symmetry breaking is significant for both ApproxMC
and ProjMC. In majority of the cases, Alloy’s default symmetry breaking is more
effective than CNF-level symmetry breaking using BreakID. For data structure
benchmarks, manual symmetry breaking is the most effective, and reports exactly the counts of the non-isomorphic solutions as desired; moreover, in cases
where Alloy’s default symmetry breaking provides full symmetry breaking, manual symmetry breaking provides much faster solving.
5.3 Discussion
The empirical evaluation in the preceding subsections clearly demonstrates the
significant impact of symmetry breaking on ApproxMC and ProjMC. While a