A Study of Symmetry Breaking Predicates and Model Counting
121
the counts and the time. Alloy’s default domain-level symmetry breaking is the
most effective, and for this problem, removes all symmetries. Some of the approximate model counts reported by ApproxMC are coincidentally the exact counts.
We validated the counts using the On-line Encyclopedia of Integer Sequences
(OEIS) [6]: the sequence #A000170 represents the number of solutions for the
n-Queen problem. The counts computed using Alloy’s default symmetry breaking with ApproxMC up to board size 8 × 8 form a subsequence of A000170. For
the other board sizes, the table lists the error, which is max(
approx
exact ,
exact
approx ) − 1,
based on multiplicative guarantees.
Note that the non-isomorphic solution count can easily be estimated from the
full count for this problem. For example, for the 7×7 board we can estimate it as
208896
7!
= 41.44, which is quite close to the actual count of 40. While the calculation is simple, the time to compute the full count is much higher (3727.1 seconds
instead of 1.14 seconds). Moreover, for larger board sizes, computing the full
count times out, so using it for those sizes may be simply infeasible. This example illustrates a case where symmetry breaking predicates reduce both the
model count and the time to compute it by relatively large factors.
3-queens. Table 2 shows the results for a variation of the n-queens problem
where the number of queens is fixed to 3, and the board size varies. To specify this
variation, we replace the expression “ (#Queen).minus[1]” in predicate ValidIndex
with the value of “k − 1” for the board size k × k, and set the scope for Queen
to “exactly 3” in the run command. We validate the ApproxMC counts using
the OEIS sequence #A047659 [6]. Once again, BreakID’s CNF-level predicates
significantly reduce the model count and time to compute it, and Alloy’s domainlevel predicates reduce them further. Since the number of queens is fixed to
3, the ratio of total number of solutions (no-sb) to number of non-isomorphic
solution is 3! = 6. For example, for 11 × 11 board, the ratio for ApproxMC
counts is exactly 6; however, the time to compute the full count is, as before,
much higher (1307.04 seconds instead of 45.1 seconds). This example shows a
case where symmetry breaking predicates reduce the model count by a relatively
small factor but the time to compute the counts by a much larger factor.
2.2 Data structure invariants
Next, consider the context of bounded exhaustive testing where the program
under test is run against every non-equivalent input within a bound on the
Table 2: ApproxMC results for 3-Queens where 3 queens are placed on n × n
board for 8 ≤ n ≤ 12.
8 × 8
9 × 9
10 × 10
11 × 11
12 × 12
#
t[s]
#
t[s]
#
t[s]
#
t[s]
#
t[s]
approx
no-sb 64512 107.56 176128 368.65 335872 695.55 688128 1307.04 1081344 4811.86
cnf-sb 18944 30.26 51200 67.43 122880 153.16 241664 280.15 417792 567.48
dom-sb 9728 7.94 25088 12.78 57344 26.14 114688
45.1 200704 111.76
OEIS 10320
25096
54400
107880
199400
error
0.061
0.000
-0.051
-0.059
-0.006
121
the counts and the time. Alloy’s default domain-level symmetry breaking is the
most effective, and for this problem, removes all symmetries. Some of the approximate model counts reported by ApproxMC are coincidentally the exact counts.
We validated the counts using the On-line Encyclopedia of Integer Sequences
(OEIS) [6]: the sequence #A000170 represents the number of solutions for the
n-Queen problem. The counts computed using Alloy’s default symmetry breaking with ApproxMC up to board size 8 × 8 form a subsequence of A000170. For
the other board sizes, the table lists the error, which is max(
approx
exact ,
exact
approx ) − 1,
based on multiplicative guarantees.
Note that the non-isomorphic solution count can easily be estimated from the
full count for this problem. For example, for the 7×7 board we can estimate it as
208896
7!
= 41.44, which is quite close to the actual count of 40. While the calculation is simple, the time to compute the full count is much higher (3727.1 seconds
instead of 1.14 seconds). Moreover, for larger board sizes, computing the full
count times out, so using it for those sizes may be simply infeasible. This example illustrates a case where symmetry breaking predicates reduce both the
model count and the time to compute it by relatively large factors.
3-queens. Table 2 shows the results for a variation of the n-queens problem
where the number of queens is fixed to 3, and the board size varies. To specify this
variation, we replace the expression “ (#Queen).minus[1]” in predicate ValidIndex
with the value of “k − 1” for the board size k × k, and set the scope for Queen
to “exactly 3” in the run command. We validate the ApproxMC counts using
the OEIS sequence #A047659 [6]. Once again, BreakID’s CNF-level predicates
significantly reduce the model count and time to compute it, and Alloy’s domainlevel predicates reduce them further. Since the number of queens is fixed to
3, the ratio of total number of solutions (no-sb) to number of non-isomorphic
solution is 3! = 6. For example, for 11 × 11 board, the ratio for ApproxMC
counts is exactly 6; however, the time to compute the full count is, as before,
much higher (1307.04 seconds instead of 45.1 seconds). This example shows a
case where symmetry breaking predicates reduce the model count by a relatively
small factor but the time to compute the counts by a much larger factor.
2.2 Data structure invariants
Next, consider the context of bounded exhaustive testing where the program
under test is run against every non-equivalent input within a bound on the
Table 2: ApproxMC results for 3-Queens where 3 queens are placed on n × n
board for 8 ≤ n ≤ 12.
8 × 8
9 × 9
10 × 10
11 × 11
12 × 12
#
t[s]
#
t[s]
#
t[s]
#
t[s]
#
t[s]
approx
no-sb 64512 107.56 176128 368.65 335872 695.55 688128 1307.04 1081344 4811.86
cnf-sb 18944 30.26 51200 67.43 122880 153.16 241664 280.15 417792 567.48
dom-sb 9728 7.94 25088 12.78 57344 26.14 114688
45.1 200704 111.76
OEIS 10320
25096
54400
107880
199400
error
0.061
0.000
-0.051
-0.059
-0.006