How to solve Hamiltonian Path using SAT solver for Undirected Graph?

general
, , , , , ,
1

I was going through the concept of NP-Complete. A question arose in my mind, can we solve Hamiltonian Path problem using SAT solver by converting undirected graph(Adjacency Matrix form) to CNF(Conjunctive Normal Form) and using DIMACS format to get the answer by SAT Solver. I am stuck in how to covert the GRAPH into CNF form for Hamiltonian Path Problem.

Can anybody help me?

2 Likes
2

Have a look at this , it will should be helpful.

link text

Happy Coding …

3

Reduction of hamiltonian path to 3-sat.

Given a graph G, we shall construct a CNF F(G) such that F(G) is satisfiable if G has a Hamiltonian path. F(G) has n^2 boolean variables x[i, j] , 1 ≤ i, j ≤ n. Here x[i, j] the ith position in the Hamiltonian path is occupied by node j.

Clauses of our CNF F(G) are as follows:

  1. Each node j must appear in the path.
  2. No node j appears twice in the path.
  3. Every position i on the path must be occupied.
  4. No two nodes j and k occupy the same position in the path.
  5. Non-adjacent nodes i and j cannot be adjacent in the path.

For proof and correctness of above clauses refer to this paper by Prof. Yuh-Dauh Lyuu, National Taiwan University.

Here is Python 3 code for same, it takes two integers V and E as input in first line denoting number of nodes and number of edges, then next E lines contain two integers u and v, denoting there is an edge between u and v (bi-directional).

clauses = []
C = 1
mymap = {}
n = 0
def varnum(i, j):
    global n
    x =  i * n + j
    global C
    if not x in mymap:
        mymap[x] = C
        C += 1
    return x



n, m = map(int, input().split())

nodes = range(1, n + 1)

mymap = {}

for i in nodes:
    for j in nodes:
        if i != j:
            mymap[(i, j)] = 0

#each node j must appear in the path
for j in nodes:
    clauses.append([varnum(i, j) for i in nodes])

#no node j appears twice in the path
for i in nodes:
    for k in nodes:
        if i < k:
            for j in nodes:
                clauses.append([-varnum(i, j), -varnum(k, j)])


#every position i on the path must be occupied
for i in nodes:
    clauses.append([varnum(i, j) for j in nodes])


#no two nodes j and k occupy the same postion in the path
for j in nodes:
    for k in nodes:
        if j < k:
            for i in nodes:
                clauses.append([-varnum(i, j), -varnum(i, k)])



for _ in range(m):
    u, v = map(int, input().split())
    mymap[(u, v)] = 1
    mymap[(v, u)] = 1

for i in nodes:
    for j in nodes:
        if (i, j) in mymap:
            if mymap[(i, j)] == 0:
                for k in range(1, n):
                    clauses.append([-varnum(k, i), -varnum(k + 1, j)])

print (len(clauses), C - 1)
for x in clauses:
    for y in x:
        p = mymap[abs(y)]
        if y < 0:
            p *= -1
        print (p , end = " ")
    print (0)
1 Like
4

I have already gone through the paper by Prof. Yuh-Dauh Lyuu, National Taiwan University. And code the solution in java but still it have some bugs. The code you implemented is giving wrong answer on SAT solver(ans should be SAT but ans shown is UNSAT). Refer this link http://ideone.com/BGbEPP .
This is link to my code if you can resolve the bug. I will be thankful http://ideone.com/qpUvDz
My algo is giving SAT if Hamiltonian Path does not exist by the SAT-Solver.

1 Like
5

The test case provided at http://ideone.com/BGbEPP is giving correct output and its SAT. Hope I understood you correctly or you are talking about some other test case.

6

I am implementing SAT solver online using DIMACS format. Use the above solution to get the answer. Answer shown is UNSAT while answer is SAT(workout the problem by hand). Visit this link and swap the clauses and number of variables required to solve according SAT solver http://dai.fmph.uniba.sk/~simko/satsolver/ .

1 Like
7

Thanks but I have already gone through this link and implemented the idea. Problem is my code have bug which I am not able to fix. If you can debug my code than thanks to you or can you code it yourself in any of your preferred language. Link to my code is http://ideone.com/qpUvDz

1 Like
8

Sorry @coderbond007, there was a bug in my hash function and now it works fine. ( I have corrected the code in the answer section.)

9

Please look into your code output and check the same on SAT-Solver(still same UNSAT is showing in your output instead of SAT). I think in resolving the bugs you have created more bugs. Because now your code is just printing one variable at a time and appended by 0. Please check your code @rahul_bhati
Visit this link to see the updated output shown by your code http://ideone.com/BGbEPP .
Please compare your result and algo with my code so that I can get where my bug too. I will be thankful.
Code link http://ideone.com/qpUvDz .

1 Like
10

@coderbond007 bug resolved.

11

@rahul_bhati I too resolved the bug of my code last night. By the way your solution is now satisfying all the conditions even the stress tests. Thanks for your support. :slight_smile:

12

please upvote me i need to get karma for asking question

1 Like