Module Dimacs

module Dimacs: sig .. end

Manage SAT problem descriptions, with input and output to DIMACS file format.

This module uses global state to maintain an implicit set of declared variables and clauses.

type literal

Litterals, i.e. propositional variables or negations of variables. We have no type for variables.

val not : literal -> literal

Negation of a literal.

val nb_variables : unit -> int

Number of variables currently declared.

val to_int : literal -> int

Convert a literal to an integer: positive literals are mapped to positive integers that are less or equal to nb_variables (); negative literals are mapped to the opposite negative integers.

type clause = literal list

Variable declaration

type '_ index =

`\|`	`O : literal index`
`\|`	`S : int * 'a index -> 'a array index`

Indices are used to create arrays of arrays of ... literals. A value S _ (S _ ... O) with n uses of constructor C is of type (variable array^n) index and it can be used to create an array of variables of dimension n. The integers are the sizes of the array for the given dimension.

val make : 'a index -> 'a

Create an n-dimensional array of variables (i.e. positive literals), where the dimension n and the sizes on respective dimensions are given by an index.

Notations for creating indices

val ( ** ) : int -> 'a index -> 'a array index

These notations notably allow to write let x = Dimacs.(make (2**i**o)) to create a two-dimensional array of size 2 on dimension 1 and size i on dimension 2, i.e. such that x.(1).(i-1) is a variable.

val o : literal index

Clause declaration

Clauses, i.e. disjunctions of literals, are represented as lists of literals.

val bigor : int -> (int -> literal) -> clause

bigor n f returns the clause f 0 \/ ... \/ f (n-1). Indices passed to f start at 0: they are meant to be used as array indices, not as literals.

val add_clause : literal list -> unit

Add a clause to the problem.

val get_clauses : unit -> clause list

Get the current problem as a list of clauses.

DIMACS input/output

val output : Stdlib.out_channel -> unit

Output the problem in DIMACS format on some output channel.

val input : Stdlib.in_channel -> unit

Read a SAT problem in DIMACS format from some input channel. This modifies the current set of variables and clauses, erasing previous declarations.

Models

type model

A model (assignment) for the current set of propositional variables.

val read_model : Stdlib.in_channel -> model

Read model from some input channel in DIMACS format. Comments are not supported.

val sat : model -> literal -> bool

Tell whether a literal is satisfied in some model.

Runners

Runners are used to launch problem encoders and provide them with a common command-line interface.

The binaries will take two arguments, the first one being "problem" or "solution" (or simply "p" and "s") and the second one being the problem description: an integer with run_int, or a filename as a string with run.

In problem mode, the application declares the problem with the problem function, then the problem is written to file "./problem.cnf". In solution mode, the solution function is ran, and it is expected to read a model from file "./output.sat" after having declared the appropriate variables.

val run : problem:(string -> unit) -> solution:(string -> unit) -> unit

val run_int : problem:(int -> unit) -> solution:(int -> unit) -> unit