rules/minion: apply weighted sum more often (negatives, equality)

[niklasdewally]

Based on PR #583

Chain of upstream PRs as of 2025-01-10

• PR Add absolute values and convert to Minion #583:
  main ← nik/pr/add-abs/01

  • PR rules/minion: apply weighted sum more often (negatives, equality) #584 (THIS ONE):
    nik/pr/add-abs/01 ← nik/pr/weighted-sum-neg-var

---

rules/minion: apply weighted sum more often (negatives, equality)

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.

• 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.

  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 inequalites. 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)).

  To fix this, this commit makes sum_eq_to_inequalities a higher
  priority than the flattening rules.

  A consequence of this is that more auxiliary variables are introduced
  than before, because non-flat expressions are being duplicated.

  For example:

  $ before
  
  (a/b) + c = d
  ~> __1 + c = d  [flatten_vecop]
  ~> __1 + c <= d /\ __1 + c >= d [sum_eq_to_inequalities]
  
  $ this commit
  
  (a/b) + c = d
  ~> (a/b) + c <= d /\ (a/b) + c >= d [sum_eq_to_inequalities]
  ~> __1 + c <= d  /\ __1 + c >= d    [flatten_vecop]
  

  I don't think this is a problem, however: because these are
  syntactically identical, CSE should easily merge them (once we
  implement it).

• Do not flatten sums inside leqs/geqs

  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)
  

  To fix this, this commit adds a special case to flatten_binop to
  ignore any Sum children of Leq and Geq.

[ozgurakgun]

I don't mind depending on identical-CSE in general.

