search

google / or-tools

Google's Operations Research tools:
https://developers.google.com/optimization/
Apache License 2.0
11.27k stars 2.13k forks source link

Negated boolean variables are getting corrupted in CPSAT #1238

Closed adihe closed 5 years ago

adihe commented 5 years ago

It appears that negated boolean variables can get corrupted in CPSAT. Maybe there is an other explanation for this issue.

Steps to reproduce:

                foreach (var k in CpSatUtils.DebugVars.Keys)
                {
                    ILiteral[] values = CpSatUtils.DebugVars[k];
                    foreach (var (i, var) in values.Select((x, i) => (i, x)))
                    {
                        sb.AppendLine($"dbg-cpsatutils {k}/{i} has value {solver.BooleanValue(var)}");
                    }
                }

Expected result: Values are printed.

Actual result: The boolean variables are printed out but the negated-boolean variables cause a crash in the C# wrapper of CPSAT: image

System: The version of cpsat is master / commit 6b1dce44bb71791eabfa8c5288875d53b2c1eafd The solving Parameters are solver.StringParameters = $"max_time_in_seconds:60.0;num_search_workers:6"; Also happened on latest stable version of cpsat.

Remarks: The model is an extended version of the nurse scheduling example. I noticed this issue due to the fact that I got many, many "false-positive" penalties on SoftSequenceConstraint:

        public static ILiteral[] NegatedBoundedSpan(IntVar[] works, int start, int length)
        {
            var sequence = new List<ILiteral>();

            if (start > 0)
                sequence.Add(works[start - 1]);

            foreach (var i in Range(length))
                sequence.Add(works[start + i].Not()); // <-- These values appear to get corrupt, causing false-positive penalties

            if (start + length < works.Length)
                sequence.Add(works[start + length]);

            return sequence.ToArray();
        }
lperron commented 5 years ago

it is not a corruption, just a bug. Laurent Perron | Operations Research | lperron@google.com | (33) 1 42 68 53 00

Le jeu. 2 mai 2019 à 09:26, adihe notifications@github.com a écrit :

It appears that negated boolean variables can get corrupted in CPSAT. Maybe there is an other explanation for this issue.

Steps to reproduce:

  • Solve this model -> https://www.dropbox.com/s/gppzzne9z62zqib/proto_3.txt?dl=0

  • Print out the boolean/negated-boolean variables as follows

            foreach (var k in CpSatUtils.DebugVars.Keys)
        {
            ILiteral[] values = CpSatUtils.DebugVars[k];
            foreach (var (i, var) in values.Select((x, i) => (i, x)))
            {
                sb.AppendLine($"dbg-cpsatutils {k}/{i} has value {solver.BooleanValue(var)}");
            }
        }

Expected result: Values are printed:

Actual result: The boolean variables are printed out but the negated-boolean variables cause a crash in the C# wrapper of CPSAT: [image: image] https://user-images.githubusercontent.com/19149841/57060670-7d18b980-6cba-11e9-912f-7f628c58b85b.png

System: The version of cpsat is master / commit 6b1dce4 https://github.com/google/or-tools/commit/6b1dce44bb71791eabfa8c5288875d53b2c1eafd The solving Parameters are solver.StringParameters = $"max_time_in_seconds:60.0;num_search_workers:6"; Also happened on latest stable version of cpsat.

Remarks: The model is an extended version of the nurse scheduling example. I noticed this issue due to the fact that I got many, many "false-positive" penalties on SoftSequenceConstraint:

    public static ILiteral[] NegatedBoundedSpan(IntVar[] works, int start, int length)
    {
        var sequence = new List<ILiteral>();

        if (start > 0)
            sequence.Add(works[start - 1]);

        foreach (var i in Range(length))
            sequence.Add(works[start + i].Not()); // <-- These values appear to get corrupt, causing false-positive penalties

        if (start + length < works.Length)
            sequence.Add(works[start + length]);

        return sequence.ToArray();
    }

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/google/or-tools/issues/1238, or mute the thread https://github.com/notifications/unsubscribe-auth/ACUPL3MGWDXDNGE7PCIN2XDPTKJRJANCNFSM4HJ36Z7Q .

adihe commented 5 years ago

Thanks alot for this very quick fix. I can confirm that reading negated boolean vars is working now with latest source from master.

However my original problem remains. I'll explain it a bit bitter - please let me know if I should create a separate issue instead.

In the method AddSoftSequenceConstraint of the sample https://github.com/google/or-tools/blob/master/examples/dotnet/ShiftSchedulingSat.cs it sais:

        // Penalize sequences that are below the soft limit.
        if (minCost > 0)
        {
            foreach (var length in Range(hardMin, softMin))
            {
                foreach (var start in Range(works.Length - length - 1))
                {
                    var span = NegatedBoundedSpan(works, start, length).ToList();
                    var name = $": under_span(start={start}, length={length})";
                    var lit = model.NewBoolVar(prefix + name);
                    span.Add(lit);
                    model.AddBoolOr(span);
                    costLiterals.Add(lit);
                    // We filter exactly the sequence with a short length.
                    // The penalty is proportional to the delta with softMin.
                    costCoefficients.Add(minCost * (softMin - length));
                }
            }
        }

