Assignment 1: Encoding the n-Queens Problem into SAT

The n-Queens Problem

Given an integer n, find a way to place n queens on an n x n chessboard so that no two queens attack each other. Since a queen attacks along her row, column, and diagonals, a solution requires that no two queens share the same row, column, or diagonal. For more information about the problem, and to see all solutions for n = 8, refer to its Wikipedia page Links to an external site..

Your Task

The n-queens problem is amenable to encoding into SAT. Your task is to write a program that takes an integer n as input and finds a solution to the n-queens problem by encoding it into SAT. Hence, you should not implement an algorithm that directly finds solutions to the n-queens problem, but rather you should let a SAT solver do most of the work.
Program input: An integer n > 0 entered as a command line argument to your binary or script. If you don't know how to deal with command like arguments let me know.
Program output: All possible solutions for the n-queens problem for a given n. The output should be in the following format (example given for n = 4), where solutions should be separated by an empty line:

.X..
...X
X...
..X.

..X.
X...
...X
.X..

In the output, queens are marked with X. It is fine to have an additional empty line in the end.

Runtime requirements: We require that your program terminates in a reasonable amount of time, meaning under 10 minutes for n = 10.

Here are some additional notes to get your started. I recommend you use MiniSat Links to an external site. as your SAT solver. It is popular, fast, small, and easy to compile and use. You can either invoke it as an external command from your program (probably easier route), or use it as a library. If you prefer to use a different SAT solver, submit its binary with your solution. Based on my experience with this assignment, implementing it as a script in e.g. Python might be the easiest approach. This is up to you and ultimately I do not care which language you use.

I suggest that you first implement the basic algorithm that generates just one solution, and then throughly test it. If it works fine, modify it so that instead of generating just one solution, it generate all possible solutions for the n-queens problem for a given n.

Assignment Deliverables

Source code and a Linux binary of your solution if applicable. Also, a brief summary (at most one page, PDF format) explaining how your encoding works and how to run your solution. Ultimately, we have to be able to run your solution on a Linux machine. You can assume that MiniSat is in the PATH variable on our grading machine. Submit your deliverables (PDF summary, source code, binary of applicable) as a zip archive through Canvas.