(**************************************************************************) (* *) (* 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/ *) (* *) (**************************************************************************) (* Satisfiabilité par un algorithme de type DPLL Travaille sur des formules en forme normale conjonctive *) open Cnf (* DPLL Pour une forme normale conjonctive `nf`, la fonction `dpll` renvoie - `Some v` si la formule est satisfiable, avec `v` une valuation qui convient - `None` si la formule n'est pas satisfiable. *) exception Unsat (* on a choisi le littéral x et on propage ; lève Unsat si contradiction *) let propagate x cl = let rec simplify = function | [] -> [] | y :: _ when y = x -> raise Exit | y :: c when y = -x -> simplify c | y :: c -> y :: simplify c in let clause cl c = match simplify c with | [] -> raise Unsat | c -> c :: cl | exception Exit -> cl in List.fold_left clause [] cl let dpll nf = if nf.kind <> CNF then invalid_arg "dpll"; let n = nf.nbvars in let v = Array.make (n + 1) false in (* est-il possible de satisfaire une liste de clauses ? *) let rec backtrack = function | [] -> true | c :: cl -> List.exists (literal cl) c (* est-il possible de satisfaire le littéral x puis la liste cl ? *) and literal cl x = v.(abs x) <- x > 0; try let cl = propagate x cl in backtrack cl with Unsat -> false in if backtrack nf.clauses then Some v else None