Def: Graph G = (V, E) mit V = {v1,..., vn},
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