<!-- 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="l00032"></a><spanclass="lineno"> 32</span> <spanclass="comment">// Fixes Booleans variables to true/false and see what is propagated. This</span></div>
<divclass="line"><aname="l00035"></a><spanclass="lineno"> 35</span> <spanclass="comment">// - Fix some Boolean variables (if we reach a conflict while probing).</span></div>
<divclass="line"><aname="l00037"></a><spanclass="lineno"> 37</span> <spanclass="comment">// - Infer new direct implications. We add them directly to the</span></div>
<divclass="line"><aname="l00038"></a><spanclass="lineno"> 38</span> <spanclass="comment">// BinaryImplicationGraph and they can later be used to detect equivalent</span></div>
<divclass="line"><aname="l00039"></a><spanclass="lineno"> 39</span> <spanclass="comment">// literals, expand at most ones clique, etc...</span></div>
<divclass="line"><aname="l00041"></a><spanclass="lineno"> 41</span> <spanclass="comment">// - Tighten the bounds of integer variables. If we probe the two possible</span></div>
<divclass="line"><aname="l00042"></a><spanclass="lineno"> 42</span> <spanclass="comment">// values of a Boolean (b=0 and b=1), we get for each integer variables two</span></div>
<divclass="line"><aname="l00043"></a><spanclass="lineno"> 43</span> <spanclass="comment">// propagated domain D_0 and D_1. The level zero domain can then be</span></div>
<divclass="line"><aname="l00044"></a><spanclass="lineno"> 44</span> <spanclass="comment">// intersected with D_0 U D_1. This can restrict the lower/upper bounds of a</span></div>
<divclass="line"><aname="l00045"></a><spanclass="lineno"> 45</span> <spanclass="comment">// variable, but it can also create holes in the domain! This will detect</span></div>
<divclass="line"><aname="l00046"></a><spanclass="lineno"> 46</span> <spanclass="comment">// common cases like an integer variable in [0, 10] that actually only take</span></div>
<divclass="line"><aname="l00047"></a><spanclass="lineno"> 47</span> <spanclass="comment">// two values [0] or [10] depending on one Boolean.</span></div>
<divclass="line"><aname="l00049"></a><spanclass="lineno"> 49</span> <spanclass="comment">// Returns false if the problem was proved INFEASIBLE during probing.</span></div>
<divclass="line"><aname="l00051"></a><spanclass="lineno"> 51</span> <spanclass="comment">// TODO(user): For now we process the Boolean in their natural order, this is</span></div>
<divclass="line"><aname="l00052"></a><spanclass="lineno"> 52</span> <spanclass="comment">// not the most efficient.</span></div>
<divclass="line"><aname="l00054"></a><spanclass="lineno"> 54</span> <spanclass="comment">// TODO(user): This might generate a lot of new direct implications. We might</span></div>
<divclass="line"><aname="l00055"></a><spanclass="lineno"> 55</span> <spanclass="comment">// not want to add them directly to the BinaryImplicationGraph and could</span></div>
<divclass="line"><aname="l00056"></a><spanclass="lineno"> 56</span> <spanclass="comment">// instead use them directly to detect equivalent literal like in</span></div>
<divclass="line"><aname="l00057"></a><spanclass="lineno"> 57</span> <spanclass="comment">// ProbeAndFindEquivalentLiteral(). The situation is not clear.</span></div>
<divclass="line"><aname="l00059"></a><spanclass="lineno"> 59</span> <spanclass="comment">// TODO(user): More generally, we might want to register any literal => bound</span></div>
<divclass="line"><aname="l00060"></a><spanclass="lineno"> 60</span> <spanclass="comment">// in the IntegerEncoder. This would allow to remember them and use them in</span></div>
<divclass="line"><aname="l00061"></a><spanclass="lineno"> 61</span> <spanclass="comment">// other part of the solver (cuts, lifting, ...).</span></div>
<divclass="line"><aname="l00063"></a><spanclass="lineno"> 63</span> <spanclass="comment">// TODO(user): Rename to include Integer in the name and distinguish better</span></div>
<divclass="line"><aname="l00064"></a><spanclass="lineno"> 64</span> <spanclass="comment">// from FailedLiteralProbing() below.</span></div>
<divclass="line"><aname="l00068"></a><spanclass="lineno"> 68</span> <spanclass="comment">// Same as above method except it probes only on the variables given in</span></div>
<divclass="line"><aname="l00088"></a><spanclass="lineno"> 88</span> <spanclass="comment">// To detect literal x that must be true because b => x and not(b) => x.</span></div>
<divclass="line"><aname="l00089"></a><spanclass="lineno"> 89</span> <spanclass="comment">// When probing b, we add all propagated literal to propagated, and when</span></div>
<divclass="line"><aname="l00090"></a><spanclass="lineno"> 90</span> <spanclass="comment">// probing not(b) we check if any are already there.</span></div>
<divclass="line"><aname="l00104"></a><spanclass="lineno"> 104</span> <spanclass="comment">// Try to randomly tweak the search and stop at the first conflict each time.</span></div>
<divclass="line"><aname="l00105"></a><spanclass="lineno"> 105</span> <spanclass="comment">// This can sometimes find feasible solution, but more importantly, it is a form</span></div>
<divclass="line"><aname="l00106"></a><spanclass="lineno"> 106</span> <spanclass="comment">// of probing that can sometimes find small and interesting conflicts or fix</span></div>
<divclass="line"><aname="l00107"></a><spanclass="lineno"> 107</span> <spanclass="comment">// variables. This seems to work well on the SAT14/app/rook-* problems and</span></div>
<divclass="line"><aname="l00108"></a><spanclass="lineno"> 108</span> <spanclass="comment">// do fix more variables if run before probing.</span></div>
<divclass="line"><aname="l00110"></a><spanclass="lineno"> 110</span> <spanclass="comment">// If a feasible SAT solution is found (i.e. all Boolean assigned), then this</span></div>
<divclass="line"><aname="l00111"></a><spanclass="lineno"> 111</span> <spanclass="comment">// abort and leave the solver with the full solution assigned.</span></div>
<divclass="line"><aname="l00117"></a><spanclass="lineno"> 117</span> <spanclass="comment">// Options for the FailedLiteralProbing() code below.</span></div>
<divclass="line"><aname="l00119"></a><spanclass="lineno"> 119</span> <spanclass="comment">// A good reference for the algorithms involved here is the paper "Revisiting</span></div>
<divclass="line"><aname="l00120"></a><spanclass="lineno"> 120</span> <spanclass="comment">// Hyper Binary Resolution" Marijn J. H. Heule, Matti Jarvisalo, Armin Biere,</span></div>
<divclass="line"><aname="l00123"></a><spanclass="lineno"> 123</span> <spanclass="comment">// The probing will consume all this deterministic time or stop if nothing</span></div>
<divclass="line"><aname="l00124"></a><spanclass="lineno"> 124</span> <spanclass="comment">// else can be deduced and everything has been probed until fix-point. The</span></div>
<divclass="line"><aname="l00125"></a><spanclass="lineno"> 125</span> <spanclass="comment">// fix point depend on the extract_binay_clauses option:</span></div>
<divclass="line"><aname="l00126"></a><spanclass="lineno"> 126</span> <spanclass="comment">// - If false, we will just stop when no more failed literal can be found.</span></div>
<divclass="line"><aname="l00127"></a><spanclass="lineno"> 127</span> <spanclass="comment">// - If true, we will do more work and stop when all failed literal have been</span></div>
<divclass="line"><aname="l00128"></a><spanclass="lineno"> 128</span> <spanclass="comment">// found and all hyper binary resolution have been performed.</span></div>
<divclass="line"><aname="l00130"></a><spanclass="lineno"> 130</span> <spanclass="comment">// TODO(user): We can also provide a middle ground and probe all failed</span></div>
<divclass="line"><aname="l00131"></a><spanclass="lineno"> 131</span> <spanclass="comment">// literal but do not extract all binary clauses.</span></div>
<divclass="line"><aname="l00133"></a><spanclass="lineno"> 133</span> <spanclass="comment">// Note that the fix-point is unique, modulo the equivalent literal detection</span></div>
<divclass="line"><aname="l00134"></a><spanclass="lineno"> 134</span> <spanclass="comment">// we do. And if we add binary clauses, modulo the transitive reduction of the</span></div>
<divclass="line"><aname="l00137"></a><spanclass="lineno"> 137</span> <spanclass="comment">// To be fast, we only use the binary clauses in the binary implication graph</span></div>
<divclass="line"><aname="l00138"></a><spanclass="lineno"> 138</span> <spanclass="comment">// for the equivalence detection. So the power of the equivalence detection</span></div>
<divclass="line"><aname="l00139"></a><spanclass="lineno"> 139</span> <spanclass="comment">// changes if the extract_binay_clauses option is true or not.</span></div>
<divclass="line"><aname="l00141"></a><spanclass="lineno"> 141</span> <spanclass="comment">// TODO(user): The fix point is not yet reached since we don't currently</span></div>
<divclass="line"><aname="l00142"></a><spanclass="lineno"> 142</span> <spanclass="comment">// simplify non-binary clauses with these equivalence, but we will.</span></div>
<divclass="line"><aname="l00145"></a><spanclass="lineno"> 145</span> <spanclass="comment">// This is also called hyper binary resolution. Basically, we make sure that</span></div>
<divclass="line"><aname="l00146"></a><spanclass="lineno"> 146</span> <spanclass="comment">// the binary implication graph is augmented with all the implication of the</span></div>
<divclass="line"><aname="l00147"></a><spanclass="lineno"> 147</span> <spanclass="comment">// form a => b that can be derived by fixing 'a' at level zero and doing a</span></div>
<divclass="line"><aname="l00148"></a><spanclass="lineno"> 148</span> <spanclass="comment">// propagation using all constraints. Note that we only add clauses that</span></div>
<divclass="line"><aname="l00149"></a><spanclass="lineno"> 149</span> <spanclass="comment">// cannot be derived by the current implication graph.</span></div>
<divclass="line"><aname="l00151"></a><spanclass="lineno"> 151</span> <spanclass="comment">// With these extra clause the power of the equivalence literal detection</span></div>
<divclass="line"><aname="l00152"></a><spanclass="lineno"> 152</span> <spanclass="comment">// using only the binary implication graph with increase. Note that it is</span></div>
<divclass="line"><aname="l00153"></a><spanclass="lineno"> 153</span> <spanclass="comment">// possible to do exactly the same thing without adding these binary clause</span></div>
<divclass="line"><aname="l00154"></a><spanclass="lineno"> 154</span> <spanclass="comment">// first. This is what is done by yet another probing algorithm (currently in</span></div>
<divclass="line"><aname="l00157"></a><spanclass="lineno"> 157</span> <spanclass="comment">// TODO(user): Note that adding binary clause before/during the SAT presolve</span></div>
<divclass="line"><aname="l00158"></a><spanclass="lineno"> 158</span> <spanclass="comment">// is currently not always a good idea. This is because we don't simplify the</span></div>
<divclass="line"><aname="l00159"></a><spanclass="lineno"> 159</span> <spanclass="comment">// other clause as much as we could. Also, there can be up to a quadratic</span></div>
<divclass="line"><aname="l00160"></a><spanclass="lineno"> 160</span> <spanclass="comment">// number of clauses added this way, which might slow down things a lot. But</span></div>
<divclass="line"><aname="l00161"></a><spanclass="lineno"> 161</span> <spanclass="comment">// then because of the deterministic limit, we usually cannot add too much</span></div>
<divclass="line"><aname="l00162"></a><spanclass="lineno"> 162</span> <spanclass="comment">// clauses, even for huge problems, since we will reach the limit before that.</span></div>
<divclass="line"><aname="l00165"></a><spanclass="lineno"> 165</span> <spanclass="comment">// Use a version of the "Tree look" algorithm as explained in the paper above.</span></div>
<divclass="line"><aname="l00166"></a><spanclass="lineno"> 166</span> <spanclass="comment">// This is usually faster and more efficient. Note that when extracting binary</span></div>
<divclass="line"><aname="l00167"></a><spanclass="lineno"> 167</span> <spanclass="comment">// clauses it might currently produce more "redundant" one in the sense that a</span></div>
<divclass="line"><aname="l00168"></a><spanclass="lineno"> 168</span> <spanclass="comment">// transitive reduction of the binary implication graph after all hyper binary</span></div>
<divclass="line"><aname="l00169"></a><spanclass="lineno"> 169</span> <spanclass="comment">// resolution have been performed may need to do more work.</span></div>
<divclass="line"><aname="l00172"></a><spanclass="lineno"> 172</span> <spanclass="comment">// There is two sligthly different implementation of the tree-look algo.</span></div>
<divclass="line"><aname="l00174"></a><spanclass="lineno"> 174</span> <spanclass="comment">// TODO(user): Decide which one is better, currently the difference seems</span></div>
<divclass="line"><aname="l00175"></a><spanclass="lineno"> 175</span> <spanclass="comment">// small but the queue seems slightly faster.</span></div>
<divclass="line"><aname="l00178"></a><spanclass="lineno"> 178</span> <spanclass="comment">// If we detect as we probe that a new binary clause subsumes one of the</span></div>
<divclass="line"><aname="l00179"></a><spanclass="lineno"> 179</span> <spanclass="comment">// non-binary clause, we will replace the long clause by the binary one. This</span></div>
<divclass="line"><aname="l00180"></a><spanclass="lineno"> 180</span> <spanclass="comment">// is orthogonal to the extract_binary_clauses parameters which will add all</span></div>
<divclass="line"><aname="l00181"></a><spanclass="lineno"> 181</span> <spanclass="comment">// binary clauses but not neceassirly check for subsumption.</span></div>
<divclass="line"><aname="l00184"></a><spanclass="lineno"> 184</span> <spanclass="comment">// We assume this is also true if --v 1 is activated.</span></div>
<divclass="line"><aname="l00195"></a><spanclass="lineno"> 195</span> <spanclass="comment">// Similar to ProbeBooleanVariables() but different :-)</span></div>
<divclass="line"><aname="l00197"></a><spanclass="lineno"> 197</span> <spanclass="comment">// First, this do not consider integer variable. It doesn't do any disjunctive</span></div>
<divclass="line"><aname="l00198"></a><spanclass="lineno"> 198</span> <spanclass="comment">// reasoning (i.e. changing the domain of an integer variable by intersecting</span></div>
<divclass="line"><aname="l00199"></a><spanclass="lineno"> 199</span> <spanclass="comment">// it with the union of what happen when x is fixed and not(x) is fixed).</span></div>
<divclass="line"><aname="l00201"></a><spanclass="lineno"> 201</span> <spanclass="comment">// However this should be more efficient and just work better for pure Boolean</span></div>
<divclass="line"><aname="l00202"></a><spanclass="lineno"> 202</span> <spanclass="comment">// problems. On integer problems, we might also want to run this one first,</span></div>
<divclass="line"><aname="l00203"></a><spanclass="lineno"> 203</span> <spanclass="comment">// and then do just one quick pass of ProbeBooleanVariables().</span></div>
<divclass="line"><aname="l00205"></a><spanclass="lineno"> 205</span> <spanclass="comment">// Note that this by itself just do one "round", look at the code in the</span></div>
<divclass="line"><aname="l00206"></a><spanclass="lineno"> 206</span> <spanclass="comment">// Inprocessing class that call this interleaved with other reductions until a</span></div>
<divclass="line"><aname="l00207"></a><spanclass="lineno"> 207</span> <spanclass="comment">// fix point is reached.</span></div>
<divclass="line"><aname="l00209"></a><spanclass="lineno"> 209</span> <spanclass="comment">// This can fix a lot of literals via failed literal detection, that is when</span></div>
<divclass="line"><aname="l00210"></a><spanclass="lineno"> 210</span> <spanclass="comment">// we detect that x => not(x) via propagation after taking x as a decision. It</span></div>
<divclass="line"><aname="l00211"></a><spanclass="lineno"> 211</span> <spanclass="comment">// also use the strongly connected component algorithm to detect equivalent</span></div>
<divclass="line"><aname="l00214"></a><spanclass="lineno"> 214</span> <spanclass="comment">// It will add any detected binary clause (via hyper binary resolution) to</span></div>
<divclass="line"><aname="l00215"></a><spanclass="lineno"> 215</span> <spanclass="comment">// the implication graph. See the option comments for more details.</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_1sat_1_1_model_html"><divclass="ttname"><ahref="classoperations__research_1_1sat_1_1_model.html">operations_research::sat::Model</a></div><divclass="ttdoc">Class that owns everything related to a particular optimization model.</div><divclass="ttdef"><b>Definition:</b><ahref="sat_2model_8h_source.html#l00038">sat/model.h:38</a></div></div>
<divclass="ttc"id="anamespaceoperations__research_1_1sat_html_a20296d1a269e973b66b403c8b1cd5785"><divclass="ttname"><ahref="namespaceoperations__research_1_1sat.html#a20296d1a269e973b66b403c8b1cd5785">operations_research::sat::LookForTrivialSatSolution</a></div><divclass="ttdeci">bool LookForTrivialSatSolution(double deterministic_time_limit, Model *model, bool log_info)</div><divclass="ttdef"><b>Definition:</b><ahref="probing_8cc_source.html#l00270">probing.cc:270</a></div></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#l00350">probing.cc:350</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>
