Understanding performance loss of solving my model with SatSolver in comparison to CspSolver

[ptr1120]

I am successfully using the ortools (old) CspSolver, but I want to migrate to the ortools SatSolver (.Net).

Therefore I converted my complex constraints to cnf (normal form) and compared the performance to the CspSolver. A typical model has for example 500 constraints, 200 variables (all boolean). I am not using reified variables. I am only interested in the feasibility of the constraint model under certain constraints. Since my constraints are in normal form I only use or and and constraints with possible negated literals.

Problem is now that I realized a massive loss of performance when using the SatSolver in comparison to the CspSolver. With the same problem, the CspSolver is around 7 times faster than the SatSolver. Even if I feed the CspSolver with the same problem in cnf it is reproducible 5 times faster. The result (feasibillity) of the solving with both solvers is correct, only the performance impact is not understandable for me.

Are there any ideas what I may be doing wrong here, or on how I can improve the performance of the solving with the SatSolver? Or may this be a problem of the .net layer over the ortools?

Best regards Peter

[lperron]

can you send me the code?

[lperron]

are we talking minutes? seconds?

[lperron]

Did you expand everything to SAT? Did you look at the CP layer?

[ptr1120]

It's difficult to send code, I could send constraints. Not minutes or seconds, I mean ratio, so e.g. 7 times (7*x) faster.

Did you expand everything to SAT? Did you look at the CP layer?

I do not understand what you mean, can you explain?

[lperron]

About runtime, the CP-SAT solver has a higher setup time. This if total runtime is 0.05s, there will be a slowdown.

The CP-SAT solver supports integer variables, global CP constraints, scheduling, routing. From your mail, I understand you rewrote everything to a pure sat model. Is it true? Did the original CP model pure boolean?

Le dim. 27 janv. 2019 à 05:36, Peter Bruch notifications@github.com a écrit :

It's difficult to send code, I could send constraints. Not minutes or seconds, I mean ratio, so e.g. 7 times (7*x) faster.

Did you expand everything to SAT? Did you look at the CP layer?

I do not understand what you mean, can you explain?

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/google/or-tools/issues/1028#issuecomment-457918513, or mute the thread https://github.com/notifications/unsubscribe-auth/AKj17RewwE0rJKRHF8Ygs3dgROlFv5Qpks5vHatMgaJpZM4aUt-n .

[ptr1120]

Yes I also realized the initial solving with the CP-Sat is longer. But also following solvings take more time. Yes, I rewrote the complete model to a pure sat model (conjunctive normal form), my testmodel has only boolean variables (also original CP model has only booleans).

I wrote a simple comparison test in C# that shows the difference. I added 500 boolean variables, 25 or constraints, 25 and constraints and assigned every second variable, then I solve the same model 5 times. The problem is feasible.

[Test]
 public void Sat()
 {
     var model = new CpModel();
     var solver = new CpSolver();
     var variables = new List<IntVar>();
     for (var i = 0; i < 500; i++)
     {
         variables.Add(model.NewBoolVar(i.ToString()));
     }

     // add constraints
     for (var i = 0; i < 25; i++)
     {
         model.AddBoolAnd(variables.Skip(i * 10).Take(10));
     }

     for (var j = 25; j < 50; j++)
     {
         model.AddBoolOr(variables.Skip(j * 10).Take(10).Select((v, i) => i % 3 == 0 ? v : v.Not()));
     }

     // assign some vars
     var k = 0;
     foreach (var variable in variables)
     {
         if (k++ % 2 == 0)
         {
             model.Add(variable == 1);
         }
     }

     // solve
     for (var i = 0; i < 5; i++)
     {
         var sw = Stopwatch.StartNew();
         var isFeasible = solver.Solve(model) == CpSolverStatus.Feasible;
         sw.Stop();
         Console.WriteLine(isFeasible);
         Console.WriteLine(sw.ElapsedMilliseconds);
     }
 }

