takahisa/chibisat

CDCL (Conflict-Driven Clause Learning) based SAT solver written in OCaml

Chibisat

About

Chibisat is a small CDCL (Conflict-Driven Clause Learning) based SAT solver written in OCaml. This software is the result of Special Exercise in Information Science II (情報特別演習II).

How to Build

Install OPAM into your system, and run the following commands.

  opam switch 4.01.0 # require 4.01.0 or later
  opam install ounit omake
  opam install menhir # optional
  omake

Usage

  ./chibiml [options] input.cnf

Reference

• "An Extensible SAT-solver" (http://minisat.se/Papers.html)

License

Chibisat is released under the MIT LICENSE