A simple SAT solver based on DPLL written in Racket.
Switch branches/tags
Nothing to show
Clone or download
Latest commit f7d02e9 Sep 20, 2018
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
lib fix mistake of assignment Sep 20, 2018
scribblings restruct the project Oct 13, 2017
tests add more test cases Sep 20, 2018
LICENSE.txt restruct the project Oct 13, 2017
README.md update readme file Oct 13, 2017
info.rkt restruct the project Oct 13, 2017
main.rkt restruct the project Oct 13, 2017
test.rkt fix mistake of assignment Sep 20, 2018

README.md

SAT.rkt

A simple SAT solver based on DPLL algorithm, written in Racket. Only less than 100 lines of code.

Usages

Use raco pkg install SAT to install this package.

As a library, use (require SAT) to load the library,

  • use (solve filepath) given a filepath of DIMACS file
  • use (get-model) to get the assignment of variables
  • use (parse-dimacs-file filepath) to transform content of a DIMACS file to S-Expressions
  • use (check-sat clauses) to check satisfiability given clauses in S-Expression form

TODO

  • Improve performance, use Conflict-Driven Clause Learning