Wrong number of answer sets

[giang-trinh]

I tried to compute all answer sets of the two below programs using Clingo 5.6.2. They have the same set of atoms and the same set of rules. However, in choice-rule.txt, I added a choice rule for every atom (e.g., {aux_1}. for atom aux_1). Clingo returned 9 (resp. 10) answer sets for choice-rule.txt (resp. no-choice-rule.txt). It seems strange because I understand that the number of answer sets of choice-rule.txt should be theoretically greater than or equal to that of no-choice-rule.txt. Could you please check it? In addition, I expect that both programs return 9 answer sets.

choice-rule.txt no-choice-rule.txt

[rkaminsk]

I tried to compute all answer sets of the two below programs using Clingo 5.6.2. They have the same set of atoms and the same set of rules. However, in choice-rule.txt, I added a choice rule for every atom (e.g., {aux_1}. for atom aux_1). Clingo returned 9 (resp. 10) answer sets for choice-rule.txt (resp. no-choice-rule.txt). It seems strange because I understand that the number of answer sets of choice-rule.txt should be theoretically greater than or equal to that of no-choice-rule.txt. Could you please check it? In addition, I expect that both programs return 9 answer sets.

choice-rule.txt no-choice-rule.txt

Thanks for the report. This is a bug in clasp. I'll have a look later. The next step will be to reduce your program to something much smaller that still triggers the bug.

[giang-trinh]

Thank you for your quick response. I could not find a way to reduce my program to something much smaller that still triggers the bug. However, I added some new rules to reduce the number of answer sets. The new no-choice-rule program (see the attached file) has two answer sets as follows.

Answer: 1 nv_p38MAPK_b3 pv_DS_B_b1 pv_S_S_B_b1 pv_senescence nv_p16IN_K4a_b2 pv_ATR_b1 pv_ATR_b2 pv_CHE_K1 nvCDK2CycE pv_cycle_arrest nv_proliferation nv_E_2F pv_Mdm2 nv_apoptosis nv_p53_b2 nv_CDK46CycD pv_p21 pv_p53_b1 aux_56 nv_p14ARF pv_RB1 pv_CHE_K2 pv_ATM_b1 pv_p38MAPK_b2 pv_p38MAPK_b1 nv_Cdc25A_b1 nv_Cdc25A_b2 pv_p16IN_K4a_b1 pv_ATM_b2 aux_18 aux_24 aux_26 aux_9 aux_6 pv_S_S_B_b2 aux_3 pv_DS_B_b2 Answer: 2 nv_p38MAPK_b3 pv_DS_B_b1 pv_S_S_B_b1 pv_senescence nv_p16IN_K4a_b2 pv_ATR_b1 nv_ATR_b2 pv_CHE_K1 nvCDK2CycE pv_cycle_arrest nv_proliferation nv_E_2F pv_Mdm2 nv_apoptosis nv_p53_b2 nv_CDK46CycD pv_p21 pv_p53_b1 aux_56 nv_p14ARF pv_RB1 pv_CHE_K2 pv_ATM_b1 pv_p38MAPK_b2 pv_p38MAPK_b1 nv_Cdc25A_b1 nv_Cdc25A_b2 pv_p16IN_K4a_b1 pv_ATM_b2 aux_18 aux_24 aux_26 aux_9 nv_S_S_B_b2 aux_5 aux_3 pv_DS_B_b2

I am sure that Answer 1 is not correct. In my program, an atom always has a complementary atom (e.g., pv_ATM_b1 and nv_ATM_b1), and every answer set must contain exactly one of them. Consider Line 308 of the new no-choice-rule program:

nv_ATM_b1; nv_ATM_b2; nv_ATR_b1; nv_ATR_b2; nv_p38MAPK_b1; nv_p38MAPK_b2 :- nv_p38MAPK_b3.

In Answer 1, we have pv_ATM_b1 = pv_ATM_b2 = pv_ATR_b1 = pv_ATR_b2 = pv_p38MAPK_b1 = pv_p38MAPK_b2 = true, leading to nv_ATM_b1 = nv_ATM_b2 = nv_ATR_b1 = nv_ATR_b2 = nv_p38MAPK_b1 = nv_p38MAPK_b2 = false. This contradicts to Line 308 because nv_p38MAPK_b3 = true.

Moreover, by adding {pv_ATR_b2}. and {nv_ATR_b2}., it returns only one answer set as follows.

Answer: 1 nv_p38MAPK_b3 pv_DS_B_b1 pv_S_S_B_b1 pv_senescence nv_p16IN_K4a_b2 pv_ATR_b1 nv_ATR_b2 pv_CHE_K1 nvCDK2CycE pv_cycle_arrest nv_proliferation nv_E_2F pv_Mdm2 nv_apoptosis nv_p53_b2 nv_CDK46CycD pv_p21 pv_p53_b1 aux_56 nv_p14ARF pv_RB1 pv_CHE_K2 pv_ATM_b1 pv_p38MAPK_b2 pv_p38MAPK_b1 nv_Cdc25A_b1 nv_Cdc25A_b2 pv_p16IN_K4a_b1 pv_ATM_b2 aux_18 aux_24 aux_26 aux_9 nv_S_S_B_b2 aux_5 aux_3 pv_DS_B_b2

The above answer set is identical to Answer 2 of the previous program.

Hope that the above observation can help you in debugging.

no-choice-rule-new.txt

[rkaminsk]

You can try to use option --no-gamma as a workaround for now.

[giang-trinh]

I tried to use option --no-gamma. Now, Clingo returns the correct number of answer sets. Thank you so much for your enthusiastic support.

In addition, could you please give me the information about this option? Just to be curious because I am learning more about ASP.

[rkaminsk]

A real fix and a closer investigation is still in the making. I do not know the implementation but the name gamma probably comes from the nogoods in Definition 3 of the paper below. It's a bit technical to read. @BenKaufmann or @mgebser might be able to tell you more.

https://www.cs.uni-potsdam.de/wv/publications/DBLP_conf/ijcai/GebserKS13.pdf

[giang-trinh]

A real fix and a closer investigation is still in the making.

I see.

I do not know the implementation but the name gamma probably comes from the nogoods in Definition 3 of the paper below. It's a bit technical to read. @BenKaufmann or @mgebser might be able to tell you more.

Oh. I will look at Definition 3 of this paper. Thank you.

[rkaminsk]

You can try the latest wip branch. The issue should be fixed.

[giang-trinh]

Thank you. I will try this branch.