OR-Tools  8.1
optimization.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 #ifndef OR_TOOLS_SAT_OPTIMIZATION_H_
15 #define OR_TOOLS_SAT_OPTIMIZATION_H_
16 
17 #include <functional>
18 #include <vector>
19 
22 #include "ortools/sat/integer.h"
24 #include "ortools/sat/model.h"
25 #include "ortools/sat/sat_base.h"
26 #include "ortools/sat/sat_solver.h"
27 
28 namespace operations_research {
29 namespace sat {
30 
31 // Like MinimizeCore() with a slower but strictly better heuristic. This
32 // algorithm should produce a minimal core with respect to propagation. We put
33 // each literal of the initial core "last" at least once, so if such literal can
34 // be inferred by propagation by any subset of the other literal, it will be
35 // removed.
36 //
37 // Note that this function doest NOT preserve the order of Literal in the core.
38 void MinimizeCoreWithPropagation(SatSolver* solver, std::vector<Literal>* core);
39 
40 // Because the Solve*() functions below are also used in scripts that requires a
41 // special output format, we use this to tell them whether or not to use the
42 // default logging framework or simply stdout. Most users should just use
43 // DEFAULT_LOG.
45 
46 // All the Solve*() functions below reuse the SatSolver::Status with a slightly
47 // different meaning:
48 // - FEASIBLE: The problem has been solved to optimality.
49 // - INFEASIBLE: Same meaning, the decision version is already unsat.
50 // - LIMIT_REACHED: we may have some feasible solution (if solution is
51 // non-empty), but the optimality is not proven.
52 
53 // Implements the "Fu & Malik" algorithm described in:
54 // Zhaohui Fu, Sharad Malik, "On solving the Partial MAX-SAT problem", 2006,
55 // International Conference on Theory and Applications of Satisfiability
56 // Testing. (SAT’06), LNCS 4121.
57 //
58 // This algorithm requires all the objective weights to be the same (CHECKed)
59 // and currently only works on minimization problems. The problem is assumed to
60 // be already loaded into the given solver.
61 //
62 // TODO(user): double-check the correctness if the objective coefficients are
63 // negative.
65  const LinearBooleanProblem& problem,
66  SatSolver* solver,
67  std::vector<bool>* solution);
68 
69 // The WPM1 algorithm is a generalization of the Fu & Malik algorithm to
70 // weighted problems. Note that if all objective weights are the same, this is
71 // almost the same as SolveWithFuMalik() but the encoding of the constraints is
72 // slightly different.
73 //
74 // Ansotegui, C., Bonet, M.L., Levy, J.: Solving (weighted) partial MaxSAT
75 // through satisfiability testing. In: Proc. of the 12th Int. Conf. on Theory and
76 // Applications of Satisfiability Testing (SAT’09). pp. 427-440 (2009)
78  const LinearBooleanProblem& problem,
79  SatSolver* solver, std::vector<bool>* solution);
80 
81 // Solves num_times the decision version of the given problem with different
82 // random parameters. Keep the best solution (regarding the objective) and
83 // returns it in solution. The problem is assumed to be already loaded into the
84 // given solver.
86  const LinearBooleanProblem& problem,
87  int num_times, SatSolver* solver,
88  std::vector<bool>* solution);
89 
90 // Starts by solving the decision version of the given LinearBooleanProblem and
91 // then simply add a constraint to find a lower objective that the current best
92 // solution and repeat until the problem becomes unsat.
93 //
94 // The problem is assumed to be already loaded into the given solver. If
95 // solution is initially a feasible solution, the search will starts from there.
96 // solution will be updated with the best solution found so far.
98  const LinearBooleanProblem& problem,
99  SatSolver* solver,
100  std::vector<bool>* solution);
101 
102 // Similar algorithm as the one used by qmaxsat, this is a linear scan with the
103 // at-most k constraint encoded in SAT. This only works on problems with
104 // constant weights.
106  LogBehavior log, const LinearBooleanProblem& problem, SatSolver* solver,
107  std::vector<bool>* solution);
108 
109 // This is an original algorithm. It is a mix between the cardinality encoding
110 // and the Fu & Malik algorithm. It also works on general weighted instances.
112  LogBehavior log, const LinearBooleanProblem& problem, SatSolver* solver,
113  std::vector<bool>* solution);
114 
115 // Model-based API, for now we just provide a basic algorithm that minimizes a
116 // given IntegerVariable by solving a sequence of decision problem by using
117 // SolveIntegerProblem(). Returns the status of the last solved decision
118 // problem.
119 //
120 // The feasible_solution_observer function will be called each time a new
121 // feasible solution is found.
122 //
123 // Note that this function will resume the search from the current state of the
124 // solver, and it is up to the client to backtrack to the root node if needed.
126  IntegerVariable objective_var,
127  const std::function<void()>& feasible_solution_observer, Model* model);
128 
129 // Use a low conflict limit and performs a binary search to try to restrict the
130 // domain of objective_var.
132  IntegerVariable objective_var,
133  const std::function<void()>& feasible_solution_observer, Model* model);
134 
135 // Same as MinimizeIntegerVariableWithLinearScanAndLazyEncoding() but use
136 // a core-based approach instead. Note that the given objective_var is just used
137 // for reporting the lower-bound/upper-bound and do not need to be linked with
138 // its linear representation.
139 //
140 // Unlike MinimizeIntegerVariableWithLinearScanAndLazyEncoding() this function
141 // just return the last solver status. In particular if it is INFEASIBLE but
142 // feasible_solution_observer() was called, it means we are at OPTIMAL.
144  public:
145  CoreBasedOptimizer(IntegerVariable objective_var,
146  const std::vector<IntegerVariable>& variables,
147  const std::vector<IntegerValue>& coefficients,
148  std::function<void()> feasible_solution_observer,
149  Model* model);
150 
151  // TODO(user): Change the algo slighlty to allow resuming from the last
152  // aborted position. Currently, the search is "resumable", but it will restart
153  // some of the work already done, so it might just never find anything.
155 
156  private:
157  CoreBasedOptimizer(const CoreBasedOptimizer&) = delete;
158  CoreBasedOptimizer& operator=(const CoreBasedOptimizer&) = delete;
159 
160  struct ObjectiveTerm {
161  IntegerVariable var;
162  IntegerValue weight;
163  int depth; // Only for logging/debugging.
164  IntegerValue old_var_lb;
165 
166  // An upper bound on the optimal solution if we were to optimize only this
167  // term. This is used by the cover optimization code.
168  IntegerValue cover_ub;
169  };
170 
171  // This will be called each time a feasible solution is found. Returns false
172  // if a conflict was detected while trying to constrain the objective to a
173  // smaller value.
174  bool ProcessSolution();
175 
176  // Use the gap an implied bounds to propagated the bounds of the objective
177  // variables and of its terms.
178  bool PropagateObjectiveBounds();
179 
180  // Heuristic that aim to find the "real" lower bound of the objective on each
181  // core by using a linear scan optimization approach.
182  bool CoverOptimization();
183 
184  // Computes the next stratification threshold.
185  // Sets it to zero if all the assumptions where already considered.
186  void ComputeNextStratificationThreshold();
187 
188  SatParameters* parameters_;
189  SatSolver* sat_solver_;
190  TimeLimit* time_limit_;
191  IntegerTrail* integer_trail_;
192  IntegerEncoder* integer_encoder_;
193  Model* model_; // TODO(user): remove this one.
194 
195  IntegerVariable objective_var_;
196  std::vector<ObjectiveTerm> terms_;
197  IntegerValue stratification_threshold_;
198  std::function<void()> feasible_solution_observer_;
199 
200  // This is used to not add the objective equation more than once if we
201  // solve in "chunk".
202  bool already_switched_to_linear_scan_ = false;
203 
204  // Set to true when we need to abort early.
205  //
206  // TODO(user): This is only used for the stop after first solution parameter
207  // which should likely be handled differently by simply using the normal way
208  // to stop a solver from the feasible solution callback.
209  bool stop_ = false;
210 };
211 
212 // Generalization of the max-HS algorithm (HS stands for Hitting Set). This is
213 // similar to MinimizeWithCoreAndLazyEncoding() but it uses a hybrid approach
214 // with a MIP solver to handle the discovered infeasibility cores.
215 //
216 // See, Jessica Davies and Fahiem Bacchus, "Solving MAXSAT by Solving a
217 // Sequence of Simpler SAT Instances",
218 // http://www.cs.toronto.edu/~jdavies/daviesCP11.pdf"
219 //
220 // Note that an implementation of this approach won the 2016 max-SAT competition
221 // on the industrial category, see
222 // http://maxsat.ia.udl.cat/results/#wpms-industrial
223 //
224 // TODO(user): This function brings dependency to the SCIP MIP solver which is
225 // quite big, maybe we should find a way not to do that.
227  const ObjectiveDefinition& objective_definition,
228  const std::function<void()>& feasible_solution_observer, Model* model);
229 
230 } // namespace sat
231 } // namespace operations_research
232 
233 #endif // OR_TOOLS_SAT_OPTIMIZATION_H_
var
IntVar * var
Definition: expr_array.cc:1858
operations_research::sat::SatSolver::Status
Status
Definition: sat_solver.h:181
operations_research::sat::MinimizeCoreWithPropagation
void MinimizeCoreWithPropagation(SatSolver *solver, std::vector< Literal > *core)
Definition: optimization.cc:218
operations_research::sat::ObjectiveDefinition
Definition: cp_model_loader.h:38
operations_research::sat::STDOUT_LOG
@ STDOUT_LOG
Definition: optimization.h:44
operations_research::sat::IntegerTrail
Definition: integer.h:533
coefficients
std::vector< double > coefficients
Definition: sat/lp_utils.cc:497
operations_research::sat::RestrictObjectiveDomainWithBinarySearch
void RestrictObjectiveDomainWithBinarySearch(IntegerVariable objective_var, const std::function< void()> &feasible_solution_observer, Model *model)
Definition: optimization.cc:1091
operations_research::sat::SolveWithLinearScan
SatSolver::Status SolveWithLinearScan(LogBehavior log, const LinearBooleanProblem &problem, SatSolver *solver, std::vector< bool > *solution)
Definition: optimization.cc:842
operations_research::sat::SolveWithRandomParameters
SatSolver::Status SolveWithRandomParameters(LogBehavior log, const LinearBooleanProblem &problem, int num_times, SatSolver *solver, std::vector< bool > *solution)
Definition: optimization.cc:762
operations_research::sat::CoreBasedOptimizer
Definition: optimization.h:143
operations_research::sat::SatSolver
Definition: sat_solver.h:58
operations_research::sat::MinimizeIntegerVariableWithLinearScanAndLazyEncoding
SatSolver::Status MinimizeIntegerVariableWithLinearScanAndLazyEncoding(IntegerVariable objective_var, const std::function< void()> &feasible_solution_observer, Model *model)
Definition: optimization.cc:1058
weight
int64 weight
Definition: pack.cc:509
model.h
operations_research
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Definition: dense_doubly_linked_list.h:21
operations_research::sat::LogBehavior
LogBehavior
Definition: optimization.h:44
sat_solver.h
operations_research::TimeLimit
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
Definition: time_limit.h:105
operations_research::sat::SolveWithWPM1
SatSolver::Status SolveWithWPM1(LogBehavior log, const LinearBooleanProblem &problem, SatSolver *solver, std::vector< bool > *solution)
Definition: optimization.cc:465
sat_base.h
operations_research::sat::SolveWithFuMalik
SatSolver::Status SolveWithFuMalik(LogBehavior log, const LinearBooleanProblem &problem, SatSolver *solver, std::vector< bool > *solution)
Definition: optimization.cc:268
operations_research::sat::MinimizeWithHittingSetAndLazyEncoding
SatSolver::Status MinimizeWithHittingSetAndLazyEncoding(const ObjectiveDefinition &objective_definition, const std::function< void()> &feasible_solution_observer, Model *model)
Definition: optimization.cc:1757
operations_research::sat::CoreBasedOptimizer::Optimize
SatSolver::Status Optimize()
Definition: optimization.cc:1540
boolean_problem.pb.h
operations_research::sat::DEFAULT_LOG
@ DEFAULT_LOG
Definition: optimization.h:44
operations_research::sat::Model
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
operations_research::sat::SolveWithCardinalityEncoding
SatSolver::Status SolveWithCardinalityEncoding(LogBehavior log, const LinearBooleanProblem &problem, SatSolver *solver, std::vector< bool > *solution)
Definition: optimization.cc:888
model
GRBmodel * model
Definition: gurobi_interface.cc:269
operations_research::sat::CoreBasedOptimizer::CoreBasedOptimizer
CoreBasedOptimizer(IntegerVariable objective_var, const std::vector< IntegerVariable > &variables, const std::vector< IntegerValue > &coefficients, std::function< void()> feasible_solution_observer, Model *model)
Definition: optimization.cc:1310
cp_model_loader.h
integer_search.h
operations_research::sat::SolveWithCardinalityEncodingAndCore
SatSolver::Status SolveWithCardinalityEncodingAndCore(LogBehavior log, const LinearBooleanProblem &problem, SatSolver *solver, std::vector< bool > *solution)
Definition: optimization.cc:956
operations_research::sat::IntegerEncoder
Definition: integer.h:276
integer.h