120
W. Wang et al.
Queen={Queen$0, Queen$1, Queen$2, Queen$3,
Queen$4, Queen$5, Queen$6, Queen$7}
Board={Board$0}
Board<:state={Board$0->Queen$0->7->5, Board$0->Queen$1->6->0,
Board$0->Queen$2->5->4, Board$0->Queen$3->4->1,
Board$0->Queen$4->3->7, Board$0->Queen$5->2->2,
Board$0->Queen$6->1->6, Board$0->Queen$7->0->3}
8
0Z0l0Z0Z
7
ZqZ0Z0Z0
6
0Z0Z0Z0l
5
Z0Z0ZqZ0
4
qZ0Z0Z0Z
3
Z0l0Z0Z0
2
0Z0ZqZ0Z
1
Z0Z0Z0l0
a b c d e f g h
Fig. 2: A solution to 8-queens created by the Alloy analyzer illustrated.
4 sub-formulas that are implicitly conjoined; each of them uses universal quantification (all); the keyword disj constrains the quantified variables to represent
distinct values. The dot operator (‘.’) is relational join [34]. A predicate (pred)
is a parameterized formula that can be invoked elsewhere; likewise, a fun is a
parameterized expression. The predicate NQueensProblem represents the overall
specification of the n-Queens constraints. Any model of the Alloy specification
must satisfy the constraints in all the facts and any predicates that are invoked
(directly or transitively).
The Alloy user writes a command and executes it to solve desired constraints.
For example, “run NQueensProblem for 5 int, exactly 8 Queen” asks the analyzer to find a solution to the 8-Queens problem. This command creates a constraint solving problem such that the integer bit-width is 5, and there are exactly
8 queens. Figure 2 shows a valuation for each set and relation created by the
Alloy analyzer to solve this problem, and graphically illustrates the solution.
Next, we illustrate the use of the approximate model counter ApproxMC [16].
For the nqueens specification, for each 7 ≤ n ≤ 12, we create three constraint
solving problems: 1) no symmetry breaking (no-sb); 2) BreakID’s default CNFlevel symmetry breaking [23] (cnf-sb); and 3) Alloy’s default domain-level symmetry breaking [58] (dom-sb). Table 1 shows the number of solutions found and
time taken in each case. The model count with no symmetry breaking is the highest and takes the longest to compute; this approach times out for 8×8 and larger
boards. BreakID’s default CNF-level symmetry breaking significantly reduces
Table 1: ApproxMC results for n-Queens for 7 ≤ n ≤ 12. Model count (“#”) and
time taken in seconds (“t[s]”) for different problem sizes are shown. Time-out
(t.o.) is 5000 sec.
7 × 7
8 × 8
9 × 9
10 × 10
11 × 11
12 × 12
#
t[s] # t[s]
# t[s]
# t[s]
#
t[s]
#
t[s]
approx
no-sb 208896 3727.1 - t.o.
- t.o.
- t.o.
-
t.o.
-
t.o
cnf-sb 67584 1446.4 - t.o.
- t.o.
- t.o.
-
t.o.
-
t.o
dom-sb
40 1.14 92 13.67 304 16.27 784 44.97 2752 199.77 15360 822.14
OEIS
40
92
352
724
2680
14200
error
0
0
0.158
-0.077
-0.026
0.076
W. Wang et al.
Queen={Queen$0, Queen$1, Queen$2, Queen$3,
Queen$4, Queen$5, Queen$6, Queen$7}
Board={Board$0}
Board<:state={Board$0->Queen$0->7->5, Board$0->Queen$1->6->0,
Board$0->Queen$2->5->4, Board$0->Queen$3->4->1,
Board$0->Queen$4->3->7, Board$0->Queen$5->2->2,
Board$0->Queen$6->1->6, Board$0->Queen$7->0->3}
8
0Z0l0Z0Z
7
ZqZ0Z0Z0
6
0Z0Z0Z0l
5
Z0Z0ZqZ0
4
qZ0Z0Z0Z
3
Z0l0Z0Z0
2
0Z0ZqZ0Z
1
Z0Z0Z0l0
a b c d e f g h
Fig. 2: A solution to 8-queens created by the Alloy analyzer illustrated.
4 sub-formulas that are implicitly conjoined; each of them uses universal quantification (all); the keyword disj constrains the quantified variables to represent
distinct values. The dot operator (‘.’) is relational join [34]. A predicate (pred)
is a parameterized formula that can be invoked elsewhere; likewise, a fun is a
parameterized expression. The predicate NQueensProblem represents the overall
specification of the n-Queens constraints. Any model of the Alloy specification
must satisfy the constraints in all the facts and any predicates that are invoked
(directly or transitively).
The Alloy user writes a command and executes it to solve desired constraints.
For example, “run NQueensProblem for 5 int, exactly 8 Queen” asks the analyzer to find a solution to the 8-Queens problem. This command creates a constraint solving problem such that the integer bit-width is 5, and there are exactly
8 queens. Figure 2 shows a valuation for each set and relation created by the
Alloy analyzer to solve this problem, and graphically illustrates the solution.
Next, we illustrate the use of the approximate model counter ApproxMC [16].
For the nqueens specification, for each 7 ≤ n ≤ 12, we create three constraint
solving problems: 1) no symmetry breaking (no-sb); 2) BreakID’s default CNFlevel symmetry breaking [23] (cnf-sb); and 3) Alloy’s default domain-level symmetry breaking [58] (dom-sb). Table 1 shows the number of solutions found and
time taken in each case. The model count with no symmetry breaking is the highest and takes the longest to compute; this approach times out for 8×8 and larger
boards. BreakID’s default CNF-level symmetry breaking significantly reduces
Table 1: ApproxMC results for n-Queens for 7 ≤ n ≤ 12. Model count (“#”) and
time taken in seconds (“t[s]”) for different problem sizes are shown. Time-out
(t.o.) is 5000 sec.
7 × 7
8 × 8
9 × 9
10 × 10
11 × 11
12 × 12
#
t[s] # t[s]
# t[s]
# t[s]
#
t[s]
#
t[s]
approx
no-sb 208896 3727.1 - t.o.
- t.o.
- t.o.
-
t.o.
-
t.o
cnf-sb 67584 1446.4 - t.o.
- t.o.
- t.o.
-
t.o.
-
t.o
dom-sb
40 1.14 92 13.67 304 16.27 784 44.97 2752 199.77 15360 822.14
OEIS
40
92
352
724
2680
14200
error
0
0
0.158
-0.077
-0.026
0.076