Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

conditional literals - clingo 5 vs clingo 4 #173

Closed
wdvorak opened this issue Oct 29, 2019 · 5 comments
Closed

conditional literals - clingo 5 vs clingo 4 #173

wdvorak opened this issue Oct 29, 2019 · 5 comments
Assignees
Labels
Milestone

Comments

@wdvorak
Copy link

wdvorak commented Oct 29, 2019

We are using several asp encodings that make use of conditional literals and noticed that on some instances clingo 4 (4.4.0) and clingo 5 (5.4.0) return different answer-sets. It seems that this only happens for programs having conditional literals in rule heads.

For instance for the program below

arg(a1). arg(a2). arg(a3). arg(a4). arg(a5). arg(a6). arg(a7). arg(a8). arg(a9).
att(a2,a1). att(a2,a6). att(a2,a7). att(a2,a8). att(a2,a9).
att(a3,a1).
att(a4,a1).
att(a5,a1).
att(a6,a1). att(a6,a2). att(a6,a3). att(a6,a4). att(a6,a5).
att(a7,a1).
att(a8,a1).
att(a9,a1).
in(X) :- arg(X), not out(X).
out(X) :- arg(X), not in(X).
in(X):-arg(X), out(Y):att(Y,X).
out(X):- in(Y), att(X,Y).
out(X):-in(Y), att(Y,X).
in(Y):att(Y,X) :-out(X).
#show in/1.
#show out/1.
:-in(a1).

clingo4 returns the answer-sets

Answer: 1
out(a1) out(a2) out(a3) out(a4) out(a5) in(a6) in(a7) in(a8) in(a9)
Answer: 2
out(a1) in(a2) in(a3) in(a4) in(a5) out(a6) out(a7) out(a8) out(a9)

while clingo5 returns UNSATISFIABLE.
When removing the last constraint ':-in(a1).' then both versions return the two answer-sets listed above.

Is there an intended difference in the semantics of conditional literals between clingo 4 and clingo 5?

Another example where clingo 4 and clingo 5 disagree on the answer-sets is
idealset_adm.txt

@rkaminsk
Copy link
Member

@BenKaufmann: This seems to be a regression in clasp.

The program bug.sm.gz grounded with

$ clingo --mode=gringo bug.lp | lpconvert > bug.sm

produces different results depending on the clasp version used. Compare

$ clasp-3.1.5-mt bug.sm -V0
out(a1) out(a2) out(a3) out(a4) out(a5) in(a6) in(a7) in(a8) in(a9)
SATISFIABLE

and

clasp-3.2.0-mt bug.sm -V0 
*** ERROR: (clasp): shifting must not introduce new atoms!
UNKNOWN

and

$ clasp-3.3.5-mt bug.sm -V0
UNSATISFIABLE

@BenKaufmann
Copy link
Contributor

@rkaminsk
This is indeed a regression in clasp. Should be fixed in dev (potassco/clasp@9389f60).

@rkaminsk
Copy link
Member

rkaminsk commented Nov 1, 2019

Thanks @BenKaufmann. There are still some other things in clingo I want to address before doing a release. @wdvorak hope you can live an older clingo version for now or apply the patch yourself.

@rkaminsk rkaminsk self-assigned this Nov 1, 2019
@rkaminsk rkaminsk added the bug label Nov 1, 2019
@rkaminsk rkaminsk added this to the v5.4.1 milestone Nov 1, 2019
@wdvorak
Copy link
Author

wdvorak commented Nov 3, 2019

thanks for your quick response. We are fine with using the older version for now and are looking forward to the next release ;).

@rkaminsk
Copy link
Member

rkaminsk commented Dec 2, 2019

Fixed in wip branch updating clasp with 4db3c47.

@rkaminsk rkaminsk closed this as completed Dec 2, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

3 participants