`module X : S`

generic failure reason

`type state`

state of the solver

`type var = int`

variables are integers numbered from 0 to (size - 1)

`type value =`

1. `| True`
2. `| False`
3. `| Unknown`

The value of a literal

`type lit`

A literal. Literals can be positive or negative

`val lit_of_var : var -> bool -> lit`

`lit_of_var` given a variable create a positive or a negative literal. By default the assigment of all variables (that is its value) is Unknown.

`val initialize_problem : ?print_var:(Stdlib.Format.formatter -> int -> unit) -> ?buffer:bool -> int -> state`

initialize the solver `initialize_problem n`

- parameter print_var

  a function to print a variable

- parameter buffer

  decide weather or not to store a human readable representaion of the sat problem.

- parameter n

  the size of the sat problem. that is the max number of variables to consider

`val copy : state -> state`

provide a deep copy of the current state of the solver

`val propagate : state -> unit`
`val protect : state -> unit`
`val reset : state -> unit`

`reset` reset the state of the solver to a state that would be obtained by re initializing the solver with an identical constraints set

`val assignment : state -> value array`

`assignment st` return the array of values associated to every variable.

`val assignment_true : state -> var list`

`assignment_true st` return the list of variables that are true

`val add_rule : state -> lit array -> X.reason list -> unit`

`add_rule st l` add a disjuction to the solver of type \Bigvee l

`val associate_vars : state -> lit -> var list -> unit`

`associate_vars st lit vl` associate a variable to a list of variables. The solver will use this information to guide the search heuristic

`val solve_all : (state -> unit) -> state -> var -> bool`
`val solve : state -> var -> bool`

`solve st v` finds a variable assignment that makes v True

`val solve_lst : state -> var list -> bool`

`solve st l` finds a variable assignment that makes `True` all variables in `l`

`val collect_reasons : state -> var -> X.reason list`

in case of failure return the list of associated reasons

`val collect_reasons_lst : state -> var list -> X.reason list`

in case of failure return the list of associated reasons

`val dump : state -> (int * bool) list list`

if the solver was initialized with `buffer = true`, dump the state of the solver. Return an empty list otherwise

`val debug : bool -> unit`

enable debug messages

`val stats : state -> unit`