126
W. Wang et al.
structures, we create formulas with manually added domain-specific symmetry
breaking predicates, which we write in Alloy following previous work [38]. This
gives us a total of 348 model counting problems.
Table 4 shows some characteristics of the benchmarks, specifically the minimum and maximum numbers of primary variables, and all variables and clauses
under the different symmetry breaking settings.
4.3 Metrics
We use two key metrics – the model counts and the time to compute them – and
measure them under different symmetry breaking settings. For model counts, we
report the tool output and the ratio of the count under one setting to the count
under another setting. For time, we report the actual wall-clock times, and the
ratio of time taken under one setting to the time taken under another setting.
In line with prior work [17], we report the error rate of the approximate model
counting which is max(
approx
exact ,
exact
approx ) − 1, based on multiplicative guarantees.
5 Experimental evaluation
The section reports the results of the experimental evaluation. Section 5.1 describes the results for ApproxMC. Section 5.2 describes the results for ProjMC.
5.1 Symmetry breaking and approximate model counting
Time. Figures 5a, 5c, and 5e illustrate the time performance of ApproxMC
on the benchmarks based on Alloy, Kodkod, and data structure invariants respectively. With no symmetry breaking, ApproxMC times out on 21 (of 47)
Alloy benchmarks, 6 (of 13) Kodkod benchmarks, and 10 (of 24) data structure benchmarks. In all but 16 cases, formulas with Alloy’s default symmetry
breaking take less time than with CNF-level symmetry breaking. In all but 10
cases, formulas with CNF-level symmetry breaking take less time than with no
symmetry breaking. Moreover, for data structure benchmarks, in all but 1 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 0.14 seconds, and the smallest time taken by
Table 4: Benchmark characteristics.
source
#prim.
no-sb
cnf-sb
dom-sb
man-sb
#var. #clause #var. #clause #var. #clause #var. #clause
Alloy: min
46
384
620
522
1037
384
620
-
-
Alloy: max
2048 93764 291349 93764 289725 93764 291349
-
-
Kodkod: min
48
631
188
932
628
990
188
-
-
Kodkod: max
8188 388755 764957 397566 834629 453358 877429
-
-
n-Queens: min
1024 3762
7163 3762
7163 3762
7163
-
-
n-Queens: max 12288 200074 532527 201064 523947 269141 704396
-
-
Data Str.: min
43
992
3039 1091
3337 1209
3401 1006
3155
Data Str.: max
510 18694 48290 19045 45562 19808 50212 18993 50696
W. Wang et al.
structures, we create formulas with manually added domain-specific symmetry
breaking predicates, which we write in Alloy following previous work [38]. This
gives us a total of 348 model counting problems.
Table 4 shows some characteristics of the benchmarks, specifically the minimum and maximum numbers of primary variables, and all variables and clauses
under the different symmetry breaking settings.
4.3 Metrics
We use two key metrics – the model counts and the time to compute them – and
measure them under different symmetry breaking settings. For model counts, we
report the tool output and the ratio of the count under one setting to the count
under another setting. For time, we report the actual wall-clock times, and the
ratio of time taken under one setting to the time taken under another setting.
In line with prior work [17], we report the error rate of the approximate model
counting which is max(
approx
exact ,
exact
approx ) − 1, based on multiplicative guarantees.
5 Experimental evaluation
The section reports the results of the experimental evaluation. Section 5.1 describes the results for ApproxMC. Section 5.2 describes the results for ProjMC.
5.1 Symmetry breaking and approximate model counting
Time. Figures 5a, 5c, and 5e illustrate the time performance of ApproxMC
on the benchmarks based on Alloy, Kodkod, and data structure invariants respectively. With no symmetry breaking, ApproxMC times out on 21 (of 47)
Alloy benchmarks, 6 (of 13) Kodkod benchmarks, and 10 (of 24) data structure benchmarks. In all but 16 cases, formulas with Alloy’s default symmetry
breaking take less time than with CNF-level symmetry breaking. In all but 10
cases, formulas with CNF-level symmetry breaking take less time than with no
symmetry breaking. Moreover, for data structure benchmarks, in all but 1 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 0.14 seconds, and the smallest time taken by
Table 4: Benchmark characteristics.
source
#prim.
no-sb
cnf-sb
dom-sb
man-sb
#var. #clause #var. #clause #var. #clause #var. #clause
Alloy: min
46
384
620
522
1037
384
620
-
-
Alloy: max
2048 93764 291349 93764 289725 93764 291349
-
-
Kodkod: min
48
631
188
932
628
990
188
-
-
Kodkod: max
8188 388755 764957 397566 834629 453358 877429
-
-
n-Queens: min
1024 3762
7163 3762
7163 3762
7163
-
-
n-Queens: max 12288 200074 532527 201064 523947 269141 704396
-
-
Data Str.: min
43
992
3039 1091
3337 1209
3401 1006
3155
Data Str.: max
510 18694 48290 19045 45562 19808 50212 18993 50696