sig
  type literal
  val not : Dimacs.literal -> Dimacs.literal
  val nb_variables : unit -> int
  val to_int : Dimacs.literal -> int
  type clause = Dimacs.literal list
  type _ index =
      O : Dimacs.literal Dimacs.index
    | S : int * 'a Dimacs.index -> 'a array Dimacs.index
  val make : 'a Dimacs.index -> 'a
  val ( ** ) : int -> 'a Dimacs.index -> 'a array Dimacs.index
  val o : Dimacs.literal Dimacs.index
  val bigor : int -> (int -> Dimacs.literal) -> Dimacs.clause
  val add_clause : Dimacs.literal list -> unit
  val get_clauses : unit -> Dimacs.clause list
  val output : Stdlib.out_channel -> unit
  val input : Stdlib.in_channel -> unit
  type model
  val read_model : Stdlib.in_channel -> Dimacs.model
  val sat : Dimacs.model -> Dimacs.literal -> bool
  val run : problem:(string -> unit) -> solution:(string -> unit) -> unit
  val run_int : problem:(int -> unit) -> solution:(int -> unit) -> unit
end