[gecode-users] Constraint deduction in Gecode

[Guido Tack]

Mauricio Toro wrote:

> Hello all,
> 
> I am trying to do logic deduction in Gecode and I do not know how to do it.
> As an example, I have a,b,c as IntVars(0,100), d as BoolVar(0,1), and I have the constraints
> a > b, b> c and a > c <-> d. I want to be able to prove that a > c can be 
> deduced from a > b ^ b > c.
> 
> I tried using propagation and the value for d is [0..1].
> I also tried using search (branching over d) and the answer is 1, but if I change
> the constraints to a > f, b > c and a > c <-> d, the answer
> is also 1, which is not true in constraint deduction.
> 
> What can I do to implement the concept of constraint deduction in Gecode?

CP solvers solve existentially quantified problems: is there an assignment to the values that satisfies the constraints.  You are asking a universally quantified question: is it true that for /all/ assignments that satisfy a>b and b>c, it follows that a>c.  In your case, this could be answered by checking whether /all/ solutions to the problem have d=1.

There are solvers that handle these kinds of problems directly.  Have a look at quantified constraint solving, e.g. Qecode:
http://www.univ-orleans.fr/lifo/software/qecode/QeCode.html

Cheers,
	Guido

-- 
Guido Tack, http://people.cs.kuleuven.be/~guido.tack/