package touist

  1. Overview
  2. Docs

Process an evaluated AST given by Eval.eval to produce a CNF AST and output DIMACS

ast_to_cnf is the main function.

Vocabulary

  • Literal: a possibly negated proposition; we denote them as a, b... and their type is homogenous to Prop _ or Not(Prop _) or Top or Bottom. Exples:

    • a is a literal,
    • not b is a literal.

  • Clause: a disjunction (= separated by "or") of possibly negated literals. Example of clause:

    • a or not b or c or d is a clause

  • Conjunction: literals separated by "and"; example:

    • a and b and not and not d is a conjunction

  • AST: abstract syntax tree; it is homogenous to Types.Ast.t and is a recursive tree representing a formula, using Or, And, Implies... Example: the formula (1) has the abstract syntax tree (2):

    • (a or b) and not c (1) natural language
    • And (Or (Prop x, Prop x),Not (Prop x)) (2) abstract syntax tree

  • CNF: a Conjunctive Normal Form is an AST that has a special structure with is a conjunction of disjunctions of literals. For example:

    • (a or not b) and (not c and d) is a CNF form
    • (a and b) or not (c or d) is not a CNF form

CNF transformation

val ast_to_cnf : ?debug_cnf:bool -> Types.Ast.t -> Types.Ast.t

ast_to_cnf translates the syntaxic tree made of Or, And, Implies, Equiv... Or, And and Not; moreover, it can only be in a conjunction of formulas (see a reminder of their definition above). For example (instead of And, Or we use "and" and "or" and "not"):

        (a or not b or c) and (not a or b or d) and (d)

The matching abstract syntax tree (ast) is

        And (Or a,(Cor (Not b),c)), (And (Or (Or (Not a),b),d), d)

Clauses transformation

val clauses_of_cnf : ('a -> 'a) -> (unit -> 'a) -> Types.Ast.t -> 'a list list * ('a, string) Hashtbl.t * (string, 'a) Hashtbl.t

clauses_of_cnf translates the cnf ast (Not, And, Or, Prop; no Bot/Top) into a CNF formula that takes the form of a list of lists of litterals (conjunctions of disjunctions of possibly negated proprositions). neg lit returns the negation of the litteral (not) fresh () returns a newly generated litteral Returns:

  • the list of lists of litterals
  • the table literal-to-name Note that the total number of literals is exactly equal to the table size; this size includes the special propositions beginning with '&' (e.g., '&4').

DIMACS output

The following functions are for displaying dimacs/qdimacs format. Example for the formula

        rain=>wet and rain and not wet

we get the dimacs file:

        c wet 1                           <-- (optionnal) [print_table]
        c rain 2
        c CNF format file                 <-- by hand
        p cnf 2 3                         <-- by hand (nb_lits, nb_clauses)
        -2 1 0                            <-- [print_clauses]
        -2 2 0
        -2 -1 0
val print_table : ('a -> int) -> out_channel -> ?prefix:string -> ('a, string) Hashtbl.t -> unit

print_table prints the correspondance table between literals (= numbers) and user-defined proposition names, e.g.,

        p(1,2) 98

where 98 is the literal id number (given automatically) and p(1,2) is the name of this proposition.

NOTE: you can add a prefix to 'p(1,2) 98', e.g. 

string_of_table ~prefix:"c " table

in order to have all lines beginning by 'c' (= comment) in order to comply to the DIMACS format.

val print_clauses : out_channel -> ('a -> string) -> 'a list list -> unit

print_clauses prints one disjunction per line ended by 0:

       -2 1 0
       -2 2 0

IMPORTANT: prints ONLY the clauses. You must print the dimacs/qdimacs header yourself, e.g.:

       p cnf <nb_lits> <nb_clauses>      with <nb_lits> = Hashtbl.length table
                                              <nb_clauses> = List.length clauses

Other functions

val is_dummy : string -> bool

is_dummy name tells (using the name of a litteral) is a 'dummy' literal that was introduced during cnf conversion; these literals are identified by their prefix '&'.