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