Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / SS 2015 / Formale Spezifikation und Verifikation / Uebungen / Lösung für Aufgabe 2-2 (OCaml)


Inhaltsbereich

Lösung für Aufgabe 2-2 (OCaml)

OCaml source code icon aufgabe2_2.ml — OCaml source code, 2 KB (2436 bytes)

Dateiinhalt

open Cnf

(* Erzeuge zufaelligen Graphen. *)

let size = 50
let graph = Graph.makeWithHamiltonCircle size


(* Hilfsfunktionen zum Erzeugen der Formeln *)

let times = fordo 0 size [] (fun t ts -> t :: ts)
let forall_times f =
  dands (List.map f times)

let nodes = Graph.nodes graph
let forall_nodes f =
  dands (List.map f nodes)
let exists_node f =
  dors (List.map f nodes)

(* Kodierung des Hamiltonkreis-Problems in Aussagenlogik *)

(* Erzeuge aussagenlogische Variablen. *)
let vars = Hashtbl.create (size * size)
let _ =
  List.iter (fun t ->
    List.iter (fun z ->
      Hashtbl.add vars (z, t) (newvar())
    ) nodes
  ) times

(* Die Variable q z t sagt, dass z der t-te Zustand im Pfad ist. *)
let q z t =
  var (Hashtbl.find vars (z, t))

(* Zu jedem Zeitpunkt besucht der Pfad mindestens einen Zustand. *)
let always_at_least_one =
  forall_times (fun t ->
    exists_node (fun z -> q z t))

let always_at_most_one =
  forall_times (fun t ->
    forall_nodes (fun z ->
      forall_nodes (fun z' ->
        if z = z' then dtrue
        else neg (dand (q z t) (q z' t)))))

(* Jeder Zustand kommt im gesamten Pfad hoechstens einmal vor. *)
let at_most_once =
  forall_nodes (fun z ->
    forall_times (fun t1 ->
      forall_times (fun t2 ->
        if t1 < t2 then
          neg (dand (q z t1) (q z t2))
        else
          dtrue)))

(* Es gibt eine Kante zwischen Zustaenden am Zeitpunkt t und am
   Zeitpunkt (t+1) mod size, fuer alle t. *)
let transition =
  forall_times (fun t ->
    exists_node (fun z ->
      exists_node (fun z' ->
        if (Graph.edge graph z z') then
          dand (q z t) (q z' ((t + 1) mod size))
        else
          dfalse)))

let main =
  Printf.printf "Eingabegraph:\n";
  Graph.print graph stdout;

  Printf.printf "\nGeneriere KNF...\n%!";
  mk_dimacs "aufgabe2_2.cnf"
    [always_at_least_one; always_at_most_one; at_most_once; transition] "";

  Printf.printf "\nSolving...\n%!";
  ignore (Sys.command "minisat aufgabe2_2.cnf aufgabe2_2.result");

  Printf.printf "\n%!";
  match parse_zchaff "aufgabe2_2.result" with
  | None ->
    print_string "Der Graph hat keinen Hamiltonkreis.\n"
  | Some l ->
    print_string "Ein Hamiltonkreis ist:\n";
    for t = 0 to size-1 do
      List.iter (fun z ->
        if List.mem (Hashtbl.find vars (z, t)) l then
          Printf.printf "%i -> " z
      ) (Graph.nodes graph)
    done;
    Printf.printf "(zurueck zum Startknoten)\n"

Artikelaktionen


Funktionsleiste