Open MaxOstrowski opened 11 months ago
a :- b(X), not X = #sum {1: a}.
seems to be equivalent to:
a :- b(X), not a.
while
a :- b(X), not X = #sum {1: not a}.
is more like:
a :- b(X), not not a.
?
@wanko can you help me out here ? When exactly do i have a positive dependency to the head.
@rkaminsk Can you give me a quick tip without challenging me mentally ;)
We have a dependency graph for aggregates in Section 5 of https://www.cs.uni-potsdam.de/wv/publications/DBLP_journals/corr/abs-2108-04769.pdf. It is inspired by the translation of aggregates into propositional formulas.
The gist is:
It is sometimes possible to drop a double negation or turn a negated antimonotone aggregate into a positive one. An easy scenario is if there is no recursion through the negated parts.
Example to deal with later:
#false :- S = #count { (X,Y): bend(X,Y,_,1) }; not S = #sum { N,(X,Y): hint(X,Y,N) }.
With a more complicated head like hint/3
would this be a positive or negative dependency ?
Currently the pdg just takes all predicates inside the body that are not directly preceeded with "not". so
a :- b(X), not X = #sum {1: a}.
creates a positive dependency. Is this true ?