I need to find a Hamiltonian cycle in a directed graph using propositional logic, and to solve it by sat solver. So after I couldn't find a working solution, I found a paper that describes how to construct a CNF formula to find an Hamiltonian path:
Xi,j - node j is in position i in the path
List of constraints:
- Each node j must appear in the path
x1j ∨ x2j ∨ · · · ∨ xnj- for every node j
- No node j appears twice in the path
¬xij ∨ ¬xkjfor all i, j, k with i 6= k.
- Every position i on the path must be occupied -
xi1 ∨ xi2 ∨ · · · ∨ xinfor each i
- No two nodes j and k occupy the same position in the path -
¬xij ∨ ¬xikfor all i, j, k with j != k
- Nonadjacent nodes i and j cannot be adjacent in the path -
¬xki ∨ ¬xk+1,jfor all (i, j) !∈ E and k = 1, 2, . . . , n − 1.
My question is, how can I find Hamiltonian cycle using these constraints? I understand that I need to check if there's a cycle (
v1==vn), that's one thing (But I got constraint 2). Second, it's a directed graph and I don't know how can I assure that the vertices would be in the right order of the edges, I thought about this:
Every two nodes must have edges -
Xki ^ Xk+1j for each (i,j)∈ E and k = 1, 2, . . . , n − 1.
But it doesn't seem to work, any help would be appreciated.
What I did was to add another constraint -
- No edges from the set: (i,j)!∈ E that are the last and the first