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"
25
26namespace operations_research {
27namespace 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.
37int 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.
53std::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.
60void 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.
69std::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.
77bool 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.
85bool ConvertBinaryMPModelProtoToBooleanProblem(const MPModelProto& mp_model,
86 LinearBooleanProblem* problem);
87
88// Converts a Boolean optimization problem to its lp formulation.
89void 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.
95int 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.
108bool 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...