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

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

Hi, just to show that it is possible, here is an encoding to enumerate all 
subset-minimal unsatisfiable cores of a CNF. But beware that such encodings 
usually don't scale well.

You can run
  
  clingo test.lp --heuristic=domain --enum-mode=domRec 0 --dom-mod=false,show

to enumerate all subset-minimal unsatisfiable cores.

I tried to explain the encoding in the comments. You probably see that 
modeling like this is not very intuitive. -R

On Sunday, December 8, 2019 10:26:15 PM CET Roland Kaminski wrote:
> Hi, sorry do hear that. Even with the minimization idea, you won't get
> something like unsatisfiable cores. In theory it is possible to calculate
> unsatisfiable cores with disjunctive logic programs. But such programs
> typically do not scale well (and are hard to understand and write). I doubt
> very much that it could handle more than a handful of packages.
> 
> On another note, did you have a look at https://github.com/openSUSE/libsolv?
> I have never looked at it but it sounds like it can do what you need... -R
> 
> On Sunday, December 8, 2019 9:53:29 PM CET 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