<ahref="optimization_8h.html">Go to the documentation of this file.</a><divclass="fragment"><divclass="line"><aid="l00001"name="l00001"></a><spanclass="lineno"> 1</span><spanclass="comment">// Copyright 2010-2021 Google LLC</span></div>
<divclass="line"><aid="l00002"name="l00002"></a><spanclass="lineno"> 2</span><spanclass="comment">// Licensed under the Apache License, Version 2.0 (the "License");</span></div>
<divclass="line"><aid="l00003"name="l00003"></a><spanclass="lineno"> 3</span><spanclass="comment">// you may not use this file except in compliance with the License.</span></div>
<divclass="line"><aid="l00004"name="l00004"></a><spanclass="lineno"> 4</span><spanclass="comment">// You may obtain a copy of the License at</span></div>
<divclass="line"><aid="l00008"name="l00008"></a><spanclass="lineno"> 8</span><spanclass="comment">// Unless required by applicable law or agreed to in writing, software</span></div>
<divclass="line"><aid="l00009"name="l00009"></a><spanclass="lineno"> 9</span><spanclass="comment">// distributed under the License is distributed on an "AS IS" BASIS,</span></div>
<divclass="line"><aid="l00010"name="l00010"></a><spanclass="lineno"> 10</span><spanclass="comment">// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.</span></div>
<divclass="line"><aid="l00011"name="l00011"></a><spanclass="lineno"> 11</span><spanclass="comment">// See the License for the specific language governing permissions and</span></div>
<divclass="line"><aid="l00012"name="l00012"></a><spanclass="lineno"> 12</span><spanclass="comment">// limitations under the License.</span></div>
<divclass="line"><aid="l00031"name="l00031"></a><spanclass="lineno"> 31</span><spanclass="comment">// Like MinimizeCore() with a slower but strictly better heuristic. This</span></div>
<divclass="line"><aid="l00032"name="l00032"></a><spanclass="lineno"> 32</span><spanclass="comment">// algorithm should produce a minimal core with respect to propagation. We put</span></div>
<divclass="line"><aid="l00033"name="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"><aid="l00034"name="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"><aid="l00037"name="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"><aid="l00039"name="l00039"></a><spanclass="lineno"> 39</span><spanclass="comment">// TODO(user): Avoid spending too much time trying to minimize a core.</span></div>
<divclass="line"><aid="l00043"name="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"><aid="l00044"name="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"><aid="l00045"name="l00045"></a><spanclass="lineno"> 45</span><spanclass="comment">// default logging framework or simply stdout. Most users should just use</span></div>
<divclass="line"><aid="l00049"name="l00049"></a><spanclass="lineno"> 49</span><spanclass="comment">// All the Solve*() functions below reuse the SatSolver::Status with a slightly</span></div>
<divclass="line"><aid="l00050"name="l00050"></a><spanclass="lineno"> 50</span><spanclass="comment">// different meaning:</span></div>
<divclass="line"><aid="l00051"name="l00051"></a><spanclass="lineno"> 51</span><spanclass="comment">// - FEASIBLE: The problem has been solved to optimality.</span></div>
<divclass="line"><aid="l00052"name="l00052"></a><spanclass="lineno"> 52</span><spanclass="comment">// - INFEASIBLE: Same meaning, the decision version is already unsat.</span></div>
<divclass="line"><aid="l00053"name="l00053"></a><spanclass="lineno"> 53</span><spanclass="comment">// - LIMIT_REACHED: we may have some feasible solution (if solution is</span></div>
<divclass="line"><aid="l00054"name="l00054"></a><spanclass="lineno"> 54</span><spanclass="comment">// non-empty), but the optimality is not proven.</span></div>
<divclass="line"><aid="l00056"name="l00056"></a><spanclass="lineno"> 56</span><spanclass="comment">// Implements the "Fu & Malik" algorithm described in:</span></div>
<divclass="line"><aid="l00058"name="l00058"></a><spanclass="lineno"> 58</span><spanclass="comment">// International Conference on Theory and Applications of Satisfiability</span></div>
<divclass="line"><aid="l00061"name="l00061"></a><spanclass="lineno"> 61</span><spanclass="comment">// This algorithm requires all the objective weights to be the same (CHECKed)</span></div>
<divclass="line"><aid="l00062"name="l00062"></a><spanclass="lineno"> 62</span><spanclass="comment">// and currently only works on minimization problems. The problem is assumed to</span></div>
<divclass="line"><aid="l00063"name="l00063"></a><spanclass="lineno"> 63</span><spanclass="comment">// be already loaded into the given solver.</span></div>
<divclass="line"><aid="l00065"name="l00065"></a><spanclass="lineno"> 65</span><spanclass="comment">// TODO(user): double-check the correctness if the objective coefficients are</span></div>
<divclass="line"><aid="l00072"name="l00072"></a><spanclass="lineno"> 72</span><spanclass="comment">// The WPM1 algorithm is a generalization of the Fu & Malik algorithm to</span></div>
<divclass="line"><aid="l00073"name="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"><aid="l00074"name="l00074"></a><spanclass="lineno"> 74</span><spanclass="comment">// almost the same as SolveWithFuMalik() but the encoding of the constraints is</span></div>
<divclass="line"><aid="l00078"name="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"><aid="l00079"name="l00079"></a><spanclass="lineno"> 79</span><spanclass="comment">// Applications of Satisfiability Testing (SAT’09). pp. 427-440 (2009)</span></div>
<divclass="line"><aid="l00084"name="l00084"></a><spanclass="lineno"> 84</span><spanclass="comment">// Solves num_times the decision version of the given problem with different</span></div>
<divclass="line"><aid="l00085"name="l00085"></a><spanclass="lineno"> 85</span><spanclass="comment">// random parameters. Keep the best solution (regarding the objective) and</span></div>
<divclass="line"><aid="l00086"name="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"><aid="l00087"name="l00087"></a><spanclass="lineno"> 87</span><spanclass="comment">// given solver.</span></div>
<divclass="line"><aid="l00092"name="l00092"></a><spanclass="lineno"> 92</span><spanclass="comment">// Starts by solving the decision version of the given LinearBooleanProblem and</span></div>
<divclass="line"><aid="l00093"name="l00093"></a><spanclass="lineno"> 93</span><spanclass="comment">// then simply add a constraint to find a lower objective that the current best</span></div>
<divclass="line"><aid="l00094"name="l00094"></a><spanclass="lineno"> 94</span><spanclass="comment">// solution and repeat until the problem becomes unsat.</span></div>
<divclass="line"><aid="l00096"name="l00096"></a><spanclass="lineno"> 96</span><spanclass="comment">// The problem is assumed to be already loaded into the given solver. If</span></div>
<divclass="line"><aid="l00097"name="l00097"></a><spanclass="lineno"> 97</span><spanclass="comment">// solution is initially a feasible solution, the search will starts from there.</span></div>
<divclass="line"><aid="l00098"name="l00098"></a><spanclass="lineno"> 98</span><spanclass="comment">// solution will be updated with the best solution found so far.</span></div>
<divclass="line"><aid="l00104"name="l00104"></a><spanclass="lineno"> 104</span><spanclass="comment">// Similar algorithm as the one used by qmaxsat, this is a linear scan with the</span></div>
<divclass="line"><aid="l00105"name="l00105"></a><spanclass="lineno"> 105</span><spanclass="comment">// at-most k constraint encoded in SAT. This only works on problems with</span></div>
<divclass="line"><aid="l00111"name="l00111"></a><spanclass="lineno"> 111</span><spanclass="comment">// This is an original algorithm. It is a mix between the cardinality encoding</span></div>
<divclass="line"><aid="l00112"name="l00112"></a><spanclass="lineno"> 112</span><spanclass="comment">// and the Fu & Malik algorithm. It also works on general weighted instances.</span></div>
<divclass="line"><aid="l00117"name="l00117"></a><spanclass="lineno"> 117</span><spanclass="comment">// Model-based API, for now we just provide a basic algorithm that minimizes a</span></div>
<divclass="line"><aid="l00118"name="l00118"></a><spanclass="lineno"> 118</span><spanclass="comment">// given IntegerVariable by solving a sequence of decision problem by using</span></div>
<divclass="line"><aid="l00119"name="l00119"></a><spanclass="lineno"> 119</span><spanclass="comment">// SolveIntegerProblem(). Returns the status of the last solved decision</span></div>
<divclass="line"><aid="l00122"name="l00122"></a><spanclass="lineno"> 122</span><spanclass="comment">// The feasible_solution_observer function will be called each time a new</span></div>
<divclass="line"><aid="l00123"name="l00123"></a><spanclass="lineno"> 123</span><spanclass="comment">// feasible solution is found.</span></div>
<divclass="line"><aid="l00125"name="l00125"></a><spanclass="lineno"> 125</span><spanclass="comment">// Note that this function will resume the search from the current state of the</span></div>
<divclass="line"><aid="l00126"name="l00126"></a><spanclass="lineno"> 126</span><spanclass="comment">// solver, and it is up to the client to backtrack to the root node if needed.</span></div>
<divclass="line"><aid="l00131"name="l00131"></a><spanclass="lineno"> 131</span><spanclass="comment">// Use a low conflict limit and performs a binary search to try to restrict the</span></div>
<divclass="line"><aid="l00132"name="l00132"></a><spanclass="lineno"> 132</span><spanclass="comment">// domain of objective_var.</span></div>
<divclass="line"><aid="l00137"name="l00137"></a><spanclass="lineno"> 137</span><spanclass="comment">// Same as MinimizeIntegerVariableWithLinearScanAndLazyEncoding() but use</span></div>
<divclass="line"><aid="l00138"name="l00138"></a><spanclass="lineno"> 138</span><spanclass="comment">// a core-based approach instead. Note that the given objective_var is just used</span></div>
<divclass="line"><aid="l00139"name="l00139"></a><spanclass="lineno"> 139</span><spanclass="comment">// for reporting the lower-bound/upper-bound and do not need to be linked with</span></div>
<divclass="line"><aid="l00140"name="l00140"></a><spanclass="lineno"> 140</span><spanclass="comment">// its linear representation.</span></div>
<divclass="line"><aid="l00142"name="l00142"></a><spanclass="lineno"> 142</span><spanclass="comment">// Unlike MinimizeIntegerVariableWithLinearScanAndLazyEncoding() this function</span></div>
<divclass="line"><aid="l00143"name="l00143"></a><spanclass="lineno"> 143</span><spanclass="comment">// just return the last solver status. In particular if it is INFEASIBLE but</span></div>
<divclass="line"><aid="l00144"name="l00144"></a><spanclass="lineno"> 144</span><spanclass="comment">// feasible_solution_observer() was called, it means we are at OPTIMAL.</span></div>
<divclass="line"><aid="l00153"name="l00153"></a><spanclass="lineno"> 153</span><spanclass="comment">// TODO(user): Change the algo slighlty to allow resuming from the last</span></div>
<divclass="line"><aid="l00154"name="l00154"></a><spanclass="lineno"> 154</span><spanclass="comment">// aborted position. Currently, the search is "resumable", but it will restart</span></div>
<divclass="line"><aid="l00155"name="l00155"></a><spanclass="lineno"> 155</span><spanclass="comment">// some of the work already done, so it might just never find anything.</span></div>
<divclass="line"><aid="l00165"name="l00165"></a><spanclass="lineno"> 165</span><spanclass="keywordtype">int</span> depth; <spanclass="comment">// Only for logging/debugging.</span></div>
<divclass="line"><aid="l00168"name="l00168"></a><spanclass="lineno"> 168</span><spanclass="comment">// An upper bound on the optimal solution if we were to optimize only this</span></div>
<divclass="line"><aid="l00169"name="l00169"></a><spanclass="lineno"> 169</span><spanclass="comment">// term. This is used by the cover optimization code.</span></div>
<divclass="line"><aid="l00173"name="l00173"></a><spanclass="lineno"> 173</span><spanclass="comment">// This will be called each time a feasible solution is found. Returns false</span></div>
<divclass="line"><aid="l00174"name="l00174"></a><spanclass="lineno"> 174</span><spanclass="comment">// if a conflict was detected while trying to constrain the objective to a</span></div>
<divclass="line"><aid="l00178"name="l00178"></a><spanclass="lineno"> 178</span><spanclass="comment">// Use the gap an implied bounds to propagated the bounds of the objective</span></div>
<divclass="line"><aid="l00179"name="l00179"></a><spanclass="lineno"> 179</span><spanclass="comment">// variables and of its terms.</span></div>
<divclass="line"><aid="l00182"name="l00182"></a><spanclass="lineno"> 182</span><spanclass="comment">// Heuristic that aim to find the "real" lower bound of the objective on each</span></div>
<divclass="line"><aid="l00183"name="l00183"></a><spanclass="lineno"> 183</span><spanclass="comment">// core by using a linear scan optimization approach.</span></div>
<divclass="line"><aid="l00186"name="l00186"></a><spanclass="lineno"> 186</span><spanclass="comment">// Computes the next stratification threshold.</span></div>
<divclass="line"><aid="l00187"name="l00187"></a><spanclass="lineno"> 187</span><spanclass="comment">// Sets it to zero if all the assumptions where already considered.</span></div>
<divclass="line"><aid="l00202"name="l00202"></a><spanclass="lineno"> 202</span><spanclass="comment">// This is used to not add the objective equation more than once if we</span></div>
<divclass="line"><aid="l00203"name="l00203"></a><spanclass="lineno"> 203</span><spanclass="comment">// solve in "chunk".</span></div>
<divclass="line"><aid="l00206"name="l00206"></a><spanclass="lineno"> 206</span><spanclass="comment">// Set to true when we need to abort early.</span></div>
<divclass="line"><aid="l00208"name="l00208"></a><spanclass="lineno"> 208</span><spanclass="comment">// TODO(user): This is only used for the stop after first solution parameter</span></div>
<divclass="line"><aid="l00209"name="l00209"></a><spanclass="lineno"> 209</span><spanclass="comment">// which should likely be handled differently by simply using the normal way</span></div>
<divclass="line"><aid="l00210"name="l00210"></a><spanclass="lineno"> 210</span><spanclass="comment">// to stop a solver from the feasible solution callback.</span></div>
<divclass="line"><aid="l00214"name="l00214"></a><spanclass="lineno"> 214</span><spanclass="comment">// Generalization of the max-HS algorithm (HS stands for Hitting Set). This is</span></div>
<divclass="line"><aid="l00215"name="l00215"></a><spanclass="lineno"> 215</span><spanclass="comment">// similar to MinimizeWithCoreAndLazyEncoding() but it uses a hybrid approach</span></div>
<divclass="line"><aid="l00216"name="l00216"></a><spanclass="lineno"> 216</span><spanclass="comment">// with a MIP solver to handle the discovered infeasibility cores.</span></div>
<divclass="line"><aid="l00218"name="l00218"></a><spanclass="lineno"> 218</span><spanclass="comment">// See, Jessica Davies and Fahiem Bacchus, "Solving MAXSAT by Solving a</span></div>
<divclass="line"><aid="l00219"name="l00219"></a><spanclass="lineno"> 219</span><spanclass="comment">// Sequence of Simpler SAT Instances",</span></div>
<divclass="line"><aid="l00222"name="l00222"></a><spanclass="lineno"> 222</span><spanclass="comment">// Note that an implementation of this approach won the 2016 max-SAT competition</span></div>
<divclass="line"><aid="l00223"name="l00223"></a><spanclass="lineno"> 223</span><spanclass="comment">// on the industrial category, see</span></div>
<divclass="line"><aid="l00226"name="l00226"></a><spanclass="lineno"> 226</span><spanclass="comment">// TODO(user): This function brings dependency to the SCIP MIP solver which is</span></div>
<divclass="line"><aid="l00227"name="l00227"></a><spanclass="lineno"> 227</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#l00106">time_limit.h:106</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_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>
