<!-- 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">probing.h</div></div>
</div><!--header-->
<divclass="contents">
<ahref="probing_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="l00024"></a><spanclass="lineno"> 24</span> <spanclass="comment">// Fixes Booleans variables to true/false and see what is propagated. This can:</span></div>
<divclass="line"><aname="l00026"></a><spanclass="lineno"> 26</span> <spanclass="comment">// - Fix some Boolean variables (if we reach a conflict while probing).</span></div>
<divclass="line"><aname="l00028"></a><spanclass="lineno"> 28</span> <spanclass="comment">// - Infer new direct implications. We add them directly to the</span></div>
<divclass="line"><aname="l00029"></a><spanclass="lineno"> 29</span> <spanclass="comment">// BinaryImplicationGraph and they can later be used to detect equivalent</span></div>
<divclass="line"><aname="l00030"></a><spanclass="lineno"> 30</span> <spanclass="comment">// literals, expand at most ones clique, etc...</span></div>
<divclass="line"><aname="l00032"></a><spanclass="lineno"> 32</span> <spanclass="comment">// - Tighten the bounds of integer variables. If we probe the two possible</span></div>
<divclass="line"><aname="l00033"></a><spanclass="lineno"> 33</span> <spanclass="comment">// values of a Boolean (b=0 and b=1), we get for each integer variables two</span></div>
<divclass="line"><aname="l00034"></a><spanclass="lineno"> 34</span> <spanclass="comment">// propagated domain D_0 and D_1. The level zero domain can then be</span></div>
<divclass="line"><aname="l00035"></a><spanclass="lineno"> 35</span> <spanclass="comment">// intersected with D_0 U D_1. This can restrict the lower/upper bounds of a</span></div>
<divclass="line"><aname="l00036"></a><spanclass="lineno"> 36</span> <spanclass="comment">// variable, but it can also create holes in the domain! This will detect</span></div>
<divclass="line"><aname="l00037"></a><spanclass="lineno"> 37</span> <spanclass="comment">// common cases like an integer variable in [0, 10] that actually only take</span></div>
<divclass="line"><aname="l00038"></a><spanclass="lineno"> 38</span> <spanclass="comment">// two values [0] or [10] depending on one Boolean.</span></div>
<divclass="line"><aname="l00040"></a><spanclass="lineno"> 40</span> <spanclass="comment">// Returns false if the problem was proved INFEASIBLE during probing.</span></div>
<divclass="line"><aname="l00042"></a><spanclass="lineno"> 42</span> <spanclass="comment">// TODO(user): For now we process the Boolean in their natural order, this is</span></div>
<divclass="line"><aname="l00043"></a><spanclass="lineno"> 43</span> <spanclass="comment">// not the most efficient.</span></div>
<divclass="line"><aname="l00045"></a><spanclass="lineno"> 45</span> <spanclass="comment">// TODO(user): This might generate a lot of new direct implications. We might</span></div>
<divclass="line"><aname="l00046"></a><spanclass="lineno"> 46</span> <spanclass="comment">// not want to add them directly to the BinaryImplicationGraph and could instead</span></div>
<divclass="line"><aname="l00047"></a><spanclass="lineno"> 47</span> <spanclass="comment">// use them directly to detect equivalent literal like in</span></div>
<divclass="line"><aname="l00048"></a><spanclass="lineno"> 48</span> <spanclass="comment">// ProbeAndFindEquivalentLiteral(). The situation is not clear.</span></div>
<divclass="line"><aname="l00050"></a><spanclass="lineno"> 50</span> <spanclass="comment">// TODO(user): More generally, we might want to register any literal => bound in</span></div>
<divclass="line"><aname="l00051"></a><spanclass="lineno"> 51</span> <spanclass="comment">// the IntegerEncoder. This would allow to remember them and use them in other</span></div>
<divclass="line"><aname="l00052"></a><spanclass="lineno"> 52</span> <spanclass="comment">// part of the solver (cuts, lifting, ...).</span></div>
<divclass="line"><aname="l00054"></a><spanclass="lineno"> 54</span> <spanclass="comment">// TODO(user): Rename to include Integer in the name and distinguish better</span></div>
<divclass="line"><aname="l00055"></a><spanclass="lineno"> 55</span> <spanclass="comment">// from FailedLiteralProbing() below.</span></div>
<divclass="line"><aname="l00059"></a><spanclass="lineno"> 59</span> <spanclass="comment">// Same as above method except it probes only on the variables given in</span></div>
<divclass="line"><aname="l00065"></a><spanclass="lineno"> 65</span> <spanclass="comment">// Try to randomly tweak the search and stop at the first conflict each time.</span></div>
<divclass="line"><aname="l00066"></a><spanclass="lineno"> 66</span> <spanclass="comment">// This can sometimes find feasible solution, but more importantly, it is a form</span></div>
<divclass="line"><aname="l00067"></a><spanclass="lineno"> 67</span> <spanclass="comment">// of probing that can sometimes find small and interesting conflicts or fix</span></div>
<divclass="line"><aname="l00068"></a><spanclass="lineno"> 68</span> <spanclass="comment">// variables. This seems to work well on the SAT14/app/rook-* problems and</span></div>
<divclass="line"><aname="l00069"></a><spanclass="lineno"> 69</span> <spanclass="comment">// do fix more variables if run before probing.</span></div>
<divclass="line"><aname="l00071"></a><spanclass="lineno"> 71</span> <spanclass="comment">// If a feasible SAT solution is found (i.e. all Boolean assigned), then this</span></div>
<divclass="line"><aname="l00072"></a><spanclass="lineno"> 72</span> <spanclass="comment">// abort and leave the solver with the full solution assigned.</span></div>
<divclass="line"><aname="l00078"></a><spanclass="lineno"> 78</span> <spanclass="comment">// Options for the FailedLiteralProbing() code below.</span></div>
<divclass="line"><aname="l00080"></a><spanclass="lineno"> 80</span> <spanclass="comment">// A good reference for the algorithms involved here is the paper "Revisiting</span></div>
<divclass="line"><aname="l00081"></a><spanclass="lineno"> 81</span> <spanclass="comment">// Hyper Binary Resolution" Marijn J. H. Heule, Matti Jarvisalo, Armin Biere,</span></div>
<divclass="line"><aname="l00084"></a><spanclass="lineno"> 84</span> <spanclass="comment">// The probing will consume all this deterministic time or stop if nothing</span></div>
<divclass="line"><aname="l00085"></a><spanclass="lineno"> 85</span> <spanclass="comment">// else can be deduced and everything has been probed until fix-point. The</span></div>
<divclass="line"><aname="l00086"></a><spanclass="lineno"> 86</span> <spanclass="comment">// fix point depend on the extract_binay_clauses option:</span></div>
<divclass="line"><aname="l00087"></a><spanclass="lineno"> 87</span> <spanclass="comment">// - If false, we will just stop when no more failed literal can be found.</span></div>
<divclass="line"><aname="l00088"></a><spanclass="lineno"> 88</span> <spanclass="comment">// - If true, we will do more work and stop when all failed literal have been</span></div>
<divclass="line"><aname="l00089"></a><spanclass="lineno"> 89</span> <spanclass="comment">// found and all hyper binary resolution have been performed.</span></div>
<divclass="line"><aname="l00091"></a><spanclass="lineno"> 91</span> <spanclass="comment">// TODO(user): We can also provide a middle ground and probe all failed</span></div>
<divclass="line"><aname="l00092"></a><spanclass="lineno"> 92</span> <spanclass="comment">// literal but do not extract all binary clauses.</span></div>
<divclass="line"><aname="l00094"></a><spanclass="lineno"> 94</span> <spanclass="comment">// Note that the fix-point is unique, modulo the equivalent literal detection</span></div>
<divclass="line"><aname="l00095"></a><spanclass="lineno"> 95</span> <spanclass="comment">// we do. And if we add binary clauses, modulo the transitive reduction of the</span></div>
<divclass="line"><aname="l00098"></a><spanclass="lineno"> 98</span> <spanclass="comment">// To be fast, we only use the binary clauses in the binary implication graph</span></div>
<divclass="line"><aname="l00099"></a><spanclass="lineno"> 99</span> <spanclass="comment">// for the equivalence detection. So the power of the equivalence detection</span></div>
<divclass="line"><aname="l00100"></a><spanclass="lineno"> 100</span> <spanclass="comment">// changes if the extract_binay_clauses option is true or not.</span></div>
<divclass="line"><aname="l00102"></a><spanclass="lineno"> 102</span> <spanclass="comment">// TODO(user): The fix point is not yet reached since we don't currently</span></div>
<divclass="line"><aname="l00103"></a><spanclass="lineno"> 103</span> <spanclass="comment">// simplify non-binary clauses with these equivalence, but we will.</span></div>
<divclass="line"><aname="l00106"></a><spanclass="lineno"> 106</span> <spanclass="comment">// This is also called hyper binary resolution. Basically, we make sure that</span></div>
<divclass="line"><aname="l00107"></a><spanclass="lineno"> 107</span> <spanclass="comment">// the binary implication graph is augmented with all the implication of the</span></div>
<divclass="line"><aname="l00108"></a><spanclass="lineno"> 108</span> <spanclass="comment">// form a => b that can be derived by fixing 'a' at level zero and doing a</span></div>
<divclass="line"><aname="l00109"></a><spanclass="lineno"> 109</span> <spanclass="comment">// propagation using all constraints. Note that we only add clauses that</span></div>
<divclass="line"><aname="l00110"></a><spanclass="lineno"> 110</span> <spanclass="comment">// cannot be derived by the current implication graph.</span></div>
<divclass="line"><aname="l00112"></a><spanclass="lineno"> 112</span> <spanclass="comment">// With these extra clause the power of the equivalence literal detection</span></div>
<divclass="line"><aname="l00113"></a><spanclass="lineno"> 113</span> <spanclass="comment">// using only the binary implication graph with increase. Note that it is</span></div>
<divclass="line"><aname="l00114"></a><spanclass="lineno"> 114</span> <spanclass="comment">// possible to do exactly the same thing without adding these binary clause</span></div>
<divclass="line"><aname="l00115"></a><spanclass="lineno"> 115</span> <spanclass="comment">// first. This is what is done by yet another probing algorithm (currently in</span></div>
<divclass="line"><aname="l00118"></a><spanclass="lineno"> 118</span> <spanclass="comment">// TODO(user): Note that adding binary clause before/during the SAT presolve</span></div>
<divclass="line"><aname="l00119"></a><spanclass="lineno"> 119</span> <spanclass="comment">// is currently not always a good idea. This is because we don't simplify the</span></div>
<divclass="line"><aname="l00120"></a><spanclass="lineno"> 120</span> <spanclass="comment">// other clause as much as we could. Also, there can be up to a quadratic</span></div>
<divclass="line"><aname="l00121"></a><spanclass="lineno"> 121</span> <spanclass="comment">// number of clauses added this way, which might slow down things a lot. But</span></div>
<divclass="line"><aname="l00122"></a><spanclass="lineno"> 122</span> <spanclass="comment">// then because of the deterministic limit, we usually cannot add too much</span></div>
<divclass="line"><aname="l00123"></a><spanclass="lineno"> 123</span> <spanclass="comment">// clauses, even for huge problems, since we will reach the limit before that.</span></div>
<divclass="line"><aname="l00126"></a><spanclass="lineno"> 126</span> <spanclass="comment">// Use a version of the "Tree look" algorithm as explained in the paper above.</span></div>
<divclass="line"><aname="l00127"></a><spanclass="lineno"> 127</span> <spanclass="comment">// This is usually faster and more efficient. Note that when extracting binary</span></div>
<divclass="line"><aname="l00128"></a><spanclass="lineno"> 128</span> <spanclass="comment">// clauses it might currently produce more "redundant" one in the sense that a</span></div>
<divclass="line"><aname="l00129"></a><spanclass="lineno"> 129</span> <spanclass="comment">// transitive reduction of the binary implication graph after all hyper binary</span></div>
<divclass="line"><aname="l00130"></a><spanclass="lineno"> 130</span> <spanclass="comment">// resolution have been performed may need to do more work.</span></div>
<divclass="line"><aname="l00133"></a><spanclass="lineno"> 133</span> <spanclass="comment">// There is two sligthly different implementation of the tree-look algo.</span></div>
<divclass="line"><aname="l00135"></a><spanclass="lineno"> 135</span> <spanclass="comment">// TODO(user): Decide which one is better, currently the difference seems</span></div>
<divclass="line"><aname="l00136"></a><spanclass="lineno"> 136</span> <spanclass="comment">// small but the queue seems slightly faster.</span></div>
<divclass="line"><aname="l00139"></a><spanclass="lineno"> 139</span> <spanclass="comment">// If we detect as we probe that a new binary clause subsumes one of the</span></div>
<divclass="line"><aname="l00140"></a><spanclass="lineno"> 140</span> <spanclass="comment">// non-binary clause, we will replace the long clause by the binary one. This</span></div>
<divclass="line"><aname="l00141"></a><spanclass="lineno"> 141</span> <spanclass="comment">// is orthogonal to the extract_binary_clauses parameters which will add all</span></div>
<divclass="line"><aname="l00142"></a><spanclass="lineno"> 142</span> <spanclass="comment">// binary clauses but not neceassirly check for subsumption.</span></div>
<divclass="line"><aname="l00145"></a><spanclass="lineno"> 145</span> <spanclass="comment">// We assume this is also true if --v 1 is activated.</span></div>
<divclass="line"><aname="l00156"></a><spanclass="lineno"> 156</span> <spanclass="comment">// Similar to ProbeBooleanVariables() but different :-)</span></div>
<divclass="line"><aname="l00158"></a><spanclass="lineno"> 158</span> <spanclass="comment">// First, this do not consider integer variable. It doesn't do any disjunctive</span></div>
<divclass="line"><aname="l00159"></a><spanclass="lineno"> 159</span> <spanclass="comment">// reasoning (i.e. changing the domain of an integer variable by intersecting it</span></div>
<divclass="line"><aname="l00160"></a><spanclass="lineno"> 160</span> <spanclass="comment">// with the union of what happen when x is fixed and not(x) is fixed).</span></div>
<divclass="line"><aname="l00162"></a><spanclass="lineno"> 162</span> <spanclass="comment">// However this should be more efficient and just work better for pure Boolean</span></div>
<divclass="line"><aname="l00163"></a><spanclass="lineno"> 163</span> <spanclass="comment">// problems. On integer problems, we might also want to run this one first, and</span></div>
<divclass="line"><aname="l00164"></a><spanclass="lineno"> 164</span> <spanclass="comment">// then do just one quick pass of ProbeBooleanVariables().</span></div>
<divclass="line"><aname="l00166"></a><spanclass="lineno"> 166</span> <spanclass="comment">// Note that this by itself just do one "round", look at the code in the</span></div>
<divclass="line"><aname="l00167"></a><spanclass="lineno"> 167</span> <spanclass="comment">// Inprocessing class that call this interleaved with other reductions until a</span></div>
<divclass="line"><aname="l00168"></a><spanclass="lineno"> 168</span> <spanclass="comment">// fix point is reached.</span></div>
<divclass="line"><aname="l00170"></a><spanclass="lineno"> 170</span> <spanclass="comment">// This can fix a lot of literals via failed literal detection, that is when we</span></div>
<divclass="line"><aname="l00171"></a><spanclass="lineno"> 171</span> <spanclass="comment">// detect that x => not(x) via propagation after taking x as a decision. It also</span></div>
<divclass="line"><aname="l00172"></a><spanclass="lineno"> 172</span> <spanclass="comment">// use the strongly connected component algorithm to detect equivalent literals.</span></div>
<divclass="line"><aname="l00174"></a><spanclass="lineno"> 174</span> <spanclass="comment">// It will add any detected binary clause (via hyper binary resolution) to</span></div>
<divclass="line"><aname="l00175"></a><spanclass="lineno"> 175</span> <spanclass="comment">// the implication graph. See the option comments for more details.</span></div>
<divclass="ttc"id="anamespaceoperations__research_1_1sat_html_a865df3eeca0b96bf7fda22b016b80bc2"><divclass="ttname"><ahref="namespaceoperations__research_1_1sat.html#a865df3eeca0b96bf7fda22b016b80bc2">operations_research::sat::FailedLiteralProbingRound</a></div><divclass="ttdeci">bool FailedLiteralProbingRound(ProbingOptions options, Model *model)</div><divclass="ttdef"><b>Definition:</b><ahref="probing_8cc_source.html#l00338">probing.cc:338</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>
