Solver (hardcaml_verify.Hardcaml_verify

type run_solver =
  dimacs_in:Base.string ->
  result_out:Base.string ->
  Base.unit ->
  Base.unit Base.Or_error.t

val minisat : run_solver

Minisat solver

val picosat : run_solver

Picosat solver

val z3 : ?seed:Base.int -> parallel:Base.bool -> Base.unit -> run_solver

Z3 solver in DIMACs mode. parallel:true enableds parallel solving, however, as of V4.8.5 Z3 does not return a proper model.

type 'a result = 'a Base.list Sat.t Base.Or_error.t

val sexp_of_result : ( 'a -> Sexplib0.Sexp.t ) -> 'a result -> Sexplib0.Sexp.t

val solve_with_model : 
  ?solver:run_solver ->
  ?print_model:Base.bool ->
  (module Cnf.Model with type input = 'input) ->
  Cnf.t ->
  'input result

Create intermediate files, run the given solver and return a model if satisfiable.

val solve : 
  ?solver:run_solver ->
  ?print_model:Base.bool ->
  Cnf.t ->
  Cnf.Model_with_vectors.input result