OR-Tools  8.2
sat/lp_utils.h
Go to the documentation of this file.
1 // Copyright 2010-2018 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"
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 
26 namespace operations_research {
27 namespace sat {
28 
29 // Returns the smallest factor f such that f * abs(x) is integer modulo the
30 // given tolerance relative to f (we use f * tolerance). It is only looking
31 // for f smaller than the given limit. Returns zero if no such factor exist.
32 //
33 // The complexity is a lot less than O(limit), but it is possible that we might
34 // miss the smallest such factor if the tolerance used is too low. This is
35 // because we only rely on the best rational approximations of x with increasing
36 // denominator.
37 int FindRationalFactor(double x, int limit = 1e4, double tolerance = 1e-6);
38 
39 // Multiplies all continuous variable by the given scaling parameters and change
40 // the rest of the model accordingly. The returned vector contains the scaling
41 // of each variable (will always be 1.0 for integers) and can be used to recover
42 // a solution of the unscaled problem from one of the new scaled problems by
43 // dividing the variable values.
44 //
45 // We usually scale a continuous variable by scaling, but if its domain is going
46 // to have larger values than max_bound, then we scale to have the max domain
47 // magnitude equal to max_bound.
48 //
49 // Note that it is recommended to call DetectImpliedIntegers() before this
50 // function so that we do not scale variables that do not need to be scaled.
51 //
52 // TODO(user): Also scale the solution hint if any.
53 std::vector<double> ScaleContinuousVariables(double scaling, double max_bound,
54  MPModelProto* mp_model);
55 
56 // To satisfy our scaling requirements, any terms that is almost zero can just
57 // be set to zero. We need to do that before operations like
58 // DetectImpliedIntegers(), becauses really low coefficients can cause issues
59 // and might lead to less detection.
60 void RemoveNearZeroTerms(const SatParameters& params, MPModelProto* mp_model);
61 
62 // This will mark implied integer as such. Note that it can also discover
63 // variable of the form coeff * Integer + offset, and will change the model
64 // so that these are marked as integer. It is why we return both a scaling and
65 // an offset to transform the solution back to its original domain.
66 //
67 // TODO(user): Actually implement the offset part. This currently only happens
68 // on the 3 neos-46470* miplib problems where we have a non-integer rhs.
69 std::vector<double> DetectImpliedIntegers(bool log_info,
70  MPModelProto* mp_model);
71 
72 // Converts a MIP problem to a CpModel. Returns false if the coefficients
73 // couldn't be converted to integers with a good enough precision.
74 //
75 // There is a bunch of caveats and you can find more details on the
76 // SatParameters proto documentation for the mip_* parameters.
77 bool ConvertMPModelProtoToCpModelProto(const SatParameters& params,
78  const MPModelProto& mp_model,
79  CpModelProto* cp_model);
80 
81 // Converts an integer program with only binary variables to a Boolean
82 // optimization problem. Returns false if the problem didn't contains only
83 // binary integer variable, or if the coefficients couldn't be converted to
84 // integer with a good enough precision.
85 bool ConvertBinaryMPModelProtoToBooleanProblem(const MPModelProto& mp_model,
86  LinearBooleanProblem* problem);
87 
88 // Converts a Boolean optimization problem to its lp formulation.
89 void ConvertBooleanProblemToLinearProgram(const LinearBooleanProblem& problem,
90  glop::LinearProgram* lp);
91 
92 // Changes the variable bounds of the lp to reflect the variables that have been
93 // fixed by the SAT solver (i.e. assigned at decision level 0). Returns the
94 // number of variables fixed this way.
95 int FixVariablesFromSat(const SatSolver& solver, glop::LinearProgram* lp);
96 
97 // Solves the given lp problem and uses the lp solution to drive the SAT solver
98 // polarity choices. The variable must have the same index in the solved lp
99 // problem and in SAT for this to make sense.
100 //
101 // Returns false if a problem occurred while trying to solve the lp.
103  const glop::LinearProgram& lp, SatSolver* sat_solver,
104  double max_time_in_seconds);
105 
106 // Solves the lp and add constraints to fix the integer variable of the lp in
107 // the LinearBoolean problem.
108 bool SolveLpAndUseIntegerVariableToStartLNS(const glop::LinearProgram& lp,
109  LinearBooleanProblem* problem);
110 
111 } // namespace sat
112 } // namespace operations_research
113 
114 #endif // OR_TOOLS_SAT_LP_UTILS_H_
bool SolveLpAndUseSolutionForSatAssignmentPreference(const glop::LinearProgram &lp, SatSolver *sat_solver, double max_time_in_seconds)
void RemoveNearZeroTerms(const SatParameters &params, MPModelProto *mp_model)
void ConvertBooleanProblemToLinearProgram(const LinearBooleanProblem &problem, glop::LinearProgram *lp)
std::vector< double > DetectImpliedIntegers(bool log_info, MPModelProto *mp_model)
bool ConvertBinaryMPModelProtoToBooleanProblem(const MPModelProto &mp_model, LinearBooleanProblem *problem)
bool SolveLpAndUseIntegerVariableToStartLNS(const glop::LinearProgram &lp, LinearBooleanProblem *problem)
int FixVariablesFromSat(const SatSolver &solver, glop::LinearProgram *lp)
std::vector< double > ScaleContinuousVariables(double scaling, double max_bound, MPModelProto *mp_model)
Definition: sat/lp_utils.cc:99
bool ConvertMPModelProtoToCpModelProto(const SatParameters &params, const MPModelProto &mp_model, CpModelProto *cp_model)
int FindRationalFactor(double x, int limit, double tolerance)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...