From: acondolu <andrea.condoluci@unibo.it>
Date: Sun, 16 Jul 2017 17:36:19 +0000 (+0200)
Subject: Extracting solutions of 3-coloring problems
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b50b673e2ed5a8c21074cc5bdc55bb4989d45b0f;p=fireball-separation.git

Extracting solutions of 3-coloring problems

Added sample unsat problems found on the internet
---

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 3426b5a..b15c360 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -773,14 +773,13 @@ let solve (p, todo) =
    | `CompleteUnseparable s -> `Complete, `False s
    | `CompleteSeparable _ -> `Complete, `True
    | `Uncomplete -> `Uncomplete, `True in
-  match to_run with
-   | `False s -> completeness, `Unseparable s
-   | `True ->
-       try
-        let sigma = run p in
-        completeness, `Separable sigma
-       with
-       | Backtrack _ -> completeness, `Unseparable "backtrack"
+ completeness, match to_run with
+  | `False s -> `Unseparable s
+  | `True ->
+      try
+       `Separable (run p)
+      with
+       Backtrack _ -> `Unseparable "backtrack"
 ;;
 
 let check p =
diff --git a/ocaml/sat.ml b/ocaml/sat.ml
index ceb90ca..01d7398 100644
--- a/ocaml/sat.ml
+++ b/ocaml/sat.ml
@@ -3,6 +3,8 @@
  of lambda-terms. Commented out the encoding from SAT.
 *)
 
+open Util;;
+
 (* type cnf = int list list;;
 
 let (++) f g x = f (g x);;
@@ -13,6 +15,7 @@ let maxvar : cnf -> int =
 ;; *)
 
 type graph = (int * int) list;;
+type color = int;;
 
 let arc x y = min x y, max x y;;
 let mem g x y = List.mem (arc x y) g;;
@@ -119,6 +122,8 @@ let encode_graph g =
  )
 ;;
 
+print_endline "Three example encodings:";;
+
 (* easy one *)
 prerr_endline (encode_graph [0,1;]);;
 
@@ -129,3 +134,402 @@ prerr_endline (
 prerr_endline (
  encode_graph [0,1; 0,2; 1,2; 0,3; 1,3; 2,3]
 );;
+
+(******************************************************************************)
+
+print_endline "\nIt will now run some problems and decode the solutions";;
+print_endline "Press ENTER to continue.";;
+let _ = read_line ();;
+
+let strip_lambda_matches =
+ let getvar = function
+  | `Var(n,_) -> n
+  | _ -> assert false in
+ let rec aux n = function
+  | `Lam(_,t) -> aux (n+1) t
+  | `Match(_,_,_,bs,_) -> Some (n, List.map (getvar ++ snd) !bs)
+  | _ -> None
+ in aux 0
+;;
+
+let next_candidates sigma cands =
+ let sigma = Util.filter_map
+  (fun x -> try Some (List.assoc x sigma) with Not_found -> None) cands in
+ match Util.find_opt strip_lambda_matches sigma with
+ | None -> -1, []
+ | Some x -> x
+;;
+
+let fix_numbers l =
+ let rec aux n = function
+ | [] -> []
+ | x::xs -> (x - 2*n - 1) :: (aux (n+1) xs)
+ in aux 0 l
+;;
+
+let color (g:graph) =
+ let p = encode_graph g in
+ let (_, _, _, _, vars as p) = Parser.problem_of_string p in
+ let _, result = Lambda4.solve (Lambda4.problem_of p) in
+ match result with
+ | `Unseparable _ -> prerr_endline "Graph not colorable"; None
+ | `Separable sigma -> (
+  (* start from variable x *)
+  let x = Util.index_of "x" vars in
+  (* List.iter (fun x -> prerr_endline (string_of_int (fst x) ^ ":" ^ Num.print ~l:vars (snd x))) sigma; *)
+  let rec iter f x =
+   let n, x = f x in if x = [] then [] else n :: iter f x in
+  let numbers = iter (next_candidates sigma) [x] in
+  let numbers = fix_numbers numbers in
+  (* display solution *)
+  let colors = ["r"; "g"; "b"] in
+  prerr_endline ("\nSolution found:\n " ^ String.concat "\n "
+   (List.mapi (fun i x ->
+     string_of_int i ^ " := " ^ List.nth colors x) numbers));
+  assert (List.for_all (fun (a,b) -> List.nth numbers a <> List.nth numbers b) g);
+  Some numbers)
+;;
+
+let bruteforce g =
+ let nodes_no = 1+
+  List.fold_left (fun acc (a,b) -> Pervasives.max acc (Pervasives.max a b)) 0 g in
+ let check x = if List.for_all (fun (a,b) -> List.nth x a <> List.nth x b) g
+  then failwith "bruteforce: sat" in
+ let rec guess l = prerr_string "+";
+  if List.length l = nodes_no
+   then check l
+    else (guess (0::l); guess (1::l); guess (2::l)) in
+ guess [];
+ prerr_endline "bruteforce: unsat"
+;;
+
+assert (color [0,1;0,2;1,2;2,3;3,0] <> None);;
+assert (color [0,1;0,2;1,2;2,3;3,0;0,4;4,2] <> None);;
+
+(* assert (color [
+ 1,2; 1,4; 1,7; 1,9; 2,3; 2,6; 2,8; 3,5;
+ 3,7; 3,0; 4,5; 4,6; 4,0; 5,8; 5,9; 6,11;
+ 7,11; 8,11; 9,11; 0,11;
+] = None);; *)
+
+(* https://turing.cs.hbg.psu.edu/txn131/file_instances/coloring/graph_color/queen5_5.col *)
+color [1,7
+; 1,13
+; 1,19
+; 1,25
+; 1,2
+; 1,3
+; 1,4
+; 1,5
+; 1,6
+; 1,11
+; 1,16
+; 1,21
+; 2,8
+; 2,14
+; 2,20
+; 2,6
+; 2,3
+; 2,4
+; 2,5
+; 2,7
+; 2,12
+; 2,17
+; 2,22
+; 2,1
+; 3,9
+; 3,15
+; 3,7
+; 3,11
+; 3,4
+; 3,5
+; 3,8
+; 3,13
+; 3,18
+; 3,23
+; 3,2
+; 3,1
+; 4,10
+; 4,8
+; 4,12
+; 4,16
+; 4,5
+; 4,9
+; 4,14
+; 4,19
+; 4,24
+; 4,3
+; 4,2
+; 4,1
+; 5,9
+; 5,13
+; 5,17
+; 5,21
+; 5,10
+; 5,15
+; 5,20
+; 5,25
+; 5,4
+; 5,3
+; 5,2
+; 5,1
+; 6,12
+; 6,18
+; 6,24
+; 6,7
+; 6,8
+; 6,9
+; 6,10
+; 6,11
+; 6,16
+; 6,21
+; 6,2
+; 6,1
+; 7,13
+; 7,19
+; 7,25
+; 7,11
+; 7,8
+; 7,9
+; 7,10
+; 7,12
+; 7,17
+; 7,22
+; 7,6
+; 7,3
+; 7,2
+; 7,1
+; 8,14
+; 8,20
+; 8,12
+; 8,16
+; 8,9
+; 8,10
+; 8,13
+; 8,18
+; 8,23
+; 8,7
+; 8,6
+; 8,4
+; 8,3
+; 8,2
+; 9,15
+; 9,13
+; 9,17
+; 9,21
+; 9,10
+; 9,14
+; 9,19
+; 9,24
+; 9,8
+; 9,7
+; 9,6
+; 9,5
+; 9,4
+; 9,3
+; 10,14
+; 10,18
+; 10,22
+; 10,15
+; 10,20
+; 10,25
+; 10,9
+; 10,8
+; 10,7
+; 10,6
+; 10,5
+; 10,4
+; 11,17
+; 11,23
+; 11,12
+; 11,13
+; 11,14
+; 11,15
+; 11,16
+; 11,21
+; 11,7
+; 11,6
+; 11,3
+; 11,1
+; 12,18
+; 12,24
+; 12,16
+; 12,13
+; 12,14
+; 12,15
+; 12,17
+; 12,22
+; 12,11
+; 12,8
+; 12,7
+; 12,6
+; 12,4
+; 12,2
+; 13,19
+; 13,25
+; 13,17
+; 13,21
+; 13,14
+; 13,15
+; 13,18
+; 13,23
+; 13,12
+; 13,11
+; 13,9
+; 13,8
+; 13,7
+; 13,5
+; 13,3
+; 13,1
+; 14,20
+; 14,18
+; 14,22
+; 14,15
+; 14,19
+; 14,24
+; 14,13
+; 14,12
+; 14,11
+; 14,10
+; 14,9
+; 14,8
+; 14,4
+; 14,2
+; 15,19
+; 15,23
+; 15,20
+; 15,25
+; 15,14
+; 15,13
+; 15,12
+; 15,11
+; 15,10
+; 15,9
+; 15,5
+; 15,3
+; 16,22
+; 16,17
+; 16,18
+; 16,19
+; 16,20
+; 16,21
+; 16,12
+; 16,11
+; 16,8
+; 16,6
+; 16,4
+; 16,1
+; 17,23
+; 17,21
+; 17,18
+; 17,19
+; 17,20
+; 17,22
+; 17,16
+; 17,13
+; 17,12
+; 17,11
+; 17,9
+; 17,7
+; 17,5
+; 17,2
+; 18,24
+; 18,22
+; 18,19
+; 18,20
+; 18,23
+; 18,17
+; 18,16
+; 18,14
+; 18,13
+; 18,12
+; 18,10
+; 18,8
+; 18,6
+; 18,3
+; 19,25
+; 19,23
+; 19,20
+; 19,24
+; 19,18
+; 19,17
+; 19,16
+; 19,15
+; 19,14
+; 19,13
+; 19,9
+; 19,7
+; 19,4
+; 19,1
+; 20,24
+; 20,25
+; 20,19
+; 20,18
+; 20,17
+; 20,16
+; 20,15
+; 20,14
+; 20,10
+; 20,8
+; 20,5
+; 20,2
+; 21,22
+; 21,23
+; 21,24
+; 21,25
+; 21,17
+; 21,16
+; 21,13
+; 21,11
+; 21,9
+; 21,6
+; 21,5
+; 21,1
+; 22,23
+; 22,24
+; 22,25
+; 22,21
+; 22,18
+; 22,17
+; 22,16
+; 22,14
+; 22,12
+; 22,10
+; 22,7
+; 22,2
+; 23,24
+; 23,25
+; 23,22
+; 23,21
+; 23,19
+; 23,18
+; 23,17
+; 23,15
+; 23,13
+; 23,11
+; 23,8
+; 23,3
+; 24,25
+; 24,23
+; 24,22
+; 24,21
+; 24,20
+; 24,19
+; 24,18
+; 24,14
+; 24,12
+; 24,9
+; 24,6
+; 24,4
+; 25,24
+; 25,23
+; 25,22
+; 25,21
+; 25,20
+; 25,19
+; 25,15
+; 25,13
+; 25,10
+; 25,7
+; 25,5
+; 25,1];;
diff --git a/ocaml/sat.mli b/ocaml/sat.mli
index 77f0239..81d7ee7 100644
--- a/ocaml/sat.mli
+++ b/ocaml/sat.mli
@@ -1,3 +1,5 @@
 type graph = (int * int) list
+type color
 
 val encode_graph : graph -> string
+val color: graph -> (color list) option