$
$ Broken weights problem in Essence'.
$
$ From
$ http://www.mathlesstraveled.com/?p=701
$ """
$ Here's a fantastic problem I recently heard. Apparently it was first
$ posed by Claude Gaspard Bachet de Méziriac in a book of arithmetic problems
$ published in 1612, and can also be found in Heinrich Dorrie’s 100
$ Great Problems of Elementary Mathematics.
$
$ A merchant had a forty pound measuring weight that broke
$ into four pieces as the result of a fall. When the pieces were
$ subsequently weighed, it was found that the weight of each piece
$ was a whole number of pounds and that the four pieces could be
$ used to weigh every integral weight between 1 and 40 pounds. What
$ were the weights of the pieces?
$
$ Note that since this was a 17th-century merchant, he of course used a
$ balance scale to weigh things. So, for example, he could use a 1-pound
$ weight and a 4-pound weight to weigh a 3-pound object, by placing the
$ 3-pound object and 1-pound weight on one side of the scale, and
$ the 4-pound weight on the other side.
$ """
$
$ Model created by Hakan Kjellerstrand, hakank@gmail.com
$ See also my Essence'/Savile Row page: http://www.hakank.org/savile_row/
$
language ESSENCE' 1.0
letting n be 4 $ number of different weights
letting m be 40 $ original weight
letting range be domain int(1..n)
find weights: matrix indexed by [ range ] of int(1..m)
find x: matrix indexed by [int(1..m), range] of int(-1..1)
such that
$ symmetry breaking
forAll i: int(2..n) . weights[i-1] <= weights[i],
sum(weights) = m,
$ Check that all weights from 1 to 40 can be made.
$
$ Since all weights can be on either side
$ of the side of the scale we allow either
$ -1, 0, or 1 or the weights, assuming that
$ -1 is the weights on the left and 1 is on the right.
$
forAll j: int(1..m) . (sum i: range . x[j,i]*weights[i]) = j