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"
27
28namespace operations_research {
29namespace 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.
40void 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