File: dpll.ml

package info (click to toggle)
coccinelle 1.0.8.deb-5
  • links: PTS, VCS
  • area: main
  • in suites: bullseye, sid
  • size: 26,148 kB
  • sloc: ml: 136,392; ansic: 23,594; sh: 2,189; makefile: 2,157; perl: 1,576; lisp: 840; python: 823; awk: 70; csh: 12
file content (95 lines) | stat: -rw-r--r-- 2,965 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
(*
 * This file is part of Coccinelle, licensed under the terms of the GPL v2.
 * See copyright.txt in the Coccinelle source code for more information.
 * The Coccinelle source code can be obtained at http://coccinelle.lip6.fr
 *)

(* A simple implementation of the DPLL algorithm:
http://en.wikipedia.org/wiki/DPLL_algorithm

A formula is in cnf.

This is not currently used, but please don't get rid of it. *)

type positive_literal = string
type negative_literal = string
type clause = positive_literal * negative_literal (*represents a disjunction*)
type formula = clause list (* represents a conjunction *)

(* The formula ((a v !b) & (c v !d v !e)) would be
[[([a],[b])];[([c],[d;e])]] *)

(* ----------------------------------------------------------------------- *)
(* evaluation *)

let rec evaluate var vl = function
    [] -> []
  | (pos,neg)::rest ->
      match vl with
	true ->
	  if List.mem var pos
	  then evaluate var vl rest
	  else (pos,Common.minus_set neg [var]) :: evaluate var vl rest
      |	false ->
	  if List.mem var neg
	  then evaluate var vl rest
	  else (Common.minus_set pos [var],neg) :: evaluate var vl rest

(* ----------------------------------------------------------------------- *)
(* Unit propagation *)

let unit_propagation formula =
  let rec loop changed prev = function
      [] -> (changed,prev)
    | ([x],[])::rest ->
	loop true (evaluate x true prev) (evaluate x true rest)
    | ([],[x])::rest ->
	loop true (evaluate x false prev) (evaluate x false rest)
    | cl::rest -> loop changed (cl::prev) rest in
  let rec oloop formula =
    let (changed,formula) = loop false [] formula in
    if changed
    then oloop formula
    else formula in
  oloop formula

(* ----------------------------------------------------------------------- *)
(* Pure literal elimination *)

let pure_literals formula =
  let rec loop pos neg = function
      [] -> (pos,neg)
    | (cpos,cneg)::rest ->
	let pos = Common.minus_set pos cneg in
	let neg = Common.minus_set neg cpos in
	let cpos = Common.minus_set cpos neg in
	let cneg = Common.minus_set cneg pos in
	let pos = Common.union_set pos cpos in
	let neg = Common.union_set neg cneg in
	loop pos neg rest in
  let (pos,neg) = loop [] [] formula in
  let formula =
    List.fold_left (fun formula pos -> evaluate pos true formula)
      formula pos in
  let formula =
    List.fold_left (fun formula neg -> evaluate neg false formula)
      formula neg in
  formula

(* ----------------------------------------------------------------------- *)
(* Main loop *)

let rec dpll formula =
  let formula = unit_propagation formula in
  let formula = pure_literals formula in
  match formula with
    [] -> true
  | ((pos,neg) :: _) as formula ->
      if List.mem ([],[]) formula
      then false
      else
	match pos@neg with
	  x::_ ->
	    (dpll (evaluate x true formula)) ||
	    (dpll (evaluate x false formula))
	| _ -> failwith "at least one of pos and neg must be nonempty"