[Test]
public void Csp()
{
    var solver = new Google.OrTools.ConstraintSolver.Solver("test");
    var variables = new List<Google.OrTools.ConstraintSolver.IntVar>();
    for (var i = 0; i < 500; i++)
    {
        variables.Add(solver.MakeBoolVar(i.ToString()));
    }

    // add constraints
    for (var i = 0; i < 25; i++)
    {
        solver.Add(variables.Skip(i * 10).Take(10).Aggregate((left, right) => left * right == 1) == 1);
    }

    for (var j = 25; j < 50; j++)
    {
        var orTerm = variables.Skip(j * 10).Take(10).Select((v, i) => i % 3 == 0 ? v : 1 - v);
        solver.Add(orTerm.Aggregate((left, right) => left + right >= 1) == 1);
    }

    // assign some vars
    var k = 0;
    foreach (var variable in variables)
    {
        if (k++ % 2 == 0)
        {
            solver.Add(variable == 1);
        }
    }

    for (var i = 0; i < 5; i++)
    {
        var sw = Stopwatch.StartNew();
        using (var decisionBuilder = solver.MakePhase(variables.ToArray(),
            Google.OrTools.ConstraintSolver.Solver.CHOOSE_FIRST_UNBOUND, Google.OrTools.ConstraintSolver.Solver.ASSIGN_MIN_VALUE))
        {
            solver.NewSearch(decisionBuilder);
            var isFeasible = solver.NextSolution();
            solver.EndSearch();
            sw.Stop();
            Console.WriteLine(isFeasible);
            Console.WriteLine(sw.ElapsedMilliseconds);
        }
    }
}

The results: CpSat: initial solving time 37 ms all following solvings 3ms. Original Solver: initial solving time 4 ms all following solvings 0ms.

This test does not have same complexity to the constraints of my real test-model (with the 500 constraints), thats why the performance difference may be not as strong.

[lperron]

Most likely, the 37ms correspond to the loading of the protobuf assembly. Laurent Perron | Operations Research | lperron@google.com | (33) 1 42 68 53 00

Le dim. 27 janv. 2019 à 08:18, Peter Bruch notifications@github.com a écrit :

Yes I also realized the initial solving with the CP-Sat is longer. But also following solvings take more time. Yes, I rewrote the complete model to a pure sat model (conjunctive normal form), my testmodel has only boolean variables (also original CP model has only booleans).

I wrote a simple comparison test in C# that shows the difference. I added 500 boolean variables, 25 or constraints, 25 and constraints and assigned every second variable, then I solve the same model 5 times. The problem is feasible.

[Test] public void Sat() { var model = new CpModel(); var solver = new CpSolver(); var variables = new List(); for (var i = 0; i < 500; i++) { variables.Add(model.NewBoolVar(i.ToString())); }

 // add constraints
 for (var i = 0; i < 25; i++)
 {
     model.AddBoolAnd(variables.Skip(i * 10).Take(10));
 }

 for (var j = 25; j < 50; j++)
 {
     model.AddBoolOr(variables.Skip(j * 10).Take(10).Select((v, i) => i % 3 == 0 ? v : v.Not()));
 }

 // assign some vars
 var k = 0;
 foreach (var variable in variables)
 {
     if (k++ % 2 == 0)
     {
         model.Add(variable == 1);
     }
 }

 // solve
 for (var i = 0; i < 5; i++)
 {
     var sw = Stopwatch.StartNew();
     var isFeasible = solver.Solve(model) == CpSolverStatus.Feasible;
     sw.Stop();
     Console.WriteLine(isFeasible);
     Console.WriteLine(sw.ElapsedMilliseconds);
 }

}

[Test] public void Csp() { var solver = new Google.OrTools.ConstraintSolver.Solver("test"); var variables = new List(); for (var i = 0; i < 500; i++) { variables.Add(solver.MakeBoolVar(i.ToString())); }

// add constraints
for (var i = 0; i < 25; i++)
{
    solver.Add(variables.Skip(i * 10).Take(10).Aggregate((left, right) => left * right == 1) == 1);
}

for (var j = 25; j < 50; j++)
{
    var orTerm = variables.Skip(j * 10).Take(10).Select((v, i) => i % 3 == 0 ? v : 1 - v);
    solver.Add(orTerm.Aggregate((left, right) => left + right >= 1) == 1);
}

// assign some vars
var k = 0;
foreach (var variable in variables)
{
    if (k++ % 2 == 0)
    {
        solver.Add(variable == 1);
    }
}

for (var i = 0; i < 5; i++)
{
    var sw = Stopwatch.StartNew();
    using (var decisionBuilder = solver.MakePhase(variables.ToArray(),
        Google.OrTools.ConstraintSolver.Solver.CHOOSE_FIRST_UNBOUND, Google.OrTools.ConstraintSolver.Solver.ASSIGN_MIN_VALUE))
    {
        solver.NewSearch(decisionBuilder);
        var isFeasible = solver.NextSolution();
        solver.EndSearch();
        sw.Stop();
        Console.WriteLine(isFeasible);
        Console.WriteLine(sw.ElapsedMilliseconds);
    }
}

}

