Module Sat
module Sat: sig .. end
Basic interface to a sat solver and convertion between cnf and dnf formulas.
Variables are given by positive integers and we use -n to denote 'not n'.
Main Functions
val set_timeout : float -> unit
Set timeout function for conversions.
val clear_timeout : unit -> unit
Clear timeout function.
val simplify : int list -> int list list -> int list list
Given a list of literals to set to true, simplify the given CNF formula.
val minimize : sep:int -> int list -> int list list -> int list
Greedy minimize the number of between-sep positive variables in a model.
val sat : int list list -> int list option
Check satisfiability of a formula in CNF, return a satisfying assignment.
val is_sat : int list list -> bool
Check satisfiability of a formula in CNF, return just true or false.
exception OverBound
val convert : ?disc_vars:int list -> ?bound:int option -> int list list -> int list list
Convert a DNF formula to CNF (or equivalently, CNF to DNF).
val convert_aux_cnf : ?disc_vars:int list ->
?bound:int option -> int -> int list list -> int list list
Convert a auxiliary CNF formula to "real" CNF (or, equivalently, to DNF).
Printing
val clause_str : int list -> string
Return the given clause (disjunction of literals) as string.
val cnf_str : int list list -> string
Return the given CNF formula as string.
val conjunct_str : int list -> string
Return the given conjunction of literals as string.
val dnf_str : int list list -> string
Return the given DNF formula as string.