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

[Roland K. <kam...@cs...>]

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
> >> 
> >> 
> >> 
> > 
> > 
> 
>