Alpha mistakenly proves Hanoi instance to be UNSAT on add_simple_completion branch

[rtaupe]

On the add_simple_completion branch, HanoiTowerTest#testSimple fails. The exact reason is unclear to me, but somehow the learnt nogoods are not processed correctly.

Notes:

• seed has been fixed to 0
• Fix bug in justification analysis, address issue #211. #220 does not help
• I do not think this has something to do specifically what has been implemented on the add_simple_completion branch. Rather, this issue probably pops up because different nogoods are learnt.

These are all the nogoods that are learned:

• { +3 +471 +475 -504 } = {+(succ(1, 2)), +(on(1, 5, 6)), +(on(1, 6, 7)), -(on(2, 5, 6))} (by analyzeTrailBased)
• { +1 +3 -95 +309 +459 +461 +463 } = {+(succ(0, 1)), +(succ(1, 2)), -(move(0, 6)), +(where(2, 5)), +(on(0, 5, 6)), +(on(0, 6, 7)), +(on(0, 7, 8))} (by analyzeTrailBased)
• { +1 +463 +465 -479 } = {+(succ(0, 1)), +(on(0, 7, 8)), +(on(0, 8, 9)), -(on(1, 7, 8))} (by analyzeTrailBased)
• { +1 +3 +135 -145 +254 +465 -648 } = {+(succ(0, 1)), +(succ(1, 2)), +(move(2, 8)), -(move(1, 9)), +(where(0, 2)), +(on(0, 8, 9)), -(on(1, 2, 9))} (by analyzeTrailBased)
• { +19 +34 +49 +64 +79 +94 +109 +124 +139 +235 } = {+(noMove(0, 1)), +(noMove(0, 2)), +(noMove(0, 3)), +(noMove(0, 4)), +(noMove(0, 5)), +(noMove(0, 6)), +(noMove(0, 7)), +(noMove(0, 8)), +(noMove(0, 9)), +(diskMoved(0))} (by justifyMbtAndBacktrack and noGoodFromJustificationReasons)
• { -34 } = {-(noMove(0, 2))} (by analyzeTrailBased)

I have converted these nogoods to the following constraints:

:- succ(1, 2), on(1, 5, 6), on(1, 6, 7), not on(2, 5, 6).
:- succ(0, 1), succ(1, 2), not move(0, 6), where(2, 5), on(0, 5, 6), on(0, 6, 7), on(0, 7, 8).
:- succ(0, 1), on(0, 7, 8), on(0, 8, 9), not on(1, 7, 8).
:- succ(0, 1), succ(1, 2), move(2, 8), not move(1, 9), where(0, 2), on(0, 8, 9), not on(1, 2, 9).
:- noMove(0, 1), noMove(0, 2), noMove(0, 3), noMove(0, 4), noMove(0, 5), noMove(0, 6), noMove(0, 7), noMove(0, 8), noMove(0, 9), diskMoved(0).
:- not noMove(0, 2).

When I add these constraints to the program and let clingo solve it, it stays satisfiable, so the constraints themselves might be correct.

When Alpha on add_simple_completion solves the program without these constraints, it wrongly proves it to be unsatisfiable (that is the main topic of this issue).
When I add the constraints, however, the program suddenly becomes satisfiable for Alpha!!!

[madmike200590]

Not sure if it's really related, but after merging the latest changes from master, the simple instance for Hanoi Tower also becomes (incorrectly) unsatisfiable in PR #207 (partial evaluation of stratifiable porgram parts). Adding the above mentioned constraints does not seem to solve the issue there, however. I'll continue investigating this

[madmike200590]

Here are some preliminary results of my investigation into this on the PR #207 branch.
I tried running the simple hanoi tower instance from commandline in a few different combinations.
Interestingly, in this case, what causes the unsatisfiable result seems to be related to the absence of the rules solved by stratified evaluation.
In the below examples, Alpha-bundled-hanoi.jar refers to the bundledJar built from the latest commit in the PR #207 branch, HanoiTower_Alpha.asp and simple.asp are the encoding and instance files used by the test case.

Original HanoiTower-simple instance with stratified evaluation enabled

Command:

java -jar Alpha-bundled-hanoi.jar -i HanoiTower_Alpha.asp -i simple.asp > hanoi_simple_stratEval_unsat.log

Result: UNSAT
The detailed output (root level=DEBUG) is in the attached logfile hanoi_simple_stratEval_unsat.log

Original HanoiTower-simple instance with stratified evaluation disabled

Command:

java -jar Alpha-bundled-hanoi.jar -nse -i HanoiTower_Alpha.asp -i simple.asp > hanoi_simple_noStratEval_sat.log

Result: Satisfiable (2 Answer Sets)
The detailed output (root level=DEBUG) is in the attached logfile hanoi_simple_noStratEval_sat.log

Preprocessed program resulting from stratified evaluation with stratified evaluation enabled

The preprocessed (i.e. stratified part evaluated) program can be obtained via

java -jar Alpha-bundled-hanoi.jar -i HanoiTower_Alpha.asp -i simple.asp -pp HanoiTower_preprocessed.asp

