1 // Copyright 2010-2021 Google LLC 2 // Licensed under the Apache License, Version 2.0 (the "License"); 3 // you may not use this file except in compliance with the License. 4 // You may obtain a copy of the License at 5 // 6 // http://www.apache.org/licenses/LICENSE-2.0 7 // 8 // Unless required by applicable law or agreed to in writing, software 9 // distributed under the License is distributed on an "AS IS" BASIS, 10 // WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. 11 // See the License for the specific language governing permissions and 12 // limitations under the License. 13 14 // Utility functions to interact with an lp solver from the SAT context. 15 16 #ifndef OR_TOOLS_SAT_LP_UTILS_H_ 17 #define OR_TOOLS_SAT_LP_UTILS_H_ 18 19 #include "ortools/linear_solver/linear_solver.pb.h" 20 #include "ortools/lp_data/lp_data.h" 21 #include "ortools/sat/boolean_problem.pb.h" 22 #include "ortools/sat/cp_model.pb.h" 23 #include "ortools/sat/sat_parameters.pb.h" 24 #include "ortools/sat/sat_solver.h" 25 #include "ortools/util/logging.h" 26 27 namespace operations_research { 28 namespace sat { 29 30 // Returns the smallest factor f such that f * abs(x) is integer modulo the 31 // given tolerance relative to f (we use f * tolerance). It is only looking 32 // for f smaller than the given limit. Returns zero if no such factor exist. 33 // 34 // The complexity is a lot less than O(limit), but it is possible that we might 35 // miss the smallest such factor if the tolerance used is too low. This is 36 // because we only rely on the best rational approximations of x with increasing 37 // denominator. 38 int FindRationalFactor(double x, int limit = 1e4, double tolerance = 1e-6); 39 40 // Multiplies all continuous variable by the given scaling parameters and change 41 // the rest of the model accordingly. The returned vector contains the scaling 42 // of each variable (will always be 1.0 for integers) and can be used to recover 43 // a solution of the unscaled problem from one of the new scaled problems by 44 // dividing the variable values. 45 // 46 // We usually scale a continuous variable by scaling, but if its domain is going 47 // to have larger values than max_bound, then we scale to have the max domain 48 // magnitude equal to max_bound. 49 // 50 // Note that it is recommended to call DetectImpliedIntegers() before this 51 // function so that we do not scale variables that do not need to be scaled. 52 // 53 // TODO(user): Also scale the solution hint if any. 54 std::vector<double> ScaleContinuousVariables(double scaling, double max_bound, 55 MPModelProto* mp_model); 56 57 // This simple step helps and should be done first. Returns false if the model 58 // is trivially infeasible because of crossing bounds. 59 bool MakeBoundsOfIntegerVariablesInteger(const SatParameters& params, 60 MPModelProto* mp_model, 61 SolverLogger* logger); 62 63 // Performs some extra tests on the given MPModelProto and returns false if one 64 // is not satisfied. These are needed before trying to convert it to the native 65 // CP-SAT format. 66 bool MPModelProtoValidationBeforeConversion(const SatParameters& params, 67 const MPModelProto& mp_model, 68 SolverLogger* logger); 69 70 // To satisfy our scaling requirements, any terms that is almost zero can just 71 // be set to zero. We need to do that before operations like 72 // DetectImpliedIntegers(), becauses really low coefficients can cause issues 73 // and might lead to less detection. 74 void RemoveNearZeroTerms(const SatParameters& params, MPModelProto* mp_model, 75 SolverLogger* logger); 76 77 // This will mark implied integer as such. Note that it can also discover 78 // variable of the form coeff * Integer + offset, and will change the model 79 // so that these are marked as integer. It is why we return both a scaling and 80 // an offset to transform the solution back to its original domain. 81 // 82 // TODO(user): Actually implement the offset part. This currently only happens 83 // on the 3 neos-46470* miplib problems where we have a non-integer rhs. 84 std::vector<double> DetectImpliedIntegers(MPModelProto* mp_model, 85 SolverLogger* logger); 86 87 // Converts a MIP problem to a CpModel. Returns false if the coefficients 88 // couldn't be converted to integers with a good enough precision. 89 // 90 // There is a bunch of caveats and you can find more details on the 91 // SatParameters proto documentation for the mip_* parameters. 92 bool ConvertMPModelProtoToCpModelProto(const SatParameters& params, 93 const MPModelProto& mp_model, 94 CpModelProto* cp_model, 95 SolverLogger* logger); 96 97 // Scales a double objective to its integer version and fills it in the proto. 98 // The variable listed in the objective must be already defined in the cp_model 99 // proto as this uses the variables bounds to compute a proper scaling. 100 // 101 // This uses params.mip_wanted_tolerance() and 102 // params.mip_max_activity_exponent() to compute the scaling. Note however that 103 // if the wanted tolerance is not satisfied this still scale with best effort. 104 // You can see in the log the tolerance guaranteed by this automatic scaling. 105 // 106 // This will almost always returns true except for really bad cases like having 107 // infinity in the objective. 108 bool ScaleAndSetObjective(const SatParameters& params, 109 const std::vector<std::pair<int, double>>& objective, 110 double objective_offset, bool maximize, 111 CpModelProto* cp_model, SolverLogger* logger); 112 113 // Given a CpModelProto with a floating point objective, and its scaled integer 114 // version with a known lower bound, this uses the variable bounds to derive a 115 // correct lower bound on the original objective. 116 // 117 // Note that the integer version can be way different, but then the bound is 118 // likely to be bad. For now, we solve this with a simple LP with one 119 // constraint. 120 // 121 // TODO(user): Code a custom algo with more precision guarantee? 122 double ComputeTrueObjectiveLowerBound( 123 const CpModelProto& model_proto_with_floating_point_objective, 124 const CpObjectiveProto& integer_objective, 125 const int64_t inner_integer_objective_lower_bound); 126 127 // Converts an integer program with only binary variables to a Boolean 128 // optimization problem. Returns false if the problem didn't contains only 129 // binary integer variable, or if the coefficients couldn't be converted to 130 // integer with a good enough precision. 131 bool ConvertBinaryMPModelProtoToBooleanProblem(const MPModelProto& mp_model, 132 LinearBooleanProblem* problem); 133 134 // Converts a Boolean optimization problem to its lp formulation. 135 void ConvertBooleanProblemToLinearProgram(const LinearBooleanProblem& problem, 136 glop::LinearProgram* lp); 137 138 // Changes the variable bounds of the lp to reflect the variables that have been 139 // fixed by the SAT solver (i.e. assigned at decision level 0). Returns the 140 // number of variables fixed this way. 141 int FixVariablesFromSat(const SatSolver& solver, glop::LinearProgram* lp); 142 143 // Solves the given lp problem and uses the lp solution to drive the SAT solver 144 // polarity choices. The variable must have the same index in the solved lp 145 // problem and in SAT for this to make sense. 146 // 147 // Returns false if a problem occurred while trying to solve the lp. 148 bool SolveLpAndUseSolutionForSatAssignmentPreference( 149 const glop::LinearProgram& lp, SatSolver* sat_solver, 150 double max_time_in_seconds); 151 152 // Solves the lp and add constraints to fix the integer variable of the lp in 153 // the LinearBoolean problem. 154 bool SolveLpAndUseIntegerVariableToStartLNS(const glop::LinearProgram& lp, 155 LinearBooleanProblem* problem); 156 157 } // namespace sat 158 } // namespace operations_research 159 160 #endif // OR_TOOLS_SAT_LP_UTILS_H_ 161