alpha UNSAT vs. clingo SAT
KillerLink opened this issue · 5 comments
As shown in the picture below, the provided input files are classified by alpha as UNSAT while clingo says it is SAT. The expected output is SAT according to my opinion.
Environment
alphaversion used was downloaded from:https://github.com/alpha-asp/Alpha/releases/download/v0.5.0/alpha.jar- Operating System: Fedora Server 32
clingoversion used:clingo version 5.4.0, Address model: 64-bit, libclingo version 5.4.0, Configuration: with Python 3.8.1, with Lua 5.3.5, libclasp version 3.3.5 (libpotassco version 1.1.0), Configuration: WITH_THREADS=1
@AntoniusW could this be an issue similar to the one from #239 (HanoiTower testcase UNSAT)?
I managed to reduce the reproduction testcase further, see attached files. Additionally, in test.instance, there is a commented line, including that line allows switching the alpha result between UNSAT (when line commented out) and SAT (line in use).
Here is an even smaller version, sadly no "trigger" to swap the behaviour was found here.
First of all, thank you for raising all the issues you encountered!
This one here, is not really a bug, but rather a missing feature regarding arithmetic expressions inside atoms. Currently, Alpha does not treat statements like pr(N+1) correctly. If you introduce a new variable, however, it works, e.g. pr(N1), N1 = N+1 would work. You can therefore fix your program by changing lines like
{ cycle(N+1) } :- cycle(N), cycle_max(K), N<K.
to
{ cycle(N1) } :- N1 = N+1, cycle(N), cycle_max(K), N<K..
Alpha is not throwing an error when it encounters arithmetic expressions inside atoms, as this feature is planned to be integrated in the near future (for some time now..). I am sorry that this missing error message wasted some of your time.
I think the pending implementation of this feature would be covered by issue #89. Linking this here in order to ensure also this specific scenario is not overlooked when implementing full arithmetics support. Thanks @KillerLink for reporting this!