SAT-Kodierung: Hamiltonkreis

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

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

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

  Welche Constraints sind dafür nötig?

• Anwendung: Rösselsprung auf Schachbrett