[gecode-users] Learning in GeCode/SMT

[Guido Tack]

Just as a quick follow-up, Choco used to have a feature called  
explanations, which would probably do what you're looking for, but as  
far as I understand, they have been removed from the current release.

Cheers,
	Guido

Max wrote:

> At first am just forwarding my private mail contact with Guido Tack,  
> as
> it may be interesting to other on the mailing list.
>
> Thank you for the answer. Its a pity that the learning techniques have
> not made it into CSP yet.
> I want to integrate a CSP solver into an ASP Solver, a reasoning  
> system
> for logic programs.
> The advantage of learning from CSP solvers would be to get a good
> "reason" why literals/constraints can be propagated. SAT and ASP  
> systems
> use a learning approach based on "reasons" and conflict-learning. So  
> my
> system could use the reasons of the CSP solver to produce better
> conflicts and prune the search space. If it is not supported i will  
> have
> to use a trivial reason, which means a constraint rule applies because
> of all other constraint rules the same variable occurs in. But this
> reason is not very specific and is not very applicable for  
> backjumping.
>
> Maybe someone of the SMT (Sat Modulo Theory) area reads this message  
> and
> can provide information on how this is done in SMT Solvers, as they
> incorporate CSP into SAT and using learning techniques. But all  
> systems
> i found up to now seam to have written their own theory(CSP) solver.
> So if someone knows a CSP library capable of producing non trivial
> reasons and maybe doing conflict analysis, it would be great to post
> them here. Or maybe someone has an understaning how the SMT people do
> the things they do.
>
> Best regards,
>
> Max Ostrowski
>
>
>
>
>
>> Hi.
>>
>> Max wrote:
>> you probably already know me from the GeCode mailing list.
>> I just have a silly? question that i do not wanted to post on the  
>> list.
>> It regards learning in gecode.
>> I'm not very familiar with constraint programming but it seems to me
>> that things like backjumping and conflict learning already made it
>> into the current CSP systems.
>> Found a paper: Backjump-based backtracking for constraint  
>> satisfaction
>> problems by Rina Dechter and Daniel Frost
>>
>> So, does GeCode really not support learning and backjumping? Because
>> these features seem to be necessary for my diploma thesis and gecode
>> seems to be a state of the art CSP solver and one of the best  
>> looking.
>> So my first question would be: Why it is not supported? - and my
>> second barefaced question- : Do you know a similar CSP lib where it  
>> is
>> supported?
>
> It is not supported (and won't be in the near future), because no one
> knows how to do it properly.  The work by Dechter et al uses a naive
> model, where CSPs are represented entirely by binary constraints which
> are given as lists of allowed pairs of values.  In this setup,  
> learning
> is relatively straightforward.  In a realistic, propagation-based
> constraint solver, it is not.
> That also answers your second question: I don't know of any realistic
> library that does learning.  None of the commercial packages (ILOG
> Solver, SICStus Prolog, B-Prolog) incorporates learning, nor does  
> any of
> the other free libraries like Choco or Minion.  The closest you can  
> get
> is the work on "Propagation = Lazy Clause Generation"
> (http://www.cs.bgu.ac.il/~mcodish/Papers/Pages/cp07.html), this is the
> most promising attempt at using SAT learning technology for CP  
> solving I
> know of (but it's quite different from classic CP solvers).
>
> Btw, you can ask questions like this on the mailing list, no problem.
> It's about why we do/don't do certain things, so it definitely fits!
> Maybe you can elaborate how learning is important for what you want  
> to do.
>
> Cheers,
>    Guido
>
> _______________________________________________
> Gecode users mailing list
> users at gecode.org
> https://www.gecode.org/mailman/listinfo/gecode-users