(* Title: HOL/Tools/function_package/scnp_solve.ML
Author: Armin Heller, TU Muenchen
Author: Alexander Krauss, TU Muenchen
Generate certificates for SCNP using a SAT solver
*)
signature SCNP_SOLVE =
sig
datatype edge = GTR | GEQ
datatype graph = G of int * int * (int * edge * int) list
datatype graph_problem = GP of int list * graph list
datatype label = MIN | MAX | MS
type certificate =
label (* which order *)
* (int * int) list list (* (multi)sets *)
* int list (* strictly ordered calls *)
* (int -> bool -> int -> (int * int) option) (* covering function *)
val generate_certificate : bool -> label list -> graph_problem -> certificate option
val solver : string ref
end
structure ScnpSolve : SCNP_SOLVE =
struct
(** Graph problems **)
datatype edge = GTR | GEQ ;
datatype graph = G of int * int * (int * edge * int) list ;
datatype graph_problem = GP of int list * graph list ;
datatype label = MIN | MAX | MS ;
type certificate =
label
* (int * int) list list
* int list
* (int -> bool -> int -> (int * int) option)
fun graph_at (GP (_, gs), i) = nth gs i ;
fun num_prog_pts (GP (arities, _)) = length arities ;
fun num_graphs (GP (_, gs)) = length gs ;
fun arity (GP (arities, gl)) i = nth arities i ;
fun ndigits (GP (arities, _)) = IntInf.log2 (List.foldl (op +) 0 arities) + 1
(** Propositional formulas **)
val Not = PropLogic.Not and And = PropLogic.And and Or = PropLogic.Or
val BoolVar = PropLogic.BoolVar
fun Implies (p, q) = Or (Not p, q)
fun Equiv (p, q) = And (Implies (p, q), Implies (q, p))
val all = PropLogic.all
(* finite indexed quantifiers:
iforall n f <==> /\
/ \ f i
0<=i<n
*)
fun iforall n f = all (map f (0 upto n - 1))
fun iexists n f = PropLogic.exists (map f (0 upto n - 1))
fun iforall2 n m f = all (map_product f (0 upto n - 1) (0 upto m - 1))
fun the_one var n x = all (var x :: map (Not o var) ((0 upto n - 1) \\ [x]))
fun exactly_one n f = iexists n (the_one f n)
(* SAT solving *)
val solver = ref "auto";
fun sat_solver x =
FundefCommon.PROFILE "sat_solving..." (SatSolver.invoke_solver (!solver)) x
(* "Virtual constructors" for various propositional variables *)
fun var_constrs (gp as GP (arities, gl)) =
let
val n = Int.max (num_graphs gp, num_prog_pts gp)
val k = List.foldl Int.max 1 arities
(* Injective, provided a < 8, x < n, and i < k. *)
fun prod a x i j = ((j * k + i) * n + x) * 8 + a + 1
fun ES (g, i, j) = BoolVar (prod 0 g i j)
fun EW (g, i, j) = BoolVar (prod 1 g i j)
fun WEAK g = BoolVar (prod 2 g 0 0)
fun STRICT g = BoolVar (prod 3 g 0 0)
fun P (p, i) = BoolVar (prod 4 p i 0)
fun GAM (g, i, j)= BoolVar (prod 5 g i j)
fun EPS (g, i) = BoolVar (prod 6 g i 0)
fun TAG (p, i) b = BoolVar (prod 7 p i b)
in
(ES,EW,WEAK,STRICT,P,GAM,EPS,TAG)
end
fun graph_info gp g =
let
val G (p, q, edgs) = graph_at (gp, g)
in
(g, p, q, arity gp p, arity gp q, edgs)
end
(* Order-independent part of encoding *)
fun encode_graphs bits gp =
let
val ng = num_graphs gp
val (ES,EW,_,_,_,_,_,TAG) = var_constrs gp
fun encode_constraint_strict 0 (x, y) = PropLogic.False
| encode_constraint_strict k (x, y) =
Or (And (TAG x (k - 1), Not (TAG y (k - 1))),
And (Equiv (TAG x (k - 1), TAG y (k - 1)),
encode_constraint_strict (k - 1) (x, y)))
fun encode_constraint_weak k (x, y) =
Or (encode_constraint_strict k (x, y),
iforall k (fn i => Equiv (TAG x i, TAG y i)))
fun encode_graph (g, p, q, n, m, edges) =
let
fun encode_edge i j =
if exists (fn x => x = (i, GTR, j)) edges then
And (ES (g, i, j), EW (g, i, j))
else if not (exists (fn x => x = (i, GEQ, j)) edges) then
And (Not (ES (g, i, j)), Not (EW (g, i, j)))
else
And (
Equiv (ES (g, i, j),
encode_constraint_strict bits ((p, i), (q, j))),
Equiv (EW (g, i, j),
encode_constraint_weak bits ((p, i), (q, j))))
in
iforall2 n m encode_edge
end
in
iforall ng (encode_graph o graph_info gp)
end
(* Order-specific part of encoding *)
fun encode bits gp mu =
let
val ng = num_graphs gp
val (ES,EW,WEAK,STRICT,P,GAM,EPS,_) = var_constrs gp
fun encode_graph MAX (g, p, q, n, m, _) =
And (
Equiv (WEAK g,
iforall m (fn j =>
Implies (P (q, j),
iexists n (fn i =>
And (P (p, i), EW (g, i, j)))))),
Equiv (STRICT g,
And (
iforall m (fn j =>
Implies (P (q, j),
iexists n (fn i =>
And (P (p, i), ES (g, i, j))))),
iexists n (fn i => P (p, i)))))
| encode_graph MIN (g, p, q, n, m, _) =
And (
Equiv (WEAK g,
iforall n (fn i =>
Implies (P (p, i),
iexists m (fn j =>
And (P (q, j), EW (g, i, j)))))),
Equiv (STRICT g,
And (
iforall n (fn i =>
Implies (P (p, i),
iexists m (fn j =>
And (P (q, j), ES (g, i, j))))),
iexists m (fn j => P (q, j)))))
| encode_graph MS (g, p, q, n, m, _) =
all [
Equiv (WEAK g,
iforall m (fn j =>
Implies (P (q, j),
iexists n (fn i => GAM (g, i, j))))),
Equiv (STRICT g,
iexists n (fn i =>
And (P (p, i), Not (EPS (g, i))))),
iforall2 n m (fn i => fn j =>
Implies (GAM (g, i, j),
all [
P (p, i),
P (q, j),
EW (g, i, j),
Equiv (Not (EPS (g, i)), ES (g, i, j))])),
iforall n (fn i =>
Implies (And (P (p, i), EPS (g, i)),
exactly_one m (fn j => GAM (g, i, j))))
]
in
all [
encode_graphs bits gp,
iforall ng (encode_graph mu o graph_info gp),
iforall ng (fn x => WEAK x),
iexists ng (fn x => STRICT x)
]
end
(*Generieren des level-mapping und diverser output*)
fun mk_certificate bits label gp f =
let
val (ES,EW,WEAK,STRICT,P,GAM,EPS,TAG) = var_constrs gp
fun assign (PropLogic.BoolVar v) = the_default false (f v)
fun assignTag i j =
(fold (fn x => fn y => 2 * y + (if assign (TAG (i, j) x) then 1 else 0))
(bits - 1 downto 0) 0)
val level_mapping =
let fun prog_pt_mapping p =
map_filter (fn x => if assign (P(p, x)) then SOME (x, assignTag p x) else NONE)
(0 upto (arity gp p) - 1)
in map prog_pt_mapping (0 upto num_prog_pts gp - 1) end
val strict_list = filter (assign o STRICT) (0 upto num_graphs gp - 1)
fun covering_pair g bStrict j =
let
val (_, p, q, n, m, _) = graph_info gp g
fun cover MAX j = find_index (fn i => assign (P (p, i)) andalso assign (EW (g, i, j))) (0 upto n - 1)
| cover MS k = find_index (fn i => assign (GAM (g, i, k))) (0 upto n - 1)
| cover MIN i = find_index (fn j => assign (P (q, j)) andalso assign (EW (g, i, j))) (0 upto m - 1)
fun cover_strict MAX j = find_index (fn i => assign (P (p, i)) andalso assign (ES (g, i, j))) (0 upto n - 1)
| cover_strict MS k = find_index (fn i => assign (GAM (g, i, k)) andalso not (assign (EPS (g, i) ))) (0 upto n - 1)
| cover_strict MIN i = find_index (fn j => assign (P (q, j)) andalso assign (ES (g, i, j))) (0 upto m - 1)
val i = if bStrict then cover_strict label j else cover label j
in
find_first (fn x => fst x = i) (nth level_mapping (if label = MIN then q else p))
end
in
(label, level_mapping, strict_list, covering_pair)
end
(*interface for the proof reconstruction*)
fun generate_certificate use_tags labels gp =
let
val bits = if use_tags then ndigits gp else 0
in
get_first
(fn l => case sat_solver (encode bits gp l) of
SatSolver.SATISFIABLE f => SOME (mk_certificate bits l gp f)
| _ => NONE)
labels
end
end