fslaborg / flips

Fsharp LInear Programming System
https://flipslibrary.com/#/
MIT License
253 stars 32 forks source link

Correctness of evaluateNode #148

Closed TysonMN closed 3 years ago

TysonMN commented 3 years ago

I am suspicious of the correctness of evaluateNode. Unfortunately I still lack sufficient understanding to either convince myself that it is correct or be confident enough to know the correct behavior.

https://github.com/fslaborg/flips/blob/16a347c18cbfd7eb4c12d6c57dea31b56dd7b54d/Flips/Types.fs#L236-L254

I am surprised by the implementation of the AddLinearExpression case on line 251.

https://github.com/fslaborg/flips/blob/16a347c18cbfd7eb4c12d6c57dea31b56dd7b54d/Flips/Types.fs#L250-L251

The multiplier used in the continuation is the multiplier returned from recursing into the left expression. This could be different if that branch of the expression includes a Multiply case. Eventually the Empty case executes the continuation by passing in the multiplier it was given.

To see what I mean, consider the LinearExpression

Multiply (2.0, AddFloat (2.0, Empty)) + AddFloat (2.0, Empty)

The floats returned for it by evaluateNode are [ 4.0; 4.0 ], but I was expecting [ 4.0; 2.0 ] because I didn't think the Multiply on the left should change what the right returns (which would have been [ 2.0 ]).

The implementation I expected to see is

| AddLinearExpression (lExpr, rExpr) ->
    evaluateNode (multiplier, state) lExpr (fun _ -> evaluateNode (multiplier, state) rExpr cont)

Is this a bug? If not, why is this the correct behavior?

matthewcrews commented 3 years ago

I'm going to have to think about this. I'm wanting to setup a test which will validate correct/incorrect behavior. I will setup some tests tomorrow and see if we are getting the intended behavior.

TysonMN commented 3 years ago

If I tweak the expression, maybe it will be easier to tell if this is the correct behavior or not.

Multiply (2.0, AddFloat (2.0, Empty)) + AddFloat (-2.0, Empty)

I negated the last float. Now the actual output from evaluateNode is [ 4.0; -4.0 ], which then sums to 0. Instead, I expect the output of evaluateNode to be [ 4.0; -2.0 ], which sums to 2.

Now amplify this by replacing every occurrence of 2 with n for some large n. The actual output after summing remains 0 while I expect the the output after summing to be n / 2.

Should the output after summing be exactly 0 or arbitrarily far away from it?

matthewcrews commented 3 years ago

I'm going to have this fixed today and put out a new release

matthewcrews commented 3 years ago

It is definitely wrong.

This code:

let d = Decision.createBoolean "d1"
let e = 2.0 * (1.0 * d) + 1.0 * d
let r = LinearExpression.Reduce e

Produces

val r : ReducedLinearExpression =
  { DecisionTypes = dict [(DecisionName "d1", Boolean)]
    Coefficients = dict [(DecisionName "d1", 4.0)]
    Offset = 0.0 }

But should produce this

val r : ReducedLinearExpression =
  { DecisionTypes = dict [(DecisionName "d1", Boolean)]
    Coefficients = dict [(DecisionName "d1", 3.0)]
    Offset = 0.0 }

The reason that it is not causing a problem in our current code is that we don't have cases where we are multiplying LinearExpression in this way.

I believe this is the correct implementation:

| AddLinearExpression (lExpr, rExpr) ->
    evaluateNode (multiplier, state) lExpr (fun (_, lState) -> evaluateNode (multiplier, lState) rExpr cont)

The behavior would technically equivalent to what you proposed @TysonMN because the state is made up of mutable collections.

TysonMN commented 3 years ago

Yep, that implementation also works. I see the test you added in https://github.com/fslaborg/flips/commit/90f4940216328094acd0e57714dfc4c00e5b57e9. It looks great.