{"action":"created","issue":{"url":"https://api.github.com/repos/potassco/clingo/issues/107","repository_url":"https://api.github.com/repos/potassco/clingo","labels_url":"https://api.github.com/repos/potassco/clingo/issues/107/labels{/name}","comments_url":"https://api.github.com/repos/potassco/clingo/issues/107/comments","events_url":"https://api.github.com/repos/potassco/clingo/issues/107/events","html_url":"https://github.com/potassco/clingo/issues/107","id":326807565,"number":107,"title":"add_clause and add_nogood behavior depends of literal assignation","user":{"login":"Aluriak","id":1257159,"avatar_url":"https://avatars2.githubusercontent.com/u/1257159?v=4","gravatar_id":"","url":"https://api.github.com/users/Aluriak","html_url":"https://github.com/Aluriak","followers_url":"https://api.github.com/users/Aluriak/followers","following_url":"https://api.github.com/users/Aluriak/following{/other_user}","gists_url":"https://api.github.com/users/Aluriak/gists{/gist_id}","starred_url":"https://api.github.com/users/Aluriak/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Aluriak/subscriptions","organizations_url":"https://api.github.com/users/Aluriak/orgs","repos_url":"https://api.github.com/users/Aluriak/repos","events_url":"https://api.github.com/users/Aluriak/events{/privacy}","received_events_url":"https://api.github.com/users/Aluriak/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2018-05-27T11:15:17Z","updated_at":"2018-05-27T15:48:42Z","closed_at":null,"author_association":"NONE","body":"I found an unexplained behavior of add_clause and add_nogood when fed with a literal that already have the given value. For instance, `add_clause([2, -2])` when literal 2 is assigned to True.\r\n\r\nMaybe this behavior is normal, but it seems not documented.\r\nMaybe it is linked to #104 ?\r\n\r\nSee file `l.lp` for MWE:\r\n\r\n```python\r\n#script(python)\r\nSHOW_BUG = True\r\n\r\nclass Propagator:\r\n    def init(self, init):\r\n        \"watch all literals, remember ko and p atoms\"\r\n        for atom in init.symbolic_atoms:\r\n            lit = init.solver_literal(atom.literal)\r\n            init.add_watch(lit)\r\n            if atom.symbol.name == 'p':  # the atom to use to discard models\r\n                self.discard_atom = lit\r\n            elif atom.symbol.name == 'ko':  # determine if a model must be discarded\r\n                self.ko_atom = lit\r\n\r\n    # def propagate(self, ctl, _):  # behavior is different (but still buggy) with propagate\r\n    def check(self, ctl):\r\n        \"if the ko atom is true, discard the model\"\r\n        if ctl.assignment.value(self.ko_atom):\r\n            adder = ctl.add_nogood  # behavior is the same with ctl.add_clause\r\n            lit = self.discard_atom\r\n            value = ctl.assignment.value(lit)\r\n            if SHOW_BUG:  # naïve implementation : send both lit and -lit whatever its value\r\n                clause = [lit, -lit]\r\n            elif value is None:  # working implementation : given arg depends on assignation\r\n                clause = [lit, -lit]\r\n            elif value is False:\r\n                clause = [lit]\r\n            elif value is True:\r\n                clause = [-lit]\r\n            if adder == ctl.add_nogood:  # note that 'is' does not behave as expected\r\n                clause = [-lit for lit in clause]\r\n            if not adder(clause) or not ctl.propagate():\r\n                return\r\n\r\n\r\ndef main(prg):\r\n    prg.register_propagator(Propagator())\r\n    prg.ground([('base', [])])\r\n    prg.solve()\r\n#end.\r\n\r\n\r\nok;ko.\r\n{p}.\r\n```\r\n\r\nRunning `clingo l.lp 0` will, in both 5.2.1 and 5.2.2 output the following:\r\n\r\n```\r\n[…]\r\nAnswer: 1\r\nok\r\nAnswer: 2\r\nok p\r\nAnswer: 3\r\nko\r\nAnswer: 4\r\nko p\r\nSATISFIABLE\r\n[…]\r\n```\r\n\r\nIt seems that the discarding is non functional. However, when choosing the arguments to add_clause/add_nogood according to the `p` atom value, it works (to enable that, set `SHOW_BUG` to `False`):\r\n\r\n```\r\n[…]\r\nAnswer: 1\r\nok\r\nAnswer: 2\r\nok p\r\nSATISFIABLE\r\n[…]\r\n```\r\n\r\nFew notes:\r\n\r\n- the naïve implementation consist in giving `[lit, -lit]` to add_clause/add_nogood, whatever the assigned value of `lit` is.\r\n- both add_nogood and add_clause are touched.\r\n- using any symbol (not necessarily `p`) to discard a model would lead to the same behavior.\r\n- using `propagate` instead of `check` in Propagator lead to the output of an invalid answer set, even with the working implementation.\r\n- `assert ctl.add_nogood is ctl.add_nogood` raises an assertion error. Not related to the problem here, but that's unexpected."},"comment":{"url":"https://api.github.com/repos/potassco/clingo/issues/comments/392341526","html_url":"https://github.com/potassco/clingo/issues/107#issuecomment-392341526","issue_url":"https://api.github.com/repos/potassco/clingo/issues/107","id":392341526,"user":{"login":"rkaminsk","id":1175198,"avatar_url":"https://avatars1.githubusercontent.com/u/1175198?v=4","gravatar_id":"","url":"https://api.github.com/users/rkaminsk","html_url":"https://github.com/rkaminsk","followers_url":"https://api.github.com/users/rkaminsk/followers","following_url":"https://api.github.com/users/rkaminsk/following{/other_user}","gists_url":"https://api.github.com/users/rkaminsk/gists{/gist_id}","starred_url":"https://api.github.com/users/rkaminsk/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/rkaminsk/subscriptions","organizations_url":"https://api.github.com/users/rkaminsk/orgs","repos_url":"https://api.github.com/users/rkaminsk/repos","events_url":"https://api.github.com/users/rkaminsk/events{/privacy}","received_events_url":"https://api.github.com/users/rkaminsk/received_events","type":"User","site_admin":false},"created_at":"2018-05-27T15:48:42Z","updated_at":"2018-05-27T15:48:42Z","author_association":"CONTRIBUTOR","body":"I cannot follow you. Adding a clause (or nogood) of form [lit,-lit] does not have any effect. Such a clause is always satisfied. Clingo's behavior looks alright to me."}}
{"actor":{"display_login":"rkaminsk"}}