Projected Answer set enumeration

[mahi045]

I tried to enumerate projected answer sets of the given program (used --project in command line): input asp program. The projection atoms are specified by #project directive.

The output of Clingo is as follows:

>> clingo -n 0 --project asp_cut_asm-overflow.c.stp.cnf 
clingo version 5.5.1
Reading from asp_cut_asm-overflow.c.stp.cnf
Solving...
Answer: 1
v36 v63 v129 v97
Answer: 2
v36 v65 v131 v99
Answer: 3
v36 v64 v130 v98
Answer: 4
v62 v128 v96
Answer: 5
v61 v127 v95
SATISFIABLE

Models       : 5
Calls        : 1
Time         : 0.004s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.004s

But neither of the literals v36, v63, v129, ..., v96 are in the projection set. Actually, the projected number of answer sets should be 1 (empty answer set). I want to know why Clingo is printing 5 answer sets. Note that --project=no also shows the same answer sets. It seems that --project has no effect.

Thanks in advance.

[rkaminsk]

All atoms you are projecting on are facts. Those get simplified and in the end nothing to project is left. As a workaround, you can explicitly request projection to get the desired solution:

clingo test.lp 0 --project=project

It would probably be best if the grounder were to send some projection statement to the solver to enable the right projection mode.

PS: Passing large ground programs to the solver will quickly lead to very slow grounding. The grounder has not been written as a translator.

[mahi045]

Thank you