1(* Title: HOL/Tools/Function/scnp_solve.ML 2 Author: Armin Heller, TU Muenchen 3 Author: Alexander Krauss, TU Muenchen 4 5Certificate generation for SCNP using a SAT solver. 6*) 7 8 9signature SCNP_SOLVE = 10sig 11 12 datatype edge = GTR | GEQ 13 datatype graph = G of int * int * (int * edge * int) list 14 datatype graph_problem = GP of int list * graph list 15 16 datatype label = MIN | MAX | MS 17 18 type certificate = 19 label (* which order *) 20 * (int * int) list list (* (multi)sets *) 21 * int list (* strictly ordered calls *) 22 * (int -> bool -> int -> (int * int) option) (* covering function *) 23 24 val generate_certificate : bool -> label list -> graph_problem -> certificate option 25 26 val solver : string Unsynchronized.ref 27end 28 29structure ScnpSolve : SCNP_SOLVE = 30struct 31 32(** Graph problems **) 33 34datatype edge = GTR | GEQ ; 35datatype graph = G of int * int * (int * edge * int) list ; 36datatype graph_problem = GP of int list * graph list ; 37 38datatype label = MIN | MAX | MS ; 39type certificate = 40 label 41 * (int * int) list list 42 * int list 43 * (int -> bool -> int -> (int * int) option) 44 45fun graph_at (GP (_, gs), i) = nth gs i ; 46fun num_prog_pts (GP (arities, _)) = length arities ; 47fun num_graphs (GP (_, gs)) = length gs ; 48fun arity (GP (arities, gl)) i = nth arities i ; 49fun ndigits (GP (arities, _)) = IntInf.log2 (Integer.sum arities) + 1 50 51 52(** Propositional formulas **) 53 54val Not = Prop_Logic.Not and And = Prop_Logic.And and Or = Prop_Logic.Or 55val BoolVar = Prop_Logic.BoolVar 56fun Implies (p, q) = Or (Not p, q) 57fun Equiv (p, q) = And (Implies (p, q), Implies (q, p)) 58val all = Prop_Logic.all 59 60(* finite indexed quantifiers: 61 62iforall n f <==> /\ 63 / \ f i 64 0<=i<n 65 *) 66fun iforall n f = all (map_range f n) 67fun iexists n f = Prop_Logic.exists (map_range f n) 68fun iforall2 n m f = all (map_product f (0 upto n - 1) (0 upto m - 1)) 69 70fun the_one var n x = all (var x :: map (Not o var) (remove (op =) x (0 upto n - 1))) 71fun exactly_one n f = iexists n (the_one f n) 72 73(* SAT solving *) 74val solver = Unsynchronized.ref "auto"; 75fun sat_solver x = 76 Function_Common.PROFILE "sat_solving..." (SAT_Solver.invoke_solver (!solver)) x 77 78(* "Virtual constructors" for various propositional variables *) 79fun var_constrs (gp as GP (arities, _)) = 80 let 81 val n = Int.max (num_graphs gp, num_prog_pts gp) 82 val k = fold Integer.max arities 1 83 84 (* Injective, provided a < 8, x < n, and i < k. *) 85 fun prod a x i j = ((j * k + i) * n + x) * 8 + a + 1 86 87 fun ES (g, i, j) = BoolVar (prod 0 g i j) 88 fun EW (g, i, j) = BoolVar (prod 1 g i j) 89 fun WEAK g = BoolVar (prod 2 g 0 0) 90 fun STRICT g = BoolVar (prod 3 g 0 0) 91 fun P (p, i) = BoolVar (prod 4 p i 0) 92 fun GAM (g, i, j)= BoolVar (prod 5 g i j) 93 fun EPS (g, i) = BoolVar (prod 6 g i 0) 94 fun TAG (p, i) b = BoolVar (prod 7 p i b) 95 in 96 (ES,EW,WEAK,STRICT,P,GAM,EPS,TAG) 97 end 98 99 100fun graph_info gp g = 101 let 102 val G (p, q, edgs) = graph_at (gp, g) 103 in 104 (g, p, q, arity gp p, arity gp q, edgs) 105 end 106 107 108(* Order-independent part of encoding *) 109 110fun encode_graphs bits gp = 111 let 112 val ng = num_graphs gp 113 val (ES,EW,_,_,_,_,_,TAG) = var_constrs gp 114 115 fun encode_constraint_strict 0 (x, y) = Prop_Logic.False 116 | encode_constraint_strict k (x, y) = 117 Or (And (TAG x (k - 1), Not (TAG y (k - 1))), 118 And (Equiv (TAG x (k - 1), TAG y (k - 1)), 119 encode_constraint_strict (k - 1) (x, y))) 120 121 fun encode_constraint_weak k (x, y) = 122 Or (encode_constraint_strict k (x, y), 123 iforall k (fn i => Equiv (TAG x i, TAG y i))) 124 125 fun encode_graph (g, p, q, n, m, edges) = 126 let 127 fun encode_edge i j = 128 if exists (fn x => x = (i, GTR, j)) edges then 129 And (ES (g, i, j), EW (g, i, j)) 130 else if not (exists (fn x => x = (i, GEQ, j)) edges) then 131 And (Not (ES (g, i, j)), Not (EW (g, i, j))) 132 else 133 And ( 134 Equiv (ES (g, i, j), 135 encode_constraint_strict bits ((p, i), (q, j))), 136 Equiv (EW (g, i, j), 137 encode_constraint_weak bits ((p, i), (q, j)))) 138 in 139 iforall2 n m encode_edge 140 end 141 in 142 iforall ng (encode_graph o graph_info gp) 143 end 144 145 146(* Order-specific part of encoding *) 147 148fun encode bits gp mu = 149 let 150 val ng = num_graphs gp 151 val (ES,EW,WEAK,STRICT,P,GAM,EPS,_) = var_constrs gp 152 153 fun encode_graph MAX (g, p, q, n, m, _) = 154 And ( 155 Equiv (WEAK g, 156 iforall m (fn j => 157 Implies (P (q, j), 158 iexists n (fn i => 159 And (P (p, i), EW (g, i, j)))))), 160 Equiv (STRICT g, 161 And ( 162 iforall m (fn j => 163 Implies (P (q, j), 164 iexists n (fn i => 165 And (P (p, i), ES (g, i, j))))), 166 iexists n (fn i => P (p, i))))) 167 | encode_graph MIN (g, p, q, n, m, _) = 168 And ( 169 Equiv (WEAK g, 170 iforall n (fn i => 171 Implies (P (p, i), 172 iexists m (fn j => 173 And (P (q, j), EW (g, i, j)))))), 174 Equiv (STRICT g, 175 And ( 176 iforall n (fn i => 177 Implies (P (p, i), 178 iexists m (fn j => 179 And (P (q, j), ES (g, i, j))))), 180 iexists m (fn j => P (q, j))))) 181 | encode_graph MS (g, p, q, n, m, _) = 182 all [ 183 Equiv (WEAK g, 184 iforall m (fn j => 185 Implies (P (q, j), 186 iexists n (fn i => GAM (g, i, j))))), 187 Equiv (STRICT g, 188 iexists n (fn i => 189 And (P (p, i), Not (EPS (g, i))))), 190 iforall2 n m (fn i => fn j => 191 Implies (GAM (g, i, j), 192 all [ 193 P (p, i), 194 P (q, j), 195 EW (g, i, j), 196 Equiv (Not (EPS (g, i)), ES (g, i, j))])), 197 iforall n (fn i => 198 Implies (And (P (p, i), EPS (g, i)), 199 exactly_one m (fn j => GAM (g, i, j)))) 200 ] 201 in 202 all [ 203 encode_graphs bits gp, 204 iforall ng (encode_graph mu o graph_info gp), 205 iforall ng (fn x => WEAK x), 206 iexists ng (fn x => STRICT x) 207 ] 208 end 209 210 211(*Generieren des level-mapping und diverser output*) 212fun mk_certificate bits label gp f = 213 let 214 val (ES,EW,WEAK,STRICT,P,GAM,EPS,TAG) = var_constrs gp 215 fun assign (Prop_Logic.BoolVar v) = the_default false (f v) 216 fun assignTag i j = 217 (fold (fn x => fn y => 2 * y + (if assign (TAG (i, j) x) then 1 else 0)) 218 (bits - 1 downto 0) 0) 219 220 val level_mapping = 221 let fun prog_pt_mapping p = 222 map_filter (fn x => if assign (P(p, x)) then SOME (x, assignTag p x) else NONE) 223 (0 upto (arity gp p) - 1) 224 in map_range prog_pt_mapping (num_prog_pts gp) end 225 226 val strict_list = filter (assign o STRICT) (0 upto num_graphs gp - 1) 227 228 fun covering_pair g bStrict j = 229 let 230 val (_, p, q, n, m, _) = graph_info gp g 231 232 fun cover MAX j = find_index (fn i => assign (P (p, i)) andalso assign (EW (g, i, j))) (0 upto n - 1) 233 | cover MS k = find_index (fn i => assign (GAM (g, i, k))) (0 upto n - 1) 234 | cover MIN i = find_index (fn j => assign (P (q, j)) andalso assign (EW (g, i, j))) (0 upto m - 1) 235 fun cover_strict MAX j = find_index (fn i => assign (P (p, i)) andalso assign (ES (g, i, j))) (0 upto n - 1) 236 | cover_strict MS k = find_index (fn i => assign (GAM (g, i, k)) andalso not (assign (EPS (g, i) ))) (0 upto n - 1) 237 | cover_strict MIN i = find_index (fn j => assign (P (q, j)) andalso assign (ES (g, i, j))) (0 upto m - 1) 238 val i = if bStrict then cover_strict label j else cover label j 239 in 240 find_first (fn x => fst x = i) (nth level_mapping (if label = MIN then q else p)) 241 end 242 in 243 (label, level_mapping, strict_list, covering_pair) 244 end 245 246(*interface for the proof reconstruction*) 247fun generate_certificate use_tags labels gp = 248 let 249 val bits = if use_tags then ndigits gp else 0 250 in 251 get_first 252 (fn l => case sat_solver (encode bits gp l) of 253 SAT_Solver.SATISFIABLE f => SOME (mk_certificate bits l gp f) 254 | _ => NONE) 255 labels 256 end 257end 258