Skip to main content
added 4 characters in body
Source Link

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(a1). # 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?

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(a). # 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 wrong way?

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?

upper case
Link
logi-kal
  • 7.9k
  • 6
  • 35
  • 48

Solving hamiltonianHamiltonian cycle in answer set programming

showing image; fixing code formatting; adding tag
Source Link
logi-kal
  • 7.9k
  • 6
  • 35
  • 48

Solving Hamiltonian Cycle by Answerhamiltonian cycle in answer set programming

Hamiltonian cycle instantiation and encoding: Instantiation

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(a). # 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 Solver: 0.002s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)! clingo file_name.lp
CPU Time Return: 0.000s

Myclingo questionversion is5.6.2 Reading from encoding.lp Solving... UNSATISFIABLE Models : is0 Calls this program really unsatisfiable or am I encoding: it1 Time wrong way? : 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 wrong way?

Solving Hamiltonian Cycle by Answer set programming

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(a). # 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 wrong way? 

Solving hamiltonian cycle in answer set programming

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(a). # 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 wrong way?

Source Link
Loading