package sattools

  1. Overview
  2. Docs
Ctypes and DIMACs interfaces to minisat, picosat and cryptominisat

Install

Dune Dependency

Authors

Maintainers

Sources

v0.1.0.tar.gz
sha256=b41ca2833e5666279e999f319801272d434049c1ccf23e0a30ab278493238b4d
md5=3f1f15d5a738ce95c92214a71c532620

Description

Published: 06 Jan 2017

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 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

Dev Dependencies

None

Conflicts

None

OCaml

Innovation. Community. Security.