Skip to content

Modelling n-queens problem as conjunctive normal form and solving it with DPLL algorithm. This project should made me familiar with Rust and the test driven approach.

Notifications You must be signed in to change notification settings

erohkohl/n-queens-sat

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

41 Commits
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

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

Build Status codecov

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

About

Modelling n-queens problem as conjunctive normal form and solving it with DPLL algorithm. This project should made me familiar with Rust and the test driven approach.

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages