Answer Set Programming - filtering from a large number of models

449 views Asked by At

instance.lp

node(1). node(2). node(3). node(4). node(5). node(6).
edge(1,2). edge(2,1). edge(4,1). edge(2,3). edge(2,6).
edge(3,4). edge(3,5). edge(5,6). edge(6,3).
begin(4).

I have this problem instance, directed graph with a beginning node begin(4) and corresponding edges. In this graph it is only possible to get hamiltonian cycle starting from node 4 (4->1->2->3->5->6 or 4->1->2->6->5->3) and my problem class is able to solve it only if I give it the starting node 4, and returns 2 Models like this:

class.lp

% generate
{path(X,Y)} :- edge(X,Y).

% define
reached(X) :- begin(X).
reached(Y) :- reached(X), path(X,Y).

% test
:- node(X), not reached(X).
:- path(X,Y), path(X,Y1), Y!=Y1.
:- path(X,Y), path(X1,Y), X!=X1.

when I run it like this with clingo:

clingo class.lp instance.lp 0

I get 2 Models (hamilton cycles) back.

I want to run it without giving it the starting point, but when I replace begin(X) with node(X):

.
.
% define
reached(X) :- node(X).
reached(Y) :- reached(X), path(X,Y).
.
.

I get 120 Models.

My guess is that now it generates all possible combinations and I have add additional constraint to filter out the correct solution.

How would I filter the two correct models from this answer set?

1

There are 1 answers

0
Duda On BEST ANSWER

Your code does not generate hamiltonian cycles but hamiltonian paths with n-1 edges for n nodes. I will just assume you want to generate paths. So your generator for begin/1 is broken:

reached(X) :- node(X).

You literally say: all my nodes are reached.
Here is the fix:

{ begin(X) : node(X) } == 1.

What does it do? It reads something like: for all nodes X, choose exactly one begin(X) to be valid. The output using

#show begin/1.
#show path/2.

is the following:

Answer: 1
path(1,2) path(4,1) path(3,4) path(5,6) path(6,3) begin(5)
Answer: 2
path(1,2) path(4,1) path(2,3) path(3,5) path(5,6) begin(4)
Answer: 3
path(1,2) path(4,1) path(2,6) path(3,5) path(6,3) begin(4)
SATISFIABLE