A Study of Symmetry Breaking Predicates and Model Counting
127
0.01
0.1
1
10
100
1000
10000
0
5
10
15
20
25
30
35
40
45
50
Time
Alloy Subjects
cnf_nosb domain_sb cnf_sb
(a) Time: ApproxMC – Alloy
0.01
0.1
1
10
100
1000
10000
0
5
10
15
20
25
30
35
40
45
50
time
Alloy Subjects
no_sb
domain_sb
cnf_sb
(b) Time: ProjMC – Alloy
0.1
1
10
100
1000
10000
0
2
4
6
8
1 0
1 2
1 4
Time
Kodkod Subjects
no_sb domain_sb cnf_sb
(c) Time: ApproxMC – Kodkod
0.1
1
10
100
1000
10000
0
2
4
6
8
1 0
1 2
1 4
Time
Kodkod Subjects
no_sb domain_sb cnf_sb
(d) Time: ProjMC – Kodkod
0.001
0.01
0.1
1
10
100
1000
10000
0
4
8
1 2
1 6
2 0
2 4
Time
Data Structure Subjects
no_sb alloy_sb cnf_sb manual_sb
(e) Time: ApproxMC – Data structures
0.001
0.01
0.1
1
10
100
1000
10000
0
4
8
1 2
1 6
2 0
2 4
Time
Data Structure Subjects
no_sb domain_sb cnf_sb manual_sb
(f) Time: ProjMC – Data structures
Fig. 5: Time results. x-axis has benchmark model counting problems. y-axis has
time in seconds (log-scale). Benchmarks on x-axis are sorted in ascending order
based on the number of primary variables; moreover, the data structure benchmarks are grouped by the type of the structure. Blue diamond is no symmetry
breaking (no-sb) ; red triangle is CNF-level symmetry breaking (cnf-sb); green
square is Alloy’s default symmetry breaking (dom-sb); and orange cross is manual symmetry breaking (man-sb).
the corresponding problem with manual symmetry breaking was 0.008 seconds.
For the Alloy benchmarks, ApproxMC does not time-out under any symmetry
breaking setting for benchmarks that have up to 90 primary variables. The time
results for the n-Queens benchmarks were presented in Section 2.1.
Model counts. Figure 6a graphically illustrates how the model counts vary
under different symmetry breaking settings. For the Alloy and Kodkod benchmarks, in all but 10 cases the model count for the formula with Alloy’s default
symmetry breaking is less than the corresponding count with CNF-level sym-