Re: [Potassco-users] Debugging large problems with clingo/clasp

[Gamblin, T. <gam...@ll...>]

I should clarify this somewhat — I added assumptions to all the rules as you suggested, and I added all facts in the problem as assumptions after grounding.  So I *think* something from that set should show up in the core.

> On May 12, 2020, at 7:54 PM, Gamblin, Todd <gam...@ll...> wrote:
> 
> Roland:
> 
> Is it possible for an unsatisfiable problem not to produce any cores?  I’m seeing that with my program.  I’m doing it slightly differently from your example — I load a base program then add atoms and rules via the backend on the python side, ground, cleanup, and solve.
> 
> -Todd
> 
>> On May 12, 2020, at 2:05 PM, Gamblin, Todd <gam...@ll...> wrote:
>> 
>> Thanks!  This is actually much better, as I should be able to use it to tag the rules with something informative (e.g., and id for the original constraint from the package manager that generated the rule).
>> 
>> -Todd
>> 
>> 
>>> On May 12, 2020, at 1:44 PM, Roland Kaminski <kam...@cs...> wrote:
>>> 
>>> There must always be assumptions. If you want to trace something back to a 
>>> rule, then you could add an assumption to the rule body. For example:
>>> 
>>>  H :- B, assumption.
>>> 
>>> If `assumption` is in a core, then you know that the rule was causing a 
>>> problem. I assume (but have no experience) that it is important in general to 
>>> use as few assumptions as possible to maintain good solver performance.
>>> 
>>> Since you were talking about a package configuration problem, I could imagine 
>>> treating installed packages as assumptions. The core should then represent a 
>>> set of packages that cannot be installed simultaneously.
>>> 
>>> Anyway, have a look at the following example, how to use externals to tag 
>>> rules with assumptions. Note that unlike with assumptions the truth value of 
>>> externals persists between solve calls. To change their truth values you can 
>>> use `Control.symbol_atoms` together with `Control.assign_external`.
>>> 
>>> Hope this helps, -R
>>> 
>>> #script (python)
>>> 
>>> from clingo import Function
>>> 
>>> def main(prg):
>>>  cores = []
>>>  prg.ground([("base", [])])
>>>  prg.solve(on_core=lambda core: cores.append(core))
>>>  core = set(cores[-1])
>>>  print("core: {}".format(", ".join(str(atom.symbol)·
>>>      for atom in prg.symbolic_atoms
>>>      if atom.literal in core)))
>>> 
>>> #end.
>>> 
>>> q(1..3).
>>> 
>>> % create an external for all possible bodies `q(X)`
>>> #external e(X) : q(X). [true]
>>> % use the above external in the rule body
>>> p(X) :- q(X), e(X).
>>> 
>>> :- 2 { p(X) }.
>>> 
>>> On Tuesday, May 12, 2020 10:14:38 PM CEST Gamblin, Todd wrote:
>>>> Hi Roland:
>>>> 
>>>> Is there a way to know which rules and derived atoms in the logic program
>>>> made the cores unsatisfiable?  Or do the cores always have to be subsets of
>>>> the input assumptions?
>>> 
>>>> Todd
>>>> 
>>>> 
>>>> 
>>>>> On Apr 25, 2020, at 12:34 PM, Roland Kaminski <kam...@cs...>
>>>>> wrote:
>>> 
>>>>> Nice. It would be cool if you can send something that is small enough and
>>>>> easy 
>>> to understand to put in the examples folder. But don't feel
>>>>> obliged too. If there are problems/missing features please let us know.
>>>>> Maybe it is easy enough to implement. -R
>>>>> 
>>>>> On Saturday, April 25, 2020 7:56:23 PM CEST Gamblin, Todd wrote:
>>>>> 
>>>>>> Roland:
>>>>>> 
>>>>>> This is awesome! Thanks for adding the feature; it’ll be very helpful to
>>>>>> us.
>>> I’ll be able to try it out in the next couple weeks — if you’d like
>>>>>> me to send along use cases I can do that.
>>>>> 
>>>>> 
>>>>> 
>>>>>> Todd
>>>>>> 
>>>>>> 
>>>>>> ---
>>>>>> Sent from Workspace ONE Boxer<https://whatisworkspaceone.com/boxer>
>>>>>> 
>>>>>> On April 25, 2020 at 10:29:59 AM PDT, Roland Kaminski
>>>>>> <kam...@cs...> wrote:
>>>>> 
>>>>> Hi,
>>>>> 
>>>>>> 
>>>>>> meanwhile it is possible to get unsatisfiable cores from clingo. There
>>>>>> is
>>>>>> no
>>>>> 
>>>>> release including this feature yet but the latest wip branch should be
>>>>> 
>>>>>> quite stable. I did not come up with a meaningful example yet but you
>>>>>> can
>>>>>> have a look at one of test cases:
>>>>>> 
>>>>>> https://github.com/potassco/clingo/blob/wip/app/clingo/tests/python/core1
>>>>>> .lp
>>> 
>>>>> 
>>>>> 
>>>>> 
>>>>>> The returned core will contain a subset of the assumptions that made a
>>>>>> problem
>>>>> 
>>>>> unsatisfiable. There are no guarantees that the core is minimal
>>>>> 
>>>>>> though. If anyone finds the time to have a look and discovers bugs,
>>>>>> please
>>>>>> report in our issue tracker.
>>>>>> 
>>>>>> You can also install a development version using conda:
>>>>>> 
>>>>>> conda install -c potassco/label/dev clingo
>>>>>> 
>>>>>> -R
>>>>>> 
>>>>>> On Sunday, December 8, 2019 8:53:29 PM CEST Gamblin, Todd via
>>>>>> Potassco-users
>>>>> 
>>>>> wrote:
>>>>> 
>>>>>> 
>>>>>> 
>>>>>>> Hi Roland,
>>>>>>> 
>>>>>>> 
>>>>>>> 
>>>>>>> Sorry, I wasn’t clear. I have (so far) about 74 actual lines of problem
>>>>>>> encoding and 6000+ facts, which are generated from packages in Spack
>>>>>>> (https://github.com/spack/spack <https://github.com/spack/spack>).
>>>>>>> 
>>>>>>> 
>>>>>>> 
>>>>>>> Thanks for the examples — I’ll hack on this a bit longer using some of
>>>>>>> these
>>>>> 
>>>>> Ideas. The issue, though, is that if the debugging is manual,
>>>>> 
>>>>>>> it’ll be very hard to use clingo/clasp in an automated tool like Spack.
>>>>>>> The reasons why certain problem instances are unsatisfiable will
>>>>>>> eventually need to be reported to users, so having to manually weaken
>>>>>>> constraints, etc. to narrow down the conflicts is unworkable.
>>>>>>> 
>>>>>>> 
>>>>>>> 
>>>>>>> I am beginning to wonder whether I should use something like z3, which
>>>>>>> will
>>>>> 
>>>>> generate proofs and unsatisfiable cores. IMO its input language
>>>>> 
>>>>>>> isn’t quite as intuitive as ASP.
>>>>>>> 
>>>>>>> 
>>>>>>> 
>>>>>>> -Todd
>>>>>>> 
>>>>>>> 
>>>>>>> 
>>>>>>> 
>>>>>>>> On Dec 8, 2019, at 12:49 PM, Roland Kaminski
>>>>>>>> <kam...@cs...>
>>>>>>>> wrote:
>>>>>>>> 
>>>>>>>> 
>>>>>>>> 
>>>>>>>> On another note, I do not know exactly what you mean by 6000+
>>>>>>>> constraints.
>>>>>>>> If your *encoding* consists of 6000+ constraints, then you should
>>>>>>>> consider thinking about the representation of your problem. Typically,
>>>>>>>> it
>>>>>>>> is a good idea to separate ASP programs into a *large* number of facts
>>>>>>>> and a *small* problem encoding. If your constraints share structure,
>>>>>>>> better generate them from facts. To give a contrived example, consider
>>>>>>>> the program
>>>>>>>> 
>>>>>>>> 
>>>>>>>> 
>>>>>>>> 
>>>>>>>> :- p(a), p(b).
>>>>>>>> :- p(b), p(c).
>>>>>>>> :- p(c), p(d).
>>>>>>>> 
>>>>>>>> 
>>>>>>>> 
>>>>>>>> 
>>>>>>>> which could be represented as:
>>>>>>>> mutex(a,b).
>>>>>>>> mutex(b,c).
>>>>>>>> mutex(c,d).
>>>>>>>> 
>>>>>>>> 
>>>>>>>> 
>>>>>>>> 
>>>>>>>> :- mutex(X,Y), p(X), p(Y).
>>>>>>>> 
>>>>>>>> 
>>>>>>>> 
>>>>>>>> 
>>>>>>>> The latter encoding will also be easier to debug by hand using some
>>>>>>>> ideas
>>>>>>>> from my previous email. -R
>>>>>>>> 
>>>>>>>> 
>>>>>>>> 
>>>>>>>> On Sunday, December 8, 2019 5:45:46 PM CET Gamblin, Todd via
>>>>>>>> Potassco-users
>>>>>>>> 
>>>>>>>> 
>>>>>>>> 
>>>>>>>> wrote:
>>>>>>>> 
>>>>>>>> 
>>>>>>>>> Hi all,
>>>>>>>>> 
>>>>>>>>> 
>>>>>>>>> 
>>>>>>>>> I’m curious whether there are any good ways to debug large ASP
>>>>>>>>> programs
>>>>>>>>> with clasp. I’m running through clingo and don’t see many options
>>>>>>>>> that’ll tell me *why* something is unsatisfiable. I’ve asked some
>>>>>>>>> more
>>>>>>>>> specific questions on here before (e.g., about minimal unsatisfiable
>>>>>>>>> cores and whether they can be displayed), but I haven’t asked the
>>>>>>>>> general question — how do you debug clasp programs?
>>>>>>>>> 
>>>>>>>>> 
>>>>>>>>> 
>>>>>>>>> I’m generating some pretty large programs (6,000+ constraints), so
>>>>>>>>> the
>>>>>>>>> traditional method of uncommenting constraints to sort things out is
>>>>>>>>> becoming quite difficult.
>>>>>>>>> 
>>>>>>>>> 
>>>>>>>>> 
>>>>>>>>> -Todd
>>>>>>>> 
>>>>>>>> 
>>>>>>>> 
>>>>>>>> 
>>>>>>>> _______________________________________________
>>>>>>>> Potassco-users mailing list
>>>>>>>> Pot...@li...
>>>>>>>> https://lists.sourceforge.net/lists/listinfo/potassco-users
>>>>>> 
>>>>>> 
>>>>>> 
>>>>> 
>>>>> 
>>>> 
>>>> 
>>> 
>>> 
>>> 
>>> 
>> 
>