Trouvez le cycle de Hamilton dans un graphique dirigé réduit au problème SAT

Question

J'ai besoin de trouver un Cycle hamiltonien Dans un graphique dirigé à l'aide de la logique propositionnelle, et pour le résoudre par SAT Solver. Donc, après avoir trouvé de solution de travail, j'ai trouvé un article qui décrit comment construire une formule CNF pour trouver un Chemin hamiltonien:

Xi,j - Le nœud J est en position I dans le chemin

Liste des contraintes:

1. Chaque nœud J doit apparaître dans le cheminx1j ∨ x2j ∨ · · · ∨ xnj - pour chaque nœud j
2. Aucun nœud j n'apparaît deux fois dans le chemin ¬xij ∨ ¬xkj Pour tous i, j, k avec i 6 = k.
3. Chaque position sur le chemin doit être occupée - xi1 ∨ xi2 ∨ · · · ∨ xin pour chaque je
4. Pas deux nœuds J et K occupent la même position dans le chemin - ¬xij ∨ ¬xik pour tout i, j, k avec j! = k
5. Les nœuds non adjacents I et J ne peuvent pas être adjacents dans le chemin - ¬xki ∨ ¬xk+1,j pour tous (i, j)! ∈ E et k = 1, 2 ,. . . , n - 1.

Ma question est, comment puis-je trouver Cycle hamiltonien en utilisant ces contraintes? Je comprends que je dois vérifier s'il y a un cycle (v1==vn), c'est une chose (mais j'ai obtenu la contrainte 2). Deuxièmement, c'est un graphique dirigé et je ne sais pas comment puis-je m'assurer que les sommets seraient dans le bon ordre des bords, j'y ai pensé: ceci:

Tous les deux nœuds doivent avoir des bords - Xki ^ Xk+1j pour chaque (i, j) ∈ E et k = 1, 2 ,. . . , n - 1.

Mais cela ne semble pas fonctionner, toute aide serait appréciée.

ÉDITER

Ce que j'ai fait, c'est d'ajouter une autre contrainte -

6. Pas de bords de l'ensemble: (i, j)! ∈ E qui sont les derniers et le premier