Re: [Potassco-users] iclingo behavior arbitrary

[Roland K. <kam...@cs...>]

On Thursday, January 30, 2014 12:25:58 PM David Spies wrote:
> I'm sorry.  I still don't see the distinction.  This program also has no
> externals beginning with the second step.  In both cases, the constraint
> which causes unsat becomes irrelevant when a later step negates its body.
> In both cases this happens because the later step provides support that
> wasn't previously present for a negated external body atom ("not
> covered(E)" in the clique example, and "not b" in the simple example).
> This is the primary feature of nonmonotonic logic.
I agree that it would be nice to just "union" the logic programs. The problem 
is implementing this. Keep in mind that our solver is based on SAT-solving 
techniques. It creates a program completion and uses clause learning. Consider 
step 1:
  a :- b.
  a :- c.
which has completion:
  a == b & c.
resulting in clauses:
  { -b, -c, a }, { -a, b }, { -a, c }
If a new definition arrives there is a problem, because these clauses and 
everything learnt from them become invalid. With the restrictions on clingo 
programs all the existing clauses can be kept as is. This is the main reason 
clingo is implemented as it is. -R