Solving Hamiltonian cycle in answer set programming

Question

Hamiltonian cycle instantiation and encoding:

Instantiation

% vertices: n=node n(1..4). % edges: e=edge e(1,(2;3)). e(2,(3;4)). e(3,(1;4)). e(4,1). % starting point s(1). # p=path, o=omit, op=on-path, r=reach, s=start% generate path p(X,Y):- not o(X,Y), e(X,Y). o(X,Y):- not p(X,Y), e(X,Y). % at most one incoming/outgoing edge :- p(X,Y), p(U,Y), X < U. :- p(X,Y), p(X,V), Y < V. % at least one incoming/outgoing edge op(Y):- p(X,Y), p(Y,Z). :- n(X), not op(X). % connectedness r(X):- s(X). r(Y):- r(X), p(X,Y). :- n(X), not r(X).

Solver: ! clingo file_name.lp
Return:

clingo version 5.6.2 Reading from encoding.lp Solving... UNSATISFIABLE Models : 0 Calls : 1 Time : 0.002s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.000s

My question is: is this program really unsatisfiable or am I encoding it the wrong way?

logi-kal · Accepted Answer · 2023-01-05 11:31:54Z

No, it is not unsatisfiable. There exists indeed exactly one Hamiltonian cycle from a, which is clearly a->b->c->d(->a).

You are just declaring the nodes using numbers, but the starting node is a (not a number).

The part in which you encoded the logics of the problem looks ok to me.

Replacing s(a) with s(1) we obtain SATISFIABLE as result:

clingo version 5.3.0 Reading from test.lp Solving... Answer: 1 n(1) n(2) n(3) n(4) e(4,1) e(1,2) e(1,3) e(2,3) e(2,4) e(3,1) e(3,4) s(1) r(1) p(1,2) o(1,3) p(2,3) r(2) r(3) op(2) p(4,1) o(2,4) o(3,1) p(3,4) r(4) op(4) op(1) op(3) SATISFIABLE Models : 1 Calls : 1 Time : 0.000s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s) CPU Time : 0.000s

P.S. Note that the two following lines:

p(X,Y):- not o(X,Y), e(X,Y). o(X,Y):- not p(X,Y), e(X,Y).

can be compacted with:

p(X,Y) | o(X,Y) :- e(X,Y).

Collectives™ on Stack Overflow

Solving Hamiltonian cycle in answer set programming

1 Answer 1

Comments

Hot Network Questions

Collectives™ on Stack Overflow

1 Answer 1

Comments

Related