Skip to content

OCaML bindings for the MiniSat satisfiability solver.

License

Notifications You must be signed in to change notification settings

abate/minisat-ocaml

 
 

Repository files navigation

OCaml Binding for minisat2
==========================

MiniSat-ocaml is a set of OCaml bindings for the SAT solver MiniSat.  Instead
of reimplementing MiniSat itself in OCaml, this library makes the MiniSat
interface available through OCaml.

The usage of the OCaml interface is pretty straightforward and mimics the C++
interface.

The package provides an example, solver.ml, that reads from standard input a
formula and print its satisfiability and a satisfying assignment (if any). A
formula is a sequence of lines that either define a variable ('v' <name>),
define a clause ('c' followed by a sequence of names, with a leading '-' if
they are negated in the clause) and comments (starting with '#'). A couple of
example formulas are available in the 'examples/' directory.

For questions, comments, suggestion, or improvements please contact 
Pietro Abate <pietro.abate@inria.fr>

Copyright:
     Pietro Abate 2009 - 2016 (c)
     Flavio Lerda 2007 - 2009 (c)

Install and use
===============

$ aptitude install minisat
$ make

To test it :
$./solver.byte examples/1.formula 
Verified 1 original clauses.
Solving examples/1.formula...
sat
  b=false
  a=false

enjoy !

About

OCaML bindings for the MiniSat satisfiability solver.

Resources

License

Stars

Watchers

Forks

Packages

No packages published

Languages

  • OCaml 57.1%
  • C 34.5%
  • Makefile 8.4%