The eight queens puzzle asks how to place eight queens on a chess board such that none of them attacks any other. The problem easily generalizes to n queens, using an nxn board. In this post, we’ll see how to solve the n-Queens puzzle in Cryptol, without lifting a finger!
Representing the board
It is easy to see that any solution to the n-Queens puzzle will have precisely one queen on each row and column of the board. Therefore, we can represent the solution as a sequence of n row numbers, corresponding to subsequent columns. For instance, the board pictured below (taken from the wikipedia page), can be represented by the sequence
3 7 0 2 5 1 6 4
recording the row of the queen appearing in each consecutive column, starting from the top-left position. (And yes, we always count from 0!)
Recognizing a valid solution
Let us start by asking a simpler question. How can we recognize that a given sequence of n row indices constitute a valid solution? We have to verify that the followings hold:
- The numbers must be between 0 and n-1. (Sanity checking.)
- The numbers should not be duplicated. (Ensures that there is exactly one queen per row.)
- For any pair of numbers in the sequence, their row-value difference should be different than their column-value difference. (Ensures that there are no diagonal conflicts.)
The first two conditions are fairly trivial. The last one simply says that if two queens are positioned such that their vertical and horizontal displacements are the same, then they are on the same diagonal: A situation we must avoid for all pairs of queens given.
Writing a Cryptol predicate
Having described how we will recognize an alleged solution, let us now consider how we can code this in Cryptol.First, we will need a helper function that applies a given predicate to all the elements of a sequence and returns True if all elements satisfy the predicate. Naturally, we call this function all:
all : {n a} (fin n) => (a -> Bit,[n]a) -> Bit;
all (f, xs) = [|f x || x <- xs|] == ~zero;
The type of this function is worth spending a few moments looking at, as it demonstrates some crucial aspects of Cryptol’s type system that sets it apart from other languages. In particular, it says that the function all takes a sequence of n elements, each of some arbitrary size a. However, it also restricts n to be finite, i.e., the type system will complain if you pass all an infinite sequence. Then, we apply the predicate f to each element in the sequence, and check that the result consists of all True bits. (The polymorphic Cryptol value zero represents a value with an arbitrary shape with all bits set to False. The complement operator (~) flips all those bits to True.)The second utility function we will need is a predicate that checks whether the elements of a given sequence are all distinct:
distinct : {a b} (fin a,fin b) => [a]b -> Bit;
distinct xs = diff == ~zero
where {
n = width xs;
diff = [|check (x, i) || x <- xs || i <- [0 .. (n-1)] |];
check (x, start) = walk (start + 1)
where walk cur = if cur == n then True else if xs @ cur == x then False else walk (cur + 1);
};
The function distinct is fairly simple: For each element in the sequence, it walk‘s through the rest to make sure that none of the remaining elements are the same as that particular element. Note how Cryptol’s width function allows us to determine the size of the input sequence, and recurse properly.Having done the heavy-lifting above, we can now write the predicate that recognizes a valid n-Queens solution in Cryptol:
type Solution(n) = [n][1+width n] -> Bit;
nQueens : {n} (fin n) => Solution(n);
nQueens qs = all(inRange, qs) & distinct qs & all(checkDiag, ijs)
where {
n = width qs;
inRange x = x < n;
ijs = [| (i, j) || i <- [0 .. n-1] , j <- [0 .. n-1] |];
checkDiag (i, j) = (i >= j) | (diffR != diffC)
where {
qi = qs @ i;
qj = qs @ j;
diffR = if qi >= qj then qi-qj else qj-qi;
diffC = j - i;
};
};
The nQueens function simply executes our checks as we described above. It first makes sure that all the elements are inRange. (Note that we do not have to check for negative numbers since all Cryptol numbers are non-negative.) Then, we check that all the elements are distinct. Following this, we generate the pairs of indices ijs, and call checkDiag on all these pairs to make sure that the row and column differences do not match.We can test this function in Cryptol, by providing sample input:
NQueens> nQueens [3 7 0 2 5 1 6 4] True NQueens> nQueens [3 7 0 2 5 6 1 4] False
In the second example, I swapped the elements 1 and 6; effectively putting the 6th queen on row 6 and the 7th on row 1. This creates a diagonal conflict as the reader can easily verify.
Solving n-Queens
It appears that all we have done so far is to write a Cryptol program to recognize whether a given solution to the n-Queens problem is valid. But, how do we actually solve the puzzle?Remember that I promised to solve n-Queens without lifting a finger, and this is where Cryptol’s formal methods based tools come into the picture. Given any predicate (like nQueens above), Cryptol can find inputs that will satisfy it automatically, at the push of a button! (We have briefly described how this works in our previous post on Sudoku, so I shall not go into any details. Suffice it to say that one can exploit modern SAT/SMT solvers to generate automatic solvers for validity problems, and Cryptol provides just the right framework for doing so.)Without further ado, here is how we solve n-Queens in Cryptol, without writing any additional code on top of what we have already seen:
NQueens> :set sbv NQueens> :set base=10 NQueens> :sat nQueens : Solution(8) (nQueens : Solution(8)) [2 7 3 6 0 5 1 4] = True
The first command puts Cryptol in the sbv mode, which allows for the use of SAT/SMT solvers. The second command tells Cryptol to print results in base 10. Finally, the :sat command finds satisfying assignments for predicates. The type-signature on the :sat command indicates that we are interested in solutions for 8-queens, for which we are given a solution almost instantaneously!If you look at the wiki-page for n-queens, you will see that they claim there is always a solution when n=1 and n>=4. We can indeed verify that there are no solutions when n is 2 or 3, using Cryptol:
NQueens> :sat nQueens : Solution(2) No variable assignment satisfies this function NQueens> :sat nQueens : Solution(3) No variable assignment satisfies this function
While these two properties are easy to see, it’s quite valuable to get independent verification!
In practice…
We would be remiss if we didn’t mention some of the actual uses of the satisfiability checker in the Cryptol tool chain. The most important application is in verifying functional equivalence of two functions. If f and g are two functions, then they are functionally equivalent exactly when the predicate (x -> f x != g x) is not satisfiable. (Conversely, if this predicate is satisfiable then the satisfying value is where f and g disagree, indicating a potential bug.) More importantly, f and g need not be both written in Cryptol. The toolchain allows performing equivalence checking between functions written in VHDL, C, and Java (with varying degrees of “seamless” integration!). Furthermore, this is also how we make sure our compiler produces correct code: The function g can be generated code, for instance in one of Cryptol’s intermediate languages as we compile Cryptol to FPGA descriptions. In summary, we can check the equivalence of 3rd party code (generated or hand-written) against “gold” Cryptol specifications, increasing assurance in the correctness of crypto-implementations.
Download
You can download the Cryptol solution for n-Queens. Cryptol licenses are also available free of charge at www.cryptol.net, although I should note that the SAT/SMT based backends are only available in the full-releases of Cryptol, which requires a simple form to be filled before downloading. Enjoy!