<ahref="sat_2lp__utils_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">// Utility functions to interact with an lp solver from the SAT context.</span></div>
<divclass="line"><aid="l00030"name="l00030"></a><spanclass="lineno"> 30</span><spanclass="comment">// Returns the smallest factor f such that f * abs(x) is integer modulo the</span></div>
<divclass="line"><aid="l00031"name="l00031"></a><spanclass="lineno"> 31</span><spanclass="comment">// given tolerance relative to f (we use f * tolerance). It is only looking</span></div>
<divclass="line"><aid="l00032"name="l00032"></a><spanclass="lineno"> 32</span><spanclass="comment">// for f smaller than the given limit. Returns zero if no such factor exist.</span></div>
<divclass="line"><aid="l00034"name="l00034"></a><spanclass="lineno"> 34</span><spanclass="comment">// The complexity is a lot less than O(limit), but it is possible that we might</span></div>
<divclass="line"><aid="l00035"name="l00035"></a><spanclass="lineno"> 35</span><spanclass="comment">// miss the smallest such factor if the tolerance used is too low. This is</span></div>
<divclass="line"><aid="l00036"name="l00036"></a><spanclass="lineno"> 36</span><spanclass="comment">// because we only rely on the best rational approximations of x with increasing</span></div>
<divclass="line"><aid="l00040"name="l00040"></a><spanclass="lineno"> 40</span><spanclass="comment">// Multiplies all continuous variable by the given scaling parameters and change</span></div>
<divclass="line"><aid="l00041"name="l00041"></a><spanclass="lineno"> 41</span><spanclass="comment">// the rest of the model accordingly. The returned vector contains the scaling</span></div>
<divclass="line"><aid="l00042"name="l00042"></a><spanclass="lineno"> 42</span><spanclass="comment">// of each variable (will always be 1.0 for integers) and can be used to recover</span></div>
<divclass="line"><aid="l00043"name="l00043"></a><spanclass="lineno"> 43</span><spanclass="comment">// a solution of the unscaled problem from one of the new scaled problems by</span></div>
<divclass="line"><aid="l00044"name="l00044"></a><spanclass="lineno"> 44</span><spanclass="comment">// dividing the variable values.</span></div>
<divclass="line"><aid="l00046"name="l00046"></a><spanclass="lineno"> 46</span><spanclass="comment">// We usually scale a continuous variable by scaling, but if its domain is going</span></div>
<divclass="line"><aid="l00047"name="l00047"></a><spanclass="lineno"> 47</span><spanclass="comment">// to have larger values than max_bound, then we scale to have the max domain</span></div>
<divclass="line"><aid="l00048"name="l00048"></a><spanclass="lineno"> 48</span><spanclass="comment">// magnitude equal to max_bound.</span></div>
<divclass="line"><aid="l00050"name="l00050"></a><spanclass="lineno"> 50</span><spanclass="comment">// Note that it is recommended to call DetectImpliedIntegers() before this</span></div>
<divclass="line"><aid="l00051"name="l00051"></a><spanclass="lineno"> 51</span><spanclass="comment">// function so that we do not scale variables that do not need to be scaled.</span></div>
<divclass="line"><aid="l00053"name="l00053"></a><spanclass="lineno"> 53</span><spanclass="comment">// TODO(user): Also scale the solution hint if any.</span></div>
<divclass="line"><aid="l00057"name="l00057"></a><spanclass="lineno"> 57</span><spanclass="comment">// To satisfy our scaling requirements, any terms that is almost zero can just</span></div>
<divclass="line"><aid="l00058"name="l00058"></a><spanclass="lineno"> 58</span><spanclass="comment">// be set to zero. We need to do that before operations like</span></div>
<divclass="line"><aid="l00059"name="l00059"></a><spanclass="lineno"> 59</span><spanclass="comment">// DetectImpliedIntegers(), becauses really low coefficients can cause issues</span></div>
<divclass="line"><aid="l00060"name="l00060"></a><spanclass="lineno"> 60</span><spanclass="comment">// and might lead to less detection.</span></div>
<divclass="line"><aid="l00064"name="l00064"></a><spanclass="lineno"> 64</span><spanclass="comment">// This will mark implied integer as such. Note that it can also discover</span></div>
<divclass="line"><aid="l00065"name="l00065"></a><spanclass="lineno"> 65</span><spanclass="comment">// variable of the form coeff * Integer + offset, and will change the model</span></div>
<divclass="line"><aid="l00066"name="l00066"></a><spanclass="lineno"> 66</span><spanclass="comment">// so that these are marked as integer. It is why we return both a scaling and</span></div>
<divclass="line"><aid="l00067"name="l00067"></a><spanclass="lineno"> 67</span><spanclass="comment">// an offset to transform the solution back to its original domain.</span></div>
<divclass="line"><aid="l00069"name="l00069"></a><spanclass="lineno"> 69</span><spanclass="comment">// TODO(user): Actually implement the offset part. This currently only happens</span></div>
<divclass="line"><aid="l00070"name="l00070"></a><spanclass="lineno"> 70</span><spanclass="comment">// on the 3 neos-46470* miplib problems where we have a non-integer rhs.</span></div>
<divclass="line"><aid="l00074"name="l00074"></a><spanclass="lineno"> 74</span><spanclass="comment">// Converts a MIP problem to a CpModel. Returns false if the coefficients</span></div>
<divclass="line"><aid="l00075"name="l00075"></a><spanclass="lineno"> 75</span><spanclass="comment">// couldn't be converted to integers with a good enough precision.</span></div>
<divclass="line"><aid="l00077"name="l00077"></a><spanclass="lineno"> 77</span><spanclass="comment">// There is a bunch of caveats and you can find more details on the</span></div>
<divclass="line"><aid="l00078"name="l00078"></a><spanclass="lineno"> 78</span><spanclass="comment">// SatParameters proto documentation for the mip_* parameters.</span></div>
<divclass="line"><aid="l00084"name="l00084"></a><spanclass="lineno"> 84</span><spanclass="comment">// Converts an integer program with only binary variables to a Boolean</span></div>
<divclass="line"><aid="l00085"name="l00085"></a><spanclass="lineno"> 85</span><spanclass="comment">// optimization problem. Returns false if the problem didn't contains only</span></div>
<divclass="line"><aid="l00086"name="l00086"></a><spanclass="lineno"> 86</span><spanclass="comment">// binary integer variable, or if the coefficients couldn't be converted to</span></div>
<divclass="line"><aid="l00087"name="l00087"></a><spanclass="lineno"> 87</span><spanclass="comment">// integer with a good enough precision.</span></div>
<divclass="line"><aid="l00091"name="l00091"></a><spanclass="lineno"> 91</span><spanclass="comment">// Converts a Boolean optimization problem to its lp formulation.</span></div>
<divclass="line"><aid="l00095"name="l00095"></a><spanclass="lineno"> 95</span><spanclass="comment">// Changes the variable bounds of the lp to reflect the variables that have been</span></div>
<divclass="line"><aid="l00096"name="l00096"></a><spanclass="lineno"> 96</span><spanclass="comment">// fixed by the SAT solver (i.e. assigned at decision level 0). Returns the</span></div>
<divclass="line"><aid="l00097"name="l00097"></a><spanclass="lineno"> 97</span><spanclass="comment">// number of variables fixed this way.</span></div>
<divclass="line"><aid="l00100"name="l00100"></a><spanclass="lineno"> 100</span><spanclass="comment">// Solves the given lp problem and uses the lp solution to drive the SAT solver</span></div>
<divclass="line"><aid="l00101"name="l00101"></a><spanclass="lineno"> 101</span><spanclass="comment">// polarity choices. The variable must have the same index in the solved lp</span></div>
<divclass="line"><aid="l00102"name="l00102"></a><spanclass="lineno"> 102</span><spanclass="comment">// problem and in SAT for this to make sense.</span></div>
<divclass="line"><aid="l00104"name="l00104"></a><spanclass="lineno"> 104</span><spanclass="comment">// Returns false if a problem occurred while trying to solve the lp.</span></div>
<divclass="line"><aid="l00109"name="l00109"></a><spanclass="lineno"> 109</span><spanclass="comment">// Solves the lp and add constraints to fix the integer variable of the lp in</span></div>
<divclass="line"><aid="l00110"name="l00110"></a><spanclass="lineno"> 110</span><spanclass="comment">// the LinearBoolean problem.</span></div>
<divclass="ttc"id="anamespaceoperations__research_1_1sat_html_af8b326626fb8ca0efd32ff0564d35731"><divclass="ttname"><ahref="namespaceoperations__research_1_1sat.html#af8b326626fb8ca0efd32ff0564d35731">operations_research::sat::FindRationalFactor</a></div><divclass="ttdeci">int FindRationalFactor(double x, int limit, double tolerance)</div><divclass="ttdef"><b>Definition:</b><ahref="sat_2lp__utils_8cc_source.html#l00119">sat/lp_utils.cc:119</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>
