Example: Pythagoras

Not all propagators exploit coreferences in products (e.g. x*x + y*y = z*z). For the example of this section it will be essential to exploit such coreferences, and you will learn how to do it.

The example also illustrates the case where a propagator for a redundant constraint improves the performance of a script by decreasing the number of necessary propagation steps, but without significantly changing the search tree.

Problem Specification

How many triples (A,B,C) exist such that A² + B² = C² and A$\le$B$\le$C$\le$1000?

Viewpoint and Constraints

The model has three variables A, B and C. Each variable is constrained to the finite domain 1 # 1000. The model imposes the constraints A² + B² = C² and A$\le$B$\le$C.

The script will also create a propagator for the redundant constraint 2 * B²$\ge$C².

Branching Strategy

We branch on the variables A, B, C using the standard first-fail strategy.

Script

fun pythagoras space =
   let
      (* problem variables *)
      val a = FD.range (space, (1, 1000))
      val b = FD.range (space, (1, 1000))
      val c = FD.range (space, (1, 1000))
      (* squares *)
      val aa = FD.range (space, (0, maxValue))
      val bb = FD.range (space, (0, maxValue))
      val cc = FD.range (space, (0, maxValue))
   in
      (* intermediate variables *)
      FD.mult (space, a, a, aa, FD.BND);
      FD.mult (space, b, b, bb, FD.BND);
      FD.mult (space, c, c, cc, FD.BND);
      (* problem constraints *)
      FD.linear (space, #[(1, aa), (1, bb), (~1, cc)], FD.EQ, 0, FD.BND);
      FD.rel (space, a, FD.LQ, b);
      FD.rel (space, b, FD.LQ, c);
      (* redundant constraint *)
      FD.linear (space, #[(2, bb), (~1, cc)], FD.GQ, 0, FD.BND);
      (* branching *)
      FD.branch (space, #[a, b, c], FD.B_SIZE_MIN, FD.B_MIN);
      {a, b, c}
   end

You can see, that for all squares new variables aa, bb, cc are introduced in Listing 15. This is a very important step in this script. As you already know, it is also possible to use the post - modelling tool. Then you would not need to write:

val aa = FD.range (space, (0, maxValue))
val bb = FD.range (space, (0, maxValue))
val cc = FD.range (space, (0, maxValue))
FD.mult (space, a, a, aa, FD.BND);
FD.mult (space, b, b, bb, FD.BND);
FD.mult (space, c, c, cc, FD.BND);
and
FD.linear (space,#[(1, aa), (1, bb), ( 1, cc)], FD.EQ, 0, FD.BND);

You just have to insert the following two new constraints:

post(space,FD(a) `* FD(a) `+ FD(b) `* FD(b) `= FD(c) `* FD(c),FD.DOM);

and replace

FD.linear (space, #[(2, bb), ( 1, cc)], FD.GQ, 0, FD.BND);

with

post(space,`2 `* FD(b) `* FD(b) `> FD(b) `* FD(b), FD.DOM);

This would result in a more readable and convenient script, but comparing the search trees of the two versions, the new version is worse. But why?

It is because of the variables aa, bb, cc. In the first version( Listing 15), the redundant constraint propagates stronger, because its variables are connected to the propagator ensuring the squares. In the second version they are independent.