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

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

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