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/ _______________________________________________ Gecode users mailing list [email protected] https://www.gecode.org/mailman/listinfo/gecode-users
