[gecode-users] Learning in GeCode/SMT

[Max]

Thank you for the advice with Choco, i will have a look at, but 
currently i tend to use GeCode.

    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.


I finally managed to read "Dechter - Backjump-based backtracking for 
constraint satisfaction" and i think it is not restricted to Binary 
Constraints, because it is mentioned several times. And i have not found 
the list of allowed pairs in the paper, i thought of nogoods as set of 
domains, not explicit values. But i can not evaluate the possibilities, 
because i have no idea of how constraint solver do work. I hope the CSP 
community will have access to learning algorithms in the future, because 
i see a huge potential in them.
By the way, can anybody say how the Benchmarks of the paper were made if 
no implementations exists of such solvers. I haven't found that in the text.


Best regards,

Max Ostrowski




Guido Tack wrote:
> 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
>>     
>
>
> _______________________________________________
> Gecode users mailing list
> users at gecode.org
> https://www.gecode.org/mailman/listinfo/gecode-users
>
>