Skip to content

Commit

Permalink
rules/minion: apply weighted sum more often (negatives, equality)
Browse files Browse the repository at this point in the history
These changes were motivated by the `basic/abs/03-flatten` test: it
should be a weighted sum, but is not. With this commit, this becomes a
weighted sum.

* Remove sumleq / sumgeq rules, and merge these into the weighted sum
  rule.

  The weighted sum rule returns not applicable near the end if a normal
  sum should be used. Instead of this, this commit builds the normal sum
  here and returns it.

* Add more cases to weighted sum, allowing negated expressions to be put
  inside the weighted sum.

  +  -x ~> (-1,x) where x is an atom
  +  -e ~> (-1,__1), with new constraint` __1=aux e`

  An alternative approach would be to add a normalisation rule `-e ~> -1
  * e`; however, I don't think this should only happen inside sums, not
  in general.

* Turn non-flat weighted sum equals expressions into weighted sums.

* Remove `sum_eq_to_inequalities` and handle `x + y = z` and `2*x + 3*y
  =z` cases directly inside `introduce_weightedsumleq_sumgeq`.

  Expressions of the form `c*e1 + d*e2 + .. = t`, (where e1,e2 are
  non-flat) were not being turned into weighted sums.

  `sum_eq_to_inequalities` needs to run before a sumeq can be turned
  into a weighted sum, as `introduce_weighted_sumleq_sumgeq` only works
  on inequalities. However, flattening has a higher priority than this
  rule, which makes `introduce_weighted_sumleq_sumgeq` unapplicable to these
  expressions. (see 2833c5f (Convert weighted sums to Minion, 2025-01-07)).

  Furthermore, the priority change above causes an infinite cycle to occur between
  `flatten_binop` and `sum_eq_to_inequalities`:

  ```
  sum([|a|, |b|]) = c

    ~~> sum_eq_to_inequalities

  (sum([|a|, |b|]) <= c /\ sum([|a|, |b|]) <= c)

  --

  sum([|a|, |b|]) <= c

    ~~> flatten_binop

   __1 <= c

   with new top level constraints:

   __1 =aux sum([|a| , |b|])

   --

  sum([|a|, |b|]) =aux __1

    ~~> sum_eq_to_inequalities

  (sum([|a|, |b|]) <= __1 /\ sum([|a|, |b|]) <= __1)
   ```

  Both of these issues are fixed in this commit by removing
  `sum_eq_to_inequalities` and handling sum equals inside this rule.
niklasdewally committed Jan 20, 2025
1 parent 9befb7f commit 9c3ccbb
Showing 77 changed files with 9,693 additions and 9,605 deletions.
Original file line number Diff line number Diff line change
@@ -9,9 +9,9 @@ such that

--

Sum([|x|, |y|]),
~~> flatten_generic ([("Minion", 4200)])
Sum([__0, __1])
(Sum([|x|, |y|]) = 10),
~~> introduce_weighted_sumleq_sumgeq ([("Minion", 4600)])
And([SumLeq([__0, __1], 10), SumGeq([__0, __1], 10)])
new variables:
__0: int(0..5)
__1: int(0..5)
@@ -32,24 +32,6 @@ AbsEq(__1,y)

--

(Sum([__0, __1]) = 10),
~~> sum_eq_to_inequalities ([("Minion", 4100)])
And([(Sum([__0, __1]) <= 10), (Sum([__0, __1]) >= 10)])

--

(Sum([__0, __1]) <= 10),
~~> introduce_sumleq ([("Minion", 4400)])
SumLeq([__0, __1], 10)

--

(Sum([__0, __1]) >= 10),
~~> introduce_sumgeq ([("Minion", 4400)])
SumGeq([__0, __1], 10)

--

Final model:

find x: int(-5..5)
Loading

0 comments on commit 9c3ccbb

Please sign in to comment.