Intro & demo
Simple SAT solver for the n-queens problem. Just input the number of queens, voilà!
The demo is at: https://huyen-nguyen.github.io/n-queens/
Encoding the problem
The source code for encoding is at https://gist.github.com/huyen-nguyen/f497216b6c2601d73fe3ca0f89f5c6d2
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]
Demo
The live demo is available at https://huyen-nguyen.github.io/n-queens/
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.