<!-- 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">simplification.h</div></div>
</div><!--header-->
<divclass="contents">
<ahref="simplification_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="l00014"></a><spanclass="lineno"> 14</span> <spanclass="comment">// Implementation of a pure SAT presolver. This roughly follows the paper:</span></div>
<divclass="line"><aname="l00016"></a><spanclass="lineno"> 16</span> <spanclass="comment">// "Effective Preprocessing in SAT through Variable and Clause Elimination",</span></div>
<divclass="line"><aname="l00017"></a><spanclass="lineno"> 17</span> <spanclass="comment">// Niklas Een and Armin Biere, published in the SAT 2005 proceedings.</span></div>
<divclass="line"><aname="l00044"></a><spanclass="lineno"> 44</span> <spanclass="comment">// The idea is that any presolve algorithm can just update this class, and at</span></div>
<divclass="line"><aname="l00045"></a><spanclass="lineno"> 45</span> <spanclass="comment">// the end, this class will recover a solution of the initial problem from a</span></div>
<divclass="line"><aname="l00046"></a><spanclass="lineno"> 46</span> <spanclass="comment">// solution of the presolved problem.</span></div>
<divclass="line"><aname="l00051"></a><spanclass="lineno"> 51</span> <spanclass="comment">// The postsolver will process the Add() calls in reverse order. If the given</span></div>
<divclass="line"><aname="l00052"></a><spanclass="lineno"> 52</span> <spanclass="comment">// clause has all its literals at false, it simply sets the literal x to true.</span></div>
<divclass="line"><aname="l00053"></a><spanclass="lineno"> 53</span> <spanclass="comment">// Note that x must be a literal of the given clause.</span></div>
<divclass="line"><aname="l00056"></a><spanclass="lineno"> 56</span> <spanclass="comment">// Tells the postsolver that the given literal must be true in any solution.</span></div>
<divclass="line"><aname="l00057"></a><spanclass="lineno"> 57</span> <spanclass="comment">// We currently check that the variable is not already fixed.</span></div>
<divclass="line"><aname="l00059"></a><spanclass="lineno"> 59</span> <spanclass="comment">// TODO(user): this as almost the same effect as adding an unit clause, and we</span></div>
<divclass="line"><aname="l00060"></a><spanclass="lineno"> 60</span> <spanclass="comment">// should probably remove this to simplify the code.</span></div>
<divclass="line"><aname="l00063"></a><spanclass="lineno"> 63</span> <spanclass="comment">// This assumes that the given variable mapping has been applied to the</span></div>
<divclass="line"><aname="l00064"></a><spanclass="lineno"> 64</span> <spanclass="comment">// problem. All the subsequent Add() and FixVariable() will refer to the new</span></div>
<divclass="line"><aname="l00065"></a><spanclass="lineno"> 65</span> <spanclass="comment">// problem. During postsolve, the initial solution must also correspond to</span></div>
<divclass="line"><aname="l00066"></a><spanclass="lineno"> 66</span> <spanclass="comment">// this new problem. Note that if mapping[v] == -1, then the literal v is</span></div>
<divclass="line"><aname="l00067"></a><spanclass="lineno"> 67</span> <spanclass="comment">// assumed to be deleted.</span></div>
<divclass="line"><aname="l00069"></a><spanclass="lineno"> 69</span> <spanclass="comment">// This can be called more than once. But each call must refer to the current</span></div>
<divclass="line"><aname="l00070"></a><spanclass="lineno"> 70</span> <spanclass="comment">// variables set (after all the previous mapping have been applied).</span></div>
<divclass="line"><aname="l00074"></a><spanclass="lineno"> 74</span> <spanclass="comment">// Extracts the current assignment of the given solver and postsolve it.</span></div>
<divclass="line"><aname="l00076"></a><spanclass="lineno"> 76</span> <spanclass="comment">// Node(fdid): This can currently be called only once (but this is easy to</span></div>
<divclass="line"><aname="l00077"></a><spanclass="lineno"> 77</span> <spanclass="comment">// change since only some CHECK will fail).</span></div>
<divclass="line"><aname="l00081"></a><spanclass="lineno"> 81</span> <spanclass="comment">// Getters to the clauses managed by this class.</span></div>
<divclass="line"><aname="l00082"></a><spanclass="lineno"> 82</span> <spanclass="comment">// Important: This will always put the associated literal first.</span></div>
<divclass="line"><aname="l00085"></a><spanclass="lineno"> 85</span> <spanclass="comment">// TODO(user): we could avoid the copy here, but because clauses_literals_</span></div>
<divclass="line"><aname="l00086"></a><spanclass="lineno"> 86</span> <spanclass="comment">// is a deque, we do need a special return class and cannot juste use</span></div>
<divclass="line"><aname="l00087"></a><spanclass="lineno"> 87</span> <spanclass="comment">// absl::Span<Literal> for instance.</span></div>
<divclass="line"><aname="l00088"></a><spanclass="lineno"> 88</span> <spanclass="keyword">const</span><spanclass="keywordtype">int</span> begin = clauses_start_[i];</div>
<divclass="line"><aname="l00089"></a><spanclass="lineno"> 89</span> <spanclass="keyword">const</span><spanclass="keywordtype">int</span> end = i + 1 < clauses_start_.size() ? clauses_start_[i + 1]</div>
<divclass="line"><aname="l00106"></a><spanclass="lineno"> 106</span> <spanclass="comment">// The presolve can add new variables, so we need to store the number of</span></div>
<divclass="line"><aname="l00107"></a><spanclass="lineno"> 107</span> <spanclass="comment">// original variables in order to return a solution with the correct number</span></div>
<divclass="line"><aname="l00108"></a><spanclass="lineno"> 108</span> <spanclass="comment">// of variables.</span></div>
<divclass="line"><aname="l00112"></a><spanclass="lineno"> 112</span> <spanclass="comment">// Stores the arguments of the Add() calls: clauses_start_[i] is the index of</span></div>
<divclass="line"><aname="l00113"></a><spanclass="lineno"> 113</span> <spanclass="comment">// the first literal of the clause #i in the clauses_literals_ deque.</span></div>
<divclass="line"><aname="l00118"></a><spanclass="lineno"> 118</span> <spanclass="comment">// All the added clauses will be mapped back to the initial variables using</span></div>
<divclass="line"><aname="l00119"></a><spanclass="lineno"> 119</span> <spanclass="comment">// this reverse mapping. This way, clauses_ and associated_literal_ are only</span></div>
<divclass="line"><aname="l00120"></a><spanclass="lineno"> 120</span> <spanclass="comment">// in term of the initial problem.</span></div>
<divclass="line"><aname="l00123"></a><spanclass="lineno"> 123</span> <spanclass="comment">// This will stores the fixed variables value and later the postsolved</span></div>
<divclass="line"><aname="l00130"></a><spanclass="lineno"> 130</span> <spanclass="comment">// This class holds a SAT problem (i.e. a set of clauses) and the logic to</span></div>
<divclass="line"><aname="l00131"></a><spanclass="lineno"> 131</span> <spanclass="comment">// presolve it by a series of subsumption, self-subsuming resolution, and</span></div>
<divclass="line"><aname="l00132"></a><spanclass="lineno"> 132</span> <spanclass="comment">// variable elimination by clause distribution.</span></div>
<divclass="line"><aname="l00134"></a><spanclass="lineno"> 134</span> <spanclass="comment">// Note that this does propagate unit-clauses, but probably much</span></div>
<divclass="line"><aname="l00135"></a><spanclass="lineno"> 135</span> <spanclass="comment">// less efficiently than the propagation code in the SAT solver. So it is better</span></div>
<divclass="line"><aname="l00136"></a><spanclass="lineno"> 136</span> <spanclass="comment">// to use a SAT solver to fix variables before using this class.</span></div>
<divclass="line"><aname="l00138"></a><spanclass="lineno"> 138</span> <spanclass="comment">// TODO(user): Interact more with a SAT solver to reuse its propagation logic.</span></div>
<divclass="line"><aname="l00140"></a><spanclass="lineno"> 140</span> <spanclass="comment">// TODO(user): Forbid the removal of some variables. This way we can presolve</span></div>
<divclass="line"><aname="l00141"></a><spanclass="lineno"> 141</span> <spanclass="comment">// only the clause part of a general Boolean problem by not removing variables</span></div>
<divclass="line"><aname="l00142"></a><spanclass="lineno"> 142</span> <spanclass="comment">// appearing in pseudo-Boolean constraints.</span></div>
<divclass="line"><aname="l00156"></a><spanclass="lineno"> 156</span> <spanclass="comment">// Registers a mapping to encode equivalent literals.</span></div>
<divclass="line"><aname="l00157"></a><spanclass="lineno"> 157</span> <spanclass="comment">// See ProbeAndFindEquivalentLiteral().</span></div>
<divclass="line"><aname="l00168"></a><spanclass="lineno"> 168</span> <spanclass="comment">// Presolves the problem currently loaded. Returns false if the model is</span></div>
<divclass="line"><aname="l00169"></a><spanclass="lineno"> 169</span> <spanclass="comment">// proven to be UNSAT during the presolving.</span></div>
<divclass="line"><aname="l00171"></a><spanclass="lineno"> 171</span> <spanclass="comment">// TODO(user): Add support for a time limit and some kind of iterations limit</span></div>
<divclass="line"><aname="l00172"></a><spanclass="lineno"> 172</span> <spanclass="comment">// so that this can never take too much time.</span></div>
<divclass="line"><aname="l00175"></a><spanclass="lineno"> 175</span> <spanclass="comment">// Same as Presolve() but only allow to remove BooleanVariable whose index</span></div>
<divclass="line"><aname="l00176"></a><spanclass="lineno"> 176</span> <spanclass="comment">// is set to true in the given vector.</span></div>
<divclass="line"><aname="l00180"></a><spanclass="lineno"> 180</span> <spanclass="comment">// All the clauses managed by this class.</span></div>
<divclass="line"><aname="l00181"></a><spanclass="lineno"> 181</span> <spanclass="comment">// Note that deleted clauses keep their indices (they are just empty).</span></div>
<divclass="line"><aname="l00187"></a><spanclass="lineno"> 187</span> <spanclass="comment">// The number of variables. This is computed automatically from the clauses</span></div>
<divclass="line"><aname="l00188"></a><spanclass="lineno"> 188</span> <spanclass="comment">// added to the SatPresolver.</span></div>
<divclass="line"><aname="l00191"></a><spanclass="lineno"> 191</span> <spanclass="comment">// After presolving, Some variables in [0, NumVariables()) have no longer any</span></div>
<divclass="line"><aname="l00192"></a><spanclass="lineno"> 192</span> <spanclass="comment">// clause pointing to them. This return a mapping that maps this interval to</span></div>
<divclass="line"><aname="l00193"></a><spanclass="lineno"> 193</span> <spanclass="comment">// [0, new_size) such that now all variables are used. The unused variable</span></div>
<divclass="line"><aname="l00194"></a><spanclass="lineno"> 194</span> <spanclass="comment">// will be mapped to BooleanVariable(-1).</span></div>
<divclass="line"><aname="l00197"></a><spanclass="lineno"> 197</span> <spanclass="comment">// Loads the current presolved problem in to the given sat solver.</span></div>
<divclass="line"><aname="l00198"></a><spanclass="lineno"> 198</span> <spanclass="comment">// Note that the variables will be re-indexed according to the mapping given</span></div>
<divclass="line"><aname="l00199"></a><spanclass="lineno"> 199</span> <spanclass="comment">// by GetMapping() so that they form a dense set.</span></div>
<divclass="line"><aname="l00201"></a><spanclass="lineno"> 201</span> <spanclass="comment">// IMPORTANT: This is not const because it deletes the presolver clauses as</span></div>
<divclass="line"><aname="l00202"></a><spanclass="lineno"> 202</span> <spanclass="comment">// they are added to the SatSolver in order to save memory. After this is</span></div>
<divclass="line"><aname="l00203"></a><spanclass="lineno"> 203</span> <spanclass="comment">// called, only VariableMapping() will still works.</span></div>
<divclass="line"><aname="l00206"></a><spanclass="lineno"> 206</span> <spanclass="comment">// Visible for Testing. Takes a given clause index and looks for clause that</span></div>
<divclass="line"><aname="l00207"></a><spanclass="lineno"> 207</span> <spanclass="comment">// can be subsumed or strengthened using this clause. Returns false if the</span></div>
<divclass="line"><aname="l00208"></a><spanclass="lineno"> 208</span> <spanclass="comment">// model is proven to be unsat.</span></div>
<divclass="line"><aname="l00211"></a><spanclass="lineno"> 211</span> <spanclass="comment">// Visible for testing. Tries to eliminate x by clause distribution.</span></div>
<divclass="line"><aname="l00212"></a><spanclass="lineno"> 212</span> <spanclass="comment">// This is also known as bounded variable elimination.</span></div>
<divclass="line"><aname="l00214"></a><spanclass="lineno"> 214</span> <spanclass="comment">// It is always possible to remove x by resolving each clause containing x</span></div>
<divclass="line"><aname="l00215"></a><spanclass="lineno"> 215</span> <spanclass="comment">// with all the clauses containing not(x). Hence the cross-product name. Note</span></div>
<divclass="line"><aname="l00216"></a><spanclass="lineno"> 216</span> <spanclass="comment">// that this function only do that if the number of clauses is reduced.</span></div>
<divclass="line"><aname="l00219"></a><spanclass="lineno"> 219</span> <spanclass="comment">// Visible for testing. Just applies the BVA step of the presolve.</span></div>
<divclass="line"><aname="l00227"></a><spanclass="lineno"> 227</span> <spanclass="comment">// Internal function used by ProcessClauseToSimplifyOthers().</span></div>
<divclass="line"><aname="l00231"></a><spanclass="lineno"> 231</span> <spanclass="comment">// Internal function to add clauses generated during the presolve. The clause</span></div>
<divclass="line"><aname="l00232"></a><spanclass="lineno"> 232</span> <spanclass="comment">// must already be sorted with the default Literal order and will be cleared</span></div>
<divclass="line"><aname="l00233"></a><spanclass="lineno"> 233</span> <spanclass="comment">// after this call.</span></div>
<divclass="line"><aname="l00241"></a><spanclass="lineno"> 241</span> <spanclass="comment">// Call ProcessClauseToSimplifyOthers() on all the clauses in</span></div>
<divclass="line"><aname="l00242"></a><spanclass="lineno"> 242</span> <spanclass="comment">// clause_to_process_ and empty the list afterwards. Note that while some</span></div>
<divclass="line"><aname="l00243"></a><spanclass="lineno"> 243</span> <spanclass="comment">// clauses are processed, new ones may be added to the list. Returns false if</span></div>
<divclass="line"><aname="l00244"></a><spanclass="lineno"> 244</span> <spanclass="comment">// the problem is shown to be UNSAT.</span></div>
<divclass="line"><aname="l00247"></a><spanclass="lineno"> 247</span> <spanclass="comment">// Finds the literal from the clause that occur the less in the clause</span></div>
<divclass="line"><aname="l00254"></a><spanclass="lineno"> 254</span> <spanclass="comment">// Tests and maybe perform a Simple Bounded Variable addition starting from</span></div>
<divclass="line"><aname="l00255"></a><spanclass="lineno"> 255</span> <spanclass="comment">// the given literal as described in the paper: "Automated Reencoding of</span></div>
<divclass="line"><aname="l00256"></a><spanclass="lineno"> 256</span> <spanclass="comment">// Boolean Formulas", Norbert Manthey, Marijn J. H. Heule, and Armin Biere,</span></div>
<divclass="line"><aname="l00257"></a><spanclass="lineno"> 257</span> <spanclass="comment">// Volume 7857 of the series Lecture Notes in Computer Science pp 102-117,</span></div>
<divclass="line"><aname="l00261"></a><spanclass="lineno"> 261</span> <spanclass="comment">// This seems to have a mostly positive effect, except on the crafted problem</span></div>
<divclass="line"><aname="l00262"></a><spanclass="lineno"> 262</span> <spanclass="comment">// familly mugrauer_balint--GI.crafted_nxx_d6_cx_numxx where the reduction</span></div>
<divclass="line"><aname="l00263"></a><spanclass="lineno"> 263</span> <spanclass="comment">// is big, but apparently the problem is harder to prove UNSAT for the solver.</span></div>
<divclass="line"><aname="l00266"></a><spanclass="lineno"> 266</span> <spanclass="comment">// Display some statistics on the current clause database.</span></div>
<divclass="line"><aname="l00269"></a><spanclass="lineno"> 269</span> <spanclass="comment">// Returns a hash of the given clause variables (not literal) in such a way</span></div>
<divclass="line"><aname="l00270"></a><spanclass="lineno"> 270</span> <spanclass="comment">// that hash1 & not(hash2) == 0 iff the set of variable of clause 1 is a</span></div>
<divclass="line"><aname="l00271"></a><spanclass="lineno"> 271</span> <spanclass="comment">// subset of the one of clause2.</span></div>
<divclass="line"><aname="l00274"></a><spanclass="lineno"> 274</span> <spanclass="comment">// The "active" variables on which we want to call CrossProduct() are kept</span></div>
<divclass="line"><aname="l00275"></a><spanclass="lineno"> 275</span> <spanclass="comment">// in a priority queue so that we process first the ones that occur the least</span></div>
<divclass="line"><aname="l00276"></a><spanclass="lineno"> 276</span> <spanclass="comment">// often in the clause database.</span></div>
<divclass="line"><aname="l00282"></a><spanclass="lineno"> 282</span> <spanclass="comment">// Interface for the AdjustablePriorityQueue.</span></div>
<divclass="line"><aname="l00286"></a><spanclass="lineno"> 286</span> <spanclass="comment">// Priority order. The AdjustablePriorityQueue returns the largest element</span></div>
<divclass="line"><aname="l00287"></a><spanclass="lineno"> 287</span> <spanclass="comment">// first, but our weight goes this other way around (smaller is better).</span></div>
<divclass="line"><aname="l00299"></a><spanclass="lineno"> 299</span> <spanclass="comment">// Literal priority queue for BVA. The literals are ordered by descending</span></div>
<divclass="line"><aname="l00300"></a><spanclass="lineno"> 300</span> <spanclass="comment">// number of occurrences in clauses.</span></div>
<divclass="line"><aname="l00307"></a><spanclass="lineno"> 307</span> <spanclass="comment">// Interface for the AdjustablePriorityQueue.</span></div>
<divclass="line"><aname="l00312"></a><spanclass="lineno"> 312</span> <spanclass="comment">// The AdjustablePriorityQueue returns the largest element first.</span></div>
<divclass="line"><aname="l00321"></a><spanclass="lineno"> 321</span>  std::deque<BvaPqElement> bva_pq_elements_; <spanclass="comment">// deque because we add variables.</span></div>
<divclass="line"><aname="l00331"></a><spanclass="lineno"> 331</span> <spanclass="comment">// List of clauses on which we need to call ProcessClauseToSimplifyOthers().</span></div>
<divclass="line"><aname="l00332"></a><spanclass="lineno"> 332</span> <spanclass="comment">// See ProcessAllClauses().</span></div>
<divclass="line"><aname="l00336"></a><spanclass="lineno"> 336</span> <spanclass="comment">// The set of all clauses.</span></div>
<divclass="line"><aname="l00337"></a><spanclass="lineno"> 337</span> <spanclass="comment">// An empty clause means that it has been removed.</span></div>
<divclass="line"><aname="l00338"></a><spanclass="lineno"> 338</span>  std::vector<std::vector<Literal>> clauses_; <spanclass="comment">// Indexed by ClauseIndex</span></div>
<divclass="line"><aname="l00340"></a><spanclass="lineno"> 340</span> <spanclass="comment">// The cached value of ComputeSignatureOfClauseVariables() for each clause.</span></div>
<divclass="line"><aname="l00341"></a><spanclass="lineno"> 341</span>  std::vector<uint64> signatures_; <spanclass="comment">// Indexed by ClauseIndex</span></div>
<divclass="line"><aname="l00345"></a><spanclass="lineno"> 345</span> <spanclass="comment">// Occurrence list. For each literal, contains the ClauseIndex of the clause</span></div>
<divclass="line"><aname="l00346"></a><spanclass="lineno"> 346</span> <spanclass="comment">// that contains it (ordered by clause index).</span></div>
<divclass="line"><aname="l00350"></a><spanclass="lineno"> 350</span> <spanclass="comment">// Because we only lazily clean the occurrence list after clause deletions,</span></div>
<divclass="line"><aname="l00351"></a><spanclass="lineno"> 351</span> <spanclass="comment">// we keep the size of the occurrence list (without the deleted clause) here.</span></div>
<divclass="line"><aname="l00368"></a><spanclass="lineno"> 368</span> <spanclass="comment">// Visible for testing. Returns true iff:</span></div>
<divclass="line"><aname="l00369"></a><spanclass="lineno"> 369</span> <spanclass="comment">// - a subsume b (subsumption): the clause a is a subset of b, in which case</span></div>
<divclass="line"><aname="l00370"></a><spanclass="lineno"> 370</span> <spanclass="comment">// opposite_literal is set to -1.</span></div>
<divclass="line"><aname="l00371"></a><spanclass="lineno"> 371</span> <spanclass="comment">// - b is strengthened by self-subsumption using a (self-subsuming resolution):</span></div>
<divclass="line"><aname="l00372"></a><spanclass="lineno"> 372</span> <spanclass="comment">// the clause a with one of its literal negated is a subset of b, in which</span></div>
<divclass="line"><aname="l00373"></a><spanclass="lineno"> 373</span> <spanclass="comment">// case opposite_literal is set to this negated literal index. Moreover, this</span></div>
<divclass="line"><aname="l00374"></a><spanclass="lineno"> 374</span> <spanclass="comment">// opposite_literal is then removed from b.</span></div>
<divclass="line"><aname="l00376"></a><spanclass="lineno"> 376</span> <spanclass="comment">// If num_inspected_literals_ is not nullptr, the "complexity" of this function</span></div>
<divclass="line"><aname="l00377"></a><spanclass="lineno"> 377</span> <spanclass="comment">// will be added to it in order to track the amount of work done.</span></div>
<divclass="line"><aname="l00379"></a><spanclass="lineno"> 379</span> <spanclass="comment">// TODO(user): when a.size() << b.size(), we should use binary search instead</span></div>
<divclass="line"><aname="l00380"></a><spanclass="lineno"> 380</span> <spanclass="comment">// of scanning b linearly.</span></div>
<divclass="line"><aname="l00385"></a><spanclass="lineno"> 385</span> <spanclass="comment">// Visible for testing. Returns kNoLiteralIndex except if:</span></div>
<divclass="line"><aname="l00386"></a><spanclass="lineno"> 386</span> <spanclass="comment">// - a and b differ in only one literal.</span></div>
<divclass="line"><aname="l00387"></a><spanclass="lineno"> 387</span> <spanclass="comment">// - For a it is the given literal l.</span></div>
<divclass="line"><aname="l00388"></a><spanclass="lineno"> 388</span> <spanclass="comment">// In which case, returns the LiteralIndex of the literal in b that is not in a.</span></div>
<divclass="line"><aname="l00392"></a><spanclass="lineno"> 392</span> <spanclass="comment">// Visible for testing. Computes the resolvant of 'a' and 'b' obtained by</span></div>
<divclass="line"><aname="l00393"></a><spanclass="lineno"> 393</span> <spanclass="comment">// performing the resolution on 'x'. If the resolvant is trivially true this</span></div>
<divclass="line"><aname="l00394"></a><spanclass="lineno"> 394</span> <spanclass="comment">// returns false, otherwise it returns true and fill 'out' with the resolvant.</span></div>
<divclass="line"><aname="l00396"></a><spanclass="lineno"> 396</span> <spanclass="comment">// Note that the resolvant is just 'a' union 'b' with the literals 'x' and</span></div>
<divclass="line"><aname="l00397"></a><spanclass="lineno"> 397</span> <spanclass="comment">// not(x) removed. The two clauses are assumed to be sorted, and the computed</span></div>
<divclass="line"><aname="l00398"></a><spanclass="lineno"> 398</span> <spanclass="comment">// resolvant will also be sorted.</span></div>
<divclass="line"><aname="l00400"></a><spanclass="lineno"> 400</span> <spanclass="comment">// This is the basic operation when a variable is eliminated by clause</span></div>
<divclass="line"><aname="l00405"></a><spanclass="lineno"> 405</span> <spanclass="comment">// Same as ComputeResolvant() but just returns the resolvant size.</span></div>
<divclass="line"><aname="l00406"></a><spanclass="lineno"> 406</span> <spanclass="comment">// Returns -1 when ComputeResolvant() returns false.</span></div>
<divclass="line"><aname="l00410"></a><spanclass="lineno"> 410</span> <spanclass="comment">// Presolver that does literals probing and finds equivalent literals by</span></div>
<divclass="line"><aname="l00411"></a><spanclass="lineno"> 411</span> <spanclass="comment">// computing the strongly connected components of the graph:</span></div>
<divclass="line"><aname="l00412"></a><spanclass="lineno"> 412</span> <spanclass="comment">// literal l -> literals propagated by l.</span></div>
<divclass="line"><aname="l00414"></a><spanclass="lineno"> 414</span> <spanclass="comment">// Clears the mapping if there are no equivalent literals. Otherwise, mapping[l]</span></div>
<divclass="line"><aname="l00415"></a><spanclass="lineno"> 415</span> <spanclass="comment">// is the representative of the equivalent class of l. Note that mapping[l] may</span></div>
<divclass="line"><aname="l00416"></a><spanclass="lineno"> 416</span> <spanclass="comment">// be equal to l.</span></div>
<divclass="line"><aname="l00418"></a><spanclass="lineno"> 418</span> <spanclass="comment">// The postsolver will be updated so it can recover a solution of the mapped</span></div>
<divclass="line"><aname="l00419"></a><spanclass="lineno"> 419</span> <spanclass="comment">// problem. Note that this works on any problem the SatSolver can handle, not</span></div>
<divclass="line"><aname="l00420"></a><spanclass="lineno"> 420</span> <spanclass="comment">// only pure SAT problem, but the returned mapping do need to be applied to all</span></div>
<divclass="line"><aname="l00427"></a><spanclass="lineno"> 427</span> <spanclass="comment">// Given a 'solver' with a problem already loaded, this will try to simplify the</span></div>
<divclass="line"><aname="l00428"></a><spanclass="lineno"> 428</span> <spanclass="comment">// problem (i.e. presolve it) before calling solver->Solve(). In the process,</span></div>
<divclass="line"><aname="l00429"></a><spanclass="lineno"> 429</span> <spanclass="comment">// because of the way the presolve is implemented, the underlying SatSolver may</span></div>
<divclass="line"><aname="l00430"></a><spanclass="lineno"> 430</span> <spanclass="comment">// change (it is why we use this unique_ptr interface). In particular, the final</span></div>
<divclass="line"><aname="l00431"></a><spanclass="lineno"> 431</span> <spanclass="comment">// variables and 'solver' state may have nothing to do with the problem</span></div>
<divclass="line"><aname="l00432"></a><spanclass="lineno"> 432</span> <spanclass="comment">// originaly present in the solver. That said, if the problem is shown to be</span></div>
<divclass="line"><aname="l00433"></a><spanclass="lineno"> 433</span> <spanclass="comment">// SAT, then the returned solution will be in term of the original variables.</span></div>
<divclass="line"><aname="l00435"></a><spanclass="lineno"> 435</span> <spanclass="comment">// Note that the full presolve is only executed if the problem is a pure SAT</span></div>
<divclass="line"><aname="l00436"></a><spanclass="lineno"> 436</span> <spanclass="comment">// problem with only clauses.</span></div>
<divclass="line"><aname="l00439"></a><spanclass="lineno"> 439</span>  std::vector<bool>* solution <spanclass="comment">/* only filled if SAT */</span>,</div>
<divclass="line"><aname="l00440"></a><spanclass="lineno"> 440</span>  DratProofHandler* drat_proof_handler <spanclass="comment">/* can be nullptr */</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_sat_presolver_html_a26fc07b3630b79be6914e6387b63a073"><divclass="ttname"><ahref="classoperations__research_1_1sat_1_1_sat_presolver.html#a26fc07b3630b79be6914e6387b63a073">operations_research::sat::SatPresolver::AddBinaryClause</a></div><divclass="ttdeci">void AddBinaryClause(Literal a, Literal b)</div><divclass="ttdef"><b>Definition:</b><ahref="simplification_8cc_source.html#l00159">simplification.cc:159</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>
