Solving n-Queens in Cryptol

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 sequence3  7  0  2  5  1  6  4recording 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 functionNQueens> :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.DownloadYou 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!

Comments

[Yitz]

Nice! This being Cryptol, one immediately thinks of extending these methods to develop a manual cipher based on the chess board, analogous to Schneier's Solitaire cipher (http://www.schneier.com/solitaire.html) based on a deck of playing cards.

[Boris Lykah]

The function of type Solution takes n words of [1 + width n] length. However, as the board is square we need only [width n] length and one bit is excess. The code with [n][width n] does not compile because in case n==0 we have an empty sequence of zero size numbers and zero size numbers are meaningless. It is possible to modify the types so that we don't have excess bits but board of 0x0 size is not processed.

type Solution(n) = [n][width n] -> Bit;nQueens : {n} (fin n, n >= 1) => Solution(n);

[Levent Erkok]

Yitz: Thanks for the Schneier reference! It's an enjoyable read.

Boris: Indeed you can save an extra bit if you ignore the 0x0 board. However, the assertion "zero size numbers are meaningless" is actually not quite right in the context of cryptography. One essential use case is in padding: Sometimes you want to pad a given word so its width is a multiple of some number, usually the block size of the underlying cipher. Then, padding with a word of width 0 makes perfect sense, if the input is already padded correctly. Indeed, the type [0] is perfectly valid in Cryptol, with zero being its only (and very useful!) inhabitant.

[Boris Lykah]

Thanks for the explanation. I misinterpreted the error.While checking type of nQueens, with the following declared signature: {n} (fin n) => [n][width n] —> Bitinferred the following constraint not implied by the signature:(width n >= max(width n,1))I thought it meant that word width always must be >= 1. However, as I see now this constraint was introduced by indexing in function checkDiag. If qs @ i,j is replaced with 0 the error disappears. Hope now I understood the reason of the restriction properly.

[Levent Erkok]

Boris: The >=1 requirement comes from ijs. Due to the expression "n-1" we get the constraint n must have at least 1 bit in it. That constraint propagates to diffC (due to j-i); which then requires the extra bit due to the comparison between diffC and diffR. I think you can avoid it by tacking on an extra bit to diffR (something like diffR#zero != diffC), or you can trim the rightmost bit from diffC. It'd be a good exercise to play with that variant and prove that the new version is equivalent to the original as an exercise!

[roy_hu]

How do you write a Crytol program to generate all solutions to N-Queens? The example you showed only found one.

Isn't verifying functional equivalence of two functions in general impossible? How is it done in Cryptol? Is it sort of like QuickCheck?

[roy_hu]

Regarding equivalence checking, it seems to have been addressed in your PLPV 09 paper. I'm going to take a look, thanks!

[Levent Erkok]

Hi Roy: Currently, there's no automatic support for generating all solutions unfortunately. However, you can easily generate them by writing new predicates, refuting the earlier solutions. Something like:

:sat (\x -> (nQueens x) & (x != [2 7 3 6 0 5 1 4]))

This will give you the "next" solution. You can keep on refuting the generated solutions to get new assignments.

Admittedly, this'll get pretty verbose quickly and hence will be a bother to write one after the other. You can give a name to the function and save it in a file to simplify things a bit. We should automate this process, but haven't gotten around to doing so yet.

Regarding how the equivalence checking is done, I think you've found the right reference. Let us know if you've any further questions.