So basically the last element (penalty) of span should only be true if all previous elements are false.

I am using this same AddSoftSequenceConstraint in my extended version and I see that often the last element (penalty) is true although one of the previous elements is true as well:

dbg-cpsatutils shift_constraint(employee 39, shift 5 Fa: under_span(start=7, length=1)/0 has name has value False
dbg-cpsatutils shift_constraint(employee 39, shift 5 Fa: under_span(start=7, length=1)/1 has name has value True
dbg-cpsatutils shift_constraint(employee 39 user, shift 5 Fa: under_span(start=7, length=1)/2 has name has value False
dbg-cpsatutils shift_constraint(employee 39 user, shift 5 Fa: under_span(start=7, length=1)/3 has name has value True

You can see from this log that both Elements span[1] and span[3] are TRUE.

How can this be fixed? Is there an additional call to model.AddImplication (or similar) necessary to ensure that the last element (penalty) of the span is only true if all previous Elements are false?

Thank you for your insights.

adihe commented 5 years ago

The following fix seems to work. If this is the proper way of doing it you might want to include it in the nurses sample code.

var span = NegatedBoundedSpan(works, start, length).ToList();
var name = $": under_span(start={start}, length={length})";
var lit = model.NewBoolVar(prefix + name);
span.Add(lit);
model.AddBoolOr(span);
costLiterals.Add(lit);
// We filter exactly the sequence with a short length.
 // The penalty is proportional to the delta with softMin.
costCoefficients.Add(minCost * (softMin - length));

// FIX: ensure the penalty is false if one of the other vars is true
foreach (var x in span.Take(span.Count - 1))
    model.AddImplication(x, lit.Not());
adihe commented 5 years ago

it is not a corruption, just a bug. Laurent Perron | Operations Research | lperron@google.com | (33) 1 42 68 53 00

Le jeu. 2 mai 2019 à 09:26, adihe notifications@github.com a écrit : …

I encountered a variation of this bug now (variable having positive index but index is still out of range). It seems the fix on master is not covering all cases. Please see screenshot below.

image

lperron commented 5 years ago

If this is the same problem you sent me, it has around 70k variables. Are you sure you have a solution when you query the value ? Laurent Perron | Operations Research | lperron@google.com | (33) 1 42 68 53 00

Le jeu. 2 mai 2019 à 15:03, adihe notifications@github.com a écrit :

it is not a corruption, just a bug. Laurent Perron | Operations Research | lperron@google.com | (33) 1 42 68 53 00

Le jeu. 2 mai 2019 à 09:26, adihe notifications@github.com a écrit : …

I encountered a variation of this bug now (variable having positive index but index is still out of range). It seems the fix on master is not covering all cases. Please see screenshot below.

[image: image] https://user-images.githubusercontent.com/19149841/57077037-4dce7080-6ceb-11e9-9420-ff7dfada8c85.png

— You are receiving this because you modified the open/close state. Reply to this email directly, view it on GitHub https://github.com/google/or-tools/issues/1238#issuecomment-488664009, or mute the thread https://github.com/notifications/unsubscribe-auth/ACUPL3LTBCFHA5O67V3VEKTPTLRBDANCNFSM4HJ36Z7Q .

adihe commented 5 years ago

Hello Laurent It was feasible solution of that I am sure. Next time I can reproduce it I will provide you another proto file.

lperron commented 5 years ago

I do not care about the proto if the bug is in the C# code :-)

Le ven. 3 mai 2019 à 11:50, adihe notifications@github.com a écrit :

Hello Laurent It was feasible solution of that I am sure. Next time I can reproduce it I will provide you another proto file.

— You are receiving this because you modified the open/close state. Reply to this email directly, view it on GitHub https://github.com/google/or-tools/issues/1238#issuecomment-489037380, or mute the thread https://github.com/notifications/unsubscribe-auth/ACUPL3K7O7U54TRWERRAMADPTQDEZANCNFSM4HJ36Z7Q .

lperron commented 5 years ago

Yes, I believe it also solve an issue in the python code too. Laurent Perron | Operations Research | lperron@google.com | (33) 1 42 68 53 00

Le jeu. 2 mai 2019 à 11:59, adihe notifications@github.com a écrit :

The following fix seems to work. If this is the proper way of doing it you might want to include it in the nurses sample code.

                        var span = NegatedBoundedSpan(works, start, length).ToList();
                        var name = $": under_span(start={start}, length={length})";
                        var lit = model.NewBoolVar(prefix + name);
                        span.Add(lit);
                        model.AddBoolOr(span);
                        costLiterals.Add(lit);
                        // We filter exactly the sequence with a short length.
                        // The penalty is proportional to the delta with softMin.
                        costCoefficients.Add(minCost * (softMin - length));

                        // FIX: ensure the penalty is false if one of the other vars is true
                        foreach (var x in span.Take(span.Count - 1))
                            model.AddImplication(x, lit.Not());

— You are receiving this because you modified the open/close state. Reply to this email directly, view it on GitHub https://github.com/google/or-tools/issues/1238#issuecomment-488617237, or mute the thread https://github.com/notifications/unsubscribe-auth/ACUPL3IALHWJYG26RKXT65LPTK3RRANCNFSM4HJ36Z7Q .