SAT-Kodierung: Hamiltonkreis

• Def: Graph G = (V, E) mit V = {v₁,…, v_n},

  Permutation π : {1,…, n}→{1,…, n} bestimmt Hamiltonkreis, wenn und v_π(1)v_π(2)∈E,…, v_π(n-1)v_π(n)∈E, v_π(n)v_π(1)∈E.

• SAT-Kodierung: benutzt Variablen p(i, j)↔π(i) = j.

  Welche Constraints sind dafür nötig?

• Anwendung: Rösselsprung auf Schachbrett