[gecode-users] Learning in GeCode/SMT

[Guido Tack]

Max wrote:
> 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.

The constraints are given in extension, as tables of allowed tuples  
(see e.g. Fig. 1).  And you're right, the techniques generalize to non- 
binary constraints, but I don't see how they generalize to non- 
extensional constraints.

The problem is that systems like Gecode, ILOG Solver, Choco, SICStus  
Prolog etc use propagators implementing the constraints.  This  
technique is not mentioned in Dechter's paper (it is similar to what  
they describe as "Backtracking with arc consistency" in 6.3).  When  
your constraints are implemented by propagators, it is much harder to  
explain the reason a certain value was removed from a domain.

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

Sure, learning is what makes SAT solvers so powerful.  It is an  
extremely interesting area of research, but it simply isn't understood  
well enough to integrate into propagation-based CP solvers yet.

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

I haven't found any benchmarks in that particular paper.  There are  
probably prototype implementations of the techniques, maybe you can  
ask the authors.

Cheers,
	Guido