erohkohl/n-queens-sat

Modelling n-queens problem as propositional formula and solve it with DPLL

This project provides a simple implementation of the Davis, Putnam, Logemann and Loveland algorithm
(see DPLL) in the modern systems programming language
Rust. The DPLL algorithm decides whether a propositional
formula in conjunctive normal form (CNF) is satisfiable and returns a satisfiable assignment. Therefore it extends the
depth first search with unit propagation (UP), if a literal must be true in the current partial assignment. You
can find my implementation of the DPLL algorithm in the Rust-file
src/logic/sat.rs. Furthermore the file
src/model/n_queens.rs
contains the modelling of the n-queens problem as propositional formula. The following listing shows one possible
solution of the four-queens problem.

. Q . . 
. . . Q 
Q . . . 
. . Q . 

This implementation is not able to solve six-queens problem in acceptable time, because it's
data structures and UP is not fast enough.

Future work

• Improve performance of UP and data structures to solve eight-queens problem in appropriate time
• Add Conflict-Driven Clause Learning (see CDCL)
  to DPLL algorithm