potassco / clingo

🤔 A grounder and solver for logic programs.
https://potassco.org/clingo
MIT License
624 stars 82 forks source link

#delayed output #331

Open stas-g opened 3 years ago

stas-g commented 3 years ago

hello,

here is a simple example to illustrate my question:

p1.lp consists of 0 {a} 1.

Calling "clingo --text p1.lp" gives ``#delayed(1).

delayed(1) <=> #count{0,a:a}``


p2.lp consists of {a}.

Calling clingo --text p2.lp gives {a}.

my question is: what does #delayed(1) <=> #count{0,a:a} mean in this example? and "#delayed" output in general as i encounter it on a regular basis when using n {....} m constructs but could not find anything about it online or in the Potassco user manual.

thank you in advance, stas

rkaminsk commented 3 years ago

When a (recursive) rule with a head aggregate is grounded, its body is instantiated before its head is grounded. Thus, you get

#delayed(n) :- Body.

when the body has been instantiated and later

#delayed(n) <=> Aggregate.

when the head aggregate is completely grounded.

Since this is often a source of confusion, I should probably store the partial rule, and then substitute the head aggregate and output it when the grounding is complete. I'll mark it as a future todo item.

Since choice rules with exactly one element are a very common language feature, I implemented a specialized grounding algorithm for them that is both faster and does not need to delay grounding the head.

stas-g commented 3 years ago

many thanks for the clarification, Roland!

best, stas

rkaminsk commented 3 years ago

I'll just reopen because I want to mark this as a future todo item.

Gregory-Gelfond commented 2 years ago

Hi @rkaminsk - do you have a way to read the ground output like this:

#delayed(1). #delayed(1) <=> #count{0,a:a}

Gregory-Gelfond commented 2 years ago

On some level I'm trying to investigate the distinction between the following pair of rules:

0{ occurs(A,T) }1 :- action(A), time(T) and

0{ occurs(A,T) : action(A) }1 :- time(T).

They have different groundings as hinted at in this discussion and knowing how to read the #delayed and the right hand side of the <=> would be helpful.

rkaminsk commented 2 years ago

delayed(1). #delayed(1) <=> #count{0,a:a}

The <=> is meant to be an equivalence. So you can read it as:

#count{0,a:a}.

Note that clingo adds some seemingly unnecessary elements to the tuples. This is to support rules like

a(X) :- p(X), { X=1; X=2 } >= 1.

as they are for example supported by lparse (in a similar form). The set aggregate says that X must be either 1 or 2. We never formally specified the semantics of this little extension but looking at the grounding it is possible to figure out what is happening.

The two rules

0{ occurs(A,T) }1 :- action(A), time(T).

and

0{ occurs(A,T) : action(A) }1 :- time(T).

have a different meaning. The first says that any number of actions might occur at a time step. The second that at most one action might occur at a time step.

Gregory-Gelfond commented 2 years ago

I understand that reading of the choice rules, but it raises the question of whether these are equivalent:

  1. { occurs(A,T) } :- action(A), time(T)
  2. { occurs(A,T) : action(A) } :- time(T)

The lack of cardinality bounds seems to blur the distinction here.

rkaminsk commented 2 years ago

I understand that reading of the choice rules, but it raises the question of whether these are equivalent:

1. { occurs(A,T) } :- action(A), time(T)

2. { occurs(A,T) : action(A) } :- time(T)

The lack of cardinality bounds seems to blur the distinction here.

Yes, one could say they are strongly equivalent. Also including

3. { occurs(A,T) : action(A), time(T) }.

Note that clingo is optimized for grounding the first version. You will notice the different output. Maybe future version will be extended to include the other variants. It depends on when I find the time to look into this.

Gregory-Gelfond commented 2 years ago

@rkaminsk thanks! This is interesting. I can take this offline but are there any rules of thumb performance-wise around choice rules (solver side) that you can maybe send me?

rkaminsk commented 2 years ago

@rkaminsk thanks! This is interesting. I can take this offline but are there any rules of thumb performance-wise around choice rules (solver side) that you can maybe send me?

When I mentioned performance, I was thinking of grounding. For the solver, all three versions of the choice rules should be equivalent. So, if the grounding is not too large, either version can be used.