The results: CpSat: initial solving time 37 ms all following solvings 3ms. Original Solver: initial solving time 4 ms all following solvings 0ms.

This test does not have same complexity to the constraints of my real test-model (with the 500 constraints), thats why the performance difference may be not as strong.

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/google/or-tools/issues/1028#issuecomment-457931534, or mute the thread https://github.com/notifications/unsubscribe-auth/AKj17ZsInD4pYQ3j20jsXh7U23Tby57Iks5vHdFsgaJpZM4aUt-n .

[ptr1120]

The initial solving time is no problem for me. The problem is the following solving times. I need to solve the model really a lot of times under different constraints. In this case the old solver takes mostly 0-1ms and the CpSat solver needs around 6-7 ms for the more complex model.

[lperron]

You can try disabling presolve to see if this is the cause of the slowdown.

https://github.com/google/or-tools/blob/master/ortools/sat/doc/solver.md#specifying-the-time-limit-in-c-1

Parameter is https://github.com/google/or-tools/blob/master/ortools/sat/sat_parameters.proto#L606, or just the SAT part below. You can also set linearization_level to 0. Laurent Perron | Operations Research | lperron@google.com | (33) 1 42 68 53 00

Le dim. 27 janv. 2019 à 23:04, Peter Bruch notifications@github.com a écrit :

The initial solving time is no problem for me. The problem is the following solving times. I need to solve the model really a lot of times under different constraints. In this case the old solver takes mostly 0-1ms and the CpSat solver needs around 6-7 ms for the more complex model.

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/google/or-tools/issues/1028#issuecomment-458018708, or mute the thread https://github.com/notifications/unsubscribe-auth/AKj17axt-hfjDwdCX75c93CfTjmCPBB4ks5vHqD1gaJpZM4aUt-n .

[ptr1120]

Thank you, lperron, the influence of these parameters is interesting, I made several tests with different parameters based on a common constraint model with 500 constraints (in cnf), 200 variables (all boolean). All solvers same model. All times are mean milliseconds of multiple tests. During the test them model is solved around 500 times with the same algorithm.

1. Without setting sat_parameters: ortools CP Solver: 340 ms ortools CPSat solver: 2100 ms Microsoft solver foundation solver: 1220 ms

2. cp_model_presolve=false ortools CPSat solver: 1650 ms

3. linearization_level:0 ortools CPSat solver: 2100 ms

4. cp_model_probing_level:0 ortools CPSat solver: 1800 ms

5. cp_model_presolve:false;cp_model_probing_level:0 ortools CPSat solver: 1500 ms

6. cp_model_presolve:false;linearization_level:0;cp_model_probing_level:0 ortools CPSat solver: 1400 ms

With the last parameters the original CP solver is only 4 times faster than the CPSat solver but unfortunately still slower than the microsoft solver. Do you have another hint for me?

Regards, Peter

[lperron]

Can you send me the proto:

model.Model.ToString() Laurent Perron | Operations Research | lperron@google.com | (33) 1 42 68 53 00

Le lun. 28 janv. 2019 à 08:03, Peter Bruch notifications@github.com a écrit :

Thank you, lperron, the influence of these parameters is interesting, I made several tests with different parameters based on a common constraint model with 500 constraints (in cnf), 200 variables (all boolean). All solvers same model. All times are mean milliseconds of multiple tests.

1.

Without setting sat_parameters: ortools CP Solver: 340 ms ortools CPSat solver: 2100 ms Microsoft solver foundation solver: 1220 ms 2.

cp_model_presolve=false ortools CPSat solver: 1650 ms 3.

linearization_level:0 ortools CPSat solver: 2100 ms 4.

cp_model_probing_level:0 ortools CPSat solver: 1800 ms 5.

cp_model_presolve:false;cp_model_probing_level:0 ortools CPSat solver: 1500 ms 6.

cp_model_presolve:false;linearization_level:0;cp_model_probing_level:0 ortools CPSat solver: 1400 ms

With the last parameters the original CP solver is only 4 times faster than the CPSat solver but unfortunately still slower than the microsoft solver. Do you have another hint for me?

Regards, Peter

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/google/or-tools/issues/1028#issuecomment-458190830, or mute the thread https://github.com/notifications/unsubscribe-auth/AKj17ewlzTo-u2UtGVHk8OJPYjumZTLTks5vHx9mgaJpZM4aUt-n .

[lperron]

Dead issue. Closing