alpha-asp / Alpha

A lazy-grounding Answer-Set Programming system
BSD 2-Clause "Simplified" License
58 stars 10 forks source link

Answer-Sets missing with negated count-equals aggregate. #357

Open AntoniusW opened 1 year ago

AntoniusW commented 1 year ago

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}.

AntoniusW commented 1 year ago

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.
AntoniusW commented 1 year ago

More testing with sometimes disappearing answer-sets revealed: bug seems to go away if justification is disabled.