128
W. Wang et al.
(a) Model count: ApproxMC
(b) Model count: ProjMC
Fig. 6: Model count results. x-axis has benchmark model counting problems. yaxis (log-scale) has count ratio n/c where n is the model count for the formula
with no symmetry breaking and c is the corresponding count with CNF-level
symmetry breaking (green-square), Alloy’s default symmetry breaking (bluediamond), and manual symmetry breaking (red-triangle – only for data structures). Only cases where the calculation of n did not time out are shown.
metry 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 but 5 cases, manual symmetry
breaking gives the lowest count (the 5 exceptions are due to approximation in
computing the model counts). 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 61167, and the
largest ratio of count with no symmetry breaking to count with manual symmetry breaking was 45056. The model count results for the n-Queens benchmarks
were presented in Section 2.1.
W. Wang et al.
(a) Model count: ApproxMC
(b) Model count: ProjMC
Fig. 6: Model count results. x-axis has benchmark model counting problems. yaxis (log-scale) has count ratio n/c where n is the model count for the formula
with no symmetry breaking and c is the corresponding count with CNF-level
symmetry breaking (green-square), Alloy’s default symmetry breaking (bluediamond), and manual symmetry breaking (red-triangle – only for data structures). Only cases where the calculation of n did not time out are shown.
metry 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 but 5 cases, manual symmetry
breaking gives the lowest count (the 5 exceptions are due to approximation in
computing the model counts). 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 61167, and the
largest ratio of count with no symmetry breaking to count with manual symmetry breaking was 45056. The model count results for the n-Queens benchmarks
were presented in Section 2.1.