sattools

Ctypes and DIMACs interfaces to minisat, picosat and cryptominisat
README

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 solvers minisat, picosat and cryptominisat(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.t
end

note; in some cases extra functionality can be accessed directly through
the FFI interface; see the modules minisat, picosat and cryptominisat

Install
Published
06 Jan 2017
Sources
v0.1.0.tar.gz
md5=3f1f15d5a738ce95c92214a71c532620
Dependencies
Reverse Dependencies