Huyen N. Nguyen

N-queens problem SAT solver

Intro & demo

Simple SAT solver for the n-queens problem. Just input the number of queens, voilà!

The demo is at:


Encoding the problem

The source code for encoding is at

We need to encode the following constraints 1) no two queens on the same row, 2) no two queens on the same column, and 3) no two queens on the same diagonal.

We assign a proposition letter (variable) for each position on the board. Let Pi denote the propositional letter for position (i) of the board. If Pi is true, there is a queen on (i); otherwise, there is no queen on (i). Let N be the size of queens; from now on, we name the cell from 1 (top left) to N*N (bottom right).

The DIMACS CNF formula starts with some comments c about the size of n-queens problem, then followed by: p cnf [N*N] [Number of clauses]


The live demo is available at

The user can input a number to specify the number of queens (size of board), then click “Run” and the program will output:

1) DIMACS CNF formula of such n-queens problem

2) Result from SAT Solver of satisfiability of the given proposition

A chess board with corresponding queen positions is provided for visual reference. User can also copy the formula to clipboard or export this formula to a .cnf file.