A Study of Symmetry Breaking Predicates and Model Counting
119
module nqueens -- name of the specification
sig Queen {} -- set of queen atoms
one sig Board { state: Queen -> Int -> Int } -- one board
fact StateOkay {
all q: Queen | one q.(Board.state) -- each queen occupies exactly one cell
all x: Queen.(Board.state).Int | ValidIndex[x] -- all x-coordinates are valid
all y: Int.(Queen.(Board.state)) | ValidIndex[y] -- all y-coordinates are valid
all disj q, r: Queen | q.(Board.state) != r.(Board.state) } -- queens do not share cells
pred ValidIndex[x: Int] { x.gte[0] and x.lte[(#Queen).minus[1]] } -- x >= 0 && x <= |Queen|-1
fun X[q: Queen]: Int { (q.(Board.state)).Int } -- x-coordinate of q
fun Y[q: Queen]: Int { Int.(q.(Board.state)) } -- y-coordinate of q
fun Abs[x: Int]: Int { x.lt[0] implies negate[x] else x } -- absolute value of x
pred SameRow[q, r: Queen] { X[q] = X[r] } -- q and r are in the same row
pred SameColumn[q, r: Queen] { Y[q] = Y[r] } -- q and r are in the same column
pred SameDiagonal[q, r: Queen] { -- q and r share a diagonal
Abs[X[q].minus[X[r]]] = Abs[Y[q].minus[Y[r]]] }
pred NQueensProblem { -- no queen attacks another queen
all disj q, r: Queen | !SameRow[q, r] and !SameColumn[q, r] and !SameDiagonal[q, r] }
Fig. 1: Alloy specification of n-Queens.
language, which allows us to explore different approaches for applying symmetry
breaking. We provide intuitive descriptions of Alloy constructs as we introduce
them; further details can be found elsewhere [34].
The first example illustrates a CSP problem [45] where Alloy’s default symmetry breaking provides full symmetry breaking; we use ApproxMC to solve
this problem (Section 2.1). The second example illustrates a software testing
problem [42] where manually written symmetry breaking predicates provide full
symmetry breaking; we use ProjMC to solve this problem (Section 2.2). Section 5 presents a detailed experimental evaluation where we use the two tools
against many additional benchmarks.
2.1 n-Queens
Consider specifying the well-known n-Queens problem of placing n interchangeable queens
4 on a fixed n×n chess-board, and computing the number of solutions
to the problem using a modern propositional model counter [16, 40, 50].
Figure 1 shows a fragment of an Alloy specification of the n-Queens problem,
which has been studied before using Alloy [2, 4, 55]. The keyword sig introduces
a set of (interchangeable) atoms. The keyword one makes the set a singleton. The
field state introduces a quaternary relation of type “ Board x Queen x Int x Int”
where Int is a built-in type that represents integers. The fact StateOkay describes
the basic constraints for the state of the board to be valid; the fact contains
4 Here, we only consider symmetries based on permuting the queens (and not other
forms, e.g., rotations of the board.)
119
module nqueens -- name of the specification
sig Queen {} -- set of queen atoms
one sig Board { state: Queen -> Int -> Int } -- one board
fact StateOkay {
all q: Queen | one q.(Board.state) -- each queen occupies exactly one cell
all x: Queen.(Board.state).Int | ValidIndex[x] -- all x-coordinates are valid
all y: Int.(Queen.(Board.state)) | ValidIndex[y] -- all y-coordinates are valid
all disj q, r: Queen | q.(Board.state) != r.(Board.state) } -- queens do not share cells
pred ValidIndex[x: Int] { x.gte[0] and x.lte[(#Queen).minus[1]] } -- x >= 0 && x <= |Queen|-1
fun X[q: Queen]: Int { (q.(Board.state)).Int } -- x-coordinate of q
fun Y[q: Queen]: Int { Int.(q.(Board.state)) } -- y-coordinate of q
fun Abs[x: Int]: Int { x.lt[0] implies negate[x] else x } -- absolute value of x
pred SameRow[q, r: Queen] { X[q] = X[r] } -- q and r are in the same row
pred SameColumn[q, r: Queen] { Y[q] = Y[r] } -- q and r are in the same column
pred SameDiagonal[q, r: Queen] { -- q and r share a diagonal
Abs[X[q].minus[X[r]]] = Abs[Y[q].minus[Y[r]]] }
pred NQueensProblem { -- no queen attacks another queen
all disj q, r: Queen | !SameRow[q, r] and !SameColumn[q, r] and !SameDiagonal[q, r] }
Fig. 1: Alloy specification of n-Queens.
language, which allows us to explore different approaches for applying symmetry
breaking. We provide intuitive descriptions of Alloy constructs as we introduce
them; further details can be found elsewhere [34].
The first example illustrates a CSP problem [45] where Alloy’s default symmetry breaking provides full symmetry breaking; we use ApproxMC to solve
this problem (Section 2.1). The second example illustrates a software testing
problem [42] where manually written symmetry breaking predicates provide full
symmetry breaking; we use ProjMC to solve this problem (Section 2.2). Section 5 presents a detailed experimental evaluation where we use the two tools
against many additional benchmarks.
2.1 n-Queens
Consider specifying the well-known n-Queens problem of placing n interchangeable queens
4 on a fixed n×n chess-board, and computing the number of solutions
to the problem using a modern propositional model counter [16, 40, 50].
Figure 1 shows a fragment of an Alloy specification of the n-Queens problem,
which has been studied before using Alloy [2, 4, 55]. The keyword sig introduces
a set of (interchangeable) atoms. The keyword one makes the set a singleton. The
field state introduces a quaternary relation of type “ Board x Queen x Int x Int”
where Int is a built-in type that represents integers. The fact StateOkay describes
the basic constraints for the state of the board to be valid; the fact contains
4 Here, we only consider symmetries based on permuting the queens (and not other
forms, e.g., rotations of the board.)