SAT-Kodierung: Hamiltonkreis

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

Permutation $\pi$ : {1,..., n}$\to${1,..., n} bestimmt Hamiltonkreis, wenn und v_$\pi$(1)v_$\pi$(2) $\in$ E,..., v_$\pi$(n-1)v_$\pi$(n) $\in$ E, v_$\pi$(n)v_$\pi$(1) $\in$ E.

SAT-Kodierung: benutzt Variablen p(i, j) $\leftrightarrow$ $\pi$(i) = j.

Welche Constraints sind dafür nötig?

Anwendung: Rösselsprung