<ahref="bop__ls_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="l00014"name="l00014"></a><spanclass="lineno"> 14</span><spanclass="comment">// This file defines the needed classes to efficiently perform Local Search in</span></div>
<divclass="line"><aid="l00016"name="l00016"></a><spanclass="lineno"> 16</span><spanclass="comment">// Local Search is a technique used to locally improve an existing solution by</span></div>
<divclass="line"><aid="l00017"name="l00017"></a><spanclass="lineno"> 17</span><spanclass="comment">// flipping a limited number of variables. To be successful the produced</span></div>
<divclass="line"><aid="l00018"name="l00018"></a><spanclass="lineno"> 18</span><spanclass="comment">// solution has to satisfy all constraints of the problem and improve the</span></div>
<divclass="line"><aid="l00021"name="l00021"></a><spanclass="lineno"> 21</span><spanclass="comment">// The class BopLocalSearchOptimizer is the only public interface for Local</span></div>
<divclass="line"><aid="l00022"name="l00022"></a><spanclass="lineno"> 22</span><spanclass="comment">// Search in Bop. For unit-testing purposes this file also contains the four</span></div>
<divclass="line"><aid="l00024"name="l00024"></a><spanclass="lineno"> 24</span><spanclass="comment">// OneFlipConstraintRepairer, SatWrapper and LocalSearchAssignmentIterator.</span></div>
<divclass="line"><aid="l00025"name="l00025"></a><spanclass="lineno"> 25</span><spanclass="comment">// They are implementation details and should not be used outside of bop_ls.</span></div>
<divclass="line"><aid="l00048"name="l00048"></a><spanclass="lineno"> 48</span><spanclass="comment">// This class is used to ease the connection with the SAT solver.</span></div>
<divclass="line"><aid="l00050"name="l00050"></a><spanclass="lineno"> 50</span><spanclass="comment">// TODO(user): remove? the meat of the logic is used in just one place, so I am</span></div>
<divclass="line"><aid="l00051"name="l00051"></a><spanclass="lineno"> 51</span><spanclass="comment">// not sure having this extra layer improve the readability.</span></div>
<divclass="line"><aid="l00056"name="l00056"></a><spanclass="lineno"> 56</span><spanclass="comment">// Returns the current state of the solver propagation trail.</span></div>
<divclass="line"><aid="l00059"name="l00059"></a><spanclass="lineno"> 59</span><spanclass="comment">// Returns true if the problem is UNSAT.</span></div>
<divclass="line"><aid="l00060"name="l00060"></a><spanclass="lineno"> 60</span><spanclass="comment">// Note that an UNSAT problem might not be marked as UNSAT at first because</span></div>
<divclass="line"><aid="l00061"name="l00061"></a><spanclass="lineno"> 61</span><spanclass="comment">// the SAT solver is not able to prove it; After some decisions / learned</span></div>
<divclass="line"><aid="l00062"name="l00062"></a><spanclass="lineno"> 62</span><spanclass="comment">// conflicts, the SAT solver might be able to prove UNSAT and so this will</span></div>
<divclass="line"><aid="l00066"name="l00066"></a><spanclass="lineno"> 66</span><spanclass="comment">// Return the current solver VariablesAssignment.</span></div>
<divclass="line"><aid="l00071"name="l00071"></a><spanclass="lineno"> 71</span><spanclass="comment">// Applies the decision that makes the given literal true and returns the</span></div>
<divclass="line"><aid="l00072"name="l00072"></a><spanclass="lineno"> 72</span><spanclass="comment">// number of decisions to backtrack due to conflicts if any.</span></div>
<divclass="line"><aid="l00073"name="l00073"></a><spanclass="lineno"> 73</span><spanclass="comment">// Two cases:</span></div>
<divclass="line"><aid="l00074"name="l00074"></a><spanclass="lineno"> 74</span><spanclass="comment">// - No conflicts: Returns 0 and fills the propagated_literals with the</span></div>
<divclass="line"><aid="l00075"name="l00075"></a><spanclass="lineno"> 75</span><spanclass="comment">// literals that have been propagated due to the decision including the</span></div>
<divclass="line"><aid="l00076"name="l00076"></a><spanclass="lineno"> 76</span><spanclass="comment">// the decision itself.</span></div>
<divclass="line"><aid="l00077"name="l00077"></a><spanclass="lineno"> 77</span><spanclass="comment">// - Conflicts: Returns the number of decisions to backtrack (the current</span></div>
<divclass="line"><aid="l00078"name="l00078"></a><spanclass="lineno"> 78</span><spanclass="comment">// decision included, i.e. returned value > 0) and fills the</span></div>
<divclass="line"><aid="l00079"name="l00079"></a><spanclass="lineno"> 79</span><spanclass="comment">// propagated_literals with the literals that the conflicts propagated.</span></div>
<divclass="line"><aid="l00080"name="l00080"></a><spanclass="lineno"> 80</span><spanclass="comment">// Note that the decision variable should not be already assigned in SAT.</span></div>
<divclass="line"><aid="l00084"name="l00084"></a><spanclass="lineno"> 84</span><spanclass="comment">// Backtracks the last decision if any.</span></div>
<divclass="line"><aid="l00090"name="l00090"></a><spanclass="lineno"> 90</span><spanclass="comment">// Extracts any new information learned during the search.</span></div>
<divclass="line"><aid="l00093"name="l00093"></a><spanclass="lineno"> 93</span><spanclass="comment">// Returns a deterministic number that should be correlated with the time</span></div>
<divclass="line"><aid="l00094"name="l00094"></a><spanclass="lineno"> 94</span><spanclass="comment">// spent in the SAT wrapper. The order of magnitude should be close to the</span></div>
<divclass="line"><aid="l00095"name="l00095"></a><spanclass="lineno"> 95</span><spanclass="comment">// time in seconds.</span></div>
<divclass="line"><aid="l00106"name="l00106"></a><spanclass="lineno"> 106</span><spanclass="comment">// This class defines a Local Search optimizer. The goal is to find a new</span></div>
<divclass="line"><aid="l00107"name="l00107"></a><spanclass="lineno"> 107</span><spanclass="comment">// solution with a better cost than the given solution by iterating on all</span></div>
<divclass="line"><aid="l00108"name="l00108"></a><spanclass="lineno"> 108</span><spanclass="comment">// assignments that can be reached in max_num_decisions decisions or less.</span></div>
<divclass="line"><aid="l00109"name="l00109"></a><spanclass="lineno"> 109</span><spanclass="comment">// The bop parameter max_number_of_explored_assignments_per_try_in_ls can be</span></div>
<divclass="line"><aid="l00110"name="l00110"></a><spanclass="lineno"> 110</span><spanclass="comment">// used to specify the number of new assignments to iterate on each time the</span></div>
<divclass="line"><aid="l00111"name="l00111"></a><spanclass="lineno"> 111</span><spanclass="comment">// method Optimize() is called. Limiting that parameter allows to reduce the</span></div>
<divclass="line"><aid="l00112"name="l00112"></a><spanclass="lineno"> 112</span><spanclass="comment">// time spent in the Optimize() method at once, and still explore all the</span></div>
<divclass="line"><aid="l00113"name="l00113"></a><spanclass="lineno"> 113</span><spanclass="comment">// reachable assignments (if Optimize() is called enough times).</span></div>
<divclass="line"><aid="l00114"name="l00114"></a><spanclass="lineno"> 114</span><spanclass="comment">// Note that due to propagation, the number of variables with a different value</span></div>
<divclass="line"><aid="l00115"name="l00115"></a><spanclass="lineno"> 115</span><spanclass="comment">// in the new solution can be greater than max_num_decisions.</span></div>
<divclass="line"><aid="l00130"name="l00130"></a><spanclass="lineno"> 130</span><spanclass="comment">// Maximum number of decisions the Local Search can take.</span></div>
<divclass="line"><aid="l00131"name="l00131"></a><spanclass="lineno"> 131</span><spanclass="comment">// Note that there is no limit on the number of changed variables due to</span></div>
<divclass="line"><aid="l00135"name="l00135"></a><spanclass="lineno"> 135</span><spanclass="comment">// A wrapper around the given sat_propagator.</span></div>
<divclass="line"><aid="l00138"name="l00138"></a><spanclass="lineno"> 138</span><spanclass="comment">// Iterator on all reachable assignments.</span></div>
<divclass="line"><aid="l00139"name="l00139"></a><spanclass="lineno"> 139</span><spanclass="comment">// Note that this iterator is only reset when Synchronize() is called, i.e.</span></div>
<divclass="line"><aid="l00140"name="l00140"></a><spanclass="lineno"> 140</span><spanclass="comment">// the iterator continues its iteration of the next assignments each time</span></div>
<divclass="line"><aid="l00141"name="l00141"></a><spanclass="lineno"> 141</span><spanclass="comment">// Optimize() is called until everything is explored or a solution is found.</span></div>
<divclass="line"><aid="l00146"name="l00146"></a><spanclass="lineno"> 146</span><spanclass="comment">// Implementation details. The declarations of those utility classes are in</span></div>
<divclass="line"><aid="l00147"name="l00147"></a><spanclass="lineno"> 147</span><spanclass="comment">// the .h for testing reasons.</span></div>
<divclass="line"><aid="l00150"name="l00150"></a><spanclass="lineno"> 150</span><spanclass="comment">// Maintains some information on a sparse set of integers in [0, n). More</span></div>
<divclass="line"><aid="l00151"name="l00151"></a><spanclass="lineno"> 151</span><spanclass="comment">// specifically this class:</span></div>
<divclass="line"><aid="l00152"name="l00152"></a><spanclass="lineno"> 152</span><spanclass="comment">// - Allows to dynamically add/remove element from the set.</span></div>
<divclass="line"><aid="l00153"name="l00153"></a><spanclass="lineno"> 153</span><spanclass="comment">// - Has a backtracking support.</span></div>
<divclass="line"><aid="l00154"name="l00154"></a><spanclass="lineno"> 154</span><spanclass="comment">// - Maintains the number of elements in the set.</span></div>
<divclass="line"><aid="l00155"name="l00155"></a><spanclass="lineno"> 155</span><spanclass="comment">// - Maintains a superset of the elements of the set that contains all the</span></div>
<divclass="line"><aid="l00162"name="l00162"></a><spanclass="lineno"> 162</span><spanclass="comment">// Prepares the class for integers in [0, n) and initializes the set to the</span></div>
<divclass="line"><aid="l00163"name="l00163"></a><spanclass="lineno"> 163</span><spanclass="comment">// empty one. Note that this run in O(n). Once resized, it is better to call</span></div>
<divclass="line"><aid="l00164"name="l00164"></a><spanclass="lineno"> 164</span><spanclass="comment">// BacktrackAll() instead of this to clear the set.</span></div>
<divclass="line"><aid="l00167"name="l00167"></a><spanclass="lineno"> 167</span><spanclass="comment">// Changes the state of the given integer i to be either inside or outside the</span></div>
<divclass="line"><aid="l00168"name="l00168"></a><spanclass="lineno"> 168</span><spanclass="comment">// set. Important: this should only be called with the opposite state of the</span></div>
<divclass="line"><aid="l00169"name="l00169"></a><spanclass="lineno"> 169</span><spanclass="comment">// current one, otherwise size() will not be correct.</span></div>
<divclass="line"><aid="l00170"name="l00170"></a><spanclass="lineno"> 170</span><spanclass="keywordtype">void</span><aclass="code hl_function"href="classoperations__research_1_1bop_1_1_backtrackable_integer_set.html#aba10677c63ecfdabe3116c4e08c31aa1">ChangeState</a>(IntType i, <spanclass="keywordtype">bool</span> should_be_inside);</div>
<divclass="line"><aid="l00172"name="l00172"></a><spanclass="lineno"> 172</span><spanclass="comment">// Returns the current number of elements in the set.</span></div>
<divclass="line"><aid="l00173"name="l00173"></a><spanclass="lineno"> 173</span><spanclass="comment">// Note that this is not its maximum size n.</span></div>
<divclass="line"><aid="l00176"name="l00176"></a><spanclass="lineno"> 176</span><spanclass="comment">// Returns a superset of the current set of integers.</span></div>
<divclass="line"><aid="l00179"name="l00179"></a><spanclass="lineno"> 179</span><spanclass="comment">// BacktrackOneLevel() backtracks to the state the class was in when the</span></div>
<divclass="line"><aid="l00180"name="l00180"></a><spanclass="lineno"> 180</span><spanclass="comment">// last AddBacktrackingLevel() was called. BacktrackAll() just restore the</span></div>
<divclass="line"><aid="l00181"name="l00181"></a><spanclass="lineno"> 181</span><spanclass="comment">// class to its state just after the last ClearAndResize().</span></div>
<divclass="line"><aid="l00189"name="l00189"></a><spanclass="lineno"> 189</span><spanclass="comment">// Contains the elements whose status has been changed at least once.</span></div>
<divclass="line"><aid="l00193"name="l00193"></a><spanclass="lineno"> 193</span><spanclass="comment">// Used for backtracking. Contains the size_ and the stack_.size() at the time</span></div>
<divclass="line"><aid="l00194"name="l00194"></a><spanclass="lineno"> 194</span><spanclass="comment">// of each call to AddBacktrackingLevel() that is not yet backtracked over.</span></div>
<divclass="line"><aid="l00199"name="l00199"></a><spanclass="lineno"> 199</span><spanclass="comment">// A simple and efficient class to hash a given set of integers in [0, n).</span></div>
<divclass="line"><aid="l00200"name="l00200"></a><spanclass="lineno"> 200</span><spanclass="comment">// It uses O(n) memory and produces a good hash (random linear function).</span></div>
<divclass="line"><aid="l00206"name="l00206"></a><spanclass="lineno"> 206</span><spanclass="comment">// Initializes the NonOrderedSetHasher to hash sets of integer in [0, n).</span></div>
<divclass="line"><aid="l00214"name="l00214"></a><spanclass="lineno"> 214</span><spanclass="comment">// Ignores the given set element in all subsequent hash computation. Note that</span></div>
<divclass="line"><aid="l00215"name="l00215"></a><spanclass="lineno"> 215</span><spanclass="comment">// this will be reset by the next call to Initialize().</span></div>
<divclass="line"><aid="l00218"name="l00218"></a><spanclass="lineno"> 218</span><spanclass="comment">// Returns the hash of the given set. The hash is independent of the set</span></div>
<divclass="line"><aid="l00219"name="l00219"></a><spanclass="lineno"> 219</span><spanclass="comment">// order, but there must be no duplicate element in the set. This uses a</span></div>
<divclass="line"><aid="l00220"name="l00220"></a><spanclass="lineno"> 220</span><spanclass="comment">// simple random linear function which has really good hashing properties.</span></div>
<divclass="line"><aid="l00227"name="l00227"></a><spanclass="lineno"> 227</span><spanclass="comment">// The hash of a set is simply the XOR of all its elements. This allows</span></div>
<divclass="line"><aid="l00228"name="l00228"></a><spanclass="lineno"> 228</span><spanclass="comment">// to compute an hash incrementally or without the need of a vector<>.</span></div>
<divclass="line"><aid="l00231"name="l00231"></a><spanclass="lineno"> 231</span><spanclass="comment">// Returns true if Initialize() has been called with a non-zero size.</span></div>
<divclass="line"><aid="l00239"name="l00239"></a><spanclass="lineno"> 239</span><spanclass="comment">// This class is used to incrementally maintain an assignment and the</span></div>
<divclass="line"><aid="l00240"name="l00240"></a><spanclass="lineno"> 240</span><spanclass="comment">// feasibility of the constraints of a given LinearBooleanProblem.</span></div>
<divclass="line"><aid="l00242"name="l00242"></a><spanclass="lineno"> 242</span><spanclass="comment">// The current assignment is initialized using a feasible reference solution,</span></div>
<divclass="line"><aid="l00243"name="l00243"></a><spanclass="lineno"> 243</span><spanclass="comment">// i.e. the reference solution satisfies all the constraints of the problem.</span></div>
<divclass="line"><aid="l00244"name="l00244"></a><spanclass="lineno"> 244</span><spanclass="comment">// The current assignment is updated using the Assign() method.</span></div>
<divclass="line"><aid="l00246"name="l00246"></a><spanclass="lineno"> 246</span><spanclass="comment">// Note that the current assignment is not a solution in the sense that it</span></div>
<divclass="line"><aid="l00247"name="l00247"></a><spanclass="lineno"> 247</span><spanclass="comment">// might not be feasible, ie. violates some constraints.</span></div>
<divclass="line"><aid="l00249"name="l00249"></a><spanclass="lineno"> 249</span><spanclass="comment">// The assignment can be accessed at any time using Assignment().</span></div>
<divclass="line"><aid="l00250"name="l00250"></a><spanclass="lineno"> 250</span><spanclass="comment">// The set of infeasible constraints can be accessed at any time using</span></div>
<divclass="line"><aid="l00253"name="l00253"></a><spanclass="lineno"> 253</span><spanclass="comment">// Note that this class is reversible, i.e. it is possible to backtrack to</span></div>
<divclass="line"><aid="l00255"name="l00255"></a><spanclass="lineno"> 255</span><spanclass="comment">// levels. Consider for instance variable a, b, c, and d.</span></div>
<divclass="line"><aid="l00256"name="l00256"></a><spanclass="lineno"> 256</span><spanclass="comment">// Method called Assigned after method call</span></div>
<divclass="line"><aid="l00257"name="l00257"></a><spanclass="lineno"> 257</span><spanclass="comment">// 1- Assign({a, b}) a b</span></div>
<divclass="line"><aid="l00258"name="l00258"></a><spanclass="lineno"> 258</span><spanclass="comment">// 2- AddBacktrackingLevel() a b |</span></div>
<divclass="line"><aid="l00259"name="l00259"></a><spanclass="lineno"> 259</span><spanclass="comment">// 3- Assign({c}) a b | c</span></div>
<divclass="line"><aid="l00260"name="l00260"></a><spanclass="lineno"> 260</span><spanclass="comment">// 4- Assign({d}) a b | c d</span></div>
<divclass="line"><aid="l00261"name="l00261"></a><spanclass="lineno"> 261</span><spanclass="comment">// 5- BacktrackOneLevel() a b</span></div>
<divclass="line"><aid="l00262"name="l00262"></a><spanclass="lineno"> 262</span><spanclass="comment">// 6- Assign({c}) a b c</span></div>
<divclass="line"><aid="l00266"name="l00266"></a><spanclass="lineno"> 266</span><spanclass="comment">// Note that the constraint indices used in this class are not the same as</span></div>
<divclass="line"><aid="l00267"name="l00267"></a><spanclass="lineno"> 267</span><spanclass="comment">// the one used in the given LinearBooleanProblem here.</span></div>
<divclass="line"><aid="l00271"name="l00271"></a><spanclass="lineno"> 271</span><spanclass="comment">// When we construct the problem, we treat the objective as one constraint.</span></div>
<divclass="line"><aid="l00272"name="l00272"></a><spanclass="lineno"> 272</span><spanclass="comment">// This is the index of this special "objective" constraint.</span></div>
<divclass="line"><aid="l00275"name="l00275"></a><spanclass="lineno"> 275</span><spanclass="comment">// Sets a new reference solution and reverts all internal structures to their</span></div>
<divclass="line"><aid="l00276"name="l00276"></a><spanclass="lineno"> 276</span><spanclass="comment">// initial state. Note that the reference solution has to be feasible.</span></div>
<divclass="line"><aid="l00279"name="l00279"></a><spanclass="lineno"> 279</span><spanclass="comment">// Behaves exactly like SetReferenceSolution() where the passed reference</span></div>
<divclass="line"><aid="l00280"name="l00280"></a><spanclass="lineno"> 280</span><spanclass="comment">// is the current assignment held by this class. Note that the current</span></div>
<divclass="line"><aid="l00281"name="l00281"></a><spanclass="lineno"> 281</span><spanclass="comment">// assignment must be feasible (i.e. IsFeasible() is true).</span></div>
<divclass="line"><aid="l00284"name="l00284"></a><spanclass="lineno"> 284</span><spanclass="comment">// Assigns all literals. That updates the assignment, the constraint values,</span></div>
<divclass="line"><aid="l00285"name="l00285"></a><spanclass="lineno"> 285</span><spanclass="comment">// and the infeasible constraints.</span></div>
<divclass="line"><aid="l00286"name="l00286"></a><spanclass="lineno"> 286</span><spanclass="comment">// Note that the assignment of those literals can be reverted thanks to</span></div>
<divclass="line"><aid="l00287"name="l00287"></a><spanclass="lineno"> 287</span><spanclass="comment">// AddBacktrackingLevel() and BacktrackOneLevel().</span></div>
<divclass="line"><aid="l00288"name="l00288"></a><spanclass="lineno"> 288</span><spanclass="comment">// Note that a variable can't be assigned twice, even for the same literal.</span></div>
<divclass="line"><aid="l00291"name="l00291"></a><spanclass="lineno"> 291</span><spanclass="comment">// Adds a new backtracking level to specify the state that will be restored</span></div>
<divclass="line"><aid="l00292"name="l00292"></a><spanclass="lineno"> 292</span><spanclass="comment">// by BacktrackOneLevel().</span></div>
<divclass="line"><aid="l00293"name="l00293"></a><spanclass="lineno"> 293</span><spanclass="comment">// See the example in the class comment.</span></div>
<divclass="line"><aid="l00296"name="l00296"></a><spanclass="lineno"> 296</span><spanclass="comment">// Backtracks internal structures to the previous level defined by</span></div>
<divclass="line"><aid="l00297"name="l00297"></a><spanclass="lineno"> 297</span><spanclass="comment">// AddBacktrackingLevel(). As a consequence the state will be exactly as</span></div>
<divclass="line"><aid="l00298"name="l00298"></a><spanclass="lineno"> 298</span><spanclass="comment">// before the previous call to AddBacktrackingLevel().</span></div>
<divclass="line"><aid="l00299"name="l00299"></a><spanclass="lineno"> 299</span><spanclass="comment">// Note that backtracking the initial state has no effect.</span></div>
<divclass="line"><aid="l00303"name="l00303"></a><spanclass="lineno"> 303</span><spanclass="comment">// This returns the list of literal that appear in exactly all the current</span></div>
<divclass="line"><aid="l00304"name="l00304"></a><spanclass="lineno"> 304</span><spanclass="comment">// infeasible constraints (ignoring the objective) and correspond to a flip in</span></div>
<divclass="line"><aid="l00305"name="l00305"></a><spanclass="lineno"> 305</span><spanclass="comment">// a good direction for all the infeasible constraint. Performing this flip</span></div>
<divclass="line"><aid="l00306"name="l00306"></a><spanclass="lineno"> 306</span><spanclass="comment">// may repair the problem without any propagations.</span></div>
<divclass="line"><aid="l00308"name="l00308"></a><spanclass="lineno"> 308</span><spanclass="comment">// Important: The returned reference is only valid until the next</span></div>
<divclass="line"><aid="l00312"name="l00312"></a><spanclass="lineno"> 312</span><spanclass="comment">// Returns true if there is no infeasible constraint in the current state.</span></div>
<divclass="line"><aid="l00315"name="l00315"></a><spanclass="lineno"> 315</span><spanclass="comment">// Returns the *exact* number of infeasible constraints.</span></div>
<divclass="line"><aid="l00316"name="l00316"></a><spanclass="lineno"> 316</span><spanclass="comment">// Note that PossiblyInfeasibleConstraints() will potentially return a larger</span></div>
<divclass="line"><aid="l00317"name="l00317"></a><spanclass="lineno"> 317</span><spanclass="comment">// number of constraints.</span></div>
<divclass="line"><aid="l00322"name="l00322"></a><spanclass="lineno"> 322</span><spanclass="comment">// Returns a superset of all the infeasible constraints in the current state.</span></div>
<divclass="line"><aid="l00327"name="l00327"></a><spanclass="lineno"> 327</span><spanclass="comment">// Returns the number of constraints of the problem, objective included,</span></div>
<divclass="line"><aid="l00328"name="l00328"></a><spanclass="lineno"> 328</span><spanclass="comment">// i.e. the number of constraint in the problem + 1.</span></div>
<divclass="line"><aid="l00331"name="l00331"></a><spanclass="lineno"> 331</span><spanclass="comment">// Returns the value of the var in the assignment.</span></div>
<divclass="line"><aid="l00332"name="l00332"></a><spanclass="lineno"> 332</span><spanclass="comment">// As the assignment is initialized with the reference solution, if the</span></div>
<divclass="line"><aid="l00333"name="l00333"></a><spanclass="lineno"> 333</span><spanclass="comment">// variable has not been assigned through Assign(), the returned value is</span></div>
<divclass="line"><aid="l00334"name="l00334"></a><spanclass="lineno"> 334</span><spanclass="comment">// the value of the variable in the reference solution.</span></div>
<divclass="line"><aid="l00340"name="l00340"></a><spanclass="lineno"> 340</span><spanclass="comment">// Returns the lower bound of the constraint.</span></div>
<divclass="line"><aid="l00345"name="l00345"></a><spanclass="lineno"> 345</span><spanclass="comment">// Returns the upper bound of the constraint.</span></div>
<divclass="line"><aid="l00350"name="l00350"></a><spanclass="lineno"> 350</span><spanclass="comment">// Returns the value of the constraint. The value is computed using the</span></div>
<divclass="line"><aid="l00351"name="l00351"></a><spanclass="lineno"> 351</span><spanclass="comment">// variable values in the assignment. Note that a constraint is feasible iff</span></div>
<divclass="line"><aid="l00352"name="l00352"></a><spanclass="lineno"> 352</span><spanclass="comment">// its value is between its two bounds (inclusive).</span></div>
<divclass="line"><aid="l00357"name="l00357"></a><spanclass="lineno"> 357</span><spanclass="comment">// Returns true if the given constraint is currently feasible.</span></div>
<divclass="line"><aid="l00367"name="l00367"></a><spanclass="lineno"> 367</span><spanclass="comment">// This is lazily called by PotentialOneFlipRepairs() once.</span></div>
<divclass="line"><aid="l00370"name="l00370"></a><spanclass="lineno"> 370</span><spanclass="comment">// This is used by PotentialOneFlipRepairs(). It encodes a ConstraintIndex</span></div>
<divclass="line"><aid="l00371"name="l00371"></a><spanclass="lineno"> 371</span><spanclass="comment">// together with a "repair" direction depending on the bound that make a</span></div>
<divclass="line"><aid="l00372"name="l00372"></a><spanclass="lineno"> 372</span><spanclass="comment">// constraint infeasible. An "up" direction means that the constraint activity</span></div>
<divclass="line"><aid="l00373"name="l00373"></a><spanclass="lineno"> 373</span><spanclass="comment">// is lower than the lower bound and we need to make the activity move up to</span></div>
<divclass="line"><aid="l00374"name="l00374"></a><spanclass="lineno"> 374</span><spanclass="comment">// fix the infeasibility.</span></div>
<divclass="line"><aid="l00381"name="l00381"></a><spanclass="lineno"> 381</span><spanclass="comment">// Over constrains the objective cost by the given delta. This should only be</span></div>
<divclass="line"><aid="l00382"name="l00382"></a><spanclass="lineno"> 382</span><spanclass="comment">// called on a feasible reference solution and a fully backtracked state.</span></div>
<divclass="line"><aid="l00385"name="l00385"></a><spanclass="lineno"> 385</span><spanclass="comment">// Local structure to represent the sparse matrix by variable used for fast</span></div>
<divclass="line"><aid="l00386"name="l00386"></a><spanclass="lineno"> 386</span><spanclass="comment">// update of the contraint values.</span></div>
<divclass="line"><aid="l00405"name="l00405"></a><spanclass="lineno"> 405</span><spanclass="comment">// This contains the list of variable flipped in assignment_.</span></div>
<divclass="line"><aid="l00406"name="l00406"></a><spanclass="lineno"> 406</span><spanclass="comment">// flipped_var_trail_backtrack_levels_[i-1] is the index in flipped_var_trail_</span></div>
<divclass="line"><aid="l00407"name="l00407"></a><spanclass="lineno"> 407</span><spanclass="comment">// of the first variable flipped after the i-th AddBacktrackingLevel() call.</span></div>
<divclass="line"><aid="l00411"name="l00411"></a><spanclass="lineno"> 411</span><spanclass="comment">// Members used by PotentialOneFlipRepairs().</span></div>
<divclass="line"><aid="l00420"name="l00420"></a><spanclass="lineno"> 420</span><spanclass="comment">// This class is an utility class used to select which infeasible constraint to</span></div>
<divclass="line"><aid="l00421"name="l00421"></a><spanclass="lineno"> 421</span><spanclass="comment">// repair and identify one variable to flip to actually repair the constraint.</span></div>
<divclass="line"><aid="l00422"name="l00422"></a><spanclass="lineno"> 422</span><spanclass="comment">// A constraint 'lb <= sum_i(w_i * x_i) <= ub', with 'lb' the lower bound,</span></div>
<divclass="line"><aid="l00423"name="l00423"></a><spanclass="lineno"> 423</span><spanclass="comment">// 'ub' the upper bound, 'w_i' the weight of the i-th term and 'x_i' the</span></div>
<divclass="line"><aid="l00424"name="l00424"></a><spanclass="lineno"> 424</span><spanclass="comment">// boolean variable appearing in the i-th term, is infeasible for a given</span></div>
<divclass="line"><aid="l00425"name="l00425"></a><spanclass="lineno"> 425</span><spanclass="comment">// assignment iff its value 'sum_i(w_i * x_i)' is outside of the bounds.</span></div>
<divclass="line"><aid="l00426"name="l00426"></a><spanclass="lineno"> 426</span><spanclass="comment">// Repairing-a-constraint-in-one-flip means making the constraint feasible by</span></div>
<divclass="line"><aid="l00427"name="l00427"></a><spanclass="lineno"> 427</span><spanclass="comment">// just flipping the value of one unassigned variable of the current assignment</span></div>
<divclass="line"><aid="l00428"name="l00428"></a><spanclass="lineno"> 428</span><spanclass="comment">// from the AssignmentAndConstraintFeasibilityMaintainer.</span></div>
<divclass="line"><aid="l00429"name="l00429"></a><spanclass="lineno"> 429</span><spanclass="comment">// For performance reasons, the pairs weight / variable (w_i, x_i) are stored</span></div>
<divclass="line"><aid="l00430"name="l00430"></a><spanclass="lineno"> 430</span><spanclass="comment">// in a sparse manner as a vector of terms (w_i, x_i). In the following the</span></div>
<divclass="line"><aid="l00431"name="l00431"></a><spanclass="lineno"> 431</span><spanclass="comment">// TermIndex term_index refers to the position of the term in the vector.</span></div>
<divclass="line"><aid="l00434"name="l00434"></a><spanclass="lineno"> 434</span><spanclass="comment">// Note that the constraint indices used in this class follow the same</span></div>
<divclass="line"><aid="l00435"name="l00435"></a><spanclass="lineno"> 435</span><spanclass="comment">// convention as the one used in the</span></div>
<divclass="line"><aid="l00438"name="l00438"></a><spanclass="lineno"> 438</span><spanclass="comment">// TODO(user): maybe merge the two classes? maintaining this implicit indices</span></div>
<divclass="line"><aid="l00439"name="l00439"></a><spanclass="lineno"> 439</span><spanclass="comment">// convention between the two classes sounds like a bad idea.</span></div>
<divclass="line"><aid="l00449"name="l00449"></a><spanclass="lineno"> 449</span><spanclass="comment">// Returns the index of a constraint to repair. This will always return the</span></div>
<divclass="line"><aid="l00450"name="l00450"></a><spanclass="lineno"> 450</span><spanclass="comment">// index of a constraint that can be repaired in one flip if there is one.</span></div>
<divclass="line"><aid="l00451"name="l00451"></a><spanclass="lineno"> 451</span><spanclass="comment">// Note however that if there is only one possible candidate, it will be</span></div>
<divclass="line"><aid="l00452"name="l00452"></a><spanclass="lineno"> 452</span><spanclass="comment">// returned without checking that it can indeed be repaired in one flip.</span></div>
<divclass="line"><aid="l00453"name="l00453"></a><spanclass="lineno"> 453</span><spanclass="comment">// This is because the later check can be expensive, and is not needed in our</span></div>
<divclass="line"><aid="l00457"name="l00457"></a><spanclass="lineno"> 457</span><spanclass="comment">// Returns the index of the next term which repairs the constraint when the</span></div>
<divclass="line"><aid="l00458"name="l00458"></a><spanclass="lineno"> 458</span><spanclass="comment">// value of its variable is flipped. This method explores terms with an</span></div>
<divclass="line"><aid="l00459"name="l00459"></a><spanclass="lineno"> 459</span><spanclass="comment">// index strictly greater than start_term_index and then terms with an index</span></div>
<divclass="line"><aid="l00460"name="l00460"></a><spanclass="lineno"> 460</span><spanclass="comment">// smaller than or equal to init_term_index if any.</span></div>
<divclass="line"><aid="l00461"name="l00461"></a><spanclass="lineno"> 461</span><spanclass="comment">// Returns kInvalidTerm when no reparing terms are found.</span></div>
<divclass="line"><aid="l00463"name="l00463"></a><spanclass="lineno"> 463</span><spanclass="comment">// Note that if init_term_index == start_term_index, then all the terms will</span></div>
<divclass="line"><aid="l00464"name="l00464"></a><spanclass="lineno"> 464</span><spanclass="comment">// be explored. Both TermIndex arguments can take values in [-1, constraint</span></div>
<divclass="line"><aid="l00470"name="l00470"></a><spanclass="lineno"> 470</span><spanclass="comment">// Returns true if the constraint is infeasible and if flipping the variable</span></div>
<divclass="line"><aid="l00471"name="l00471"></a><spanclass="lineno"> 471</span><spanclass="comment">// at the given index will repair it.</span></div>
<divclass="line"><aid="l00474"name="l00474"></a><spanclass="lineno"> 474</span><spanclass="comment">// Returns the literal formed by the variable at the given constraint term and</span></div>
<divclass="line"><aid="l00475"name="l00475"></a><spanclass="lineno"> 475</span><spanclass="comment">// assigned to the opposite value of this variable in the current assignment.</span></div>
<divclass="line"><aid="l00478"name="l00478"></a><spanclass="lineno"> 478</span><spanclass="comment">// Local structure to represent the sparse matrix by constraint used for fast</span></div>
<divclass="line"><aid="l00487"name="l00487"></a><spanclass="lineno"> 487</span><spanclass="comment">// Sorts the terms of each constraints in the by_constraint_matrix_ to iterate</span></div>
<divclass="line"><aid="l00488"name="l00488"></a><spanclass="lineno"> 488</span><spanclass="comment">// on most promising variables first.</span></div>
<divclass="line"><aid="l00500"name="l00500"></a><spanclass="lineno"> 500</span><spanclass="comment">// This class is used to iterate on all assignments that can be obtained by</span></div>
<divclass="line"><aid="l00501"name="l00501"></a><spanclass="lineno"> 501</span><spanclass="comment">// deliberately flipping 'n' variables from the reference solution, 'n' being</span></div>
<divclass="line"><aid="l00502"name="l00502"></a><spanclass="lineno"> 502</span><spanclass="comment">// smaller than or equal to max_num_decisions.</span></div>
<divclass="line"><aid="l00503"name="l00503"></a><spanclass="lineno"> 503</span><spanclass="comment">// Note that one deliberate variable flip may lead to many other flips due to</span></div>
<divclass="line"><aid="l00504"name="l00504"></a><spanclass="lineno"> 504</span><spanclass="comment">// constraint propagation, those additional flips are not counted in 'n'.</span></div>
<divclass="line"><aid="l00519"name="l00519"></a><spanclass="lineno"> 519</span><spanclass="comment">// Synchronizes the iterator with the problem state, e.g. set fixed variables,</span></div>
<divclass="line"><aid="l00520"name="l00520"></a><spanclass="lineno"> 520</span><spanclass="comment">// set the reference solution. Call this only when a new solution has been</span></div>
<divclass="line"><aid="l00521"name="l00521"></a><spanclass="lineno"> 521</span><spanclass="comment">// found. This will restart the LS.</span></div>
<divclass="line"><aid="l00524"name="l00524"></a><spanclass="lineno"> 524</span><spanclass="comment">// Synchronize the SatWrapper with our current search state. This needs to be</span></div>
<divclass="line"><aid="l00525"name="l00525"></a><spanclass="lineno"> 525</span><spanclass="comment">// called before calls to NextAssignment() if the underlying SatWrapper was</span></div>
<divclass="line"><aid="l00526"name="l00526"></a><spanclass="lineno"> 526</span><spanclass="comment">// used by someone else than this class.</span></div>
<divclass="line"><aid="l00529"name="l00529"></a><spanclass="lineno"> 529</span><spanclass="comment">// Move to the next assignment. Returns false when the search is finished.</span></div>
<divclass="line"><aid="l00532"name="l00532"></a><spanclass="lineno"> 532</span><spanclass="comment">// Returns the last feasible assignment.</span></div>
<divclass="line"><aid="l00537"name="l00537"></a><spanclass="lineno"> 537</span><spanclass="comment">// Returns true if the current assignment has a better solution than the one</span></div>
<divclass="line"><aid="l00538"name="l00538"></a><spanclass="lineno"> 538</span><spanclass="comment">// passed to the last Synchronize() call.</span></div>
<divclass="line"><aid="l00543"name="l00543"></a><spanclass="lineno"> 543</span><spanclass="comment">// Returns a deterministic number that should be correlated with the time</span></div>
<divclass="line"><aid="l00544"name="l00544"></a><spanclass="lineno"> 544</span><spanclass="comment">// spent in the iterator. The order of magnitude should be close to the time</span></div>
<divclass="line"><aid="l00545"name="l00545"></a><spanclass="lineno"> 545</span><spanclass="comment">// in seconds.</span></div>
<divclass="line"><aid="l00551"name="l00551"></a><spanclass="lineno"> 551</span><spanclass="comment">// This is called when a better solution has been found to restore the search</span></div>
<divclass="line"><aid="l00552"name="l00552"></a><spanclass="lineno"> 552</span><spanclass="comment">// to the new "root" node.</span></div>
<divclass="line"><aid="l00558"name="l00558"></a><spanclass="lineno"> 558</span><spanclass="comment">// Internal structure used to represent a node of the search tree during local</span></div>
<divclass="line"><aid="l00569"name="l00569"></a><spanclass="lineno"> 569</span><spanclass="comment">// Applies the decision. Automatically backtracks when SAT detects conflicts.</span></div>
<divclass="line"><aid="l00572"name="l00572"></a><spanclass="lineno"> 572</span><spanclass="comment">// Adds one more decision to repair infeasible constraints.</span></div>
<divclass="line"><aid="l00573"name="l00573"></a><spanclass="lineno"> 573</span><spanclass="comment">// Returns true in case of success.</span></div>
<divclass="line"><aid="l00576"name="l00576"></a><spanclass="lineno"> 576</span><spanclass="comment">// Backtracks and moves to the next decision in the search tree.</span></div>
<divclass="line"><aid="l00579"name="l00579"></a><spanclass="lineno"> 579</span><spanclass="comment">// Looks if the current decisions (in search_nodes_) plus the new one (given</span></div>
<divclass="line"><aid="l00580"name="l00580"></a><spanclass="lineno"> 580</span><spanclass="comment">// by l) lead to a position already present in transposition_table_.</span></div>
<divclass="line"><aid="l00583"name="l00583"></a><spanclass="lineno"> 583</span><spanclass="comment">// Inserts the current set of decisions in transposition_table_.</span></div>
<divclass="line"><aid="l00586"name="l00586"></a><spanclass="lineno"> 586</span><spanclass="comment">// Initializes the given array with the current decisions in search_nodes_ and</span></div>
<divclass="line"><aid="l00587"name="l00587"></a><spanclass="lineno"> 587</span><spanclass="comment">// by filling the other positions with 0.</span></div>
<divclass="line"><aid="l00591"name="l00591"></a><spanclass="lineno"> 591</span><spanclass="comment">// Looks for the next repairing term in the given constraints while skipping</span></div>
<divclass="line"><aid="l00592"name="l00592"></a><spanclass="lineno"> 592</span><spanclass="comment">// the position already present in transposition_table_. A given TermIndex of</span></div>
<divclass="line"><aid="l00593"name="l00593"></a><spanclass="lineno"> 593</span><spanclass="comment">// -1 means that this is the first time we explore this constraint.</span></div>
<divclass="line"><aid="l00606"name="l00606"></a><spanclass="lineno"> 606</span><spanclass="comment">// Temporary vector used by ApplyDecision().</span></div>
<divclass="line"><aid="l00609"name="l00609"></a><spanclass="lineno"> 609</span><spanclass="comment">// For each set of explored decisions, we store it in this table so that we</span></div>
<divclass="line"><aid="l00610"name="l00610"></a><spanclass="lineno"> 610</span><spanclass="comment">// don't explore decisions (a, b) and later (b, a) for instance. The decisions</span></div>
<divclass="line"><aid="l00611"name="l00611"></a><spanclass="lineno"> 611</span><spanclass="comment">// are converted to int32_t, sorted and padded with 0 before beeing inserted</span></div>
<divclass="line"><aid="l00614"name="l00614"></a><spanclass="lineno"> 614</span><spanclass="comment">// TODO(user): We may still miss some equivalent states because it is possible</span></div>
<divclass="line"><aid="l00615"name="l00615"></a><spanclass="lineno"> 615</span><spanclass="comment">// that completely differents decisions lead to exactly the same state.</span></div>
<divclass="line"><aid="l00616"name="l00616"></a><spanclass="lineno"> 616</span><spanclass="comment">// However this is more time consuming to detect because we must apply the</span></div>
<divclass="line"><aid="l00617"name="l00617"></a><spanclass="lineno"> 617</span><spanclass="comment">// last decision first before trying to compare the states.</span></div>
<divclass="line"><aid="l00619"name="l00619"></a><spanclass="lineno"> 619</span><spanclass="comment">// TODO(user): Currently, we only store kStoredMaxDecisions or less decisions.</span></div>
<divclass="line"><aid="l00620"name="l00620"></a><spanclass="lineno"> 620</span><spanclass="comment">// Ideally, this should be related to the maximum number of decision in the</span></div>
<divclass="line"><aid="l00621"name="l00621"></a><spanclass="lineno"> 621</span><spanclass="comment">// LS, but that requires templating the whole LS optimizer.</span></div>
<divclass="line"><aid="l00631"name="l00631"></a><spanclass="lineno"> 631</span><spanclass="comment">// The number of skipped nodes thanks to the transposition table.</span></div>
<divclass="line"><aid="l00634"name="l00634"></a><spanclass="lineno"> 634</span><spanclass="comment">// The overall number of better solution found. And the ones found by the</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_1bop_1_1_assignment_and_constraint_feasibility_maintainer_html_ab75ee4d5d3256f8f0997e7620a0881b7"><divclass="ttname"><ahref="classoperations__research_1_1bop_1_1_assignment_and_constraint_feasibility_maintainer.html#ab75ee4d5d3256f8f0997e7620a0881b7">operations_research::bop::AssignmentAndConstraintFeasibilityMaintainer::reference</a></div><divclass="ttdeci">const BopSolution & reference() const</div><divclass="ttdef"><b>Definition:</b><ahref="bop__ls_8h_source.html#l00338">bop_ls.h:338</a></div></div>
<divclass="ttc"id="aclassoperations__research_1_1bop_1_1_backtrackable_integer_set_html_aba10677c63ecfdabe3116c4e08c31aa1"><divclass="ttname"><ahref="classoperations__research_1_1bop_1_1_backtrackable_integer_set.html#aba10677c63ecfdabe3116c4e08c31aa1">operations_research::bop::BacktrackableIntegerSet::ChangeState</a></div><divclass="ttdeci">void ChangeState(IntType i, bool should_be_inside)</div><divclass="ttdef"><b>Definition:</b><ahref="bop__ls_8cc_source.html#l00133">bop_ls.cc:133</a></div></div>
<divclass="ttc"id="aclassoperations__research_1_1bop_1_1_bop_optimizer_base_html_a24dcbf29c0d6cd766009a182a6484e3b"><divclass="ttname"><ahref="classoperations__research_1_1bop_1_1_bop_optimizer_base.html#a24dcbf29c0d6cd766009a182a6484e3b">operations_research::bop::BopOptimizerBase::name</a></div><divclass="ttdeci">const std::string & name() const</div><divclass="ttdef"><b>Definition:</b><ahref="bop__base_8h_source.html#l00049">bop_base.h:49</a></div></div>
<divclass="ttc"id="aclassoperations__research_1_1bop_1_1_local_search_assignment_iterator_html_a1aecf270882e0c103c53773297b1d96a"><divclass="ttname"><ahref="classoperations__research_1_1bop_1_1_local_search_assignment_iterator.html#a1aecf270882e0c103c53773297b1d96a">operations_research::bop::LocalSearchAssignmentIterator::LastReferenceAssignment</a></div><divclass="ttdeci">const BopSolution & LastReferenceAssignment() const</div><divclass="ttdef"><b>Definition:</b><ahref="bop__ls_8h_source.html#l00533">bop_ls.h:533</a></div></div>
<divclass="ttc"id="aclassoperations__research_1_1bop_1_1_local_search_assignment_iterator_html_a4c13a1377925d2ceefaea09f0c5747ff"><divclass="ttname"><ahref="classoperations__research_1_1bop_1_1_local_search_assignment_iterator.html#a4c13a1377925d2ceefaea09f0c5747ff">operations_research::bop::LocalSearchAssignmentIterator::LocalSearchAssignmentIterator</a></div><divclass="ttdeci">LocalSearchAssignmentIterator(const ProblemState &problem_state, int max_num_decisions, int max_num_broken_constraints, SatWrapper *sat_wrapper)</div><divclass="ttdef"><b>Definition:</b><ahref="bop__ls_8cc_source.html#l00679">bop_ls.cc:679</a></div></div>
<divclass="ttc"id="aclassoperations__research_1_1bop_1_1_sat_wrapper_html_ad5d7d187cc8a2b70a360d4cede96cfe9"><divclass="ttname"><ahref="classoperations__research_1_1bop_1_1_sat_wrapper.html#ad5d7d187cc8a2b70a360d4cede96cfe9">operations_research::bop::SatWrapper::SatAssignment</a></div><divclass="ttdeci">const sat::VariablesAssignment & SatAssignment() const</div><divclass="ttdef"><b>Definition:</b><ahref="bop__ls_8h_source.html#l00067">bop_ls.h:67</a></div></div>
<divclass="ttc"id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a4793952607a98dfddfbcc17abfabbb4b"><divclass="ttname"><ahref="classoperations__research_1_1sat_1_1_sat_solver.html#a4793952607a98dfddfbcc17abfabbb4b">operations_research::sat::SatSolver::Assignment</a></div><divclass="ttdeci">const VariablesAssignment & Assignment() const</div><divclass="ttdef"><b>Definition:</b><ahref="sat__solver_8h_source.html#l00363">sat_solver.h:363</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>
