diff --git a/ortools/base/file.cc b/ortools/base/file.cc index 41f9ed937d..c9cd2e08f2 100644 --- a/ortools/base/file.cc +++ b/ortools/base/file.cc @@ -263,6 +263,16 @@ void WriteProtoToFileOrDie(const google::protobuf::Message& proto, CHECK(WriteProtoToFile(proto, file_name)) << "file_name: " << file_name; } +util::Status GetTextProto(const absl::string_view& filename, + google::protobuf::Message* proto, int flags) { + if (flags == Defaults()) { + if (ReadFileToProto(filename, proto)) return util::Status::OK; + } + return util::Status( + util::error::INVALID_ARGUMENT, + absl::StrCat("Could not read proto from '", filename, "'.")); +} + util::Status SetTextProto(const absl::string_view& filename, const google::protobuf::Message& proto, int flags) { if (flags == Defaults()) { diff --git a/ortools/base/file.h b/ortools/base/file.h index 651f11fefc..048d1d2941 100644 --- a/ortools/base/file.h +++ b/ortools/base/file.h @@ -123,6 +123,8 @@ util::Status Open(const absl::string_view& filename, const absl::string_view& mode, File** f, int flags); File* OpenOrDie(const absl::string_view& filename, const absl::string_view& mode, int flags); +util::Status GetTextProto(const absl::string_view& filename, + google::protobuf::Message* proto, int flags); util::Status SetTextProto(const absl::string_view& filename, const google::protobuf::Message& proto, int flags); util::Status SetBinaryProto(const absl::string_view& filename, diff --git a/ortools/base/random.cc b/ortools/base/random.cc index 95ae0f92b5..6f4621aae2 100644 --- a/ortools/base/random.cc +++ b/ortools/base/random.cc @@ -37,9 +37,7 @@ uint32 ACMRandom::Next() { return absl::uniform_int_distribution(0, kuint32max)(generator_); } -uint32 ACMRandom::Uniform(uint32 n) { - return n == 0 ? 0 : Next() % n; -} +uint32 ACMRandom::Uniform(uint32 n) { return n == 0 ? 0 : Next() % n; } uint64 ACMRandom::Next64() { return absl::uniform_int_distribution(0, kuint64max)(generator_); diff --git a/ortools/base/random.h b/ortools/base/random.h index 8cb07fd8dc..643fc2ac8d 100644 --- a/ortools/base/random.h +++ b/ortools/base/random.h @@ -60,6 +60,7 @@ class MTRandom : public ACMRandom { : ACMRandom(GenerateInt32SeedFromString(str_seed)) {} MTRandom() : ACMRandom(ACMRandom::HostnamePidTimeSeed()) {} + private: int32 GenerateInt32SeedFromString(const std::string& str) { uint32 seed = 1234567; diff --git a/ortools/constraint_solver/routing.h b/ortools/constraint_solver/routing.h index 58f6a3a417..10cadbeaba 100644 --- a/ortools/constraint_solver/routing.h +++ b/ortools/constraint_solver/routing.h @@ -3238,7 +3238,7 @@ class SavingsFilteredHeuristic : public RoutingFilteredHeuristic { private: /// Used when add_reverse_arcs_ is true. - /// Given the vector of adjacency lists of a graph, adds symetric arcs not + /// Given the vector of adjacency lists of a graph, adds symmetric arcs not /// already in the graph to the adjacencies (i.e. if n1-->n2 is present and /// not n2-->n1, then n1 is added to adjacency_matrix[n2]. // clang-format off diff --git a/ortools/constraint_solver/routing_search.cc b/ortools/constraint_solver/routing_search.cc index 1a101cbc01..24f187215f 100644 --- a/ortools/constraint_solver/routing_search.cc +++ b/ortools/constraint_solver/routing_search.cc @@ -2218,8 +2218,6 @@ class VehicleVarFilter : public BasePathFilter { public: explicit VehicleVarFilter(const RoutingModel& routing_model); ~VehicleVarFilter() override {} - bool Accept(const Assignment* delta, const Assignment* deltadelta, - int64 objective_min, int64 objective_max) override; bool AcceptPath(int64 path_start, int64 chain_start, int64 chain_end) override; std::string DebugString() const override { return "VehicleVariableFilter"; } @@ -2244,38 +2242,17 @@ VehicleVarFilter::VehicleVarFilter(const RoutingModel& routing_model) } } -// Avoid filtering if variable domains are unconstrained. -bool VehicleVarFilter::Accept(const Assignment* delta, - const Assignment* deltadelta, int64 objective_min, - int64 objective_max) { - if (IsDisabled()) return true; - const Assignment::IntContainer& container = delta->IntVarContainer(); - const int size = container.Size(); - bool all_unconstrained = true; - for (int i = 0; i < size; ++i) { - int64 index = -1; - if (FindIndex(container.Element(i).Var(), &index) && - IsVehicleVariableConstrained(index)) { - all_unconstrained = false; - break; - } - } - if (all_unconstrained) return true; - return BasePathFilter::Accept(delta, deltadelta, objective_min, - objective_max); -} - bool VehicleVarFilter::AcceptPath(int64 path_start, int64 chain_start, int64 chain_end) { const int64 vehicle = start_to_vehicle_[path_start]; - int64 node = path_start; - while (node < Size()) { + int64 node = chain_start; + while (node != chain_end) { if (!vehicle_vars_[node]->Contains(vehicle)) { return false; } node = GetNext(node); } - return true; + return vehicle_vars_[node]->Contains(vehicle); } bool VehicleVarFilter::DisableFiltering() const { diff --git a/ortools/graph/io.h b/ortools/graph/io.h index d4e3f1f8d2..dd70a7a495 100644 --- a/ortools/graph/io.h +++ b/ortools/graph/io.h @@ -34,7 +34,7 @@ namespace util { -// Returns a std::string representation of a graph. +// Returns a string representation of a graph. enum GraphToStringFormat { // One arc per line, eg. "3->1". PRINT_GRAPH_ARCS, diff --git a/ortools/linear_solver/gurobi_proto_solver.cc b/ortools/linear_solver/gurobi_proto_solver.cc index 95c53abe29..9a6a8802cb 100644 --- a/ortools/linear_solver/gurobi_proto_solver.cc +++ b/ortools/linear_solver/gurobi_proto_solver.cc @@ -291,7 +291,7 @@ util::StatusOr GurobiSolveProto( if (request.has_solver_specific_parameters()) { const auto parameters_status = SetSolverSpecificParameters( - request.solver_specific_parameters(), gurobi); + request.solver_specific_parameters(), GRBgetenv(gurobi_model)); if (!parameters_status.ok()) { response.set_status(MPSOLVER_MODEL_INVALID_SOLVER_PARAMETERS); response.set_status_str(parameters_status.error_message()); diff --git a/ortools/linear_solver/java/linear_solver.i b/ortools/linear_solver/java/linear_solver.i index 74ddaff6bc..783576bbd9 100644 --- a/ortools/linear_solver/java/linear_solver.i +++ b/ortools/linear_solver/java/linear_solver.i @@ -86,7 +86,8 @@ PROTO2_RETURN( * Loads a model and returns the error message, which will be empty iff the * model is valid. */ - std::string loadModelFromProto(const operations_research::MPModelProto& input_model) { + std::string loadModelFromProto( + const operations_research::MPModelProto& input_model) { std::string error_message; $self->LoadModelFromProto(input_model, &error_message); return error_message; diff --git a/ortools/linear_solver/samples/mip_var_array.py b/ortools/linear_solver/samples/mip_var_array.py index 2663f843bd..884174038f 100644 --- a/ortools/linear_solver/samples/mip_var_array.py +++ b/ortools/linear_solver/samples/mip_var_array.py @@ -10,7 +10,7 @@ # WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. # See the License for the specific language governing permissions and # limitations under the License. -"""Integer programming examples that show how to use the APIs.""" +"""MIP example that uses a variable array.""" # [START program] # [START import] from __future__ import print_function @@ -23,7 +23,6 @@ from ortools.linear_solver import pywraplp def create_data_model(): """Stores the data for the problem.""" data = {} - # Locations in block units data['constraint_coeffs'] = [ [5, 7, 9, 2, 1], [18, 4, -9, 10, 12], @@ -50,6 +49,7 @@ def main(): solver = pywraplp.Solver('simple_mip_program', pywraplp.Solver.CBC_MIXED_INTEGER_PROGRAMMING) # [END solver] + # [START variables] infinity = solver.infinity() x = {} diff --git a/ortools/linear_solver/samples/simple_mip_program.py b/ortools/linear_solver/samples/simple_mip_program.py index 167b5584db..9df03bd43a 100644 --- a/ortools/linear_solver/samples/simple_mip_program.py +++ b/ortools/linear_solver/samples/simple_mip_program.py @@ -50,20 +50,17 @@ def main(): # [END objective] # [START solve] - result_status = solver.Solve() - # The problem has an optimal solution. - assert result_status == pywraplp.Solver.OPTIMAL - - # The solution looks legit (when using solvers others than - # GLOP_LINEAR_PROGRAMMING, verifying the solution is highly recommended!). - assert solver.VerifySolution(1e-7, True) + status = solver.Solve() # [END solve] # [START print_solution] - print('Solution:') - print('Objective value =', solver.Objective().Value()) - print('x =', x.solution_value()) - print('y =', y.solution_value()) + if status == pywraplp.Solver.OPTIMAL: + print('Solution:') + print('Objective value =', solver.Objective().Value()) + print('x =', x.solution_value()) + print('y =', y.solution_value()) + else: + print('The problem does not have an optimal solution.') # [END print_solution] # [START advanced] diff --git a/ortools/linear_solver/scip_interface.cc b/ortools/linear_solver/scip_interface.cc index 6fd7d9b2e9..487075666e 100644 --- a/ortools/linear_solver/scip_interface.cc +++ b/ortools/linear_solver/scip_interface.cc @@ -159,6 +159,7 @@ SCIPInterface::~SCIPInterface() { DeleteSCIP(); } void SCIPInterface::Reset() { DeleteSCIP(); + scip_constraint_handler_.reset(); status_ = CreateSCIP(); ResetExtractionInformation(); } diff --git a/ortools/port/file_nonport.cc b/ortools/port/file_nonport.cc index 0b6257537f..5ab5764e52 100644 --- a/ortools/port/file_nonport.cc +++ b/ortools/port/file_nonport.cc @@ -11,6 +11,7 @@ // See the License for the specific language governing permissions and // limitations under the License. +#include "ortools/port/file.h" #if !defined(_MSC_VER) #include @@ -19,7 +20,6 @@ #include "absl/strings/str_format.h" #include "absl/time/clock.h" #include "ortools/base/file.h" -#include "ortools/port/file.h" namespace operations_research { diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index 629db82851..abd1271a12 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -2589,6 +2589,7 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) { wall_timer.Get()); } LoadCpModel(new_cp_model_proto, &shared_response_manager, model); + shared_response_manager.LoadDebugSolution(model); if (log_search) { LOG(INFO) << absl::StrFormat("*** starting sequential search at %.2fs", wall_timer.Get()); diff --git a/ortools/sat/implied_bounds.cc b/ortools/sat/implied_bounds.cc index 2a52500bc0..236eefcf40 100644 --- a/ortools/sat/implied_bounds.cc +++ b/ortools/sat/implied_bounds.cc @@ -71,25 +71,40 @@ void ImpliedBounds::Add(Literal literal, IntegerLiteral integer_literal) { // crosses integer_literal.bound. const auto it = bounds_.find(std::make_pair(literal.NegatedIndex(), var)); if (it != bounds_.end()) { - const IntegerValue deduction = std::min(integer_literal.bound, it->second); - - // TODO(user): support Enqueueing level zero fact at a positive level. That - // is, do not loose the info on backtrack. This should be doable. It is also - // why we return a bool in case of conflict when pushing deduction. - ++num_deductions_; - level_zero_lower_bounds_[var] = deduction; - new_level_zero_bounds_.Set(var); - - // The entries that are equal to the min no longer need to be stored once - // the level zero bound is enqueued. - if (it->second == deduction) { + if (it->second <= level_zero_lower_bounds_[var]) { + // The other bounds is worse than the new level-zero bound which can + // happen because of lazy update, so here we just remove it. bounds_.erase(it); - } - if (integer_literal.bound == deduction) { - bounds_.erase(std::make_pair(literal.Index(), var)); + } else { + const IntegerValue deduction = + std::min(integer_literal.bound, it->second); + DCHECK_GT(deduction, level_zero_lower_bounds_[var]); + DCHECK_GT(deduction, integer_trail_->LevelZeroLowerBound(var)); - // No need to update var_to_bounds_ in this case. - return; + // TODO(user): support Enqueueing level zero fact at a positive level. + // That is, do not loose the info on backtrack. This should be doable. It + // is also why we return a bool in case of conflict when pushing + // deduction. + ++num_deductions_; + level_zero_lower_bounds_[var] = deduction; + new_level_zero_bounds_.Set(var); + + VLOG(1) << "Deduction old: " + << IntegerLiteral::GreaterOrEqual( + var, integer_trail_->LevelZeroLowerBound(var)) + << " new: " << IntegerLiteral::GreaterOrEqual(var, deduction); + + // The entries that are equal to the min no longer need to be stored once + // the level zero bound is enqueued. + if (it->second == deduction) { + bounds_.erase(it); + } + if (integer_literal.bound == deduction) { + bounds_.erase(std::make_pair(literal.Index(), var)); + + // No need to update var_to_bounds_ in this case. + return; + } } } diff --git a/ortools/sat/integer.h b/ortools/sat/integer.h index 7d9f5e740b..ae46ed8eec 100644 --- a/ortools/sat/integer.h +++ b/ortools/sat/integer.h @@ -201,6 +201,13 @@ struct IntegerDomains : public gtl::ITIVector { explicit IntegerDomains(Model* model) {} }; +// A singleton used for debugging. If this is set in the model, then we can +// check that various derived constraint do not exclude this solution (if it is +// a known optimal solution for instance). +struct DebugSolution : public gtl::ITIVector { + explicit DebugSolution(Model* model) {} +}; + // Some heuristics may be generated automatically, for instance by constraints. // Those will be stored in a SearchHeuristicsVector object owned by the model. // diff --git a/ortools/sat/linear_constraint_manager.cc b/ortools/sat/linear_constraint_manager.cc index 9adf62ddaf..7910c27ca2 100644 --- a/ortools/sat/linear_constraint_manager.cc +++ b/ortools/sat/linear_constraint_manager.cc @@ -135,6 +135,7 @@ LinearConstraintManager::ConstraintIndex LinearConstraintManager::Add( SimplifyConstraint(&ct); DivideByGCD(&ct); CanonicalizeConstraint(&ct); + DCHECK(DebugCheckConstraint(ct)); // If an identical constraint exists, only updates its bound. const size_t key = ComputeHashOfTerms(ct); @@ -224,7 +225,7 @@ void LinearConstraintManager::AddCut( // Only add cut with sufficient efficacy. if (violation / l2_norm < 1e-5) return; - VLOG(2) << "Cut '" << type_name << "'" + VLOG(1) << "Cut '" << type_name << "'" << " size=" << ct.vars.size() << " max_magnitude=" << ComputeInfinityNorm(ct) << " norm=" << l2_norm << " violation=" << violation << " eff=" << violation / l2_norm; @@ -402,6 +403,8 @@ bool LinearConstraintManager::ChangeLp( if (simplify_constraints && SimplifyConstraint(&constraint_infos_[i].constraint)) { DivideByGCD(&constraint_infos_[i].constraint); + DCHECK(DebugCheckConstraint(constraint_infos_[i].constraint)); + constraint_infos_[i].objective_parallelism_computed = false; constraint_infos_[i].l2_norm = ComputeL2Norm(constraint_infos_[i].constraint); @@ -570,5 +573,25 @@ void LinearConstraintManager::AddAllConstraintsToLp() { } } +bool LinearConstraintManager::DebugCheckConstraint( + const LinearConstraint& cut) { + if (model_->Get() == nullptr) return true; + const auto& debug_solution = *(model_->Get()); + if (debug_solution.empty()) return true; + + IntegerValue activity(0); + for (int i = 0; i < cut.vars.size(); ++i) { + const IntegerVariable var = cut.vars[i]; + const IntegerValue coeff = cut.coeffs[i]; + activity += coeff * debug_solution[var]; + } + if (activity > cut.ub || activity < cut.lb) { + LOG(INFO) << "activity " << activity << " not in [" << cut.lb << "," + << cut.ub << "]"; + return false; + } + return true; +} + } // namespace sat } // namespace operations_research diff --git a/ortools/sat/linear_constraint_manager.h b/ortools/sat/linear_constraint_manager.h index 3e76afdfa8..f88f56811b 100644 --- a/ortools/sat/linear_constraint_manager.h +++ b/ortools/sat/linear_constraint_manager.h @@ -60,7 +60,8 @@ class LinearConstraintManager { explicit LinearConstraintManager(Model* model) : sat_parameters_(*model->GetOrCreate()), integer_trail_(*model->GetOrCreate()), - time_limit_(model->GetOrCreate()) {} + time_limit_(model->GetOrCreate()), + model_(model) {} ~LinearConstraintManager(); // Add a new constraint to the manager. Note that we canonicalize constraints @@ -110,6 +111,11 @@ class LinearConstraintManager { int64 num_shortened_constraints() const { return num_shortened_constraints_; } int64 num_coeff_strenghtening() const { return num_coeff_strenghtening_; } + // If a debug solution has been loaded, this checks if the given constaint cut + // it or not. Returns true iff everything is fine and the cut does not violate + // the loaded solution. + bool DebugCheckConstraint(const LinearConstraint& cut); + private: // Heuristic that decide which constraints we should remove from the current // LP. Note that such constraints can be added back later by the heuristic @@ -172,6 +178,7 @@ class LinearConstraintManager { gtl::ITIVector dense_objective_coeffs_; TimeLimit* time_limit_; + Model* model_; }; } // namespace sat diff --git a/ortools/sat/linear_programming_constraint.cc b/ortools/sat/linear_programming_constraint.cc index 015ef44cf9..54438f7ab1 100644 --- a/ortools/sat/linear_programming_constraint.cc +++ b/ortools/sat/linear_programming_constraint.cc @@ -1209,6 +1209,10 @@ absl::int128 FloorRatio128(absl::int128 x, IntegerValue positive_div) { void LinearProgrammingConstraint::PreventOverflow(LinearConstraint* constraint, int max_pow) { // Compute the min/max possible partial sum. + // + // Note that since we currently only use this cut locally, it is okay to + // use the current lb/ub here to decide if we have an overflow or not. Below + // however, we do have to use the level zero lower bound. double sum_min = std::min(0.0, ToDouble(-constraint->ub)); double sum_max = std::max(0.0, ToDouble(-constraint->ub)); const int size = constraint->vars.size(); @@ -1227,6 +1231,13 @@ void LinearProgrammingConstraint::PreventOverflow(LinearConstraint* constraint, // To be correct, we need to shift all variable so that they are positive. // + // Important: One might be tempted to think that using the current variable + // bounds is okay here since we only use this to derive cut/constraint that + // only needs to be locally valid. However, in some corner cases (like when + // one term become zero), we might loose the fact that we used one of the + // variable bound to derive the new constraint, so we will miss it in the + // explanation !! + // // TODO(user): This code is tricky and similar to the one to generate cuts. // Test and may reduce the duplication? note however that here we use int128 // to deal with potential overflow. @@ -1242,7 +1253,8 @@ void LinearProgrammingConstraint::PreventOverflow(LinearConstraint* constraint, absl::int128(new_coeff.value()) * absl::int128(divisor.value()); adjust += remainder * - absl::int128(integer_trail_->LowerBound(constraint->vars[i]).value()); + absl::int128( + integer_trail_->LevelZeroLowerBound(constraint->vars[i]).value()); if (new_coeff == 0) continue; constraint->vars[new_size] = constraint->vars[i]; @@ -1565,7 +1577,8 @@ bool LinearProgrammingConstraint::ExactLpReasonning() { new_constraint.coeffs.push_back(-obj_scale); DivideByGCD(&new_constraint); PreventOverflow(&new_constraint); - CHECK(!PossibleOverflow(new_constraint)); + DCHECK(!PossibleOverflow(new_constraint)); + DCHECK(constraint_manager_.DebugCheckConstraint(new_constraint)); IntegerSumLE* cp_constraint = new IntegerSumLE({}, new_constraint.vars, new_constraint.coeffs, @@ -1601,7 +1614,8 @@ bool LinearProgrammingConstraint::FillExactDualRayReason() { ConvertToLinearConstraint(dense_new_constraint, new_constraint_ub); DivideByGCD(&new_constraint); PreventOverflow(&new_constraint); - CHECK(!PossibleOverflow(new_constraint)); + DCHECK(!PossibleOverflow(new_constraint)); + DCHECK(constraint_manager_.DebugCheckConstraint(new_constraint)); const IntegerValue implied_lb = GetImpliedLowerBound(new_constraint); if (implied_lb <= new_constraint.ub) { diff --git a/ortools/sat/samples/nurses_sat.py b/ortools/sat/samples/nurses_sat.py index 2c55e1c882..f5411b4a86 100644 --- a/ortools/sat/samples/nurses_sat.py +++ b/ortools/sat/samples/nurses_sat.py @@ -117,8 +117,9 @@ def main(): solver.parameters.linearization_level = 0 # Display the first five solutions. a_few_solutions = range(5) - solution_printer = NursesPartialSolutionPrinter( - shifts, num_nurses, num_days, num_shifts, a_few_solutions) + solution_printer = NursesPartialSolutionPrinter(shifts, num_nurses, + num_days, num_shifts, + a_few_solutions) solver.SearchForAllSolutions(model, solution_printer) # [END solve] diff --git a/ortools/sat/samples/rabbits_and_pheasants_sat.py b/ortools/sat/samples/rabbits_and_pheasants_sat.py index aa9916dcf4..7ad2a969ce 100644 --- a/ortools/sat/samples/rabbits_and_pheasants_sat.py +++ b/ortools/sat/samples/rabbits_and_pheasants_sat.py @@ -36,8 +36,8 @@ def RabbitsAndPheasantsSat(): status = solver.Solve(model) if status == cp_model.FEASIBLE: - print( - '%i rabbits and %i pheasants' % (solver.Value(r), solver.Value(p))) + print('%i rabbits and %i pheasants' % + (solver.Value(r), solver.Value(p))) RabbitsAndPheasantsSat() diff --git a/ortools/sat/samples/ranking_sample_sat.py b/ortools/sat/samples/ranking_sample_sat.py index e51be07ff5..a9231a93b5 100644 --- a/ortools/sat/samples/ranking_sample_sat.py +++ b/ortools/sat/samples/ranking_sample_sat.py @@ -52,17 +52,17 @@ def RankTasks(model, starts, presences, ranks): if presences[i] != 1: tmp_array.append(presences[i].Not()) # Makes sure that if i is not performed, all precedences are false. - model.AddImplication(presences[i].Not(), precedences[(i, - j)].Not()) - model.AddImplication(presences[i].Not(), precedences[(j, - i)].Not()) + model.AddImplication(presences[i].Not(), + precedences[(i, j)].Not()) + model.AddImplication(presences[i].Not(), + precedences[(j, i)].Not()) if presences[j] != 1: tmp_array.append(presences[j].Not()) # Makes sure that if j is not performed, all precedences are false. - model.AddImplication(presences[j].Not(), precedences[(i, - j)].Not()) - model.AddImplication(presences[j].Not(), precedences[(j, - i)].Not()) + model.AddImplication(presences[j].Not(), + precedences[(i, j)].Not()) + model.AddImplication(presences[j].Not(), + precedences[(j, i)].Not()) # The following bool_or will enforce that for any two intervals: # i precedes j or j precedes i or at least one interval is not # performed. @@ -102,8 +102,9 @@ def RankingSampleSat(): presence = True else: presence = model.NewBoolVar('presence_%i' % t) - interval = model.NewOptionalIntervalVar( - start, duration, end, presence, 'o_interval_%i' % t) + interval = model.NewOptionalIntervalVar(start, duration, end, + presence, + 'o_interval_%i' % t) starts.append(start) ends.append(end) intervals.append(interval) diff --git a/ortools/sat/samples/schedule_requests_sat.py b/ortools/sat/samples/schedule_requests_sat.py index 562b8d18eb..7bbecded1a 100644 --- a/ortools/sat/samples/schedule_requests_sat.py +++ b/ortools/sat/samples/schedule_requests_sat.py @@ -16,7 +16,6 @@ # [START import] from __future__ import print_function from ortools.sat.python import cp_model - # [END import] diff --git a/ortools/sat/synchronization.cc b/ortools/sat/synchronization.cc index 471f0e0f8e..d142b5649f 100644 --- a/ortools/sat/synchronization.cc +++ b/ortools/sat/synchronization.cc @@ -13,6 +13,11 @@ #include "ortools/sat/synchronization.h" +#if !defined(__PORTABLE_PLATFORM__) +#include "ortools/base/file.h" +#include "ortools/sat/cp_model_loader.h" +#endif // __PORTABLE_PLATFORM__ + #include "absl/container/flat_hash_set.h" #include "ortools/base/integral_types.h" #include "ortools/base/stl_util.h" @@ -24,6 +29,15 @@ #include "ortools/sat/sat_base.h" #include "ortools/util/time_limit.h" +DEFINE_bool(cp_model_dump_solutions, false, + "DEBUG ONLY. If true, all the intermediate solution will be dumped " + "under '/tmp/solution_xxx.pb.txt'."); +DEFINE_string( + cp_model_load_debug_solution, "", + "DEBUG ONLY. When this is set to a non-empty file name, " + "we will interpret this as an internal solution which can be used for " + "debugging. For instance we use it to identify wrong cuts/reasons."); + namespace operations_research { namespace sat { @@ -372,6 +386,50 @@ void SharedResponseManager::NewSolution(const CpSolverResponse& response, pair.second(best_response_); } } + +#if !defined(__PORTABLE_PLATFORM__) + if (FLAGS_cp_model_dump_solutions) { + const std::string file = + absl::StrCat("/tmp/solution_", num_solutions_, ".pb.txt"); + LOG(INFO) << "Dumping solution to '" << file << "'."; + CHECK_OK(file::SetTextProto(file, best_response_, file::Defaults())); + } +#endif // __PORTABLE_PLATFORM__ +} + +void SharedResponseManager::LoadDebugSolution(Model* model) { +#if !defined(__PORTABLE_PLATFORM__) + if (FLAGS_cp_model_load_debug_solution.empty()) return; + if (model->Get() != nullptr) return; // Already loaded. + + CpSolverResponse response; + LOG(INFO) << "Reading solution from '" << FLAGS_cp_model_load_debug_solution + << "'."; + CHECK_OK(file::GetTextProto(FLAGS_cp_model_load_debug_solution, &response, + file::Defaults())); + + const auto& mapping = *model->GetOrCreate(); + auto& debug_solution = *model->GetOrCreate(); + debug_solution.resize( + model->GetOrCreate()->NumIntegerVariables().value()); + for (int i = 0; i < response.solution().size(); ++i) { + if (!mapping.IsInteger(i)) continue; + const IntegerVariable var = mapping.Integer(i); + debug_solution[var] = response.solution(i); + debug_solution[NegationOf(var)] = -response.solution(i); + } + + // The objective variable is usually not part of the proto, but it is still + // nice to have it, so we recompute it here. + auto* objective_def = model->Get(); + if (objective_def == nullptr) return; + + const IntegerVariable objective_var = objective_def->objective_var; + const int64 objective_value = + ComputeInnerObjective(model_proto_.objective(), response); + debug_solution[objective_var] = objective_value; + debug_solution[NegationOf(objective_var)] = -objective_value; +#endif // __PORTABLE_PLATFORM__ } void SharedResponseManager::SetStatsFromModel(Model* model) { diff --git a/ortools/sat/synchronization.h b/ortools/sat/synchronization.h index e8f12426a9..f18eedf9ca 100644 --- a/ortools/sat/synchronization.h +++ b/ortools/sat/synchronization.h @@ -175,6 +175,14 @@ class SharedResponseManager { } SharedSolutionRepository* MutableSolutionsRepository() { return &solutions_; } + // This should be called after the model is loaded. It will read the file + // specified by --cp_model_load_debug_solution and properly fill the + // model->Get() vector. + // + // TODO(user): Note that for now, only the IntegerVariable value are loaded, + // not the value of the pure Booleans variables. + void LoadDebugSolution(Model*); + private: void FillObjectiveValuesInBestResponse() EXCLUSIVE_LOCKS_REQUIRED(mutex_); void SetStatsFromModelInternal(Model* model) EXCLUSIVE_LOCKS_REQUIRED(mutex_);