Add option to support founded constraints.

[rkaminsk]

@wanko and @javier-romero, it is relatively easy to provide founded constraints similar to what we did in lc2casp.

Consider the following program:

&diff { x - y } :- B.
H :- &diff { x - y }.

We can rewrite the program into:

&diff { x - y } :- B.
def(x) :- B.
def(y) :- B.
H :- &diff { x - y }, def(x), def(y).

Now that I thought about this a little longer, there is a problem. There can actually be spurious answer sets.

For the program

&diff { x - 0 } >= 0.
&diff { y - 0 } >= 0.

{ c }.
:- c.

a :- c, &diff { x - y } >= 2.

clingo-dl outputs the solutions { x=0, y=0 } and { x=2, y=0 }. The second one is undesired and also depends on the kind of simplifications performed. The same would happen if we add the foundedness atoms.

[javier-romero]

Interesting.

I think a key issue here is to specify mathematically why is { x=2, y=0 } an undesired solution.
I would say that the answer is: because it is not a stable model in the logic of HT_{LB}.
What do you think about it?

Also, it seems that the solution with { x=2, y=0 } is undesired in that encoding, but what happens if we replace the rule

a :- c, &diff { x - y } >= 2.

by these ones?

a :- c, aux.
aux :- &diff { x - y } >= 2.

One would expect that such replacement should not change the fact that { aux, x=2, y=0 } is undesired.
Again, this is what happens in HT_{LB}, because that solution is not a stable model.
But in clingo-dl you would obtain that solution again.
Note that in this case there is no issue with simplifications.

All this goes back to the original question:
what is the intended semantics for clingo-dl considering:

1. logic programs with variables, and
2. the fact that the values of the integer variables are part of the stable models.

It seems to me that point 2 has not been considered when defining the semantics of clingo-dl, even in the propositional case: is this correct?

[rkaminsk]

All this goes back to the original question: what is the intended semantics for clingo-dl considering logic programs with variables.

For now, my answer is that you can use DL constraints in the head and things work nicely. Then an answer set is kept whenever the derived constraints are satisfiable.

A semantics that also works nicely with constraints in the body is a research question.

[javier-romero]

Sounds good to me.

It would be nice to have a definition that covers programs with variables and DL constraints in the head, and
it would be great if the definition would also sayo what are the values of the integer variables.

[rkaminsk]

It would be nice to have a definition that covers programs with variables and DL constraints in the head, and
it would be great if the definition would also sayo what are the values of the integer variables.

Then someone has to go ahead and write one. Maybe as part of a paper or thesis to have some synergies. Unfortunately, it does not really fit into what I am working on right now. 😉

[rkaminsk]

Playing a bit with some ideas I stumbled above a glitch and a bug. The bug is that clingo-dl enumerates two (equal) answer sets for the program below. The glitch is that it assigns -3 to both x and y. We should not subtract the value of the zero node from variables that are not reachable from the zero node. Furthermore, we should make the assignment for disconnected "graphs" unique. This could probably be done by shifting the values of the variables by value of the variable with the smallest value. This hinges a bit on what a minimal assignment is supposed to look like...

&diff { z - 0 } <= -3. 
&diff { x - y } >= 0.  
                      
{ c }.
:- c.                     
&diff { y - z } <= 0 :- c.

The bug can be prevented by writing it like this:

&diff { z - 0 } <= -3.
&diff { x - y } >= 0.

{ c; d }.
:- c, d.
:- c, not d.
:- not c, d.
&diff { y - z } <= 0 :- c.

EDIT: I opened bug report in clasp's issue tracker: potassco/clasp#71.

[rkaminsk]

We'll leave this to fclingo.