Article 6X731 Formulating eight queens as a SAT problem

Formulating eight queens as a SAT problem

by
John
from John D. Cook on (#6X731)

The Boolean satisfiability problem is to determine whether there is a way to assign values to variables in a set of Boolean formulas to make the formulas hold [1]. If there is a solution, the next task would be to enumerate the solutions.

You can solve the famous eight queens problem, or its generalization ton-queens, by formulating the problem as a Boolean formula then using a SAT solver to find the solutions.

It's pretty obvious how to start. A chessboard is an 8 by 8 grid, so you have a variable for each square on the board, representing whether or not that square holds a queen. Call the variables bij wherei andj run from 1 to 8.

The requirement that every row contains exactly one queen can be turned into two subrequirements:

  1. Each row contains at least one queen.
  2. Each row contains at most one queen.

The first requirement is easy. For each rowi, we have a clause

bi1 bi2 bi3 ... bi8

The second requirement is harder. How do you express in terms of our boolean variables that there is no more than one queen in each row? This is the key difficulty. If we can solve this problem, then we're essentially done. We just need to do the analogous thing for columns and diagonals. (We don't require a queen on every diagonal, but we require that there be at most one queen on every diagonal.)

First approach

There are two ways to encode the requirement that every row contain at most one queen. The first is to use implication. If there's a queen in the first column, then there is not a queen in the remaining columns. If there's a queen in the second column, then there is not a queen in all but the second column, etc. We have an implication for each row in each column. Let's just look at the first row and first column.

b11 (b12 b13 ... b18)

We can turn an implication of the form a b into the clause a b.

Second approach

The second way to encode the requirement that every row contain at most one queen is to say that for every pair of squares in a row (a,b) eithera has no queen orb has no queen. So for the first row we would have 8C2 = 28 clauses because there are 28 ways to choose pairs from a set of 8 things.

(b11 b12) (b11 b13) ... (b17 b18)

An advantage of this approach is that it directly puts the problem into conjunctive normal form (CNF). That is, our formula is a conjunction of terms that contain only disjunctions, an AND of ORs.

Related posts

[1] You'll see the SAT problem described as finding the solution toa Boolean formula. If you have multiple formulas, then the first holds, and the second, etc. So you can AND them all together to make one formula.

The post Formulating eight queens as a SAT problem first appeared on John D. Cook.
External Content
Source RSS or Atom Feed
Feed Location http://feeds.feedburner.com/TheEndeavour?format=xml
Feed Title John D. Cook
Feed Link https://www.johndcook.com/blog
Reply 0 comments