From 604587eec79d9c84dd0104b37e82e08b5e656138 Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Mon, 15 Jan 2018 10:41:09 +0100 Subject: [PATCH] minor changes; change the search parameters in the cp_model.proto --- dependencies/archives/autoconf.patch | 69 --------------- ortools/base/inlined_vector.h | 4 +- ortools/base/string_view.cc | 3 +- ortools/flatzinc/cp_model_fz_solver.cc | 5 +- ortools/linear_solver/bop_interface.cc | 1 + ortools/linear_solver/cbc_interface.cc | 1 + ortools/linear_solver/clp_interface.cc | 1 + ortools/linear_solver/glop_interface.cc | 4 +- ortools/linear_solver/glpk_interface.cc | 2 + ortools/linear_solver/gurobi_interface.cc | 1 + ortools/linear_solver/linear_solver.cc | 15 ++-- ortools/linear_solver/scip_interface.cc | 1 + ortools/sat/cp_model.proto | 6 +- ortools/sat/cp_model_solver.cc | 3 +- ortools/sat/integer_search.cc | 91 +++++++++++++------- ortools/sat/linear_programming_constraint.cc | 1 + ortools/sat/linear_programming_constraint.h | 53 +++++++----- ortools/sat/sat_parameters.proto | 35 +++++--- ortools/sat/simplification.cc | 41 ++++++--- ortools/sat/simplification.h | 4 +- ortools/util/functions_swig_test_helpers.h | 1 + ortools/util/stats.cc | 3 - ortools/util/stats.h | 9 +- 23 files changed, 179 insertions(+), 175 deletions(-) delete mode 100644 dependencies/archives/autoconf.patch diff --git a/dependencies/archives/autoconf.patch b/dependencies/archives/autoconf.patch deleted file mode 100644 index b98ba71c09..0000000000 --- a/dependencies/archives/autoconf.patch +++ /dev/null @@ -1,69 +0,0 @@ -diff --git i/doc/autoconf.texi w/doc/autoconf.texi ---- i/doc/autoconf.texi -+++ w/doc/autoconf.texi -@@ -15,7 +15,7 @@ - @c The ARG is an optional argument. To be used for macro arguments in - @c their documentation (@defmac). - @macro ovar{varname} --@r{[}@var{\varname\}@r{]}@c -+@r{[}@var{\varname\}@r{]} - @end macro - - @c @dvar(ARG, DEFAULT) -@@ -23,7 +23,7 @@ - @c The ARG is an optional argument, defaulting to DEFAULT. To be used - @c for macro arguments in their documentation (@defmac). - @macro dvar{varname, default} --@r{[}@var{\varname\} = @samp{\default\}@r{]}@c -+@r{[}@var{\varname\} = @samp{\default\}@r{]} - @end macro - - @c Handling the indexes with Texinfo yields several different problems. -@@ -8013,10 +8013,10 @@ - @code{ac_cv_f77_libs} or @code{ac_cv_fc_libs}, respectively. - @end defmac - --@defmac AC_F77_DUMMY_MAIN (@ovar{action-if-found}, @dvar{action-if-not-found, @ -- AC_MSG_FAILURE}) --@defmacx AC_FC_DUMMY_MAIN (@ovar{action-if-found}, @dvar{action-if-not-found, @ -- AC_MSG_FAILURE}) -+@defmac AC_F77_DUMMY_MAIN (@ovar{action-if-found}, @ -+ @dvar{action-if-not-found, AC_MSG_FAILURE}) -+@defmacx AC_FC_DUMMY_MAIN (@ovar{action-if-found}, @ -+ @dvar{action-if-not-found, AC_MSG_FAILURE}) - @acindex{F77_DUMMY_MAIN} - @cvindex F77_DUMMY_MAIN - @acindex{FC_DUMMY_MAIN} -@@ -8267,8 +8267,8 @@ - @code{ac_cv_fc_pp_srcext_@var{ext}} variables, respectively. - @end defmac - --@defmac AC_FC_PP_DEFINE (@ovar{action-if-success}, @dvar{action-if-failure, @ -- AC_MSG_FAILURE}) -+@defmac AC_FC_PP_DEFINE (@ovar{action-if-success}, @ -+ @dvar{action-if-failure, AC_MSG_FAILURE}) - @acindex{FC_PP_DEFINE} - @caindex fc_pp_define - -@@ -8286,8 +8286,8 @@ - variable. - @end defmac - --@defmac AC_FC_FREEFORM (@ovar{action-if-success}, @dvar{action-if-failure, @ -- AC_MSG_FAILURE}) -+@defmac AC_FC_FREEFORM (@ovar{action-if-success}, @ -+ @dvar{action-if-failure, AC_MSG_FAILURE}) - @acindex{FC_FREEFORM} - @caindex fc_freeform - -@@ -8313,8 +8313,8 @@ - the @code{ac_cv_fc_freeform} variable. - @end defmac - --@defmac AC_FC_FIXEDFORM (@ovar{action-if-success}, @dvar{action-if-failure, @ -- AC_MSG_FAILURE}) -+@defmac AC_FC_FIXEDFORM (@ovar{action-if-success}, @ -+ @dvar{action-if-failure, AC_MSG_FAILURE}) - @acindex{FC_FIXEDFORM} - @caindex fc_fixedform - diff --git a/ortools/base/inlined_vector.h b/ortools/base/inlined_vector.h index 01860f3ebd..edf83885b8 100644 --- a/ortools/base/inlined_vector.h +++ b/ortools/base/inlined_vector.h @@ -699,14 +699,14 @@ void InlinedVector::swap(InlinedVector& other) { template template inline void InlinedVector::AppendRange(Iter first, Iter last, - std::input_iterator_tag) { + std::input_iterator_tag) { std::copy(first, last, std::back_inserter(*this)); } template template inline void InlinedVector::AppendRange(Iter first, Iter last, - std::forward_iterator_tag) { + std::forward_iterator_tag) { typedef typename std::iterator_traits::difference_type Length; Length length = std::distance(first, last); size_t s = size(); diff --git a/ortools/base/string_view.cc b/ortools/base/string_view.cc index 51746ae0d3..c6833f6e82 100644 --- a/ortools/base/string_view.cc +++ b/ortools/base/string_view.cc @@ -93,7 +93,8 @@ int string_view::rfind(const string_view& s, size_type pos) const { int string_view::rfind(char c, size_type pos) const { if (length_ <= 0) return npos; - for (int i = std::min(pos, static_cast(length_ - 1)); i >= 0; --i) { + for (int i = std::min(pos, static_cast(length_ - 1)); i >= 0; + --i) { if (ptr_[i] == c) { return i; } diff --git a/ortools/flatzinc/cp_model_fz_solver.cc b/ortools/flatzinc/cp_model_fz_solver.cc index 83a6be0173..f577b44a44 100644 --- a/ortools/flatzinc/cp_model_fz_solver.cc +++ b/ortools/flatzinc/cp_model_fz_solver.cc @@ -835,7 +835,10 @@ void SolveFzWithCpModelProto(const fz::Model& fz_model, // Enumerate all sat solutions. m.parameters.set_enumerate_all_solutions(true); } - m.parameters.set_use_fixed_search(!p.free_search); + if (!p.free_search) { + m.parameters.set_search_branching(SatParameters::FIXED_SEARCH); + } + if (p.time_limit_in_ms > 0) { m.parameters.set_max_time_in_seconds(p.time_limit_in_ms * 1e-3); } diff --git a/ortools/linear_solver/bop_interface.cc b/ortools/linear_solver/bop_interface.cc index 70267becf8..9b80625b27 100644 --- a/ortools/linear_solver/bop_interface.cc +++ b/ortools/linear_solver/bop_interface.cc @@ -21,6 +21,7 @@ #include "ortools/base/stringprintf.h" #include "ortools/base/file.h" #include "google/protobuf/text_format.h" +#include "ortools/base/port.h" #include "ortools/base/hash.h" #include "ortools/bop/bop_parameters.pb.h" #include "ortools/bop/integral_solver.h" diff --git a/ortools/linear_solver/cbc_interface.cc b/ortools/linear_solver/cbc_interface.cc index ca3bc91a5e..219d1de8fa 100644 --- a/ortools/linear_solver/cbc_interface.cc +++ b/ortools/linear_solver/cbc_interface.cc @@ -25,6 +25,7 @@ #include "ortools/base/logging.h" #include "ortools/base/stringprintf.h" #include "ortools/base/timer.h" +#include "ortools/base/port.h" #include "ortools/base/hash.h" #include "ortools/linear_solver/linear_solver.h" diff --git a/ortools/linear_solver/clp_interface.cc b/ortools/linear_solver/clp_interface.cc index fa50381929..593710b132 100644 --- a/ortools/linear_solver/clp_interface.cc +++ b/ortools/linear_solver/clp_interface.cc @@ -25,6 +25,7 @@ #include "ortools/base/stringprintf.h" #include "ortools/base/timer.h" #include "ortools/base/strutil.h" +#include "ortools/base/port.h" #include "ortools/base/hash.h" #include "ortools/linear_solver/linear_solver.h" diff --git a/ortools/linear_solver/glop_interface.cc b/ortools/linear_solver/glop_interface.cc index 8e029d6de7..673e572cd9 100644 --- a/ortools/linear_solver/glop_interface.cc +++ b/ortools/linear_solver/glop_interface.cc @@ -17,13 +17,11 @@ #include #include -#include "ortools/base/commandlineflags.h" - -#include "ortools/base/commandlineflags.h" #include "ortools/base/integral_types.h" #include "ortools/base/logging.h" #include "ortools/base/stringprintf.h" +#include "ortools/base/port.h" #include "ortools/base/hash.h" #include "ortools/glop/lp_solver.h" diff --git a/ortools/linear_solver/glpk_interface.cc b/ortools/linear_solver/glpk_interface.cc index 8e9699bb4b..6d0abf2b6d 100644 --- a/ortools/linear_solver/glpk_interface.cc +++ b/ortools/linear_solver/glpk_interface.cc @@ -29,6 +29,7 @@ #include "ortools/base/logging.h" #include "ortools/base/stringprintf.h" #include "ortools/base/timer.h" +#include "ortools/base/port.h" #include "ortools/base/hash.h" #include "ortools/linear_solver/linear_solver.h" @@ -992,5 +993,6 @@ MPSolverInterface* BuildGLPKInterface(bool mip, MPSolver* const solver) { return new GLPKInterface(solver, mip); } + } // namespace operations_research #endif // #if defined(USE_GLPK) diff --git a/ortools/linear_solver/gurobi_interface.cc b/ortools/linear_solver/gurobi_interface.cc index b548d94fe7..54bdc34ace 100644 --- a/ortools/linear_solver/gurobi_interface.cc +++ b/ortools/linear_solver/gurobi_interface.cc @@ -27,6 +27,7 @@ #include "ortools/base/logging.h" #include "ortools/base/stringprintf.h" #include "ortools/base/timer.h" +#include "ortools/base/port.h" #include "ortools/base/map_util.h" #include "ortools/linear_solver/linear_solver.h" diff --git a/ortools/linear_solver/linear_solver.cc b/ortools/linear_solver/linear_solver.cc index 424f14ad2e..021d039388 100644 --- a/ortools/linear_solver/linear_solver.cc +++ b/ortools/linear_solver/linear_solver.cc @@ -33,6 +33,7 @@ #include "ortools/port/file.h" +#include "ortools/base/join.h" #include "ortools/base/map_util.h" #include "ortools/base/stl_util.h" #include "ortools/base/hash.h" @@ -41,8 +42,7 @@ #include "ortools/linear_solver/model_exporter.h" #include "ortools/linear_solver/model_validator.h" #include "ortools/util/fp_utils.h" - -// TODO(user): Clean up includes. E.g., parameters.pb.h seems not used. +#include "ortools/base/canonical_errors.h" DEFINE_bool(verify_solution, false, "Systematically verify the solution when calling Solve()" @@ -399,7 +399,7 @@ MPSolverInterface* BuildSolverInterface(MPSolver* const solver) { namespace { int NumDigits(int n) { // Number of digits needed to write a non-negative integer in base 10. -// Note(user): std::max(1, log(0) + 1) == std::max(1, -inf) == 1. +// Note(user): max(1, log(0) + 1) == max(1, -inf) == 1. #if defined(_MSC_VER) return static_cast(std::max(1.0L, log(1.0L * n) / log(10.0L) + 1.0)); #else @@ -764,12 +764,12 @@ bool MPSolver::LoadSolutionFromProto(const MPSolutionResponse& response) { } double largest_error = 0; interface_->ExtractModel(); + + // Look further: verify that the variable values are within the bounds. int num_vars_out_of_bounds = 0; const double tolerance = MPSolverParameters::kDefaultPrimalTolerance; + int last_offending_var = -1; for (int i = 0; i < response.variable_value_size(); ++i) { - // Look further: verify the bounds. Since linear solvers yield (small) - // numerical errors, though, we just log a warning if the variables look - // like they are out of their bounds. The user should inspect the values. const double var_value = response.variable_value(i); MPVariable* var = variables_[i]; // TODO(user): Use parameter when they become available in this class. @@ -778,8 +778,8 @@ bool MPSolver::LoadSolutionFromProto(const MPSolutionResponse& response) { if (lb_error > tolerance || ub_error > tolerance) { ++num_vars_out_of_bounds; largest_error = std::max(largest_error, std::max(lb_error, ub_error)); + last_offending_var = i; } - var->set_solution_value(var_value); } if (num_vars_out_of_bounds > 0) { LOG(WARNING) @@ -789,6 +789,7 @@ bool MPSolver::LoadSolutionFromProto(const MPSolutionResponse& response) { << tolerance; } // Set the objective value, if is known. + // NOTE(user): We do not verify the objective, even though we could! if (response.has_objective_value()) { interface_->objective_value_ = response.objective_value(); } diff --git a/ortools/linear_solver/scip_interface.cc b/ortools/linear_solver/scip_interface.cc index 7088006f42..6811eb0287 100644 --- a/ortools/linear_solver/scip_interface.cc +++ b/ortools/linear_solver/scip_interface.cc @@ -25,6 +25,7 @@ #include "ortools/base/logging.h" #include "ortools/base/stringprintf.h" #include "ortools/base/timer.h" +#include "ortools/base/port.h" #include "scip/scip.h" #include "scip/scipdefplugins.h" #include "ortools/base/hash.h" diff --git a/ortools/sat/cp_model.proto b/ortools/sat/cp_model.proto index 537c79c15b..f9f3217e01 100644 --- a/ortools/sat/cp_model.proto +++ b/ortools/sat/cp_model.proto @@ -377,9 +377,9 @@ message CpModelProto { // The objective to minimize. Can be empty for pure decision problems. CpObjectiveProto objective = 4; - // Defines the strategy that the solver should follow when the "fixed_search" - // parameters is set to true. Note that this strategy is also used as an - // heuristic when we are not in fixed search. + // Defines the strategy that the solver should follow when the + // search_branching parameter is set to FIXED_SEARCH. Note that this strategy + // is also used as a heuristic when we are not in fixed search. // // If empty, the solver will try to assign all variables to their min value in // the order of their appearance in the variables field above. Otherwise, it diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index 393d59fbd0..12b7c6c6fd 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -506,7 +506,8 @@ ModelWithMapping::ModelWithMapping(const CpModelProto& model_proto, const SatParameters& parameters = *(model->GetOrCreate()); const bool view_all_booleans_as_integers = (parameters.linearization_level() > 2) || - (parameters.use_fixed_search() && model_proto.search_strategy().empty()); + (parameters.search_branching() == SatParameters::FIXED_SEARCH && + model_proto.search_strategy().empty()); if (view_all_booleans_as_integers) { var_to_instantiate_as_integer.resize(num_proto_variables); for (int i = 0; i < num_proto_variables; ++i) { diff --git a/ortools/sat/integer_search.cc b/ortools/sat/integer_search.cc index 2f04162fb4..d8a5e19059 100644 --- a/ortools/sat/integer_search.cc +++ b/ortools/sat/integer_search.cc @@ -19,10 +19,10 @@ namespace operations_research { namespace sat { -// TODO(user): the complexity of this heuristic and the one below is ok when -// use_fixed_search() is false because it is not executed often, however, we do -// a linear scan for each search decision when use_fixed_search() is true, which -// seems bad. Improve. +// TODO(user): the complexity caused by the linear scan in this heuristic and +// the one below is ok when search_branching is set to SAT_SEARCH because it is +// not executed often, but otherwise it is done for each search decision, +// which seems expensive. Improve. std::function FirstUnassignedVarAtItsMinHeuristic( const std::vector& vars, Model* model) { IntegerEncoder* const integer_encoder = model->GetOrCreate(); @@ -99,18 +99,15 @@ std::function ExploitIntegerLpSolution( auto* trail = model->GetOrCreate(); auto* integer_trail = model->GetOrCreate(); auto* lp_dispatcher = model->GetOrCreate(); - - // Note that the order of the constraints in lp_constraints does not matter. - // TODO(user): keep this list somewhere instead of re-creating it like this? - std::set lp_constraints; - for (auto entry : *lp_dispatcher) lp_constraints.insert(entry.second); + auto* lp_constraints = + model->GetOrCreate(); // Use the normal heuristic if the LP(s) do not seem to cover enough variables // to be relevant. // TODO(user): Instead, try and depending on the result call it again or not? { int num_lp_variables = 0; - for (LinearProgrammingConstraint* lp : lp_constraints) { + for (LinearProgrammingConstraint* lp : *lp_constraints) { num_lp_variables += lp->NumVariables(); } const int num_integer_variables = @@ -134,7 +131,7 @@ std::function ExploitIntegerLpSolution( bool all_lp_integers = true; double obj = 0.0; - for (LinearProgrammingConstraint* lp : lp_constraints) { + for (LinearProgrammingConstraint* lp : *lp_constraints) { if (!lp->HasSolution() || !lp->SolutionIsInteger()) { all_lp_integers = false; break; @@ -223,28 +220,56 @@ SatSolver::Status SolveIntegerProblemWithLazyEncoding( solver->SetAssumptionLevel(0); const SatParameters& parameters = *(model->GetOrCreate()); - if (parameters.use_fixed_search()) { - CHECK(assumptions.empty()) << "Not supported yet"; - // Note that it is important to do the level-zero propagation if it wasn't - // already done because EnqueueDecisionAndBackjumpOnConflict() assumes that - // the solver is in a "propagated" state. - if (!solver->Propagate()) return SatSolver::MODEL_UNSAT; - } - - if (parameters.use_portfolio_search() && assumptions.empty()) { - auto incomplete_portfolio = AddModelHeuristics({next_decision}, model); - auto portfolio = CompleteHeuristics( - incomplete_portfolio, - SequentialSearch({SatSolverHeuristic(model), next_decision})); - if (parameters.exploit_integer_lp_solution()) { - for (auto& ref : portfolio) { - ref = ExploitIntegerLpSolution(ref, model); - } + switch (parameters.search_branching()) { + case SatParameters::AUTOMATIC_SEARCH: + break; + case SatParameters::FIXED_SEARCH: { + CHECK(assumptions.empty()) << "Not supported yet"; + // Note that it is important to do the level-zero propagation if it wasn't + // already done because EnqueueDecisionAndBackjumpOnConflict() assumes + // that the solver is in a "propagated" state. + if (!solver->Propagate()) return SatSolver::MODEL_UNSAT; + break; + } + case SatParameters::PORTFOLIO_SEARCH: { + CHECK(assumptions.empty()) << "Not supported yet"; + auto incomplete_portfolio = AddModelHeuristics({next_decision}, model); + auto portfolio = CompleteHeuristics( + incomplete_portfolio, + SequentialSearch({SatSolverHeuristic(model), next_decision})); + if (parameters.exploit_integer_lp_solution()) { + for (auto& ref : portfolio) { + ref = ExploitIntegerLpSolution(ref, model); + } + } + auto default_restart_policy = SatSolverRestartPolicy(model); + auto restart_policies = std::vector>( + portfolio.size(), default_restart_policy); + return SolveProblemWithPortfolioSearch(portfolio, restart_policies, + model); + } + case SatParameters::LP_SEARCH: { + CHECK(assumptions.empty()) << "Not supported yet"; + // Fill portfolio with pseudocost heuristics. + std::vector> lp_heuristics; + for (const auto& ct : + *(model->GetOrCreate())) { + lp_heuristics.push_back(ct->HeuristicLPPseudoCostBinary(model)); + } + auto portfolio = CompleteHeuristics( + lp_heuristics, + SequentialSearch({SatSolverHeuristic(model), next_decision})); + if (parameters.exploit_integer_lp_solution()) { + for (auto& ref : portfolio) { + ref = ExploitIntegerLpSolution(ref, model); + } + } + auto default_restart_policy = SatSolverRestartPolicy(model); + auto restart_policies = std::vector>( + portfolio.size(), default_restart_policy); + return SolveProblemWithPortfolioSearch(portfolio, restart_policies, + model); } - auto default_restart_policy = SatSolverRestartPolicy(model); - auto restart_policies = std::vector>( - portfolio.size(), default_restart_policy); - return SolveProblemWithPortfolioSearch(portfolio, restart_policies, model); } if (parameters.exploit_integer_lp_solution() && assumptions.empty()) { @@ -259,7 +284,7 @@ SatSolver::Status SolveIntegerProblemWithLazyEncoding( while (!time_limit->LimitReached()) { // If we are not in fixed search, let the SAT solver do a full search to // instantiate all the already created Booleans. - if (!parameters.use_fixed_search()) { + if (parameters.search_branching() == SatParameters::AUTOMATIC_SEARCH) { if (assumptions.empty()) { const SatSolver::Status status = solver->Solve(); if (status != SatSolver::MODEL_SAT) return status; diff --git a/ortools/sat/linear_programming_constraint.cc b/ortools/sat/linear_programming_constraint.cc index ca2f1d1abf..5f263ddf8d 100644 --- a/ortools/sat/linear_programming_constraint.cc +++ b/ortools/sat/linear_programming_constraint.cc @@ -93,6 +93,7 @@ void LinearProgrammingConstraint::SetObjectiveCoefficient(IntegerVariable ivar, void LinearProgrammingConstraint::RegisterWith(Model* model) { DCHECK(!lp_constraint_is_registered_); lp_constraint_is_registered_ = true; + model->GetOrCreate()->push_back(this); // Note that the order is important so that the lp objective is exactly the // same as the cp objective after scaling by the factor stored in lp_data_. diff --git a/ortools/sat/linear_programming_constraint.h b/ortools/sat/linear_programming_constraint.h index 06544a2b3a..e72ed9eccb 100644 --- a/ortools/sat/linear_programming_constraint.h +++ b/ortools/sat/linear_programming_constraint.h @@ -222,29 +222,6 @@ class LinearProgrammingConstraint : public PropagatorInterface, int NumVariables() const { return integer_variables_.size(); } std::string DimensionString() const { return lp_data_.GetDimensionString(); } - private: - // Generates a set of IntegerLiterals explaining why the best solution can not - // be improved using reduced costs. This is used to generate explanations for - // both infeasibility and bounds deductions. - void FillReducedCostsReason(); - - // Same as FillReducedCostReason() but for the case of a DUAL_UNBOUNDED - // problem. This exploit the dual ray as a reason for the primal infeasiblity. - void FillDualRayReason(); - - // Fills the deductions vector with reduced cost deductions that can be made - // from the current state of the LP solver. The given delta should be the - // difference between the cp objective upper bound and lower bound given by - // the lp. - void ReducedCostStrengtheningDeductions(double cp_objective_delta); - - // Gets or creates an LP variable that mirrors a CP variable. - // The variable should be a positive reference. - glop::ColIndex GetOrCreateMirrorVariable(IntegerVariable positive_variable); - - // Returns the variable value on the same scale as the CP variable value. - glop::Fractional GetVariableValueAtCpScale(glop::ColIndex var); - // Returns a LiteralIndex guided by the underlying LP constraints. // This looks at all unassigned 0-1 variables, takes the one with // a support value closest to 0.5, and tries to assign it to 1. @@ -273,6 +250,29 @@ class LinearProgrammingConstraint : public PropagatorInterface, // pseudo = a * pseudo + (1-a) reduced. std::function HeuristicLPPseudoCostBinary(Model* model); + private: + // Generates a set of IntegerLiterals explaining why the best solution can not + // be improved using reduced costs. This is used to generate explanations for + // both infeasibility and bounds deductions. + void FillReducedCostsReason(); + + // Same as FillReducedCostReason() but for the case of a DUAL_UNBOUNDED + // problem. This exploit the dual ray as a reason for the primal infeasiblity. + void FillDualRayReason(); + + // Fills the deductions vector with reduced cost deductions that can be made + // from the current state of the LP solver. The given delta should be the + // difference between the cp objective upper bound and lower bound given by + // the lp. + void ReducedCostStrengtheningDeductions(double cp_objective_delta); + + // Gets or creates an LP variable that mirrors a CP variable. + // The variable should be a positive reference. + glop::ColIndex GetOrCreateMirrorVariable(IntegerVariable positive_variable); + + // Returns the variable value on the same scale as the CP variable value. + glop::Fractional GetVariableValueAtCpScale(glop::ColIndex var); + // TODO(user): use solver's precision epsilon. static const double kEpsilon; @@ -338,6 +338,13 @@ class LinearProgrammingDispatcher explicit LinearProgrammingDispatcher(Model* model) {} }; +// A class that stores the collection of all LP constraints in a model. +class LinearProgrammingConstraintCollection + : public std::vector { + public: + LinearProgrammingConstraintCollection() {} +}; + // Cut generator for the circuit constraint, where in any feasible solution, the // arcs that are present (variable at 1) must form a circuit through all the // nodes of the graph. Self arc are forbidden in this case. diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto index d48f17a40d..1176063dcb 100644 --- a/ortools/sat/sat_parameters.proto +++ b/ortools/sat/sat_parameters.proto @@ -18,7 +18,7 @@ package operations_research.sat; // Contains the definitions for all the sat algorithm parameters and their // default values. // -// NEXT TAG: 96 +// NEXT TAG: 95 message SatParameters { // ========================================================================== // Branching and polarity @@ -472,23 +472,34 @@ message SatParameters { optional int32 max_num_cuts = 91 [default = 1000]; optional bool only_add_cuts_at_level_zero = 92 [default = false]; - // If true then all decisions taken by the solver are made using a fixed order - // as specified in the API or in the cp_model.proto search_order field. - // - // TODO(user): This is not working in all situation yet. The time limit is not - // really enforced properly, we don't support assumptions, and all the - // decisions variables must be integers. - optional bool use_fixed_search = 82 [default = false]; + // The search branching will be used to decide how to branch on unfixed nodes. + enum SearchBranching { + // Try to fix all literals using the underlying SAT solver's heuristics, + // then generate and fix literals until integer variables are fixed. + AUTOMATIC_SEARCH = 0; - // If true, the solver will use generic heuristics to find solutions and - // prove optimality. Incompatible with use_fixed_search. - optional bool use_portfolio_search = 94 [default = false]; + // If used then all decisions taken by the solver are made using a fixed + // order as specified in the API or in the cp_model.proto search_order + // field. + // + // TODO(user): This is not working in all situation yet. The time limit is + // not really enforced properly, we don't support assumptions, and all the + // decisions variables must be integers. + FIXED_SEARCH = 1; + + // If used, the solver will use various generic heuristics in turn. + PORTFOLIO_SEARCH = 2; + + // If used, the solver will use heuristics from the LP relaxation. + LP_SEARCH = 3; + } + optional SearchBranching search_branching = 82 [default = AUTOMATIC_SEARCH]; // If true and the Lp relaxation of the problem has an integer optimal // solution, try to exploit it. Note that since the LP relaxation may not // contain all the constraints, such a solution is not necessarily a solution // of the full problem. - optional bool exploit_integer_lp_solution = 95 [default = true]; + optional bool exploit_integer_lp_solution = 94 [default = true]; // The default optimization method is a simple "linear scan", each time trying // to find a better solution than the previous one. If this is true, then we diff --git a/ortools/sat/simplification.cc b/ortools/sat/simplification.cc index 219a670932..d38428ab1c 100644 --- a/ortools/sat/simplification.cc +++ b/ortools/sat/simplification.cc @@ -335,6 +335,10 @@ void SatPresolver::PresolveWithBva() { // We use the same notation as in the article mentionned in the .h void SatPresolver::SimpleBva(LiteralIndex l) { + literal_to_p_size_.resize(literal_to_clauses_.size(), 0); + DCHECK(std::all_of(literal_to_p_size_.begin(), literal_to_p_size_.end(), + [](int v) { return v == 0; })); + // We will try to add a literal to m_lit_ and take a subset of m_cls_ such // that |m_lit_| * |m_cls_| - |m_lit_| - |m_cls_| is maximized. m_lit_ = {l}; @@ -342,7 +346,10 @@ void SatPresolver::SimpleBva(LiteralIndex l) { int reduction = 0; while (true) { - p_.clear(); + LiteralIndex lmax = kNoLiteralIndex; + int max_size = 0; + + flattened_p_.clear(); for (const ClauseIndex c : m_cls_) { const std::vector& clause = clauses_[c]; if (clause.empty()) continue; // It has been deleted. @@ -368,24 +375,21 @@ void SatPresolver::SimpleBva(LiteralIndex l) { VLOG(1) << "self-subsumbtion"; } - DCHECK(p_[l_diff].empty() || p_[l_diff].back() != c); - p_[l_diff].push_back(c); + flattened_p_.push_back({l_diff, c}); + const int new_size = ++literal_to_p_size_[l_diff]; + if (new_size > max_size) { + lmax = l_diff; + max_size = new_size; + } } } - LiteralIndex lmax = kNoLiteralIndex; - int max_size = 0; - for (const auto& entry : p_) { - if (entry.second.size() > max_size) { - lmax = entry.first; - max_size = entry.second.size(); - } - } if (lmax == kNoLiteralIndex) break; const int new_m_lit_size = m_lit_.size() + 1; - const int new_m_cls_size = p_[lmax].size(); + const int new_m_cls_size = max_size; const int new_reduction = new_m_lit_size * new_m_cls_size - new_m_cls_size - new_m_lit_size; + if (new_reduction <= reduction) break; CHECK_NE(1, new_m_lit_size); CHECK_NE(1, new_m_cls_size); @@ -396,9 +400,20 @@ void SatPresolver::SimpleBva(LiteralIndex l) { // not that often compared to the initial computation of p. reduction = new_reduction; m_lit_.insert(lmax); - m_cls_ = p_[lmax]; + + // Set m_cls_ to p_[lmax]. + m_cls_.clear(); + for (const auto entry : flattened_p_) { + literal_to_p_size_[entry.first] = 0; + if (entry.first == lmax) m_cls_.push_back(entry.second); + } + flattened_p_.clear(); } + // Make sure literal_to_p_size_ is all zero. + for (const auto entry : flattened_p_) literal_to_p_size_[entry.first] = 0; + flattened_p_.clear(); + // A strictly positive reduction means that applying the BVA transform will // reduce the overall number of clauses by that much. Here we can control // what kind of reduction we want to apply. diff --git a/ortools/sat/simplification.h b/ortools/sat/simplification.h index afc9045b46..cd406e6edf 100644 --- a/ortools/sat/simplification.h +++ b/ortools/sat/simplification.h @@ -20,7 +20,6 @@ #define OR_TOOLS_SAT_SIMPLIFICATION_H_ #include -#include #include #include #include @@ -302,7 +301,8 @@ class SatPresolver { // Temporary data for SimpleBva(). std::set m_lit_; std::vector m_cls_; - std::unordered_map> p_; + ITIVector literal_to_p_size_; + std::vector> flattened_p_; std::vector tmp_new_clause_; // List of clauses on which we need to call ProcessClauseToSimplifyOthers(). diff --git a/ortools/util/functions_swig_test_helpers.h b/ortools/util/functions_swig_test_helpers.h index eab08e2cae..8e351c9914 100644 --- a/ortools/util/functions_swig_test_helpers.h +++ b/ortools/util/functions_swig_test_helpers.h @@ -22,6 +22,7 @@ // to find (whereas the class methods are easy to find). #include +#include #include "ortools/base/integral_types.h" namespace operations_research { diff --git a/ortools/util/stats.cc b/ortools/util/stats.cc index 47c1c3e761..357b59d634 100644 --- a/ortools/util/stats.cc +++ b/ortools/util/stats.cc @@ -24,9 +24,6 @@ namespace operations_research { -const char inst_retired_event[] = "inst_retired:any_p:u"; -const char cycles_event[] = "cycles:u"; - std::string MemoryUsage() { const int64 mem = operations_research::sysinfo::MemoryUsageProcess(); static const int64 kDisplayThreshold = 2; diff --git a/ortools/util/stats.h b/ortools/util/stats.h index e396ef619e..b986730a28 100644 --- a/ortools/util/stats.h +++ b/ortools/util/stats.h @@ -341,6 +341,11 @@ class DisabledScopedTimeDistributionUpdater { #ifdef HAS_PERF_SUBSYSTEM // Helper classes to count instructions during execution of a block of code and // add print the results to logs. +// +// Note: To enable instruction counting on machines running Debian, execute the +// following commands to modify the permissions. +// sudo echo "1" > /proc/sys/kernel/perf_event_paranoid +// sudo echo "0" > /proc/sys/kernel/kptr_restrict class EnabledScopedInstructionCounter { public: explicit EnabledScopedInstructionCounter(const std::string& name, @@ -402,8 +407,8 @@ inline std::string RemoveOperationsResearchAndGlop(const std::string& pretty_fun pretty_function, {{"operations_research::", ""}, {"glop::", ""}}); } -#define SCOPED_INSTRUCTION_COUNT(time_limit) \ - operations_research::ScopedInstructionCounterTemp scoped_instruction_count( \ +#define SCOPED_INSTRUCTION_COUNT(time_limit) \ + operations_research::ScopedInstructionCounter scoped_instruction_count( \ RemoveOperationsResearchAndGlop(__PRETTY_FUNCTION__), time_limit) #endif // HAS_PERF_SUBSYSTEM