package touist

  1. Overview
  2. Docs

Requires minisat Process a CNF AST to clauses in order to solve them with Minisat.

CNF to clauses

val minisat_clauses_of_cnf : TouistTypes.Ast.t -> Minisat.Lit.t list list * (Minisat.Lit.t, string) Hashtbl.t

minisat_clauses_of_cnf ast takes a CNF ast and outputs

  • a list of lists of Minisat litterals,
  • a mapping table (Minisat litterals -> name of the proposition)

Solving clauses (using Minisat)

module Model : sig ... end
module ModelSet : sig ... end
val solve_clauses : ?verbose:bool -> ?print:(Model.t -> int -> unit) -> ?continue:(Model.t -> int -> bool) -> (Minisat.Lit.t list list * (Minisat.Lit.t, string) Hashtbl.t) -> ModelSet.t Pervasives.ref

solve_clauses finds the models for the given clauses.

print model N is a function that will print a model as soon as it is found. N is the number of the model, it begins at 1. It can be useful to print the models as they appear because finding all models (if limit is large) can be extremely long. Example: ~print:(TouistSatSolve.Model.pprint table model)

verbose allows to turn on the verbose mode of minisat; apparently, this minisat feature doesn't seem to be working and doesn't display any time information.

continue model nth is a function called after every model that has been found. model contains the found model and N says that this model was the nth model found. This function tells solve_clauses to go on searching models or not.

val string_of_clause : Minisat.Lit.t list -> string
val string_of_clauses : Minisat.Lit.t list list -> string
OCaml

Innovation. Community. Security.