problems generating interval information

Question

Given a a binary function over time, I try to extract the information about the intervals occuring in this function. E.g. I have the states a and b, and the following function:

a, a, b, b, b, a, b, b, a, a

Then i would want a fact interval(Start, Length, Value) like this:

interval(0, 2, a)
interval(2, 3, b) 
interval(5, 1, a) 
interval(6, 2, b) 
interval(8, 2, a)

Here is what I got so far:

time(0..9).

duration(1..10).
value(a;b).

1{ function(T, V): value(V) }1 :- time(T).

interval1(T, Length, Value) :- 
    time(T), duration(Length), value(Value),
    function(Ti, Value): Ti >= T, Ti < T + Length, time(Ti).

:- interval1(T, L, V), function(T + L, V).

#show function/2.
#show interval1/3.

This actually works kinda well, but still not correctly, this is my output, when I run it with clingo 4.5.4:

function(0,b)
function(1,a)
function(2,b)
function(3,a)
function(4,b)
function(5,a)
function(6,b)
function(7,a)
function(8,b)
function(9,a)
interval1(0,1,b)
interval1(1,1,a)
interval1(2,1,b)
interval1(3,1,a)
interval1(4,1,b)
interval1(5,1,a)
interval1(6,1,b)
interval1(7,1,a)
interval1(8,1,b)
interval1(9,1,a)
interval1(9,10,a)
interval1(9,2,a)
interval1(9,3,a)
interval1(9,4,a)
interval1(9,5,a)
interval1(9,6,a)
interval1(9,7,a)
interval1(9,8,a)
interval1(9,9,a)

which has only one bug: all the intervals at T == 9 (except for the one where L == 1)

So I tried to add the following constraint, to get rid of those:

:- interval1(T, L, V), not time(T + L - 1).

which in my mind translates to "it is prohibited, to have an interval, such that T + L is not a time" But now clingo said the problem would be unsatisfiable.

So I tried another solution, which should do the same, but in a little less general way:

:- interval1(T, L, V), T + L > 10. 

Which also made the whole thing unsolvable. Which I really don't understand, I'd just expect both of those rules to just get rid of the intervals, that run out of the function. So why do they completely kill all elements of the model?

Also, during my experiments, I replaced the function rule with:

function(
    0, a;
    1, a;
    2, b;
    3, b;
    4, b;
    5, b;
    6, a;
    7, b;
    8, a;
    9, a
).

Which would make the whole thing unsatisfiable even without the problematic constraints, why is that?

So yeah ... I guess, I fundamentally missunderstood something, and I would be really greatfull if someone would tell me what exactly that is.

Best Regards Uzaku

Answer 1

The programs with constraints are inconsistent because in ASP any program which contains both the fact a. and the constraint :-a. is inconsistent. You are basically saying that a is true, and, at the same time, a cannot be true.

In your case, for example, you have a rule which tells that interval1(9,10,a) is true for some function, and, on the other hand, you have a constraint which says that interval(9,10,a) cannot be true, so you get inconsistency.

A way to get rid of the undesired intervals would be, for example, to add the extra atom in the definition of an interval, e.g:

interval1(T, Length, Value) :- 
    time(T), duration(Length), value(Value),
    time(T+Length-1), % I added this
    function(Ti, Value): Ti >= T, Ti < T + Length, time(Ti).

Now the program is consistent.

I couldn't reproduce the inconsistency for the specific function you have provided. For me, the following is consistent:

time(0..9).

duration(1..10).
value(a;b).

%1{ function(T, V): value(V) }1 :- time(T).

function(0,a).
function(1,a).
function(2,b).
function(3,b).
function(4,b).
function(5,b).
function(6,a).
function(7,b).
function(8,a).
function(9,a).


interval1(T, Length, Value) :- 
    time(T), duration(Length), value(Value),
    time(T+Length-1),
    function(Ti, Value): Ti >= T, Ti < T + Length, time(Ti).


#show function/2.
#show interval1/3.

This is what I get in the output:

$ clingo test 0
clingo version 4.5.4
Reading from test
Solving...
Answer: 1
function(0,a) function(1,a) function(2,b) function(3,b) function(4,b) function(5,b) function(6,a) function(7,b) function(8,a) function(9,a) interval1(0,1,a) interval1(1,1,a) interval1(0,2,a) interval1(6,1,a) interval1(8,1,a) interval1(9,1,a) interval1(8,2,a) interval1(2,1,b) interval1(3,1,b) interval1(2,2,b) interval1(4,1,b) interval1(3,2,b) interval1(2,3,b) interval1(5,1,b) interval1(4,2,b) interval1(3,3,b) interval1(2,4,b) interval1(7,1,b)
SATISFIABLE

Models       : 1     
Calls        : 1
Time         : 0.002s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.000s

We are getting more intervals than needed, since some of them are not maximal, but I am leaving this for you to think about :)

Hope this helps.