Frank Schwidom
Frank Schwidom

Reputation: 146

I am encountering an early recursion termination in clingo

When I write :


move( a, b).
move( b, c).
move( c, d).

{ p( 0, A, B) : move( A, B) } = 1 .

0 { p( N+1, B, C) : p( N, A, B), move( B, C) } 1.

Then I get the result:

Solving...
Answer: 1
p(0,c,d)
Answer: 2
p(0,a,b)
Answer: 3
p(1,b,c) p(0,a,b)
Answer: 4
p(0,b,c)
Answer: 5
p(1,c,d) p(0,b,c)
SATISFIABLE

Here I am missing the combination p(2,c,d) p(1,b,c) p(0,a,b) .

I can simulate it by partitioning the recursion steps:


move( a, b).
move( b, c).
move( c, d).

{ p( 0, A, B) : move( A, B) } = 1 .

0 { p2( N+1, B, C) : p( N, A, B), move( B, C) } 1.

0 { p3( N+1, B, C) : p2( N, A, B), move( B, C) } 1.


leads to:


Solving...
Answer: 1
p(0,c,d)
Answer: 2
p(0,b,c)
Answer: 3
p(0,b,c) p2(1,c,d)
Answer: 4
p(0,a,b)
Answer: 5
p2(1,b,c) p(0,a,b)
Answer: 6
p3(2,c,d) p2(1,b,c) p(0,a,b)
SATISFIABLE

In this case I have the result : p3(2,c,d) p2(1,b,c) p(0,a,b) .

Why don't I get this in the first code variant?

Thanks in advance for your answers.

Upvotes: 2

Views: 38

Answers (0)

Related Questions