3
$\begingroup$

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:

  1. Each node j must appear in the path x1j ∨ x2j ∨ · · · ∨ xnj - for every node j
  2. No node j appears twice in the path ¬xij ∨ ¬xkj for all i, j, k with i 6= k.
  3. Every position i on the path must be occupied - xi1 ∨ xi2 ∨ · · · ∨ xin for each i
  4. No two nodes j and k occupy the same position in the path - ¬xij ∨ ¬xik for all i, j, k with j != k
  5. Nonadjacent nodes i and j cannot be adjacent in the path - ¬xki ∨ ¬xk+1,j for 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.

EDIT

What I did was to add another constraint -

  1. No edges from the set: (i,j)!∈ E that are the last and the first
$\endgroup$
2
$\begingroup$

Just add the constraint that $x_{1j}=x_{nj}$ for all $j$, and make a special exception to constraint 2 so that you omit constraint 2 in the case where $i=1$ and $k=n$.

Everything works fine for a directed graph. You just need to interpret constraint 5 appropriately.

$\endgroup$
2
$\begingroup$

I suppose practical SAT solvers might search for and remove them, but I'd still suggest not giving it redundant variables - if you do know v1==vn, then just replace each instance of vn with v1.
If n is the number of vertices then you'd actually have v0 == vn, rather than v1==vn.

You can remove any one of {1.,2.,3.,4.}, since the combination {3.,4.} or {1.,2.}
will force X or its transpose respectively to be the graph of a function, and
for functions from a finite set to itself, surjectivity is equivalent to injectivity.

$\endgroup$
  • $\begingroup$ Regarding your first sentence: I'd expect it won't make any difference, given how unit propagation works in modern SAT solvers -- but there's no harm in doing what you suggest. $\endgroup$ – D.W. Nov 18 '15 at 2:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.