Preprocessing output attached for reference: HanoiTower_preprocessed.asp.txt

Command:

java -jar Alpha-bundled-hanoi.jar -i HanoiTower_preprocessed.asp.txt > hanoi_simple-preproc_stratEval_unsat.log

Result: UNSAT
Detailed log output: hanoi_simple-preproc_stratEval_unsat.log

Preprocessed program resulting from stratified evaluation with stratified evaluation disabled

Command:

java -jar Alpha-bundled-hanoi.jar -nse -i HanoiTower_preprocessed.asp.txt > hanoi_simple-preproc_noStratEval_unsat.log

Result: UNSAT
Detailed log output: hanoi_simple-preproc_noStratEval_unsat.log

Original HanoiTower-simple instance and additional facts from stratified part with stratified evaluation enabled

(Note that only the facts resulting from stratified evaluation were added, but all rules kept)
For reference, the additional facts resulting from stratified evaluation are:

peg(1).
peg(2).
peg(3).
peg(4).
succ(3, 4).
succ(2, 3).
succ(1, 2).
succ(0, 1).
onG(3, 1, 5).
onG(3, 2, 8).
onG(3, 5, 6).
onG(3, 6, 7).
onG(3, 8, 9).

See also: hanoi_stratEvalFacts.asp.txt

Command:

java -jar Alpha-bundled-hanoi.jar -i HanoiTower_Alpha.asp -i simple.asp -i hanoi_stratEvalFacts.asp.txt > hanoi_simple-addFacts_stratEval_unsat.log

Result: UNSAT
Log output: hanoi_simple-addFacts_stratEval_unsat.log

Original HanoiTower-simple instance and additional facts from stratified part with stratified evaluation disabled

Command:

java -jar Alpha-bundled-hanoi.jar -nse -i HanoiTower_Alpha.asp -i simple.asp -i hanoi_stratEvalFacts.asp.txt > hanoi_simple-addFacts_noStratEval_sat.log

Result: Satisfiable (2 Answer Sets)
Log output: hanoi_simple-addFacts_noStratEval_sat.log

Conclusion

Interestingly,

• All of the above input combinations are satisfiable in clingo
• The instance becomes incorrectly unsatisfiable whenever the rules solved by stratified evaluation are not passed to the grounder/solver (either because stratified evaluation is enabled or Alpha is called with the result of stratified evaluation as it's input)

The rules that are fully solved by stratified evaluation (and therefore not part of grounder/solver input when running with stratified evaluation enabled) are:

onG(K, N1, N) :- ongoal(N, N1), steps(K).

succ(0,1) :- time(0).
succ(1,2) :- time(1).
succ(2,3) :- time(2).
succ(3,4) :- time(3).
succ(4,5) :- time(4).
succ(5,6) :- time(5).
succ(6,7) :- time(6).
succ(7,8) :- time(7).
succ(8,9) :- time(8).
succ(9,10) :- time(9).
succ(10,11) :- time(10).
succ(11,12) :- time(11).
succ(12,13) :- time(12).
succ(13,14) :- time(13).
succ(14,15) :- time(14).
succ(15,16) :- time(15).
succ(16,17) :- time(16).
succ(17,18) :- time(17).
succ(18,19) :- time(18).
succ(19,20) :- time(19).
succ(20,21) :- time(20).
succ(21,22) :- time(21).
succ(22,23) :- time(22).
succ(23,24) :- time(23).
succ(24,25) :- time(24).
succ(25,26) :- time(25).
succ(26,27) :- time(26).
succ(27,28) :- time(27).
succ(28,29) :- time(28).
succ(29,30) :- time(29).
succ(30,31) :- time(30).
succ(31,32) :- time(31).
succ(32,33) :- time(32).
succ(33,34) :- time(33).
succ(34,35) :- time(34).
succ(35,36) :- time(35).
succ(36,37) :- time(36).
succ(37,38) :- time(37).
succ(38,39) :- time(38).
succ(39,40) :- time(39).

Due to my lacking expertise with the core solving code, I'm not sure how useful these results are.. my "layman's impression" is that evaluating the stratified part (more concisely, the absence of the rules from the stratified part) leads to the solver (incorrectly) learning too restrictive nogoods (or incorrectly processing correct nogoods?)

[rtaupe]

Wow, thank you for this detailed investigation!

What speaks against the theory that incorrect nogoods are learned is that (if I did not make a mistake) I already added all the learned nogoods as constraints (see above) and this did not make the program unsatisfiable for clingo.
So maybe correct nogoods are somehow processed incorrectly...

[rtaupe]

Incidentally, I stumbled upon a different approach to this issue recently:
All the succ/2 atoms have been introduced to this program at a time when Alpha did not yet support arithmetics as well as today. I thought I could just replace all usages of this atom with its definition, i.e., replace succ(TM1,T) by TM1 = T - 1 and succ(T,TP1) by TP1 = T + 1 and remove all succ/2 facts.
This also led to unsatisfiability.