An OCaml implementation of the DPLL algorithm for solving SAT instances. Uses nothing beyond the OCaml List library.
OCaml
Switch branches/tags
Nothing to show
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
Makefile
README.md
cnf.ml
dpll.ml
generator.ml
test.ml

README.md

OCaml-SAT-Solvers

A fully functional set of OCaml modules to solve satisfiability problems represented in conjunctive normal form (CNF) using only the OCaml list library and the DPLL algorithm.

File Structure

The repository is broken down into several files:

  • cnf.ml: contains representations for literals, symbols, cnf statements, clauses, etc., as well as utility methods for generalized operations on CNF statements, including satisfiability checkers.

  • dpll.ml: contains an OCaml list-only implementation of the Davis-Putnam-Logemann-Loveland (DPLL) algorithm for solving satisfiability problems.

  • generator.ml: contains methods for generating random cnf statements of a specified size, as well as a method to print and solve said statements, all with a single function call.

  • test.ml: contains a sample test case.