[gecode-users] Learning in GeCode/SMT

[Max]

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