module Sat

: sig

A general purpose SAT solver.

module type USER = sig

type t

val to_string : t -> string

end

module MakeSAT : functor (User : USER) -> sig

type sat_problem

A SAT problem consists of a set of variables and a set of clauses which must be satisfied.

type var_value =

# \| True
# \| False
# \| Undecided

type lit

A literal is either a variable (e.g. A) or a negated variable (not A).

val neg : lit -> lit

val add_variable : sat_problem -> User.t -> lit

type clause

A clause is a boolean expression made up of literals. e.g. A and B and not(C)

Setting up the problem.

val create : unit -> sat_problem

type solution = lit -> bool

Get the assignment for this literal in the discovered solution.

val impossible : sat_problem -> unit -> unit

Indicate that the problem is unsolvable, before even starting. This is a convenience feature so that clients don't need a separate code path for problems they discover during setup vs problems discovered by the solver.

type added_result =

# \| AddedFact of bool
# \| AddedClause of clause	(*	Add a clause requiring at least one literal to be `True`. e.g. `A or B or not(C)`. `reason` is used in debug messages.	*)

val at_least_one : sat_problem -> ?reason:string -> lit list -> unit

val implies : sat_problem -> ?reason:string -> lit -> lit list -> unit

If the first variable is true, at least one of the others must be. implies p a bs is equivalent to at_least_one p ((neg a) :: bs). reason is used in debug messages.

type at_most_one_clause

Add a clause preventing more than one literal in the list from being True.

val at_most_one : sat_problem -> lit list -> at_most_one_clause

val run_solver : sat_problem -> (unit -> lit option) -> solution option

run_solver decider tries to solve the SAT problem. It simplifies it as much as possible first. When it has two paths which both appear possible, it calls decider () to choose which to explore first. If this leads to a solution, it will be used. If not, the other path will be tried. If decider returns None, we try setting the remaining variables to False (decider will not be called again unless we backtrack). Use this to tidy up at the end, when you no longer care about the order.

Returns true on success.

val get_best_undecided : at_most_one_clause -> lit option

Return the first literal in the list whose value is Undecided, or None if they're all decided. The decider function may find this useful.

val get_selected : at_most_one_clause -> lit option

Return the selected literal, if any.

Debugging

type reason =

# \| Clause of clause
# \| External of string

val string_of_clause : clause -> string

val string_of_reason : reason -> string

val string_of_value : var_value -> string

val name_lit : lit -> string

val string_of_lits : lit list -> string

val lit_value : lit -> var_value

val get_user_data_for_lit : lit -> User.t

val explain_reason : lit -> string

end