(**************************************************************************) (* *) (* Thibaut Balabonski, Sylvain Conchon, Jean-Christophe Filliâtre, *) (* Kim Nguyen, Laurent Sartre *) (* *) (* Informatique - MP2I/MPI - CPGE 1re et 2e années. *) (* Cours et exercices corrigés. Éditions Ellipses, 2022. *) (* *) (* https://www.informatique-mpi.fr/ *) (* *) (**************************************************************************) (* Formes normales conjonctives Un littéral `x` est un entier dans 1..n (variable x) ou dans -n..-1 (négation de la variable -x). Une clause `c` est une liste de littéraux, sans doublons, triée par ordre croissant de valeur absolue. *) open Fmla open Format type literal = int type clause = literal list type kind = CNF | DNF type nf = { kind: kind; nbvars: int; clauses: clause list } let dimacs fmt nf = let nc = List.length nf.clauses in fprintf fmt "p %s %d %d@\n" (match nf.kind with CNF -> "cnf" | DNF -> "dnf") nf.nbvars nc; let literal x = fprintf fmt "%d " x in let clause c = List.iter literal c; fprintf fmt "0@\n" in List.iter clause nf.clauses (* Forme normale conjonctive (CNF en anglais) Invariant : une CNF est - soit [] (true) - soit [[]] (false) - soit une liste non vide de clauses non vides *) exception Tauto (* la disjonction de deux clauses (exploite le caractère trié) *) let rec merge_or = function | [], c | c, [] -> c | (x1 :: s1 as c1), (x2 :: s2 as c2) -> if x1 = x2 then x1 :: merge_or (s1, s2) else if x1 = -x2 then raise Tauto else if abs x1 < abs x2 then x1 :: merge_or (s1, c2) else x2 :: merge_or (c1, s2) (* toutes les disjonctions c1\/c2 avec c1 dans cl1 et c2 dans cl2 *) let cnf_or cl1 cl2 = match cl1, cl2 with | [], _ | _, [] -> [] | [[]], c | c, [[]] -> c | _ -> let combine11 c2 acc c1 = try let c = merge_or (c1, c2) in c :: acc with Tauto -> acc in let combine1 acc c2 = List.fold_left (combine11 c2) acc cl1 in List.fold_left combine1 [] cl2 let cnf_and cl1 cl2 = if cl1 = [[]] || cl2 = [[]] then [[]] else cl1 @ cl2 (* mise en forme normale conjonctive de `f` *) let rec cnf = function | True -> [] | False -> [[]] | Var x -> [[x]] | Not f -> cnf_neg f | Bin (And, f1, f2) -> cnf_and (cnf f1) (cnf f2) | Bin (Or, f1, f2) -> cnf_or (cnf f1) (cnf f2) | Bin (Imp, f1, f2) -> cnf_or (cnf_neg f1) (cnf f2) (* mise en forme normale conjonctive de `non f` *) and cnf_neg = function | True -> [[]] | False -> [] | Var x -> [[-x]] | Not f -> cnf f | Bin (And, f1, f2) -> cnf_or (cnf_neg f1) (cnf_neg f2) | Bin (Or, f1, f2) -> cnf_and (cnf_neg f1) (cnf_neg f2) | Bin (Imp, f1, f2) -> cnf_and (cnf f1) (cnf_neg f2) let cnf f = { kind = CNF; nbvars = varmax f; clauses = cnf f }