<!-- iframe showing the search results (closed by default) -->
<divid="MSearchResultsWindow">
<iframesrc="javascript:void(0)"frameborder="0"
name="MSearchResults" id="MSearchResults">
</iframe>
</div>
<divclass="header">
<divclass="headertitle">
<divclass="title">integer_search.h</div></div>
</div><!--header-->
<divclass="contents">
<ahref="integer__search_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-2018 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="l00014"></a><spanclass="lineno"> 14</span> <spanclass="comment">// This file contains all the top-level logic responsible for driving the search</span></div>
<divclass="line"><aname="l00015"></a><spanclass="lineno"> 15</span> <spanclass="comment">// of a satisfiability integer problem. What decision we take next, which new</span></div>
<divclass="line"><aname="l00016"></a><spanclass="lineno"> 16</span> <spanclass="comment">// Literal associated to an IntegerLiteral we create and when we restart.</span></div>
<divclass="line"><aname="l00018"></a><spanclass="lineno"> 18</span> <spanclass="comment">// For an optimization problem, our algorithm solves a sequence of decision</span></div>
<divclass="line"><aname="l00019"></a><spanclass="lineno"> 19</span> <spanclass="comment">// problem using this file as an entry point. Note that some heuristics here</span></div>
<divclass="line"><aname="l00020"></a><spanclass="lineno"> 20</span> <spanclass="comment">// still use the objective if there is one in order to orient the search towards</span></div>
<divclass="line"><aname="l00021"></a><spanclass="lineno"> 21</span> <spanclass="comment">// good feasible solution though.</span></div>
<divclass="line"><aname="l00035"></a><spanclass="lineno"> 35</span> <spanclass="comment">// Model struct that contains the search heuristics used to find a feasible</span></div>
<divclass="line"><aname="l00036"></a><spanclass="lineno"> 36</span> <spanclass="comment">// solution to an integer problem.</span></div>
<divclass="line"><aname="l00038"></a><spanclass="lineno"> 38</span> <spanclass="comment">// This is reset by ConfigureSearchHeuristics() and used by</span></div>
<divclass="line"><aname="l00039"></a><spanclass="lineno"> 39</span> <spanclass="comment">// SolveIntegerProblem(), see below.</span></div>
<divclass="line"><aname="l00041"></a><spanclass="lineno"> 41</span> <spanclass="comment">// Decision and restart heuristics. The two vectors must be of the same size</span></div>
<divclass="line"><aname="l00042"></a><spanclass="lineno"> 42</span> <spanclass="comment">// and restart_policies[i] will always be used in conjunction with</span></div>
<divclass="line"><aname="l00047"></a><spanclass="lineno"> 47</span> <spanclass="comment">// Index in the vector above that indicate the current configuration.</span></div>
<divclass="line"><aname="l00050"></a><spanclass="lineno"> 50</span> <spanclass="comment">// Two special decision functions that are constructed at loading time.</span></div>
<divclass="line"><aname="l00051"></a><spanclass="lineno"> 51</span> <spanclass="comment">// These are used by ConfigureSearchHeuristics() to fill the policies above.</span></div>
<divclass="line"><aname="l00056"></a><spanclass="lineno"> 56</span> <spanclass="comment">// Given a base "fixed_search" function that should mainly control in which</span></div>
<divclass="line"><aname="l00057"></a><spanclass="lineno"> 57</span> <spanclass="comment">// order integer variables are lazily instantiated (and at what value), this</span></div>
<divclass="line"><aname="l00058"></a><spanclass="lineno"> 58</span> <spanclass="comment">// uses the current solver parameters to set the SearchHeuristics class in the</span></div>
<divclass="line"><aname="l00059"></a><spanclass="lineno"> 59</span> <spanclass="comment">// given model.</span></div>
<divclass="line"><aname="l00062"></a><spanclass="lineno"> 62</span> <spanclass="comment">// Callbacks that will be called when the search goes back to level 0.</span></div>
<divclass="line"><aname="l00063"></a><spanclass="lineno"> 63</span> <spanclass="comment">// Callbacks should return false if the propagation fails.</span></div>
<divclass="line"><aname="l00068"></a><spanclass="lineno"> 68</span> <spanclass="comment">// Tries to find a feasible solution to the current model.</span></div>
<divclass="line"><aname="l00070"></a><spanclass="lineno"> 70</span> <spanclass="comment">// This function continues from the current state of the solver and loop until</span></div>
<divclass="line"><aname="l00071"></a><spanclass="lineno"> 71</span> <spanclass="comment">// all variables are instantiated (i.e. the next decision is kNoLiteralIndex) or</span></div>
<divclass="line"><aname="l00072"></a><spanclass="lineno"> 72</span> <spanclass="comment">// a search limit is reached. It uses the heuristic from the SearchHeuristics</span></div>
<divclass="line"><aname="l00073"></a><spanclass="lineno"> 73</span> <spanclass="comment">// class in the model to decide when to restart and what next decision to take.</span></div>
<divclass="line"><aname="l00075"></a><spanclass="lineno"> 75</span> <spanclass="comment">// Each time a restart happen, this increment the policy index modulo the number</span></div>
<divclass="line"><aname="l00076"></a><spanclass="lineno"> 76</span> <spanclass="comment">// of heuristics to act as a portfolio search.</span></div>
<divclass="line"><aname="l00079"></a><spanclass="lineno"> 79</span> <spanclass="comment">// Resets the solver to the given assumptions before calling</span></div>
<divclass="line"><aname="l00084"></a><spanclass="lineno"> 84</span> <spanclass="comment">// Only used in tests. Move to a test utility file.</span></div>
<divclass="line"><aname="l00086"></a><spanclass="lineno"> 86</span> <spanclass="comment">// This configures the model SearchHeuristics with a simple default heuristic</span></div>
<divclass="line"><aname="l00087"></a><spanclass="lineno"> 87</span> <spanclass="comment">// and then call ResetAndSolveIntegerProblem() without any assumptions.</span></div>
<divclass="line"><aname="l00090"></a><spanclass="lineno"> 90</span> <spanclass="comment">// Helper methods to return up (>=) and down (<=) branching decisions.</span></div>
<divclass="line"><aname="l00094"></a><spanclass="lineno"> 94</span> <spanclass="comment">// Returns decision corresponding to var at its lower bound. Returns</span></div>
<divclass="line"><aname="l00095"></a><spanclass="lineno"> 95</span> <spanclass="comment">// kNoLiteralIndex if the variable is fixed.</span></div>
<divclass="line"><aname="l00103"></a><spanclass="lineno"> 103</span> <spanclass="comment">// This method first tries var <= value. If this does not reduce the domain it</span></div>
<divclass="line"><aname="l00104"></a><spanclass="lineno"> 104</span> <spanclass="comment">// tries var >= value. If that also does not reduce the domain then returns</span></div>
<divclass="line"><aname="l00109"></a><spanclass="lineno"> 109</span> <spanclass="comment">// Returns decision corresponding to var <= round(lp_value). If the variable</span></div>
<divclass="line"><aname="l00110"></a><spanclass="lineno"> 110</span> <spanclass="comment">// does not appear in the LP, this method returns kNoLiteralIndex.</span></div>
<divclass="line"><aname="l00113"></a><spanclass="lineno"> 113</span> <spanclass="comment">// Returns decision corresponding to var <= best_solution[var]. If no solution</span></div>
<divclass="line"><aname="l00114"></a><spanclass="lineno"> 114</span> <spanclass="comment">// has been found, this method returns kNoLiteralIndex. This was suggested in</span></div>
<divclass="line"><aname="l00115"></a><spanclass="lineno"> 115</span> <spanclass="comment">// paper: "Solution-Based Phase Saving for CP" (2018) by Emir Demirovic,</span></div>
<divclass="line"><aname="l00116"></a><spanclass="lineno"> 116</span> <spanclass="comment">// Geoffrey Chu, and Peter J. Stuckey</span></div>
<divclass="line"><aname="l00120"></a><spanclass="lineno"> 120</span> <spanclass="comment">// Decision heuristic for SolveIntegerProblemWithLazyEncoding(). Returns a</span></div>
<divclass="line"><aname="l00121"></a><spanclass="lineno"> 121</span> <spanclass="comment">// function that will return the literal corresponding to the fact that the</span></div>
<divclass="line"><aname="l00122"></a><spanclass="lineno"> 122</span> <spanclass="comment">// first currently non-fixed variable value is <= its min. The function will</span></div>
<divclass="line"><aname="l00123"></a><spanclass="lineno"> 123</span> <spanclass="comment">// return kNoLiteralIndex if all the given variables are fixed.</span></div>
<divclass="line"><aname="l00125"></a><spanclass="lineno"> 125</span> <spanclass="comment">// Note that this function will create the associated literal if needed.</span></div>
<divclass="line"><aname="l00129"></a><spanclass="lineno"> 129</span> <spanclass="comment">// Decision heuristic for SolveIntegerProblemWithLazyEncoding(). Like</span></div>
<divclass="line"><aname="l00130"></a><spanclass="lineno"> 130</span> <spanclass="comment">// FirstUnassignedVarAtItsMinHeuristic() but the function will return the</span></div>
<divclass="line"><aname="l00131"></a><spanclass="lineno"> 131</span> <spanclass="comment">// literal corresponding to the fact that the currently non-assigned variable</span></div>
<divclass="line"><aname="l00132"></a><spanclass="lineno"> 132</span> <spanclass="comment">// with the lowest min has a value <= this min.</span></div>
<divclass="line"><aname="l00136"></a><spanclass="lineno"> 136</span> <spanclass="comment">// Set the first unassigned Literal/Variable to its value.</span></div>
<divclass="line"><aname="l00138"></a><spanclass="lineno"> 138</span> <spanclass="comment">// TODO(user): This is currently quadratic as we scan all variables to find the</span></div>
<divclass="line"><aname="l00139"></a><spanclass="lineno"> 139</span> <spanclass="comment">// first unassigned one. Fix. Note that this is also the case in many other</span></div>
<divclass="line"><aname="l00140"></a><spanclass="lineno"> 140</span> <spanclass="comment">// heuristics and should be fixed.</span></div>
<divclass="line"><aname="l00149"></a><spanclass="lineno"> 149</span> <spanclass="comment">// Combines search heuristics in order: if the i-th one returns kNoLiteralIndex,</span></div>
<divclass="line"><aname="l00150"></a><spanclass="lineno"> 150</span> <spanclass="comment">// ask the (i+1)-th. If every heuristic returned kNoLiteralIndex,</span></div>
<divclass="line"><aname="l00155"></a><spanclass="lineno"> 155</span> <spanclass="comment">// Changes the value of the given decision by 'var_selection_heuristic'. We try</span></div>
<divclass="line"><aname="l00156"></a><spanclass="lineno"> 156</span> <spanclass="comment">// to see if the decision is "associated" with an IntegerVariable, and if it is</span></div>
<divclass="line"><aname="l00157"></a><spanclass="lineno"> 157</span> <spanclass="comment">// the case, we choose the new value by the first 'value_selection_heuristics'</span></div>
<divclass="line"><aname="l00158"></a><spanclass="lineno"> 158</span> <spanclass="comment">// that is applicable (return value != kNoLiteralIndex). If none of the</span></div>
<divclass="line"><aname="l00159"></a><spanclass="lineno"> 159</span> <spanclass="comment">// heuristics are applicable then the given decision by</span></div>
<divclass="line"><aname="l00160"></a><spanclass="lineno"> 160</span> <spanclass="comment">// 'var_selection_heuristic' is returned.</span></div>
<divclass="line"><aname="l00166"></a><spanclass="lineno"> 166</span> <spanclass="comment">// Changes the value of the given decision by 'var_selection_heuristic'</span></div>
<divclass="line"><aname="l00167"></a><spanclass="lineno"> 167</span> <spanclass="comment">// according to various value selection heuristics. Looks at the code to know</span></div>
<divclass="line"><aname="l00168"></a><spanclass="lineno"> 168</span> <spanclass="comment">// exactly what heuristic we use.</span></div>
<divclass="line"><aname="l00172"></a><spanclass="lineno"> 172</span> <spanclass="comment">// Returns the LiteralIndex advised by the underliying SAT solver.</span></div>
<divclass="line"><aname="l00175"></a><spanclass="lineno"> 175</span> <spanclass="comment">// Gets the branching variable using pseudo costs and combines it with a value</span></div>
<divclass="line"><aname="l00176"></a><spanclass="lineno"> 176</span> <spanclass="comment">// for branching.</span></div>
<divclass="line"><aname="l00179"></a><spanclass="lineno"> 179</span> <spanclass="comment">// Returns true if the number of variables in the linearized part represent</span></div>
<divclass="line"><aname="l00180"></a><spanclass="lineno"> 180</span> <spanclass="comment">// a large enough proportion of all the problem variables.</span></div>
<divclass="line"><aname="l00183"></a><spanclass="lineno"> 183</span> <spanclass="comment">// A restart policy that restarts every k failures.</span></div>
<divclass="line"><aname="l00186"></a><spanclass="lineno"> 186</span> <spanclass="comment">// A restart policy that uses the underlying sat solver's policy.</span></div>
<divclass="line"><aname="l00189"></a><spanclass="lineno"> 189</span> <spanclass="comment">// Appends model-owned automatic heuristics to input_heuristics in a new vector.</span></div>
<divclass="line"><aname="l00194"></a><spanclass="lineno"> 194</span> <spanclass="comment">// Concatenates each input_heuristic with a default heuristic that instantiate</span></div>
<divclass="line"><aname="l00195"></a><spanclass="lineno"> 195</span> <spanclass="comment">// all the problem's Boolean variables, into a new vector.</span></div>
<divclass="ttc"id="anamespaceoperations__research_1_1sat_html_af73dd5cdec05a6bbd9fb677f45fac2be"><divclass="ttname"><ahref="namespaceoperations__research_1_1sat.html#af73dd5cdec05a6bbd9fb677f45fac2be">operations_research::sat::BranchDown</a></div><divclass="ttdeci">LiteralIndex BranchDown(IntegerVariable var, IntegerValue value, Model *model)</div><divclass="ttdef"><b>Definition:</b><ahref="integer__search_8cc_source.html#l00037">integer_search.cc:37</a></div></div>
<divclass="ttc"id="anamespaceoperations__research_1_1sat_html_a55a7ac53a157135c072ad9d31bd47c38"><divclass="ttname"><ahref="namespaceoperations__research_1_1sat.html#a55a7ac53a157135c072ad9d31bd47c38">operations_research::sat::SplitAroundLpValue</a></div><divclass="ttdeci">LiteralIndex SplitAroundLpValue(IntegerVariable var, Model *model)</div><divclass="ttdef"><b>Definition:</b><ahref="integer__search_8cc_source.html#l00109">integer_search.cc:109</a></div></div>
<divclass="ttc"id="anamespaceoperations__research_1_1sat_html_a1aeef60fc8c9e76ebdd6ee5652e86ba9"><divclass="ttname"><ahref="namespaceoperations__research_1_1sat.html#a1aeef60fc8c9e76ebdd6ee5652e86ba9">operations_research::sat::AtMinValue</a></div><divclass="ttdeci">LiteralIndex AtMinValue(IntegerVariable var, IntegerTrail *integer_trail, IntegerEncoder *integer_encoder)</div><divclass="ttdef"><b>Definition:</b><ahref="integer__search_8cc_source.html#l00055">integer_search.cc:55</a></div></div>
<divclass="ttc"id="anamespaceoperations__research_html"><divclass="ttname"><ahref="namespaceoperations__research.html">operations_research</a></div><divclass="ttdoc">The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...</div><divclass="ttdef"><b>Definition:</b><ahref="dense__doubly__linked__list_8h_source.html#l00021">dense_doubly_linked_list.h:21</a></div></div>
<divclass="ttc"id="anamespaceoperations__research_1_1sat_html_a37d0780b10099ec4c75b6a7e1651e0cf"><divclass="ttname"><ahref="namespaceoperations__research_1_1sat.html#a37d0780b10099ec4c75b6a7e1651e0cf">operations_research::sat::FirstUnassignedVarAtItsMinHeuristic</a></div><divclass="ttdeci">std::function< LiteralIndex()> FirstUnassignedVarAtItsMinHeuristic(const std::vector< IntegerVariable >&vars, Model *model)</div><divclass="ttdef"><b>Definition:</b><ahref="integer__search_8cc_source.html#l00161">integer_search.cc:161</a></div></div>
<divclass="ttc"id="anamespaceoperations__research_1_1sat_html_ae6b68e19d66776a0728fc418c3a1fa14"><divclass="ttname"><ahref="namespaceoperations__research_1_1sat.html#ae6b68e19d66776a0728fc418c3a1fa14">operations_research::sat::GreaterOrEqualToMiddleValue</a></div><divclass="ttdeci">LiteralIndex GreaterOrEqualToMiddleValue(IntegerVariable var, Model *model)</div><divclass="ttdef"><b>Definition:</b><ahref="integer__search_8cc_source.html#l00067">integer_search.cc:67</a></div></div>
<divclass="ttc"id="anamespaceoperations__research_1_1sat_html_a77b16f43c9fc18688bfda50a953cbce0"><divclass="ttname"><ahref="namespaceoperations__research_1_1sat.html#a77b16f43c9fc18688bfda50a953cbce0">operations_research::sat::SplitDomainUsingBestSolutionValue</a></div><divclass="ttdeci">LiteralIndex SplitDomainUsingBestSolutionValue(IntegerVariable var, Model *model)</div></div>
<divclass="ttc"id="anamespaceoperations__research_1_1sat_html_aea96708896c3142cfb0d6c8dadd071fc"><divclass="ttname"><ahref="namespaceoperations__research_1_1sat.html#aea96708896c3142cfb0d6c8dadd071fc">operations_research::sat::BranchUp</a></div><divclass="ttdeci">LiteralIndex BranchUp(IntegerVariable var, IntegerValue value, Model *model)</div><divclass="ttdef"><b>Definition:</b><ahref="integer__search_8cc_source.html#l00046">integer_search.cc:46</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>
