Module Minisat

Basic set of OCaml bindings for the MiniSat SAT solver.

Datatypes

type t

The type of MiniSAT solvers.

type var

The type of variables.

val pp_var : Ppx_deriving_runtime.Format.formatter -> var -> Ppx_deriving_runtime.unit
val show_var : var -> Ppx_deriving_runtime.string
type lit

The type of literals.

val pp_lit : Ppx_deriving_runtime.Format.formatter -> lit -> Ppx_deriving_runtime.unit
val show_lit : lit -> Ppx_deriving_runtime.string
type value =
  1. | False
  2. | True
  3. | Unknown

The type of variable values.

type solution =
  1. | SAT
  2. | UNSAT

The type of MiniSAT solver solutions.

type stat = {
  1. v : int;
    (*

    Number of variables.

    *)
  2. c : int;
    (*

    Number of clauses.

    *)
  3. mem : float;
    (*

    Memory used in MB.

    *)
  4. cpu : float;
    (*

    CPU time in seconds.

    *)
}

The type of MiniSAT solver statistics.

val create : unit -> t

Create a MiniSAT instance.

val add_clause : t -> lit list -> unit

Add a clause (i.e. disjunction of literals) to the set of problem constraints. A clause is represented as a list of literals.

val add_clause_empty : t -> unit
val add_clause_unit : t -> lit -> unit
val add_clause_binary : t -> lit -> lit -> unit
val add_clause_ternary : t -> lit -> lit -> lit -> unit
val add_clause_quaternary : t -> lit -> lit -> lit -> lit -> unit
val set_verbosity : t -> int -> unit

Set verbosity level (0=silent, 1=some, 2=more).

val new_var : t -> var

Create a fresh variable.

val simplify : t -> unit

simplify can be called before solve to simplify the set of problem constraints. It will first propagate all unit information and then remove all satisfied constraints.

val solve : t -> solution

Find a solution to the current sat problem.

val okay : t -> bool

okay s is false if the solver has already derived a contradiction from the currently added constraints.

Note. A return value of true does not guarantee satisfiability.

val value_of : t -> var -> value

Return the value associated to a variable. Note, this method can only be invoked after solve returned SAT.

Raises Invalid_argument when the input variable is not a valid index.

val get_models : ?vars:var list -> t -> var list list

Return a list of valid models. Note, only true variables are included in each model. Optional argument vars is a list of variables that are banned at each iteration. If this argument is missing all variables are banned.

val get_stats : t -> stat

Return some current statistics. Note, this method can only be invoked after solve has been invoked.

val cpu_time : unit -> float

Cumulative user CPU time (seconds) for the process, as measured by the solver's C layer. Monotonic; not reset per solve.

val print_stats : t -> unit

Print some current statistics to standard output. Note, this method can only be invoked after solve has been invoked.

val string_of_value : value -> string

Convert a value to a string.

val pos_lit : var -> lit

Return the positive literal for a variable.

val neg_lit : var -> lit

Return the negative literal for a variable.

val negate : lit -> lit

Negate a literal.