ocaml bindings for picosat

The code is on github . Get in touch if you find this useful.

ocaml bingings for picosat

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’ ), 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 documentation refer to picosat.h and picosat.mli

Install and use

To compile ocaml-picosat you need the picosat solver (compiled as a dynamic library) installed on the system.

The library assumes : /usr/include/picosat/picosat.h and /usr/lib/libpicosat.so.1.0.0

Picosat is a stateless module. I’ve also add an higher level api to add clauses and to generate a model and an unset core. It mimics a bit the same concept of the minisat bindings, but without the OO interface. We can set the number of variables, the trace (on by default and the picosat library must be compiled with -DTRACE) and the initial seed.

type var = int
type lit
type value = True | False | Unknown
type solution = SAT | UNSAT | UNKNOWN

val init : ?seed : int -> ?nvars : int -> ?trace : bool -> unit -> unit
external reset: unit -> unit = "caml_picosat_reset"

external model: unit -> var list = "caml_model"
external unsatcore : unit -> var list = "caml_unsatcore"

val add_clause : lit list -> unit

val solve : ?limit : int -> unit -> solution 
val solve_with_assumptions : ?limit : int  -> lit list -> solution 

val new_var : unit -> var
val value_of : var -> value

val pos_lit : var -> lit
val neg_lit : var -> lit

val string_of_value : value -> string

This is a snippet from the test file :

let solve file =
  Picosat.init ();
  let vars = process_file file in
  let revs =
    let acc = Hashtbl.create (Hashtbl.length vars) in
    Hashtbl.iter (fun name v -> Hashtbl.add acc v name) vars ;
    acc
  in
  match Picosat.solve () with
  | Picosat.UNKNOWN -> printf "Limit exausted\n"
  | Picosat.UNSAT ->
      begin
        printf "unsat\nunsat core : %s\n"
        (String.concat "," (List.map (fun i -> (Hashtbl.find revs i)) (Picosat.unsatcore ())))
      end
  | Picosat.SAT   ->
      begin
        printf "sat\nmodel : \n";
        List.iter (fun i ->
          printf "  %s=%s\n"
          (Hashtbl.find revs i)
          (Picosat.string_of_value (Picosat.value_of i))
        ) (Picosat.model ())
      end