README

Sattools

Interfaces to SAT solvers and related utility functions.

The solvers can be accessed through DIMAC files, or through their c/c++ interface using ctypes.

The solversminisat,picosat andcryptominisat(4) are supported.

The appropriate solver library must exist on the system at build time for the FFI interface to be built. Access via DIMACs files it always built in and is detected at run-time.

The following lists available solvers

# Sattools.Libs.available_solvers();;- : bytes list =["crypto"; "pico"; "mini"; "dimacs-crypto"; "dimacs-mini"; "dimacs-pico"]

An available solver module can be instantiated with

# module X = (val (Sattools.Libs.get_solver "mini"));;module X : Sattools.Libs.Solver

and provides the following simple API

module type Solver = sig  type solver  val create : unit -> solver  val destroy : solver -> unit  val add_clause : solver -> int list -> unit  val solve : solver -> unit Result.t  val solve_with_model : solver -> int list Result.t  val model : solver -> int -> Lbool.tend

note; in some cases extra functionality can be accessed directly through the FFI interface; see the modulesminisat,picosat andcryptominisat

1. astring
2. ctypes
3. ctypes-foreign
4. base-unix
5. base-bytes
6. topkgbuild
7. ocamlbuildbuild
8. ocamlfindbuild
9. ocaml>= "4.01.0"

None

None

None