Multi-threaded CP-SAT solver is crashed
What version of OR-tools and what language are you using?
Version: stable/v7.6
Language: C++ (Visual Studio 2019, version 16.5.4)
Which solver are you using (e.g. CP-SAT, Routing Solver, GLOP, BOP, Gurobi)
CP-SAT
What operating system (Linux, Windows, ...) and version?
Windows 10, build 18363.778
What did you do?
Solved the following multiple knapsacks problem using the CP-SAT solver
#include "ortools/sat/cp_model.h" struct DataModel { const std::vector<int> weights = { 48, 30, 42, 36, 36, 48, 42, 42, 36, 24, 30, 30, 42, 36, 36 }; const std::vector<int> values = { 10, 30, 25, 50, 35, 30, 15, 40, 30, 35, 45, 10, 20, 30, 25 }; const int num_items = (int)weights.size(); const std::vector<int> bin_capacities = { 100, 100, 100, 100, 100 }; const int num_bins = (int)bin_capacities.size(); }; namespace operations_research { namespace sat { void MulitpleKnapsackSat() { DataModel data; std::vector<BoolVar> variables(data.num_items * data.num_bins); auto x = [&](int item_index, int bin_index) -> BoolVar& { return variables[item_index * data.num_bins + bin_index]; }; CpModelBuilder cp_model; for (auto i = 0; i < data.num_items; ++i) { for (auto j = 0; j < data.num_bins; ++j) { x(i, j) = cp_model.NewBoolVar(); } } for (auto i = 0; i < data.num_items; ++i) { LinearExpr sum; for (auto j = 0; j < data.num_bins; ++j) { sum.AddTerm(x(i, j), 1); } cp_model.AddLessOrEqual(sum, 1); } for (auto j = 0; j < data.num_bins; ++j) { LinearExpr sum; for (auto i = 0; i < data.num_items; ++i) { sum.AddTerm(x(i, j), data.weights[i]); } cp_model.AddLessOrEqual(sum, data.bin_capacities[j]); } LinearExpr obj; for (auto i = 0; i < data.num_items; ++i) { for (auto j = 0; j < data.num_bins; ++j) { obj.AddTerm(x(i, j), data.values[i]); } } cp_model.Maximize(obj); SatParameters parameters; parameters.set_num_search_workers(16); const CpSolverResponse responce = SolveWithParameters(cp_model.Build(), parameters); } } // namespace sat } // namespace operations_research int main() { operations_research::sat::MulitpleKnapsackSat(); return EXIT_SUCCESS; }
What did you expect to see
Successful solving of the problem as the single-threaded solver does
What did you see instead?
The solver is crashed in the destructor LinearConstraintManager::~LinearConstraintManager() while trying to check the flag sat_parameters_.log_search_progress()
Make sure you include information that can help us debug (full error message, model Proto).
Anything else we should know about your project / environment
The library was built from the sources using cmake