To understand the issue better here: so in your first example c*e1 + d*e2 + .. = t, (where e1,e2 are non-flat you are saying c*e1 is extracted into an aux instead of just e1, right?

[niklasdewally]

I don't mind depending on identical-CSE in general.

To understand the issue better here: so in your first example c*e1 + d*e2 + .. = t, (where e1,e2 are non-flat you are saying c*e1 is extracted into an aux instead of just e1, right?

yes

[niklasdewally]

Looking again at abs-03, I think i'm missing a case here so will mark this as draft.

[niklasdewally]

Looking again at abs-03, I think i'm missing a case here so will mark this as draft.

I have one SumLeq / SumGeq left in the output, but I think it's the best I can do as the sum is inside an abs. May have missed a trick though!

[niklasdewally]

Savile row with -O0 also gets a SumLeq / SumGeq

MINION 3
**VARIABLES**
DISCRETE x #
{-5..2}
DISCRETE y #
{-5..2}
DISCRETE z #
{-5..2}
DISCRETE aux0 #|y|
{0..5}
DISCRETE aux1 #(aux0/2)
{0..2}
DISCRETE aux2 #(x/2)
{-3..1}
DISCRETE aux3 #(y - z + aux2)
{-10..8}
DISCRETE aux4 #|aux3|
{0..10}
**SEARCH**
PRINT[[x],[y],[z]]
VARORDER STATIC [x, y, z]
**CONSTRAINTS**
abs(aux0, y)
div(aux0, 2, aux1)
div(x, 2, aux2)
abs(aux4, aux3)
weightedsumleq([1,-1,1],[y,z,aux2],aux3)
weightedsumgeq([1,-1,1],[y,z,aux2],aux3)
sumleq([aux1,aux4],10)
sumgeq([aux1,aux4],10)
**EOF**

Conjure Oxide:

find x: int(-5..2)
find y: int(-5..2)
find z: int(-5..2)
find __0: int(0..10)
find __1: int(0..2)
find __2: int(0..10)
find __3: int(0..2)
find __4: int(-10..8)
find __5: int(-3..1)
find __6: int(-3..1)
find __7: int(0..5)
find __8: int(-10..8)
find __9: int(-3..1)
find __10: int(-3..1)
find __11: int(0..5)

such that

And([SumLeq([__0, __1], 10), SumGeq([__2, __3], 10)]),
AbsEq(__0,__4),
DivEq(__7, 2, __1),
AbsEq(__2,__8),
DivEq(__11, 2, __3),
And([FlatWeightedSumLeq([1, 1, -1],[__5, y, z],__4), FlatWeightedSumGeq([1, 1, -1],[__6, y, z],__4)]),
DivEq(x, 2, __5),
DivEq(x, 2, __6),
AbsEq(__7,y),
And([FlatWeightedSumLeq([1, 1, -1],[__9, y, z],__8), FlatWeightedSumGeq([1, 1, -1],[__10, y, z],__8)]),
DivEq(x, 2, __9),
DivEq(x, 2, __10),
AbsEq(__11,y)

[ozgurakgun]

Alternatively could you choose never to flatten inside Expr::Sum, would that work? This would make non-weighted sumleq and sumgeq also create duplicate aux variables, but would remove the need for that cycle check inside flatten_binop?

[niklasdewally]

Alternatively could you choose never to flatten inside Expr::Sum, would that work? This would make non-weighted sumleq and sumgeq also create duplicate aux variables, but would remove the need for that cycle check inside flatten_binop?

I think we need it to do things like:

( a + b + c/d) * d = e

Without flattening inside the sum:

( a + b + c/d) * d = e
~~> __1 * d = e with new constraint __1 =aux a + b + c/d

Then __1 would never get flattened.

[niklasdewally]

Originally I wanted to keep flattening in one place where possible.

I see that the other way potentially could reduce auxvar usage though...

[ozgurakgun]

Originally I wanted to keep flattening in one place where possible.

In fact i was going to suggest merging flatten_unary, flatten_binary and flatten_vector as well, so I am with you on that.

[ozgurakgun]

How about an alternative where we have a rule that matches a potential weighted sum expression, and does this style of auxiliary extraction in one go? I think you mentioned this as an option.

Main thing I don't like with the PR as it stands is the cycle breaking. If we had a high-priority rule that handles the weighted sums that would fit in well with the rest of the bag-of-rules.

[niklasdewally]

How about an alternative where we have a rule that matches a potential weighted sum expression, and does this style of auxiliary extraction in one go? I think you mentioned this as an option.

Main thing I don't like with the PR as it stands is the cycle breaking. If we had a high-priority rule that handles the weighted sums that would fit in well with the rest of the bag-of-rules.

I don't quite get what you mean - do you mean adding Eq handling inside the weighted sum rule?

I think going from sum eq to constraints in one step instead of via inequalities might be better for both weighted and normal sums actually - it should reduce the number of aux variables needed.

[ozgurakgun]

not sure what you mean with "Eq handling"

I think the special case is that you don't want to extract an aux for c*x (where c is a constant and x is an expression whose category is decision) instead you want to extract an aux for x only. This is a good idea if you are going to use a weighted sum constraint, otherwise the default aux-extractor/flattener can be used.

[niklasdewally]

Currently we do

1*x + 2*e  = 10   (where e is some non-atomic expression)

  ~~> sumeq_to_inequalities

1*x + 2*e <= 10 /\ 1*x + 2*e >= 10

-- 

1*x + 2*e <= 10

  ~~> introduce_weightedsumleq_sumgeq

flat_weightedsumleq([1,2],[x,__0],10)

with new top level constraints
 +  __0 =aux e

-- 

1*x + 2*e <= 10

  ~~> introduce_weightedsumleq_sumgeq

flat_weightedsumgeq([1,2],[x,__1],10)

with new top level constraints
 +  __1 =aux e

We could remove sumeq_to_inequalities, adding a case to introduce_weightedsumleq_sumgeq to handle expressions in the form <sum> = <expr>:

1*x + 2*e  = 10   (where e is some non-atomic expression)

  ~~> introduce_weightedsumleq_sumgeq

flat_weightedsumleq([1,2],[x,__0],10) /\
flat_weightedsumgeq([1,2],[x,__0],10)

with new top level constraints
 +  __0 =aux e

[niklasdewally]

@ozgurakgun I have done the above - see the amended commit message for details.

[ozgurakgun]

the rest of the PR looks good, see comment.

[niklasdewally]

MacOS CI failure due to #595