Alpha
Alpha copied to clipboard
Answer-Sets missing with negated count-equals aggregate.
The following program unexpectedly has Alpha report 2 answer sets while there should be three.
:- not 1=#count{ na_1 : a; nb_1 : b; nc_1 : c }.
na_1 :- not a.
a :- not na_1.
nb_1 :- not b.
b :- not nb_1.
nc_1 :- not c.
c :- not nc_1.
Commandline: -n 0 -str [above program]
Output:
Answer set 1:
{ b, na_1, nc_1 }
Answer set 2:
{ c, na_1, nb_1 }
SATISFIABLE
Expected: a third answer set { a, nb_1, nc_1}.
Narrowed it down a bit to an aggregate using ground versus non-ground count-equals.
foo(1) :- 1=#count{ na_1 : a; nb_1 : b }.
:- not foo(1).
na_1 :- not a.
a :- not na_1.
nb_1 :- not b.
b :- not nb_1.
The program above erroneously yields 1 answer set, while the variant below yields the correct 2 answer sets. The major difference is 1=#count{..} versus X=#count{..}.
foo(X) :- X=#count{ na_1 : a; nb_1 : b }.
:- not foo(1).
na_1 :- not a.
a :- not na_1.
nb_1 :- not b.
b :- not nb_1.
More testing with sometimes disappearing answer-sets revealed: bug seems to go away if justification is disabled.