Unexpected outputs on simple purely existential examples.

[AbdallahS]

Consider the following programs / output pairs

P1:

{ a; b }.
_exists(1,a).
_exists(1,b).

The output is is fine and expected:

Running: clingo --output=smodels example4.lp | qasp2qbf.py --no-warnings | lp2normal2 | lp2acyc | lp2sat | qasp2qbf.py --cnf2qdimacs | caqe-linux --partial-assignments | qasp2qbf.py --interpret
V -4 -5 8 9 0
Answer:

SAT

P2, forcing either a or b.

{ a; b }. _exists(1,a). _exists(1,b).
:- not a, not b.

The output is fine too.

Running: clingo --output=smodels example4.lp | qasp2qbf.py --no-warnings | lp2normal2 | lp2acyc | lp2sat | qasp2qbf.py --cnf2qdimacs | caqe-linux --partial-assignments | qasp2qbf.py --interpret
V 4 -5 -8 9 0
Answer:
a
SAT

P3, forcing a.

{ a; b }. _exists(1,a). _exists(1,b).
:- not a.

The output is wrong, as far as I understand.

Running: clingo --output=smodels example4.lp | qasp2qbf.py --no-warnings | lp2normal2 | lp2acyc | lp2sat | qasp2qbf.py --cnf2qdimacs | caqe-linux --partial-assignments | qasp2qbf.py --interpret
V -5 9 0
Answer:

SAT

Explicitely listing #show a/0. and #show _exists/2 does not fix the problem.

P4, forcing a and b.

{ a; b }. _exists(1,a). _exists(1,b).
:- not a.
:- not b.

The output is incomplete: there is "answer" line, nor any "V..." line, and this is not fixed by adding --keep-facts to the clingo invocation.

Running: clingo --output=smodels example4.lp | qasp2qbf.py --no-warnings | lp2normal2 | lp2acyc | lp2sat | qasp2qbf.py --cnf2qdimacs | caqe-linux --partial-assignments | qasp2qbf.py --interpret
SAT

PS: the readme file has a typo. It states that the level for existential quantifiers is even and for univeral is odd, but this needs to be swapped so that existentials are odd and universals are even. See the example files and also the E X1 A X2 E X3 ... explanations in the readme itself.

[javier-romero]

Thank you @AbdallahS!

I will change now the readme.

With respect to the first issue on P3, the result is correct. The quantified logic program is ''equivalent'' to the QBF exists a exists b ((b or -b) and a). More formally, it says that there is a subset X of {a,b} such that there is some stable model of

{ a; b }.
:- not a.

that contains the atoms in X and no other atoms from {a,b}. The set X={a} satisfies the condition, hence SAT is the right answer.

With respect to P4, the problem happens becuase the QBF solver does not return any assignment. It seems to me that the problem is so simple that the preprocessor solves it, and then the QBF solver does not return any assignment. I would be very happy if you have any ideas on how to fix this :)

[AbdallahS]

I agree that the set X={a} satisfies the condition and that the QASP is SAT. However, X is not returned/printed in the Answer: field, as if the empty set satisfied the condition. Compare to what happens with P2.

[javier-romero]

Oh man, sorry Abdallah, I had completely missed the point... Yes, you are right, this is the same issue as with the other example. The problem is that the QBF solver does not print any assignment with the input program, and then qasp2qbf is lost...

For example, with the following input:

$ cat in.qdimacs
p cnf 2 2
e 1 2
1 0
2 0

caqe-linux does not print the solution with 1 and 2:

$ cat in.qdimacs | caqe-linux
SAT

I will have to investigate more the QBF solvers to see what to do. I am very happy to take suggestions (or PRs :)