<ahref="probing_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="l00041"name="l00041"></a><spanclass="lineno"> 41</span><spanclass="comment">// Fixes Booleans variables to true/false and see what is propagated. This</span></div>
<divclass="line"><aid="l00044"name="l00044"></a><spanclass="lineno"> 44</span><spanclass="comment">// - Fix some Boolean variables (if we reach a conflict while probing).</span></div>
<divclass="line"><aid="l00046"name="l00046"></a><spanclass="lineno"> 46</span><spanclass="comment">// - Infer new direct implications. We add them directly to the</span></div>
<divclass="line"><aid="l00047"name="l00047"></a><spanclass="lineno"> 47</span><spanclass="comment">// BinaryImplicationGraph and they can later be used to detect equivalent</span></div>
<divclass="line"><aid="l00048"name="l00048"></a><spanclass="lineno"> 48</span><spanclass="comment">// literals, expand at most ones clique, etc...</span></div>
<divclass="line"><aid="l00050"name="l00050"></a><spanclass="lineno"> 50</span><spanclass="comment">// - Tighten the bounds of integer variables. If we probe the two possible</span></div>
<divclass="line"><aid="l00051"name="l00051"></a><spanclass="lineno"> 51</span><spanclass="comment">// values of a Boolean (b=0 and b=1), we get for each integer variables two</span></div>
<divclass="line"><aid="l00052"name="l00052"></a><spanclass="lineno"> 52</span><spanclass="comment">// propagated domain D_0 and D_1. The level zero domain can then be</span></div>
<divclass="line"><aid="l00053"name="l00053"></a><spanclass="lineno"> 53</span><spanclass="comment">// intersected with D_0 U D_1. This can restrict the lower/upper bounds of a</span></div>
<divclass="line"><aid="l00054"name="l00054"></a><spanclass="lineno"> 54</span><spanclass="comment">// variable, but it can also create holes in the domain! This will detect</span></div>
<divclass="line"><aid="l00055"name="l00055"></a><spanclass="lineno"> 55</span><spanclass="comment">// common cases like an integer variable in [0, 10] that actually only take</span></div>
<divclass="line"><aid="l00056"name="l00056"></a><spanclass="lineno"> 56</span><spanclass="comment">// two values [0] or [10] depending on one Boolean.</span></div>
<divclass="line"><aid="l00058"name="l00058"></a><spanclass="lineno"> 58</span><spanclass="comment">// Returns false if the problem was proved INFEASIBLE during probing.</span></div>
<divclass="line"><aid="l00060"name="l00060"></a><spanclass="lineno"> 60</span><spanclass="comment">// TODO(user): For now we process the Boolean in their natural order, this is</span></div>
<divclass="line"><aid="l00061"name="l00061"></a><spanclass="lineno"> 61</span><spanclass="comment">// not the most efficient.</span></div>
<divclass="line"><aid="l00063"name="l00063"></a><spanclass="lineno"> 63</span><spanclass="comment">// TODO(user): This might generate a lot of new direct implications. We might</span></div>
<divclass="line"><aid="l00064"name="l00064"></a><spanclass="lineno"> 64</span><spanclass="comment">// not want to add them directly to the BinaryImplicationGraph and could</span></div>
<divclass="line"><aid="l00065"name="l00065"></a><spanclass="lineno"> 65</span><spanclass="comment">// instead use them directly to detect equivalent literal like in</span></div>
<divclass="line"><aid="l00066"name="l00066"></a><spanclass="lineno"> 66</span><spanclass="comment">// ProbeAndFindEquivalentLiteral(). The situation is not clear.</span></div>
<divclass="line"><aid="l00068"name="l00068"></a><spanclass="lineno"> 68</span><spanclass="comment">// TODO(user): More generally, we might want to register any literal => bound</span></div>
<divclass="line"><aid="l00069"name="l00069"></a><spanclass="lineno"> 69</span><spanclass="comment">// in the IntegerEncoder. This would allow to remember them and use them in</span></div>
<divclass="line"><aid="l00070"name="l00070"></a><spanclass="lineno"> 70</span><spanclass="comment">// other part of the solver (cuts, lifting, ...).</span></div>
<divclass="line"><aid="l00072"name="l00072"></a><spanclass="lineno"> 72</span><spanclass="comment">// TODO(user): Rename to include Integer in the name and distinguish better</span></div>
<divclass="line"><aid="l00073"name="l00073"></a><spanclass="lineno"> 73</span><spanclass="comment">// from FailedLiteralProbing() below.</span></div>
<divclass="line"><aid="l00076"name="l00076"></a><spanclass="lineno"> 76</span><spanclass="comment">// Same as above method except it probes only on the variables given in</span></div>
<divclass="line"><aid="l00084"name="l00084"></a><spanclass="lineno"> 84</span><spanclass="comment">// They are reset each time ProbleBooleanVariables() is called.</span></div>
<divclass="line"><aid="l00085"name="l00085"></a><spanclass="lineno"> 85</span><spanclass="comment">// Note however that we do not reset them on a call to ProbeOneVariable().</span></div>
<divclass="line"><aid="l00101"name="l00101"></a><spanclass="lineno"> 101</span><spanclass="comment">// To detect literal x that must be true because b => x and not(b) => x.</span></div>
<divclass="line"><aid="l00102"name="l00102"></a><spanclass="lineno"> 102</span><spanclass="comment">// When probing b, we add all propagated literal to propagated, and when</span></div>
<divclass="line"><aid="l00103"name="l00103"></a><spanclass="lineno"> 103</span><spanclass="comment">// probing not(b) we check if any are already there.</span></div>
<divclass="line"><aid="l00106"name="l00106"></a><spanclass="lineno"> 106</span><spanclass="comment">// Modifications found during probing.</span></div>
<divclass="line"><aid="l00121"name="l00121"></a><spanclass="lineno"> 121</span><spanclass="comment">// Try to randomly tweak the search and stop at the first conflict each time.</span></div>
<divclass="line"><aid="l00122"name="l00122"></a><spanclass="lineno"> 122</span><spanclass="comment">// This can sometimes find feasible solution, but more importantly, it is a form</span></div>
<divclass="line"><aid="l00123"name="l00123"></a><spanclass="lineno"> 123</span><spanclass="comment">// of probing that can sometimes find small and interesting conflicts or fix</span></div>
<divclass="line"><aid="l00124"name="l00124"></a><spanclass="lineno"> 124</span><spanclass="comment">// variables. This seems to work well on the SAT14/app/rook-* problems and</span></div>
<divclass="line"><aid="l00125"name="l00125"></a><spanclass="lineno"> 125</span><spanclass="comment">// do fix more variables if run before probing.</span></div>
<divclass="line"><aid="l00127"name="l00127"></a><spanclass="lineno"> 127</span><spanclass="comment">// If a feasible SAT solution is found (i.e. all Boolean assigned), then this</span></div>
<divclass="line"><aid="l00128"name="l00128"></a><spanclass="lineno"> 128</span><spanclass="comment">// abort and leave the solver with the full solution assigned.</span></div>
<divclass="line"><aid="l00130"name="l00130"></a><spanclass="lineno"> 130</span><spanclass="comment">// Returns false iff the problem is UNSAT.</span></div>
<divclass="line"><aid="l00133"name="l00133"></a><spanclass="lineno"> 133</span><spanclass="comment">// Options for the FailedLiteralProbing() code below.</span></div>
<divclass="line"><aid="l00135"name="l00135"></a><spanclass="lineno"> 135</span><spanclass="comment">// A good reference for the algorithms involved here is the paper "Revisiting</span></div>
<divclass="line"><aid="l00136"name="l00136"></a><spanclass="lineno"> 136</span><spanclass="comment">// Hyper Binary Resolution" Marijn J. H. Heule, Matti Jarvisalo, Armin Biere,</span></div>
<divclass="line"><aid="l00139"name="l00139"></a><spanclass="lineno"> 139</span><spanclass="comment">// The probing will consume all this deterministic time or stop if nothing</span></div>
<divclass="line"><aid="l00140"name="l00140"></a><spanclass="lineno"> 140</span><spanclass="comment">// else can be deduced and everything has been probed until fix-point. The</span></div>
<divclass="line"><aid="l00141"name="l00141"></a><spanclass="lineno"> 141</span><spanclass="comment">// fix point depend on the extract_binay_clauses option:</span></div>
<divclass="line"><aid="l00142"name="l00142"></a><spanclass="lineno"> 142</span><spanclass="comment">// - If false, we will just stop when no more failed literal can be found.</span></div>
<divclass="line"><aid="l00143"name="l00143"></a><spanclass="lineno"> 143</span><spanclass="comment">// - If true, we will do more work and stop when all failed literal have been</span></div>
<divclass="line"><aid="l00144"name="l00144"></a><spanclass="lineno"> 144</span><spanclass="comment">// found and all hyper binary resolution have been performed.</span></div>
<divclass="line"><aid="l00146"name="l00146"></a><spanclass="lineno"> 146</span><spanclass="comment">// TODO(user): We can also provide a middle ground and probe all failed</span></div>
<divclass="line"><aid="l00147"name="l00147"></a><spanclass="lineno"> 147</span><spanclass="comment">// literal but do not extract all binary clauses.</span></div>
<divclass="line"><aid="l00149"name="l00149"></a><spanclass="lineno"> 149</span><spanclass="comment">// Note that the fix-point is unique, modulo the equivalent literal detection</span></div>
<divclass="line"><aid="l00150"name="l00150"></a><spanclass="lineno"> 150</span><spanclass="comment">// we do. And if we add binary clauses, modulo the transitive reduction of the</span></div>
<divclass="line"><aid="l00153"name="l00153"></a><spanclass="lineno"> 153</span><spanclass="comment">// To be fast, we only use the binary clauses in the binary implication graph</span></div>
<divclass="line"><aid="l00154"name="l00154"></a><spanclass="lineno"> 154</span><spanclass="comment">// for the equivalence detection. So the power of the equivalence detection</span></div>
<divclass="line"><aid="l00155"name="l00155"></a><spanclass="lineno"> 155</span><spanclass="comment">// changes if the extract_binay_clauses option is true or not.</span></div>
<divclass="line"><aid="l00157"name="l00157"></a><spanclass="lineno"> 157</span><spanclass="comment">// TODO(user): The fix point is not yet reached since we don't currently</span></div>
<divclass="line"><aid="l00158"name="l00158"></a><spanclass="lineno"> 158</span><spanclass="comment">// simplify non-binary clauses with these equivalence, but we will.</span></div>
<divclass="line"><aid="l00161"name="l00161"></a><spanclass="lineno"> 161</span><spanclass="comment">// This is also called hyper binary resolution. Basically, we make sure that</span></div>
<divclass="line"><aid="l00162"name="l00162"></a><spanclass="lineno"> 162</span><spanclass="comment">// the binary implication graph is augmented with all the implication of the</span></div>
<divclass="line"><aid="l00163"name="l00163"></a><spanclass="lineno"> 163</span><spanclass="comment">// form a => b that can be derived by fixing 'a' at level zero and doing a</span></div>
<divclass="line"><aid="l00164"name="l00164"></a><spanclass="lineno"> 164</span><spanclass="comment">// propagation using all constraints. Note that we only add clauses that</span></div>
<divclass="line"><aid="l00165"name="l00165"></a><spanclass="lineno"> 165</span><spanclass="comment">// cannot be derived by the current implication graph.</span></div>
<divclass="line"><aid="l00167"name="l00167"></a><spanclass="lineno"> 167</span><spanclass="comment">// With these extra clause the power of the equivalence literal detection</span></div>
<divclass="line"><aid="l00168"name="l00168"></a><spanclass="lineno"> 168</span><spanclass="comment">// using only the binary implication graph with increase. Note that it is</span></div>
<divclass="line"><aid="l00169"name="l00169"></a><spanclass="lineno"> 169</span><spanclass="comment">// possible to do exactly the same thing without adding these binary clause</span></div>
<divclass="line"><aid="l00170"name="l00170"></a><spanclass="lineno"> 170</span><spanclass="comment">// first. This is what is done by yet another probing algorithm (currently in</span></div>
<divclass="line"><aid="l00173"name="l00173"></a><spanclass="lineno"> 173</span><spanclass="comment">// TODO(user): Note that adding binary clause before/during the SAT presolve</span></div>
<divclass="line"><aid="l00174"name="l00174"></a><spanclass="lineno"> 174</span><spanclass="comment">// is currently not always a good idea. This is because we don't simplify the</span></div>
<divclass="line"><aid="l00175"name="l00175"></a><spanclass="lineno"> 175</span><spanclass="comment">// other clause as much as we could. Also, there can be up to a quadratic</span></div>
<divclass="line"><aid="l00176"name="l00176"></a><spanclass="lineno"> 176</span><spanclass="comment">// number of clauses added this way, which might slow down things a lot. But</span></div>
<divclass="line"><aid="l00177"name="l00177"></a><spanclass="lineno"> 177</span><spanclass="comment">// then because of the deterministic limit, we usually cannot add too much</span></div>
<divclass="line"><aid="l00178"name="l00178"></a><spanclass="lineno"> 178</span><spanclass="comment">// clauses, even for huge problems, since we will reach the limit before that.</span></div>
<divclass="line"><aid="l00181"name="l00181"></a><spanclass="lineno"> 181</span><spanclass="comment">// Use a version of the "Tree look" algorithm as explained in the paper above.</span></div>
<divclass="line"><aid="l00182"name="l00182"></a><spanclass="lineno"> 182</span><spanclass="comment">// This is usually faster and more efficient. Note that when extracting binary</span></div>
<divclass="line"><aid="l00183"name="l00183"></a><spanclass="lineno"> 183</span><spanclass="comment">// clauses it might currently produce more "redundant" one in the sense that a</span></div>
<divclass="line"><aid="l00184"name="l00184"></a><spanclass="lineno"> 184</span><spanclass="comment">// transitive reduction of the binary implication graph after all hyper binary</span></div>
<divclass="line"><aid="l00185"name="l00185"></a><spanclass="lineno"> 185</span><spanclass="comment">// resolution have been performed may need to do more work.</span></div>
<divclass="line"><aid="l00188"name="l00188"></a><spanclass="lineno"> 188</span><spanclass="comment">// There is two sligthly different implementation of the tree-look algo.</span></div>
<divclass="line"><aid="l00190"name="l00190"></a><spanclass="lineno"> 190</span><spanclass="comment">// TODO(user): Decide which one is better, currently the difference seems</span></div>
<divclass="line"><aid="l00191"name="l00191"></a><spanclass="lineno"> 191</span><spanclass="comment">// small but the queue seems slightly faster.</span></div>
<divclass="line"><aid="l00194"name="l00194"></a><spanclass="lineno"> 194</span><spanclass="comment">// If we detect as we probe that a new binary clause subsumes one of the</span></div>
<divclass="line"><aid="l00195"name="l00195"></a><spanclass="lineno"> 195</span><spanclass="comment">// non-binary clause, we will replace the long clause by the binary one. This</span></div>
<divclass="line"><aid="l00196"name="l00196"></a><spanclass="lineno"> 196</span><spanclass="comment">// is orthogonal to the extract_binary_clauses parameters which will add all</span></div>
<divclass="line"><aid="l00197"name="l00197"></a><spanclass="lineno"> 197</span><spanclass="comment">// binary clauses but not neceassirly check for subsumption.</span></div>
<divclass="line"><aid="l00200"name="l00200"></a><spanclass="lineno"> 200</span><spanclass="comment">// We assume this is also true if --v 1 is activated.</span></div>
<divclass="line"><aid="l00211"name="l00211"></a><spanclass="lineno"> 211</span><spanclass="comment">// Similar to ProbeBooleanVariables() but different :-)</span></div>
<divclass="line"><aid="l00213"name="l00213"></a><spanclass="lineno"> 213</span><spanclass="comment">// First, this do not consider integer variable. It doesn't do any disjunctive</span></div>
<divclass="line"><aid="l00214"name="l00214"></a><spanclass="lineno"> 214</span><spanclass="comment">// reasoning (i.e. changing the domain of an integer variable by intersecting</span></div>
<divclass="line"><aid="l00215"name="l00215"></a><spanclass="lineno"> 215</span><spanclass="comment">// it with the union of what happen when x is fixed and not(x) is fixed).</span></div>
<divclass="line"><aid="l00217"name="l00217"></a><spanclass="lineno"> 217</span><spanclass="comment">// However this should be more efficient and just work better for pure Boolean</span></div>
<divclass="line"><aid="l00218"name="l00218"></a><spanclass="lineno"> 218</span><spanclass="comment">// problems. On integer problems, we might also want to run this one first,</span></div>
<divclass="line"><aid="l00219"name="l00219"></a><spanclass="lineno"> 219</span><spanclass="comment">// and then do just one quick pass of ProbeBooleanVariables().</span></div>
<divclass="line"><aid="l00221"name="l00221"></a><spanclass="lineno"> 221</span><spanclass="comment">// Note that this by itself just do one "round", look at the code in the</span></div>
<divclass="line"><aid="l00222"name="l00222"></a><spanclass="lineno"> 222</span><spanclass="comment">// Inprocessing class that call this interleaved with other reductions until a</span></div>
<divclass="line"><aid="l00223"name="l00223"></a><spanclass="lineno"> 223</span><spanclass="comment">// fix point is reached.</span></div>
<divclass="line"><aid="l00225"name="l00225"></a><spanclass="lineno"> 225</span><spanclass="comment">// This can fix a lot of literals via failed literal detection, that is when</span></div>
<divclass="line"><aid="l00226"name="l00226"></a><spanclass="lineno"> 226</span><spanclass="comment">// we detect that x => not(x) via propagation after taking x as a decision. It</span></div>
<divclass="line"><aid="l00227"name="l00227"></a><spanclass="lineno"> 227</span><spanclass="comment">// also use the strongly connected component algorithm to detect equivalent</span></div>
<divclass="line"><aid="l00230"name="l00230"></a><spanclass="lineno"> 230</span><spanclass="comment">// It will add any detected binary clause (via hyper binary resolution) to</span></div>
<divclass="line"><aid="l00231"name="l00231"></a><spanclass="lineno"> 231</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#l00106">time_limit.h:106</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#l00042">sat/model.h:42</a></div></div>
<divclass="ttc"id="anamespaceoperations__research_1_1sat_html_a227161ebe5ee0b44d69f7bd8655a3e49"><divclass="ttname"><ahref="namespaceoperations__research_1_1sat.html#a227161ebe5ee0b44d69f7bd8655a3e49">operations_research::sat::LookForTrivialSatSolution</a></div><divclass="ttdeci">bool LookForTrivialSatSolution(double deterministic_time_limit, Model *model)</div><divclass="ttdef"><b>Definition:</b><ahref="probing_8cc_source.html#l00290">probing.cc:290</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#l00368">probing.cc:368</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>
