<ahref="optimization_8h.html">Go to the documentation of this file.</a><divclass="fragment"><divclass="line"><aname="l00001"></a><spanclass="lineno"> 1</span> <spanclass="comment">// Copyright 2010-2021 Google LLC</span></div>
<divclass="line"><aname="l00002"></a><spanclass="lineno"> 2</span> <spanclass="comment">// Licensed under the Apache License, Version 2.0 (the "License");</span></div>
<divclass="line"><aname="l00003"></a><spanclass="lineno"> 3</span> <spanclass="comment">// you may not use this file except in compliance with the License.</span></div>
<divclass="line"><aname="l00004"></a><spanclass="lineno"> 4</span> <spanclass="comment">// You may obtain a copy of the License at</span></div>
<divclass="line"><aname="l00008"></a><spanclass="lineno"> 8</span> <spanclass="comment">// Unless required by applicable law or agreed to in writing, software</span></div>
<divclass="line"><aname="l00009"></a><spanclass="lineno"> 9</span> <spanclass="comment">// distributed under the License is distributed on an "AS IS" BASIS,</span></div>
<divclass="line"><aname="l00010"></a><spanclass="lineno"> 10</span> <spanclass="comment">// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.</span></div>
<divclass="line"><aname="l00011"></a><spanclass="lineno"> 11</span> <spanclass="comment">// See the License for the specific language governing permissions and</span></div>
<divclass="line"><aname="l00012"></a><spanclass="lineno"> 12</span> <spanclass="comment">// limitations under the License.</span></div>
<divclass="line"><aname="l00031"></a><spanclass="lineno"> 31</span> <spanclass="comment">// Like MinimizeCore() with a slower but strictly better heuristic. This</span></div>
<divclass="line"><aname="l00032"></a><spanclass="lineno"> 32</span> <spanclass="comment">// algorithm should produce a minimal core with respect to propagation. We put</span></div>
<divclass="line"><aname="l00033"></a><spanclass="lineno"> 33</span> <spanclass="comment">// each literal of the initial core "last" at least once, so if such literal can</span></div>
<divclass="line"><aname="l00034"></a><spanclass="lineno"> 34</span> <spanclass="comment">// be inferred by propagation by any subset of the other literal, it will be</span></div>
<divclass="line"><aname="l00037"></a><spanclass="lineno"> 37</span> <spanclass="comment">// Note that this function doest NOT preserve the order of Literal in the core.</span></div>
<divclass="line"><aname="l00039"></a><spanclass="lineno"> 39</span> <spanclass="comment">// TODO(user): Avoid spending too much time trying to minimize a core.</span></div>
<divclass="line"><aname="l00043"></a><spanclass="lineno"> 43</span> <spanclass="comment">// Because the Solve*() functions below are also used in scripts that requires a</span></div>
<divclass="line"><aname="l00044"></a><spanclass="lineno"> 44</span> <spanclass="comment">// special output format, we use this to tell them whether or not to use the</span></div>
<divclass="line"><aname="l00045"></a><spanclass="lineno"> 45</span> <spanclass="comment">// default logging framework or simply stdout. Most users should just use</span></div>
<divclass="line"><aname="l00049"></a><spanclass="lineno"> 49</span> <spanclass="comment">// All the Solve*() functions below reuse the SatSolver::Status with a slightly</span></div>
<divclass="line"><aname="l00050"></a><spanclass="lineno"> 50</span> <spanclass="comment">// different meaning:</span></div>
<divclass="line"><aname="l00051"></a><spanclass="lineno"> 51</span> <spanclass="comment">// - FEASIBLE: The problem has been solved to optimality.</span></div>
<divclass="line"><aname="l00052"></a><spanclass="lineno"> 52</span> <spanclass="comment">// - INFEASIBLE: Same meaning, the decision version is already unsat.</span></div>
<divclass="line"><aname="l00053"></a><spanclass="lineno"> 53</span> <spanclass="comment">// - LIMIT_REACHED: we may have some feasible solution (if solution is</span></div>
<divclass="line"><aname="l00054"></a><spanclass="lineno"> 54</span> <spanclass="comment">// non-empty), but the optimality is not proven.</span></div>
<divclass="line"><aname="l00056"></a><spanclass="lineno"> 56</span> <spanclass="comment">// Implements the "Fu & Malik" algorithm described in:</span></div>
<divclass="line"><aname="l00058"></a><spanclass="lineno"> 58</span> <spanclass="comment">// International Conference on Theory and Applications of Satisfiability</span></div>
<divclass="line"><aname="l00061"></a><spanclass="lineno"> 61</span> <spanclass="comment">// This algorithm requires all the objective weights to be the same (CHECKed)</span></div>
<divclass="line"><aname="l00062"></a><spanclass="lineno"> 62</span> <spanclass="comment">// and currently only works on minimization problems. The problem is assumed to</span></div>
<divclass="line"><aname="l00063"></a><spanclass="lineno"> 63</span> <spanclass="comment">// be already loaded into the given solver.</span></div>
<divclass="line"><aname="l00065"></a><spanclass="lineno"> 65</span> <spanclass="comment">// TODO(user): double-check the correctness if the objective coefficients are</span></div>
<divclass="line"><aname="l00072"></a><spanclass="lineno"> 72</span> <spanclass="comment">// The WPM1 algorithm is a generalization of the Fu & Malik algorithm to</span></div>
<divclass="line"><aname="l00073"></a><spanclass="lineno"> 73</span> <spanclass="comment">// weighted problems. Note that if all objective weights are the same, this is</span></div>
<divclass="line"><aname="l00074"></a><spanclass="lineno"> 74</span> <spanclass="comment">// almost the same as SolveWithFuMalik() but the encoding of the constraints is</span></div>
<divclass="line"><aname="l00078"></a><spanclass="lineno"> 78</span> <spanclass="comment">// through satisfiability testing. In: Proc. of the 12th Int. Conf. on Theory and</span></div>
<divclass="line"><aname="l00079"></a><spanclass="lineno"> 79</span> <spanclass="comment">// Applications of Satisfiability Testing (SAT’09). pp. 427-440 (2009)</span></div>
<divclass="line"><aname="l00084"></a><spanclass="lineno"> 84</span> <spanclass="comment">// Solves num_times the decision version of the given problem with different</span></div>
<divclass="line"><aname="l00085"></a><spanclass="lineno"> 85</span> <spanclass="comment">// random parameters. Keep the best solution (regarding the objective) and</span></div>
<divclass="line"><aname="l00086"></a><spanclass="lineno"> 86</span> <spanclass="comment">// returns it in solution. The problem is assumed to be already loaded into the</span></div>
<divclass="line"><aname="l00087"></a><spanclass="lineno"> 87</span> <spanclass="comment">// given solver.</span></div>
<divclass="line"><aname="l00093"></a><spanclass="lineno"> 93</span> <spanclass="comment">// Starts by solving the decision version of the given LinearBooleanProblem and</span></div>
<divclass="line"><aname="l00094"></a><spanclass="lineno"> 94</span> <spanclass="comment">// then simply add a constraint to find a lower objective that the current best</span></div>
<divclass="line"><aname="l00095"></a><spanclass="lineno"> 95</span> <spanclass="comment">// solution and repeat until the problem becomes unsat.</span></div>
<divclass="line"><aname="l00097"></a><spanclass="lineno"> 97</span> <spanclass="comment">// The problem is assumed to be already loaded into the given solver. If</span></div>
<divclass="line"><aname="l00098"></a><spanclass="lineno"> 98</span> <spanclass="comment">// solution is initially a feasible solution, the search will starts from there.</span></div>
<divclass="line"><aname="l00099"></a><spanclass="lineno"> 99</span> <spanclass="comment">// solution will be updated with the best solution found so far.</span></div>
<divclass="line"><aname="l00105"></a><spanclass="lineno"> 105</span> <spanclass="comment">// Similar algorithm as the one used by qmaxsat, this is a linear scan with the</span></div>
<divclass="line"><aname="l00106"></a><spanclass="lineno"> 106</span> <spanclass="comment">// at-most k constraint encoded in SAT. This only works on problems with</span></div>
<divclass="line"><aname="l00112"></a><spanclass="lineno"> 112</span> <spanclass="comment">// This is an original algorithm. It is a mix between the cardinality encoding</span></div>
<divclass="line"><aname="l00113"></a><spanclass="lineno"> 113</span> <spanclass="comment">// and the Fu & Malik algorithm. It also works on general weighted instances.</span></div>
<divclass="line"><aname="l00118"></a><spanclass="lineno"> 118</span> <spanclass="comment">// Model-based API, for now we just provide a basic algorithm that minimizes a</span></div>
<divclass="line"><aname="l00119"></a><spanclass="lineno"> 119</span> <spanclass="comment">// given IntegerVariable by solving a sequence of decision problem by using</span></div>
<divclass="line"><aname="l00120"></a><spanclass="lineno"> 120</span> <spanclass="comment">// SolveIntegerProblem(). Returns the status of the last solved decision</span></div>
<divclass="line"><aname="l00123"></a><spanclass="lineno"> 123</span> <spanclass="comment">// The feasible_solution_observer function will be called each time a new</span></div>
<divclass="line"><aname="l00124"></a><spanclass="lineno"> 124</span> <spanclass="comment">// feasible solution is found.</span></div>
<divclass="line"><aname="l00126"></a><spanclass="lineno"> 126</span> <spanclass="comment">// Note that this function will resume the search from the current state of the</span></div>
<divclass="line"><aname="l00127"></a><spanclass="lineno"> 127</span> <spanclass="comment">// solver, and it is up to the client to backtrack to the root node if needed.</span></div>
<divclass="line"><aname="l00132"></a><spanclass="lineno"> 132</span> <spanclass="comment">// Use a low conflict limit and performs a binary search to try to restrict the</span></div>
<divclass="line"><aname="l00133"></a><spanclass="lineno"> 133</span> <spanclass="comment">// domain of objective_var.</span></div>
<divclass="line"><aname="l00138"></a><spanclass="lineno"> 138</span> <spanclass="comment">// Same as MinimizeIntegerVariableWithLinearScanAndLazyEncoding() but use</span></div>
<divclass="line"><aname="l00139"></a><spanclass="lineno"> 139</span> <spanclass="comment">// a core-based approach instead. Note that the given objective_var is just used</span></div>
<divclass="line"><aname="l00140"></a><spanclass="lineno"> 140</span> <spanclass="comment">// for reporting the lower-bound/upper-bound and do not need to be linked with</span></div>
<divclass="line"><aname="l00141"></a><spanclass="lineno"> 141</span> <spanclass="comment">// its linear representation.</span></div>
<divclass="line"><aname="l00143"></a><spanclass="lineno"> 143</span> <spanclass="comment">// Unlike MinimizeIntegerVariableWithLinearScanAndLazyEncoding() this function</span></div>
<divclass="line"><aname="l00144"></a><spanclass="lineno"> 144</span> <spanclass="comment">// just return the last solver status. In particular if it is INFEASIBLE but</span></div>
<divclass="line"><aname="l00145"></a><spanclass="lineno"> 145</span> <spanclass="comment">// feasible_solution_observer() was called, it means we are at OPTIMAL.</span></div>
<divclass="line"><aname="l00154"></a><spanclass="lineno"> 154</span> <spanclass="comment">// TODO(user): Change the algo slighlty to allow resuming from the last</span></div>
<divclass="line"><aname="l00155"></a><spanclass="lineno"> 155</span> <spanclass="comment">// aborted position. Currently, the search is "resumable", but it will restart</span></div>
<divclass="line"><aname="l00156"></a><spanclass="lineno"> 156</span> <spanclass="comment">// some of the work already done, so it might just never find anything.</span></div>
<divclass="line"><aname="l00166"></a><spanclass="lineno"> 166</span> <spanclass="keywordtype">int</span> depth; <spanclass="comment">// Only for logging/debugging.</span></div>
<divclass="line"><aname="l00169"></a><spanclass="lineno"> 169</span> <spanclass="comment">// An upper bound on the optimal solution if we were to optimize only this</span></div>
<divclass="line"><aname="l00170"></a><spanclass="lineno"> 170</span> <spanclass="comment">// term. This is used by the cover optimization code.</span></div>
<divclass="line"><aname="l00174"></a><spanclass="lineno"> 174</span> <spanclass="comment">// This will be called each time a feasible solution is found. Returns false</span></div>
<divclass="line"><aname="l00175"></a><spanclass="lineno"> 175</span> <spanclass="comment">// if a conflict was detected while trying to constrain the objective to a</span></div>
<divclass="line"><aname="l00179"></a><spanclass="lineno"> 179</span> <spanclass="comment">// Use the gap an implied bounds to propagated the bounds of the objective</span></div>
<divclass="line"><aname="l00180"></a><spanclass="lineno"> 180</span> <spanclass="comment">// variables and of its terms.</span></div>
<divclass="line"><aname="l00183"></a><spanclass="lineno"> 183</span> <spanclass="comment">// Heuristic that aim to find the "real" lower bound of the objective on each</span></div>
<divclass="line"><aname="l00184"></a><spanclass="lineno"> 184</span> <spanclass="comment">// core by using a linear scan optimization approach.</span></div>
<divclass="line"><aname="l00187"></a><spanclass="lineno"> 187</span> <spanclass="comment">// Computes the next stratification threshold.</span></div>
<divclass="line"><aname="l00188"></a><spanclass="lineno"> 188</span> <spanclass="comment">// Sets it to zero if all the assumptions where already considered.</span></div>
<divclass="line"><aname="l00203"></a><spanclass="lineno"> 203</span> <spanclass="comment">// This is used to not add the objective equation more than once if we</span></div>
<divclass="line"><aname="l00204"></a><spanclass="lineno"> 204</span> <spanclass="comment">// solve in "chunk".</span></div>
<divclass="line"><aname="l00207"></a><spanclass="lineno"> 207</span> <spanclass="comment">// Set to true when we need to abort early.</span></div>
<divclass="line"><aname="l00209"></a><spanclass="lineno"> 209</span> <spanclass="comment">// TODO(user): This is only used for the stop after first solution parameter</span></div>
<divclass="line"><aname="l00210"></a><spanclass="lineno"> 210</span> <spanclass="comment">// which should likely be handled differently by simply using the normal way</span></div>
<divclass="line"><aname="l00211"></a><spanclass="lineno"> 211</span> <spanclass="comment">// to stop a solver from the feasible solution callback.</span></div>
<divclass="line"><aname="l00215"></a><spanclass="lineno"> 215</span> <spanclass="comment">// Generalization of the max-HS algorithm (HS stands for Hitting Set). This is</span></div>
<divclass="line"><aname="l00216"></a><spanclass="lineno"> 216</span> <spanclass="comment">// similar to MinimizeWithCoreAndLazyEncoding() but it uses a hybrid approach</span></div>
<divclass="line"><aname="l00217"></a><spanclass="lineno"> 217</span> <spanclass="comment">// with a MIP solver to handle the discovered infeasibility cores.</span></div>
<divclass="line"><aname="l00219"></a><spanclass="lineno"> 219</span> <spanclass="comment">// See, Jessica Davies and Fahiem Bacchus, "Solving MAXSAT by Solving a</span></div>
<divclass="line"><aname="l00220"></a><spanclass="lineno"> 220</span> <spanclass="comment">// Sequence of Simpler SAT Instances",</span></div>
<divclass="line"><aname="l00223"></a><spanclass="lineno"> 223</span> <spanclass="comment">// Note that an implementation of this approach won the 2016 max-SAT competition</span></div>
<divclass="line"><aname="l00224"></a><spanclass="lineno"> 224</span> <spanclass="comment">// on the industrial category, see</span></div>
<divclass="line"><aname="l00227"></a><spanclass="lineno"> 227</span> <spanclass="comment">// TODO(user): This function brings dependency to the SCIP MIP solver which is</span></div>
<divclass="line"><aname="l00228"></a><spanclass="lineno"> 228</span> <spanclass="comment">// quite big, maybe we should find a way not to do that.</span></div>
<divclass="ttc"id="aclassoperations__research_1_1_time_limit_html"><divclass="ttname"><ahref="classoperations__research_1_1_time_limit.html">operations_research::TimeLimit</a></div><divclass="ttdoc">A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...</div><divclass="ttdef"><b>Definition:</b><ahref="time__limit_8h_source.html#l00105">time_limit.h:105</a></div></div>
<divclass="ttc"id="aclassoperations__research_1_1sat_1_1_model_html"><divclass="ttname"><ahref="classoperations__research_1_1sat_1_1_model.html">operations_research::sat::Model</a></div><divclass="ttdoc">Class that owns everything related to a particular optimization model.</div><divclass="ttdef"><b>Definition:</b><ahref="sat_2model_8h_source.html#l00038">sat/model.h:38</a></div></div>
<divclass="ttc"id="anamespaceoperations__research_1_1sat_html_affe1669ec9e0e7cbd54e895bbbff43af"><divclass="ttname"><ahref="namespaceoperations__research_1_1sat.html#affe1669ec9e0e7cbd54e895bbbff43af">operations_research::sat::MinimizeIntegerVariableWithLinearScanAndLazyEncoding</a></div><divclass="ttdeci">SatSolver::Status MinimizeIntegerVariableWithLinearScanAndLazyEncoding(IntegerVariable objective_var, const std::function< void()>&feasible_solution_observer, Model *model)</div><divclass="ttdef"><b>Definition:</b><ahref="optimization_8cc_source.html#l01059">optimization.cc:1059</a></div></div>
<divclass="ttc"id="anamespaceoperations__research_html"><divclass="ttname"><ahref="namespaceoperations__research.html">operations_research</a></div><divclass="ttdoc">Collection of objects used to extend the Constraint Solver library.</div><divclass="ttdef"><b>Definition:</b><ahref="dense__doubly__linked__list_8h_source.html#l00021">dense_doubly_linked_list.h:21</a></div></div>
