Files
ortools-clone/docs/cpp/sat__solver_8h_source.html
2021-01-26 11:34:47 +01:00

1298 lines
258 KiB
HTML

<!-- HTML header for doxygen 1.8.18-->
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "https://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<meta http-equiv="X-UA-Compatible" content="IE=9"/>
<meta name="generator" content="Doxygen 1.9.1"/>
<meta name="viewport" content="width=device-width, initial-scale=1"/>
<title>OR-Tools: sat_solver.h Source File</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="jquery.js"></script>
<script type="text/javascript" src="dynsections.js"></script>
<link href="navtree.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="resize.js"></script>
<script type="text/javascript" src="navtreedata.js"></script>
<script type="text/javascript" src="navtree.js"></script>
<link href="search/search.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="search/searchdata.js"></script>
<script type="text/javascript" src="search/search.js"></script>
<link href="doxygen.css" rel="stylesheet" type="text/css" />
<link href="styleSheet.tmp.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<div id="top"><!-- do not remove this div, it is closed by doxygen! -->
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td id="projectlogo"><img alt="Logo" src="orLogo.png"/></td>
<td id="projectalign" style="padding-left: 0.5em;">
<div id="projectname">OR-Tools
&#160;<span id="projectnumber">8.2</span>
</div>
</td>
</tr>
</tbody>
</table>
</div>
<!-- end header part -->
<!-- Generated by Doxygen 1.9.1 -->
<script type="text/javascript">
/* @license magnet:?xt=urn:btih:cf05388f2679ee054f2beb29a391d25f4e673ac3&amp;dn=gpl-2.0.txt GPL-v2 */
var searchBox = new SearchBox("searchBox", "search",false,'Search','.html');
/* @license-end */
</script>
<script type="text/javascript" src="menudata.js"></script>
<script type="text/javascript" src="menu.js"></script>
<script type="text/javascript">
/* @license magnet:?xt=urn:btih:cf05388f2679ee054f2beb29a391d25f4e673ac3&amp;dn=gpl-2.0.txt GPL-v2 */
$(function() {
initMenu('',true,false,'search.php','Search');
$(document).ready(function() { init_search(); });
});
/* @license-end */</script>
<div id="main-nav"></div>
</div><!-- top -->
<div id="side-nav" class="ui-resizable side-nav-resizable">
<div id="nav-tree">
<div id="nav-tree-contents">
<div id="nav-sync" class="sync"></div>
</div>
</div>
<div id="splitbar" style="-moz-user-select:none;"
class="ui-resizable-handle">
</div>
</div>
<script type="text/javascript">
/* @license magnet:?xt=urn:btih:cf05388f2679ee054f2beb29a391d25f4e673ac3&amp;dn=gpl-2.0.txt GPL-v2 */
$(document).ready(function(){initNavTree('sat__solver_8h_source.html',''); initResizable(); });
/* @license-end */
</script>
<div id="doc-content">
<!-- window showing the filter options -->
<div id="MSearchSelectWindow"
onmouseover="return searchBox.OnSearchSelectShow()"
onmouseout="return searchBox.OnSearchSelectHide()"
onkeydown="return searchBox.OnSearchSelectKey(event)">
</div>
<!-- iframe showing the search results (closed by default) -->
<div id="MSearchResultsWindow">
<iframe src="javascript:void(0)" frameborder="0"
name="MSearchResults" id="MSearchResults">
</iframe>
</div>
<div class="header">
<div class="headertitle">
<div class="title">sat_solver.h</div> </div>
</div><!--header-->
<div class="contents">
<a href="sat__solver_8h.html">Go to the documentation of this file.</a><div class="fragment"><div class="line"><a name="l00001"></a><span class="lineno"> 1</span>&#160;<span class="comment">// Copyright 2010-2018 Google LLC</span></div>
<div class="line"><a name="l00002"></a><span class="lineno"> 2</span>&#160;<span class="comment">// Licensed under the Apache License, Version 2.0 (the &quot;License&quot;);</span></div>
<div class="line"><a name="l00003"></a><span class="lineno"> 3</span>&#160;<span class="comment">// you may not use this file except in compliance with the License.</span></div>
<div class="line"><a name="l00004"></a><span class="lineno"> 4</span>&#160;<span class="comment">// You may obtain a copy of the License at</span></div>
<div class="line"><a name="l00005"></a><span class="lineno"> 5</span>&#160;<span class="comment">//</span></div>
<div class="line"><a name="l00006"></a><span class="lineno"> 6</span>&#160;<span class="comment">// http://www.apache.org/licenses/LICENSE-2.0</span></div>
<div class="line"><a name="l00007"></a><span class="lineno"> 7</span>&#160;<span class="comment">//</span></div>
<div class="line"><a name="l00008"></a><span class="lineno"> 8</span>&#160;<span class="comment">// Unless required by applicable law or agreed to in writing, software</span></div>
<div class="line"><a name="l00009"></a><span class="lineno"> 9</span>&#160;<span class="comment">// distributed under the License is distributed on an &quot;AS IS&quot; BASIS,</span></div>
<div class="line"><a name="l00010"></a><span class="lineno"> 10</span>&#160;<span class="comment">// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.</span></div>
<div class="line"><a name="l00011"></a><span class="lineno"> 11</span>&#160;<span class="comment">// See the License for the specific language governing permissions and</span></div>
<div class="line"><a name="l00012"></a><span class="lineno"> 12</span>&#160;<span class="comment">// limitations under the License.</span></div>
<div class="line"><a name="l00013"></a><span class="lineno"> 13</span>&#160; </div>
<div class="line"><a name="l00014"></a><span class="lineno"> 14</span>&#160;<span class="comment">// This file implements a SAT solver.</span></div>
<div class="line"><a name="l00015"></a><span class="lineno"> 15</span>&#160;<span class="comment">// see http://en.wikipedia.org/wiki/Boolean_satisfiability_problem</span></div>
<div class="line"><a name="l00016"></a><span class="lineno"> 16</span>&#160;<span class="comment">// for more detail.</span></div>
<div class="line"><a name="l00017"></a><span class="lineno"> 17</span>&#160;<span class="comment">// TODO(user): Expand.</span></div>
<div class="line"><a name="l00018"></a><span class="lineno"> 18</span>&#160; </div>
<div class="line"><a name="l00019"></a><span class="lineno"> 19</span>&#160;<span class="preprocessor">#ifndef OR_TOOLS_SAT_SAT_SOLVER_H_</span></div>
<div class="line"><a name="l00020"></a><span class="lineno"> 20</span>&#160;<span class="preprocessor">#define OR_TOOLS_SAT_SAT_SOLVER_H_</span></div>
<div class="line"><a name="l00021"></a><span class="lineno"> 21</span>&#160; </div>
<div class="line"><a name="l00022"></a><span class="lineno"> 22</span>&#160;<span class="preprocessor">#include &lt;functional&gt;</span></div>
<div class="line"><a name="l00023"></a><span class="lineno"> 23</span>&#160;<span class="preprocessor">#include &lt;limits&gt;</span></div>
<div class="line"><a name="l00024"></a><span class="lineno"> 24</span>&#160;<span class="preprocessor">#include &lt;memory&gt;</span></div>
<div class="line"><a name="l00025"></a><span class="lineno"> 25</span>&#160;<span class="preprocessor">#include &lt;string&gt;</span></div>
<div class="line"><a name="l00026"></a><span class="lineno"> 26</span>&#160;<span class="preprocessor">#include &lt;utility&gt;</span></div>
<div class="line"><a name="l00027"></a><span class="lineno"> 27</span>&#160;<span class="preprocessor">#include &lt;vector&gt;</span></div>
<div class="line"><a name="l00028"></a><span class="lineno"> 28</span>&#160; </div>
<div class="line"><a name="l00029"></a><span class="lineno"> 29</span>&#160;<span class="preprocessor">#include &quot;absl/container/flat_hash_map.h&quot;</span></div>
<div class="line"><a name="l00030"></a><span class="lineno"> 30</span>&#160;<span class="preprocessor">#include &quot;absl/types/span.h&quot;</span></div>
<div class="line"><a name="l00031"></a><span class="lineno"> 31</span>&#160;<span class="preprocessor">#include &quot;<a class="code" href="hash_8h.html">ortools/base/hash.h</a>&quot;</span></div>
<div class="line"><a name="l00032"></a><span class="lineno"> 32</span>&#160;<span class="preprocessor">#include &quot;<a class="code" href="int__type_8h.html">ortools/base/int_type.h</a>&quot;</span></div>
<div class="line"><a name="l00033"></a><span class="lineno"> 33</span>&#160;<span class="preprocessor">#include &quot;<a class="code" href="integral__types_8h.html">ortools/base/integral_types.h</a>&quot;</span></div>
<div class="line"><a name="l00034"></a><span class="lineno"> 34</span>&#160;<span class="preprocessor">#include &quot;<a class="code" href="base_2logging_8h.html">ortools/base/logging.h</a>&quot;</span></div>
<div class="line"><a name="l00035"></a><span class="lineno"> 35</span>&#160;<span class="preprocessor">#include &quot;<a class="code" href="macros_8h.html">ortools/base/macros.h</a>&quot;</span></div>
<div class="line"><a name="l00036"></a><span class="lineno"> 36</span>&#160;<span class="preprocessor">#include &quot;<a class="code" href="timer_8h.html">ortools/base/timer.h</a>&quot;</span></div>
<div class="line"><a name="l00037"></a><span class="lineno"> 37</span>&#160;<span class="preprocessor">#include &quot;<a class="code" href="clause_8h.html">ortools/sat/clause.h</a>&quot;</span></div>
<div class="line"><a name="l00038"></a><span class="lineno"> 38</span>&#160;<span class="preprocessor">#include &quot;<a class="code" href="drat__proof__handler_8h.html">ortools/sat/drat_proof_handler.h</a>&quot;</span></div>
<div class="line"><a name="l00039"></a><span class="lineno"> 39</span>&#160;<span class="preprocessor">#include &quot;<a class="code" href="sat_2model_8h.html">ortools/sat/model.h</a>&quot;</span></div>
<div class="line"><a name="l00040"></a><span class="lineno"> 40</span>&#160;<span class="preprocessor">#include &quot;<a class="code" href="pb__constraint_8h.html">ortools/sat/pb_constraint.h</a>&quot;</span></div>
<div class="line"><a name="l00041"></a><span class="lineno"> 41</span>&#160;<span class="preprocessor">#include &quot;<a class="code" href="restart_8h.html">ortools/sat/restart.h</a>&quot;</span></div>
<div class="line"><a name="l00042"></a><span class="lineno"> 42</span>&#160;<span class="preprocessor">#include &quot;<a class="code" href="sat__base_8h.html">ortools/sat/sat_base.h</a>&quot;</span></div>
<div class="line"><a name="l00043"></a><span class="lineno"> 43</span>&#160;<span class="preprocessor">#include &quot;<a class="code" href="sat__decision_8h.html">ortools/sat/sat_decision.h</a>&quot;</span></div>
<div class="line"><a name="l00044"></a><span class="lineno"> 44</span>&#160;<span class="preprocessor">#include &quot;<a class="code" href="sat__parameters_8pb_8h.html">ortools/sat/sat_parameters.pb.h</a>&quot;</span></div>
<div class="line"><a name="l00045"></a><span class="lineno"> 45</span>&#160;<span class="preprocessor">#include &quot;<a class="code" href="stats_8h.html">ortools/util/stats.h</a>&quot;</span></div>
<div class="line"><a name="l00046"></a><span class="lineno"> 46</span>&#160;<span class="preprocessor">#include &quot;<a class="code" href="time__limit_8h.html">ortools/util/time_limit.h</a>&quot;</span></div>
<div class="line"><a name="l00047"></a><span class="lineno"> 47</span>&#160; </div>
<div class="line"><a name="l00048"></a><span class="lineno"> 48</span>&#160;<span class="keyword">namespace </span><a class="code" href="namespaceoperations__research.html">operations_research</a> {</div>
<div class="line"><a name="l00049"></a><span class="lineno"> 49</span>&#160;<span class="keyword">namespace </span>sat {</div>
<div class="line"><a name="l00050"></a><span class="lineno"> 50</span>&#160; </div>
<div class="line"><a name="l00051"></a><span class="lineno"> 51</span>&#160;<span class="comment">// A constant used by the EnqueueDecision*() API.</span></div>
<div class="line"><a name="l00052"></a><span class="lineno"><a class="line" href="namespaceoperations__research_1_1sat.html#aed3a7826cb80e5dfe7cadb141fde73f2"> 52</a></span>&#160;<span class="keyword">const</span> <span class="keywordtype">int</span> <a class="code" href="namespaceoperations__research_1_1sat.html#aed3a7826cb80e5dfe7cadb141fde73f2">kUnsatTrailIndex</a> = -1;</div>
<div class="line"><a name="l00053"></a><span class="lineno"> 53</span>&#160; </div>
<div class="line"><a name="l00054"></a><span class="lineno"> 54</span>&#160;<span class="comment">// The main SAT solver.</span></div>
<div class="line"><a name="l00055"></a><span class="lineno"> 55</span>&#160;<span class="comment">// It currently implements the CDCL algorithm. See</span></div>
<div class="line"><a name="l00056"></a><span class="lineno"> 56</span>&#160;<span class="comment">// http://en.wikipedia.org/wiki/Conflict_Driven_Clause_Learning</span></div>
<div class="line"><a name="l00057"></a><span class="lineno"><a class="line" href="classoperations__research_1_1sat_1_1_sat_solver.html"> 57</a></span>&#160;<span class="keyword">class </span><a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html">SatSolver</a> {</div>
<div class="line"><a name="l00058"></a><span class="lineno"> 58</span>&#160; <span class="keyword">public</span>:</div>
<div class="line"><a name="l00059"></a><span class="lineno"> 59</span>&#160; <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#adc7569321b063bae82803229623c8f4f">SatSolver</a>();</div>
<div class="line"><a name="l00060"></a><span class="lineno"> 60</span>&#160; <span class="keyword">explicit</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#adc7569321b063bae82803229623c8f4f">SatSolver</a>(<a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>* <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a6ce6ed209f0abff6cdbf46e2de1c8a48">model</a>);</div>
<div class="line"><a name="l00061"></a><span class="lineno"> 61</span>&#160; <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a8c6812e05685c0b43d4dd8efaf68aa23">~SatSolver</a>();</div>
<div class="line"><a name="l00062"></a><span class="lineno"> 62</span>&#160; </div>
<div class="line"><a name="l00063"></a><span class="lineno"> 63</span>&#160; <span class="comment">// TODO(user): Remove. This is temporary for accessing the model deep within</span></div>
<div class="line"><a name="l00064"></a><span class="lineno"> 64</span>&#160; <span class="comment">// some old code that didn&#39;t use the Model object.</span></div>
<div class="line"><a name="l00065"></a><span class="lineno"><a class="line" href="classoperations__research_1_1sat_1_1_sat_solver.html#a6ce6ed209f0abff6cdbf46e2de1c8a48"> 65</a></span>&#160; <a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>* <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a6ce6ed209f0abff6cdbf46e2de1c8a48">model</a>() { <span class="keywordflow">return</span> model_; }</div>
<div class="line"><a name="l00066"></a><span class="lineno"> 66</span>&#160; </div>
<div class="line"><a name="l00067"></a><span class="lineno"> 67</span>&#160; <span class="comment">// Parameters management. Note that calling SetParameters() will reset the</span></div>
<div class="line"><a name="l00068"></a><span class="lineno"> 68</span>&#160; <span class="comment">// value of many heuristics. For instance:</span></div>
<div class="line"><a name="l00069"></a><span class="lineno"> 69</span>&#160; <span class="comment">// - The restart strategy will be reinitialized.</span></div>
<div class="line"><a name="l00070"></a><span class="lineno"> 70</span>&#160; <span class="comment">// - The random seed and random generator will be reset to the value given in</span></div>
<div class="line"><a name="l00071"></a><span class="lineno"> 71</span>&#160; <span class="comment">// parameters.</span></div>
<div class="line"><a name="l00072"></a><span class="lineno"> 72</span>&#160; <span class="comment">// - The global TimeLimit singleton will be reset and time will be</span></div>
<div class="line"><a name="l00073"></a><span class="lineno"> 73</span>&#160; <span class="comment">// counted from this call.</span></div>
<div class="line"><a name="l00074"></a><span class="lineno"> 74</span>&#160; <span class="keywordtype">void</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a9d584b84d7b882a6017b072b33475172">SetParameters</a>(<span class="keyword">const</span> SatParameters&amp; <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a1a5e26554d014197de9434d2c39e07e9">parameters</a>);</div>
<div class="line"><a name="l00075"></a><span class="lineno"> 75</span>&#160; <span class="keyword">const</span> SatParameters&amp; <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a1a5e26554d014197de9434d2c39e07e9">parameters</a>() <span class="keyword">const</span>;</div>
<div class="line"><a name="l00076"></a><span class="lineno"> 76</span>&#160; </div>
<div class="line"><a name="l00077"></a><span class="lineno"> 77</span>&#160; <span class="comment">// Increases the number of variables of the current problem.</span></div>
<div class="line"><a name="l00078"></a><span class="lineno"> 78</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00079"></a><span class="lineno"> 79</span>&#160; <span class="comment">// TODO(user): Rename to IncreaseNumVariablesTo() until we support removing</span></div>
<div class="line"><a name="l00080"></a><span class="lineno"> 80</span>&#160; <span class="comment">// variables...</span></div>
<div class="line"><a name="l00081"></a><span class="lineno"> 81</span>&#160; <span class="keywordtype">void</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a0b58ef3a397720b272662f8bc45585cb">SetNumVariables</a>(<span class="keywordtype">int</span> num_variables);</div>
<div class="line"><a name="l00082"></a><span class="lineno"><a class="line" href="classoperations__research_1_1sat_1_1_sat_solver.html#a9d3beb2afe4ae647674b054bf29290e2"> 82</a></span>&#160; <span class="keywordtype">int</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a9d3beb2afe4ae647674b054bf29290e2">NumVariables</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> num_variables_.value(); }</div>
<div class="line"><a name="l00083"></a><span class="lineno"><a class="line" href="classoperations__research_1_1sat_1_1_sat_solver.html#a43684a0a8ef85b1cea0076dba3fb271d"> 83</a></span>&#160; BooleanVariable <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a43684a0a8ef85b1cea0076dba3fb271d">NewBooleanVariable</a>() {</div>
<div class="line"><a name="l00084"></a><span class="lineno"> 84</span>&#160; <span class="keyword">const</span> <span class="keywordtype">int</span> num_vars = <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a9d3beb2afe4ae647674b054bf29290e2">NumVariables</a>();</div>
<div class="line"><a name="l00085"></a><span class="lineno"> 85</span>&#160; </div>
<div class="line"><a name="l00086"></a><span class="lineno"> 86</span>&#160; <span class="comment">// We need to be able to encode the variable as a literal.</span></div>
<div class="line"><a name="l00087"></a><span class="lineno"> 87</span>&#160; <a class="code" href="base_2logging_8h.html#a4bd2e815ca2f702a4b6aa744b1ff3b82">CHECK_LT</a>(2 * num_vars, <a class="code" href="alldiff__cst_8cc.html#a9d0c202d5fdd62f4fa2c613339ff168a">std::numeric_limits&lt;int32&gt;::max</a>());</div>
<div class="line"><a name="l00088"></a><span class="lineno"> 88</span>&#160; <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a0b58ef3a397720b272662f8bc45585cb">SetNumVariables</a>(num_vars + 1);</div>
<div class="line"><a name="l00089"></a><span class="lineno"> 89</span>&#160; <span class="keywordflow">return</span> BooleanVariable(num_vars);</div>
<div class="line"><a name="l00090"></a><span class="lineno"> 90</span>&#160; }</div>
<div class="line"><a name="l00091"></a><span class="lineno"> 91</span>&#160; </div>
<div class="line"><a name="l00092"></a><span class="lineno"> 92</span>&#160; <span class="comment">// Fixes a variable so that the given literal is true. This can be used to</span></div>
<div class="line"><a name="l00093"></a><span class="lineno"> 93</span>&#160; <span class="comment">// solve a subproblem where some variables are fixed. Note that it is more</span></div>
<div class="line"><a name="l00094"></a><span class="lineno"> 94</span>&#160; <span class="comment">// efficient to add such unit clause before all the others.</span></div>
<div class="line"><a name="l00095"></a><span class="lineno"> 95</span>&#160; <span class="comment">// Returns false if the problem is detected to be UNSAT.</span></div>
<div class="line"><a name="l00096"></a><span class="lineno"> 96</span>&#160; <span class="keywordtype">bool</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#afbbbc2f0845a82a5a5cfb3f00a61abe9">AddUnitClause</a>(<a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> true_literal);</div>
<div class="line"><a name="l00097"></a><span class="lineno"> 97</span>&#160; </div>
<div class="line"><a name="l00098"></a><span class="lineno"> 98</span>&#160; <span class="comment">// Same as AddProblemClause() below, but for small clauses.</span></div>
<div class="line"><a name="l00099"></a><span class="lineno"> 99</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00100"></a><span class="lineno"> 100</span>&#160; <span class="comment">// TODO(user): Remove this and AddUnitClause() when initializer lists can be</span></div>
<div class="line"><a name="l00101"></a><span class="lineno"> 101</span>&#160; <span class="comment">// used in the open-source code like in AddClause({a, b}).</span></div>
<div class="line"><a name="l00102"></a><span class="lineno"> 102</span>&#160; <span class="keywordtype">bool</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#aac912e9410b8989493f492fcbb2d9094">AddBinaryClause</a>(<a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> <a class="code" href="constraint__solver_2table_8cc.html#af730895c6c6ef6e03caaf6251192dfd2">a</a>, <a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> <a class="code" href="constraint__solver_2table_8cc.html#a344010e26426d6a13411648d988bc9b6">b</a>);</div>
<div class="line"><a name="l00103"></a><span class="lineno"> 103</span>&#160; <span class="keywordtype">bool</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a0e8b0117614d340615ab66abec430d78">AddTernaryClause</a>(<a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> <a class="code" href="constraint__solver_2table_8cc.html#af730895c6c6ef6e03caaf6251192dfd2">a</a>, <a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> <a class="code" href="constraint__solver_2table_8cc.html#a344010e26426d6a13411648d988bc9b6">b</a>, <a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> c);</div>
<div class="line"><a name="l00104"></a><span class="lineno"> 104</span>&#160; </div>
<div class="line"><a name="l00105"></a><span class="lineno"> 105</span>&#160; <span class="comment">// Adds a clause to the problem. Returns false if the problem is detected to</span></div>
<div class="line"><a name="l00106"></a><span class="lineno"> 106</span>&#160; <span class="comment">// be UNSAT.</span></div>
<div class="line"><a name="l00107"></a><span class="lineno"> 107</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00108"></a><span class="lineno"> 108</span>&#160; <span class="comment">// TODO(user): Rename this to AddClause().</span></div>
<div class="line"><a name="l00109"></a><span class="lineno"> 109</span>&#160; <span class="keywordtype">bool</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#af67fe279478772a6d1492a7f673bda5d">AddProblemClause</a>(absl::Span&lt;const Literal&gt; literals);</div>
<div class="line"><a name="l00110"></a><span class="lineno"> 110</span>&#160; </div>
<div class="line"><a name="l00111"></a><span class="lineno"> 111</span>&#160; <span class="comment">// Adds a pseudo-Boolean constraint to the problem. Returns false if the</span></div>
<div class="line"><a name="l00112"></a><span class="lineno"> 112</span>&#160; <span class="comment">// problem is detected to be UNSAT. If the constraint is always true, this</span></div>
<div class="line"><a name="l00113"></a><span class="lineno"> 113</span>&#160; <span class="comment">// detects it and does nothing.</span></div>
<div class="line"><a name="l00114"></a><span class="lineno"> 114</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00115"></a><span class="lineno"> 115</span>&#160; <span class="comment">// Note(user): There is an optimization if the same constraint is added</span></div>
<div class="line"><a name="l00116"></a><span class="lineno"> 116</span>&#160; <span class="comment">// consecutively (even if the bounds are different). This is particularly</span></div>
<div class="line"><a name="l00117"></a><span class="lineno"> 117</span>&#160; <span class="comment">// useful for an optimization problem when we want to constrain the objective</span></div>
<div class="line"><a name="l00118"></a><span class="lineno"> 118</span>&#160; <span class="comment">// of the problem more and more. Just re-adding such constraint is relatively</span></div>
<div class="line"><a name="l00119"></a><span class="lineno"> 119</span>&#160; <span class="comment">// efficient.</span></div>
<div class="line"><a name="l00120"></a><span class="lineno"> 120</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00121"></a><span class="lineno"> 121</span>&#160; <span class="comment">// OVERFLOW: The sum of the absolute value of all the coefficients</span></div>
<div class="line"><a name="l00122"></a><span class="lineno"> 122</span>&#160; <span class="comment">// in the constraint must not overflow. This is currently CHECKed().</span></div>
<div class="line"><a name="l00123"></a><span class="lineno"> 123</span>&#160; <span class="comment">// TODO(user): Instead of failing, implement an error handling code.</span></div>
<div class="line"><a name="l00124"></a><span class="lineno"> 124</span>&#160; <span class="keywordtype">bool</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a05c49a95f6af6f8d873c96cae6ab6653">AddLinearConstraint</a>(<span class="keywordtype">bool</span> use_lower_bound, Coefficient lower_bound,</div>
<div class="line"><a name="l00125"></a><span class="lineno"> 125</span>&#160; <span class="keywordtype">bool</span> use_upper_bound, Coefficient upper_bound,</div>
<div class="line"><a name="l00126"></a><span class="lineno"> 126</span>&#160; std::vector&lt;LiteralWithCoeff&gt;* cst);</div>
<div class="line"><a name="l00127"></a><span class="lineno"> 127</span>&#160; </div>
<div class="line"><a name="l00128"></a><span class="lineno"> 128</span>&#160; <span class="comment">// Returns true if the model is UNSAT. Note that currently the status is</span></div>
<div class="line"><a name="l00129"></a><span class="lineno"> 129</span>&#160; <span class="comment">// &quot;sticky&quot; and once this happen, nothing else can be done with the solver.</span></div>
<div class="line"><a name="l00130"></a><span class="lineno"> 130</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00131"></a><span class="lineno"> 131</span>&#160; <span class="comment">// Thanks to this function, a client can safely ignore the return value of any</span></div>
<div class="line"><a name="l00132"></a><span class="lineno"> 132</span>&#160; <span class="comment">// Add*() functions. If one of them return false, then IsModelUnsat() will</span></div>
<div class="line"><a name="l00133"></a><span class="lineno"> 133</span>&#160; <span class="comment">// return true.</span></div>
<div class="line"><a name="l00134"></a><span class="lineno"> 134</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00135"></a><span class="lineno"> 135</span>&#160; <span class="comment">// TODO(user): Rename to ModelIsUnsat().</span></div>
<div class="line"><a name="l00136"></a><span class="lineno"><a class="line" href="classoperations__research_1_1sat_1_1_sat_solver.html#ad2a33e1d9335cce63548abed6b5c8aab"> 136</a></span>&#160; <span class="keywordtype">bool</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#ad2a33e1d9335cce63548abed6b5c8aab">IsModelUnsat</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> model_is_unsat_; }</div>
<div class="line"><a name="l00137"></a><span class="lineno"> 137</span>&#160; </div>
<div class="line"><a name="l00138"></a><span class="lineno"> 138</span>&#160; <span class="comment">// Adds and registers the given propagator with the sat solver. Note that</span></div>
<div class="line"><a name="l00139"></a><span class="lineno"> 139</span>&#160; <span class="comment">// during propagation, they will be called in the order they were added.</span></div>
<div class="line"><a name="l00140"></a><span class="lineno"> 140</span>&#160; <span class="keywordtype">void</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a2d1cea64152ca53ac5df160b48059800">AddPropagator</a>(<a class="code" href="classoperations__research_1_1sat_1_1_sat_propagator.html">SatPropagator</a>* propagator);</div>
<div class="line"><a name="l00141"></a><span class="lineno"> 141</span>&#160; <span class="keywordtype">void</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a17c09186d8dd4922296e97185f685c97">AddLastPropagator</a>(<a class="code" href="classoperations__research_1_1sat_1_1_sat_propagator.html">SatPropagator</a>* propagator);</div>
<div class="line"><a name="l00142"></a><span class="lineno"><a class="line" href="classoperations__research_1_1sat_1_1_sat_solver.html#ad085476234b92559b93383f9e1264af6"> 142</a></span>&#160; <span class="keywordtype">void</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#ad085476234b92559b93383f9e1264af6">TakePropagatorOwnership</a>(std::unique_ptr&lt;SatPropagator&gt; propagator) {</div>
<div class="line"><a name="l00143"></a><span class="lineno"> 143</span>&#160; owned_propagators_.push_back(std::move(propagator));</div>
<div class="line"><a name="l00144"></a><span class="lineno"> 144</span>&#160; }</div>
<div class="line"><a name="l00145"></a><span class="lineno"> 145</span>&#160; </div>
<div class="line"><a name="l00146"></a><span class="lineno"> 146</span>&#160; <span class="comment">// Wrapper around the same functions in SatDecisionPolicy.</span></div>
<div class="line"><a name="l00147"></a><span class="lineno"> 147</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00148"></a><span class="lineno"> 148</span>&#160; <span class="comment">// TODO(user): Clean this up by making clients directly talk to</span></div>
<div class="line"><a name="l00149"></a><span class="lineno"> 149</span>&#160; <span class="comment">// SatDecisionPolicy.</span></div>
<div class="line"><a name="l00150"></a><span class="lineno"><a class="line" href="classoperations__research_1_1sat_1_1_sat_solver.html#a955786dcbe82b7c4dc9924a5473ac1e8"> 150</a></span>&#160; <span class="keywordtype">void</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a955786dcbe82b7c4dc9924a5473ac1e8">SetAssignmentPreference</a>(<a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> <a class="code" href="optimization_8cc.html#af63dcc00f2023fdf498e0829e6fb8a6b">literal</a>, <span class="keywordtype">double</span> <a class="code" href="pack_8cc.html#ae42ca38a167164c07831993889216903">weight</a>) {</div>
<div class="line"><a name="l00151"></a><span class="lineno"> 151</span>&#160; decision_policy_-&gt;<a class="code" href="classoperations__research_1_1sat_1_1_sat_decision_policy.html#a955786dcbe82b7c4dc9924a5473ac1e8">SetAssignmentPreference</a>(<a class="code" href="optimization_8cc.html#af63dcc00f2023fdf498e0829e6fb8a6b">literal</a>, <a class="code" href="pack_8cc.html#ae42ca38a167164c07831993889216903">weight</a>);</div>
<div class="line"><a name="l00152"></a><span class="lineno"> 152</span>&#160; }</div>
<div class="line"><a name="l00153"></a><span class="lineno"><a class="line" href="classoperations__research_1_1sat_1_1_sat_solver.html#a05725f6398ef1b0d50c87c4d9e719260"> 153</a></span>&#160; std::vector&lt;std::pair&lt;Literal, double&gt;&gt; <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a05725f6398ef1b0d50c87c4d9e719260">AllPreferences</a>()<span class="keyword"> const </span>{</div>
<div class="line"><a name="l00154"></a><span class="lineno"> 154</span>&#160; <span class="keywordflow">return</span> decision_policy_-&gt;<a class="code" href="classoperations__research_1_1sat_1_1_sat_decision_policy.html#a0b5d7f31620ad7b364e7415c47ee5e0d">AllPreferences</a>();</div>
<div class="line"><a name="l00155"></a><span class="lineno"> 155</span>&#160; }</div>
<div class="line"><a name="l00156"></a><span class="lineno"><a class="line" href="classoperations__research_1_1sat_1_1_sat_solver.html#a1dc177ee88f0a7ce2e46a032e5c3cf02"> 156</a></span>&#160; <span class="keywordtype">void</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a1dc177ee88f0a7ce2e46a032e5c3cf02">ResetDecisionHeuristic</a>() {</div>
<div class="line"><a name="l00157"></a><span class="lineno"> 157</span>&#160; <span class="keywordflow">return</span> decision_policy_-&gt;<a class="code" href="classoperations__research_1_1sat_1_1_sat_decision_policy.html#a1dc177ee88f0a7ce2e46a032e5c3cf02">ResetDecisionHeuristic</a>();</div>
<div class="line"><a name="l00158"></a><span class="lineno"> 158</span>&#160; }</div>
<div class="line"><a name="l00159"></a><span class="lineno"><a class="line" href="classoperations__research_1_1sat_1_1_sat_solver.html#a1cf106c907fb0a4114a08a76ae2e874f"> 159</a></span>&#160; <span class="keywordtype">void</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a1cf106c907fb0a4114a08a76ae2e874f">ResetDecisionHeuristicAndSetAllPreferences</a>(</div>
<div class="line"><a name="l00160"></a><span class="lineno"> 160</span>&#160; <span class="keyword">const</span> std::vector&lt;std::pair&lt;Literal, double&gt;&gt;&amp; prefs) {</div>
<div class="line"><a name="l00161"></a><span class="lineno"> 161</span>&#160; decision_policy_-&gt;<a class="code" href="classoperations__research_1_1sat_1_1_sat_decision_policy.html#a1dc177ee88f0a7ce2e46a032e5c3cf02">ResetDecisionHeuristic</a>();</div>
<div class="line"><a name="l00162"></a><span class="lineno"> 162</span>&#160; <span class="keywordflow">for</span> (<span class="keyword">const</span> std::pair&lt;Literal, double&gt; p : prefs) {</div>
<div class="line"><a name="l00163"></a><span class="lineno"> 163</span>&#160; decision_policy_-&gt;<a class="code" href="classoperations__research_1_1sat_1_1_sat_decision_policy.html#a955786dcbe82b7c4dc9924a5473ac1e8">SetAssignmentPreference</a>(p.first, p.second);</div>
<div class="line"><a name="l00164"></a><span class="lineno"> 164</span>&#160; }</div>
<div class="line"><a name="l00165"></a><span class="lineno"> 165</span>&#160; }</div>
<div class="line"><a name="l00166"></a><span class="lineno"> 166</span>&#160; </div>
<div class="line"><a name="l00167"></a><span class="lineno"> 167</span>&#160; <span class="comment">// Solves the problem and returns its status.</span></div>
<div class="line"><a name="l00168"></a><span class="lineno"> 168</span>&#160; <span class="comment">// An empty problem is considered to be SAT.</span></div>
<div class="line"><a name="l00169"></a><span class="lineno"> 169</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00170"></a><span class="lineno"> 170</span>&#160; <span class="comment">// Note that the conflict limit applies only to this function and starts</span></div>
<div class="line"><a name="l00171"></a><span class="lineno"> 171</span>&#160; <span class="comment">// counting from the time it is called.</span></div>
<div class="line"><a name="l00172"></a><span class="lineno"> 172</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00173"></a><span class="lineno"> 173</span>&#160; <span class="comment">// This will restart from the current solver configuration. If a previous call</span></div>
<div class="line"><a name="l00174"></a><span class="lineno"> 174</span>&#160; <span class="comment">// to Solve() was interrupted by a conflict or time limit, calling this again</span></div>
<div class="line"><a name="l00175"></a><span class="lineno"> 175</span>&#160; <span class="comment">// will resume the search exactly as it would have continued.</span></div>
<div class="line"><a name="l00176"></a><span class="lineno"> 176</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00177"></a><span class="lineno"> 177</span>&#160; <span class="comment">// Note that this will use the TimeLimit singleton, so the time limit</span></div>
<div class="line"><a name="l00178"></a><span class="lineno"> 178</span>&#160; <span class="comment">// will be counted since the last time TimeLimit was reset, not from</span></div>
<div class="line"><a name="l00179"></a><span class="lineno"> 179</span>&#160; <span class="comment">// the start of this function.</span></div>
<div class="line"><a name="l00180"></a><span class="lineno"><a class="line" href="classoperations__research_1_1sat_1_1_sat_solver.html#a67a0db04d321a74b7e7fcfd3f1a3f70b"> 180</a></span>&#160; <span class="keyword">enum</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a67a0db04d321a74b7e7fcfd3f1a3f70b">Status</a> {</div>
<div class="line"><a name="l00181"></a><span class="lineno"><a class="line" href="classoperations__research_1_1sat_1_1_sat_solver.html#a67a0db04d321a74b7e7fcfd3f1a3f70bae5ba802809eb747ea486ca3fae32a885"> 181</a></span>&#160; <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a67a0db04d321a74b7e7fcfd3f1a3f70bae5ba802809eb747ea486ca3fae32a885">ASSUMPTIONS_UNSAT</a>,</div>
<div class="line"><a name="l00182"></a><span class="lineno"><a class="line" href="classoperations__research_1_1sat_1_1_sat_solver.html#a67a0db04d321a74b7e7fcfd3f1a3f70ba2884fa43446c0cbc9c7a9b74d41d7483"> 182</a></span>&#160; <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a67a0db04d321a74b7e7fcfd3f1a3f70ba2884fa43446c0cbc9c7a9b74d41d7483">INFEASIBLE</a>,</div>
<div class="line"><a name="l00183"></a><span class="lineno"><a class="line" href="classoperations__research_1_1sat_1_1_sat_solver.html#a67a0db04d321a74b7e7fcfd3f1a3f70ba03f919221217f95d21a593a7120165e1"> 183</a></span>&#160; <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a67a0db04d321a74b7e7fcfd3f1a3f70ba03f919221217f95d21a593a7120165e1">FEASIBLE</a>,</div>
<div class="line"><a name="l00184"></a><span class="lineno"><a class="line" href="classoperations__research_1_1sat_1_1_sat_solver.html#a67a0db04d321a74b7e7fcfd3f1a3f70ba72c2402449caa8f3edc8aa0a3816baed"> 184</a></span>&#160; <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a67a0db04d321a74b7e7fcfd3f1a3f70ba72c2402449caa8f3edc8aa0a3816baed">LIMIT_REACHED</a>,</div>
<div class="line"><a name="l00185"></a><span class="lineno"> 185</span>&#160; };</div>
<div class="line"><a name="l00186"></a><span class="lineno"> 186</span>&#160; <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a67a0db04d321a74b7e7fcfd3f1a3f70b">Status</a> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a2b006481369eb4f4cb7f3037dfdd8404">Solve</a>();</div>
<div class="line"><a name="l00187"></a><span class="lineno"> 187</span>&#160; </div>
<div class="line"><a name="l00188"></a><span class="lineno"> 188</span>&#160; <span class="comment">// Same as Solve(), but with a given time limit. Note that this will not</span></div>
<div class="line"><a name="l00189"></a><span class="lineno"> 189</span>&#160; <span class="comment">// update the TimeLimit singleton, but only the passed object instead.</span></div>
<div class="line"><a name="l00190"></a><span class="lineno"> 190</span>&#160; <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a67a0db04d321a74b7e7fcfd3f1a3f70b">Status</a> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a27e14216f4d9330375fc0089a1919f20">SolveWithTimeLimit</a>(<a class="code" href="classoperations__research_1_1_time_limit.html">TimeLimit</a>* <a class="code" href="cp__model__solver_8cc.html#ac3cf9db02b23ea1455b5ae6955d03e47">time_limit</a>);</div>
<div class="line"><a name="l00191"></a><span class="lineno"> 191</span>&#160; </div>
<div class="line"><a name="l00192"></a><span class="lineno"> 192</span>&#160; <span class="comment">// Simple interface to solve a problem under the given assumptions. This</span></div>
<div class="line"><a name="l00193"></a><span class="lineno"> 193</span>&#160; <span class="comment">// simply ask the solver to solve a problem given a set of variables fixed to</span></div>
<div class="line"><a name="l00194"></a><span class="lineno"> 194</span>&#160; <span class="comment">// a given value (the assumptions). Compared to simply calling AddUnitClause()</span></div>
<div class="line"><a name="l00195"></a><span class="lineno"> 195</span>&#160; <span class="comment">// and fixing the variables once and for all, this allow to backtrack over the</span></div>
<div class="line"><a name="l00196"></a><span class="lineno"> 196</span>&#160; <span class="comment">// assumptions and thus exploit the incrementally between subsequent solves.</span></div>
<div class="line"><a name="l00197"></a><span class="lineno"> 197</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00198"></a><span class="lineno"> 198</span>&#160; <span class="comment">// This function backtrack over all the current decision, tries to enqueue the</span></div>
<div class="line"><a name="l00199"></a><span class="lineno"> 199</span>&#160; <span class="comment">// given assumptions, sets the assumption level accordingly and finally calls</span></div>
<div class="line"><a name="l00200"></a><span class="lineno"> 200</span>&#160; <span class="comment">// Solve().</span></div>
<div class="line"><a name="l00201"></a><span class="lineno"> 201</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00202"></a><span class="lineno"> 202</span>&#160; <span class="comment">// If, given these assumptions, the model is UNSAT, this returns the</span></div>
<div class="line"><a name="l00203"></a><span class="lineno"> 203</span>&#160; <span class="comment">// ASSUMPTIONS_UNSAT status. INFEASIBLE is reserved for the case where the</span></div>
<div class="line"><a name="l00204"></a><span class="lineno"> 204</span>&#160; <span class="comment">// model is proven to be unsat without any assumptions.</span></div>
<div class="line"><a name="l00205"></a><span class="lineno"> 205</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00206"></a><span class="lineno"> 206</span>&#160; <span class="comment">// If ASSUMPTIONS_UNSAT is returned, it is possible to get a &quot;core&quot; of unsat</span></div>
<div class="line"><a name="l00207"></a><span class="lineno"> 207</span>&#160; <span class="comment">// assumptions by calling GetLastIncompatibleDecisions().</span></div>
<div class="line"><a name="l00208"></a><span class="lineno"> 208</span>&#160; <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a67a0db04d321a74b7e7fcfd3f1a3f70b">Status</a> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a2abca6db0c780a4482d1ac9eb6365057">ResetAndSolveWithGivenAssumptions</a>(</div>
<div class="line"><a name="l00209"></a><span class="lineno"> 209</span>&#160; <span class="keyword">const</span> std::vector&lt;Literal&gt;&amp; assumptions);</div>
<div class="line"><a name="l00210"></a><span class="lineno"> 210</span>&#160; </div>
<div class="line"><a name="l00211"></a><span class="lineno"> 211</span>&#160; <span class="comment">// Changes the assumption level. All the decisions below this level will be</span></div>
<div class="line"><a name="l00212"></a><span class="lineno"> 212</span>&#160; <span class="comment">// treated as assumptions by the next Solve(). Note that this may impact some</span></div>
<div class="line"><a name="l00213"></a><span class="lineno"> 213</span>&#160; <span class="comment">// heuristics, like the LBD value of a clause.</span></div>
<div class="line"><a name="l00214"></a><span class="lineno"> 214</span>&#160; <span class="keywordtype">void</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a5ca47674a4a0b5e7f40eb430ab474440">SetAssumptionLevel</a>(<span class="keywordtype">int</span> assumption_level);</div>
<div class="line"><a name="l00215"></a><span class="lineno"> 215</span>&#160; </div>
<div class="line"><a name="l00216"></a><span class="lineno"> 216</span>&#160; <span class="comment">// Returns the current assumption level. Note that if a solve was done since</span></div>
<div class="line"><a name="l00217"></a><span class="lineno"> 217</span>&#160; <span class="comment">// the last SetAssumptionLevel(), then the returned level may be lower than</span></div>
<div class="line"><a name="l00218"></a><span class="lineno"> 218</span>&#160; <span class="comment">// the one that was set. This is because some assumptions may now be</span></div>
<div class="line"><a name="l00219"></a><span class="lineno"> 219</span>&#160; <span class="comment">// consequences of others before them due to the newly learned clauses.</span></div>
<div class="line"><a name="l00220"></a><span class="lineno"><a class="line" href="classoperations__research_1_1sat_1_1_sat_solver.html#a88dcaf0cf27bb4991376ed54d8f2698f"> 220</a></span>&#160; <span class="keywordtype">int</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a88dcaf0cf27bb4991376ed54d8f2698f">AssumptionLevel</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> assumption_level_; }</div>
<div class="line"><a name="l00221"></a><span class="lineno"> 221</span>&#160; </div>
<div class="line"><a name="l00222"></a><span class="lineno"> 222</span>&#160; <span class="comment">// This can be called just after SolveWithAssumptions() returned</span></div>
<div class="line"><a name="l00223"></a><span class="lineno"> 223</span>&#160; <span class="comment">// ASSUMPTION_UNSAT or after EnqueueDecisionAndBacktrackOnConflict() leaded</span></div>
<div class="line"><a name="l00224"></a><span class="lineno"> 224</span>&#160; <span class="comment">// to a conflict. It returns a subsequence (in the correct order) of the</span></div>
<div class="line"><a name="l00225"></a><span class="lineno"> 225</span>&#160; <span class="comment">// previously enqueued decisions that cannot be taken together without making</span></div>
<div class="line"><a name="l00226"></a><span class="lineno"> 226</span>&#160; <span class="comment">// the problem UNSAT.</span></div>
<div class="line"><a name="l00227"></a><span class="lineno"> 227</span>&#160; std::vector&lt;Literal&gt; <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#acfbfa9df611cb625ff79785c05784580">GetLastIncompatibleDecisions</a>();</div>
<div class="line"><a name="l00228"></a><span class="lineno"> 228</span>&#160; </div>
<div class="line"><a name="l00229"></a><span class="lineno"> 229</span>&#160; <span class="comment">// Advanced usage. The next 3 functions allow to drive the search from outside</span></div>
<div class="line"><a name="l00230"></a><span class="lineno"> 230</span>&#160; <span class="comment">// the solver.</span></div>
<div class="line"><a name="l00231"></a><span class="lineno"> 231</span>&#160; </div>
<div class="line"><a name="l00232"></a><span class="lineno"> 232</span>&#160; <span class="comment">// Takes a new decision (the given true_literal must be unassigned) and</span></div>
<div class="line"><a name="l00233"></a><span class="lineno"> 233</span>&#160; <span class="comment">// propagates it. Returns the trail index of the first newly propagated</span></div>
<div class="line"><a name="l00234"></a><span class="lineno"> 234</span>&#160; <span class="comment">// literal. If there is a conflict and the problem is detected to be UNSAT,</span></div>
<div class="line"><a name="l00235"></a><span class="lineno"> 235</span>&#160; <span class="comment">// returns kUnsatTrailIndex.</span></div>
<div class="line"><a name="l00236"></a><span class="lineno"> 236</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00237"></a><span class="lineno"> 237</span>&#160; <span class="comment">// A client can determine if there is a conflict by checking if the</span></div>
<div class="line"><a name="l00238"></a><span class="lineno"> 238</span>&#160; <span class="comment">// CurrentDecisionLevel() was increased by 1 or not.</span></div>
<div class="line"><a name="l00239"></a><span class="lineno"> 239</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00240"></a><span class="lineno"> 240</span>&#160; <span class="comment">// If there is a conflict, the given decision is not applied and:</span></div>
<div class="line"><a name="l00241"></a><span class="lineno"> 241</span>&#160; <span class="comment">// - The conflict is learned.</span></div>
<div class="line"><a name="l00242"></a><span class="lineno"> 242</span>&#160; <span class="comment">// - The decisions are potentially backtracked to the first decision that</span></div>
<div class="line"><a name="l00243"></a><span class="lineno"> 243</span>&#160; <span class="comment">// propagates more variables because of the newly learned conflict.</span></div>
<div class="line"><a name="l00244"></a><span class="lineno"> 244</span>&#160; <span class="comment">// - The returned value is equal to trail_-&gt;Index() after this backtracking</span></div>
<div class="line"><a name="l00245"></a><span class="lineno"> 245</span>&#160; <span class="comment">// and just before the new propagation (due to the conflict) which is also</span></div>
<div class="line"><a name="l00246"></a><span class="lineno"> 246</span>&#160; <span class="comment">// performed by this function.</span></div>
<div class="line"><a name="l00247"></a><span class="lineno"> 247</span>&#160; <span class="keywordtype">int</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a9ae69b015a43c1a94e8815ab0dd8189c">EnqueueDecisionAndBackjumpOnConflict</a>(<a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> true_literal);</div>
<div class="line"><a name="l00248"></a><span class="lineno"> 248</span>&#160; </div>
<div class="line"><a name="l00249"></a><span class="lineno"> 249</span>&#160; <span class="comment">// This function starts by calling EnqueueDecisionAndBackjumpOnConflict(). If</span></div>
<div class="line"><a name="l00250"></a><span class="lineno"> 250</span>&#160; <span class="comment">// there is no conflict, it stops there. Otherwise, it tries to reapply all</span></div>
<div class="line"><a name="l00251"></a><span class="lineno"> 251</span>&#160; <span class="comment">// the decisions that were backjumped over until the first one that can&#39;t be</span></div>
<div class="line"><a name="l00252"></a><span class="lineno"> 252</span>&#160; <span class="comment">// taken because it is incompatible. Note that during this process, more</span></div>
<div class="line"><a name="l00253"></a><span class="lineno"> 253</span>&#160; <span class="comment">// conflicts may happen and the trail may be backtracked even further.</span></div>
<div class="line"><a name="l00254"></a><span class="lineno"> 254</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00255"></a><span class="lineno"> 255</span>&#160; <span class="comment">// In any case, the new decisions stack will be the largest valid &quot;prefix&quot;</span></div>
<div class="line"><a name="l00256"></a><span class="lineno"> 256</span>&#160; <span class="comment">// of the old stack. Note that decisions that are now consequence of the ones</span></div>
<div class="line"><a name="l00257"></a><span class="lineno"> 257</span>&#160; <span class="comment">// before them will no longer be decisions.</span></div>
<div class="line"><a name="l00258"></a><span class="lineno"> 258</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00259"></a><span class="lineno"> 259</span>&#160; <span class="comment">// Note(user): This function can be called with an already assigned literal.</span></div>
<div class="line"><a name="l00260"></a><span class="lineno"> 260</span>&#160; <span class="keywordtype">int</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#ab63a08713131e63e9cc4109f98ecf859">EnqueueDecisionAndBacktrackOnConflict</a>(<a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> true_literal);</div>
<div class="line"><a name="l00261"></a><span class="lineno"> 261</span>&#160; </div>
<div class="line"><a name="l00262"></a><span class="lineno"> 262</span>&#160; <span class="comment">// Tries to enqueue the given decision and performs the propagation.</span></div>
<div class="line"><a name="l00263"></a><span class="lineno"> 263</span>&#160; <span class="comment">// Returns true if no conflict occurred. Otherwise, returns false and restores</span></div>
<div class="line"><a name="l00264"></a><span class="lineno"> 264</span>&#160; <span class="comment">// the solver to the state just before this was called.</span></div>
<div class="line"><a name="l00265"></a><span class="lineno"> 265</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00266"></a><span class="lineno"> 266</span>&#160; <span class="comment">// Note(user): With this function, the solver doesn&#39;t learn anything.</span></div>
<div class="line"><a name="l00267"></a><span class="lineno"> 267</span>&#160; <span class="keywordtype">bool</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a093c00c2bd81c8ec7a5f86a4466fa7d5">EnqueueDecisionIfNotConflicting</a>(<a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> true_literal);</div>
<div class="line"><a name="l00268"></a><span class="lineno"> 268</span>&#160; </div>
<div class="line"><a name="l00269"></a><span class="lineno"> 269</span>&#160; <span class="comment">// Restores the state to the given target decision level. The decision at that</span></div>
<div class="line"><a name="l00270"></a><span class="lineno"> 270</span>&#160; <span class="comment">// level and all its propagation will not be undone. But all the trail after</span></div>
<div class="line"><a name="l00271"></a><span class="lineno"> 271</span>&#160; <span class="comment">// this will be cleared. Calling this with 0 will revert all the decisions and</span></div>
<div class="line"><a name="l00272"></a><span class="lineno"> 272</span>&#160; <span class="comment">// only the fixed variables will be left on the trail.</span></div>
<div class="line"><a name="l00273"></a><span class="lineno"> 273</span>&#160; <span class="keywordtype">void</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#ac035378cea0ed7b0978105547402faa8">Backtrack</a>(<span class="keywordtype">int</span> target_level);</div>
<div class="line"><a name="l00274"></a><span class="lineno"> 274</span>&#160; </div>
<div class="line"><a name="l00275"></a><span class="lineno"> 275</span>&#160; <span class="comment">// Advanced usage. This is meant to restore the solver to a &quot;proper&quot; state</span></div>
<div class="line"><a name="l00276"></a><span class="lineno"> 276</span>&#160; <span class="comment">// after a solve was interupted due to a limit reached.</span></div>
<div class="line"><a name="l00277"></a><span class="lineno"> 277</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00278"></a><span class="lineno"> 278</span>&#160; <span class="comment">// Without assumption (i.e. if AssumptionLevel() is 0), this will revert all</span></div>
<div class="line"><a name="l00279"></a><span class="lineno"> 279</span>&#160; <span class="comment">// decisions and make sure that all the fixed literals are propagated. In</span></div>
<div class="line"><a name="l00280"></a><span class="lineno"> 280</span>&#160; <span class="comment">// presence of assumptions, this will either backtrack to the assumption level</span></div>
<div class="line"><a name="l00281"></a><span class="lineno"> 281</span>&#160; <span class="comment">// or re-enqueue any assumptions that may have been backtracked over due to</span></div>
<div class="line"><a name="l00282"></a><span class="lineno"> 282</span>&#160; <span class="comment">// conflits resolution. In both cases, the propagation is finished.</span></div>
<div class="line"><a name="l00283"></a><span class="lineno"> 283</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00284"></a><span class="lineno"> 284</span>&#160; <span class="comment">// Note that this may prove the model to be UNSAT or ASSUMPTION_UNSAT in which</span></div>
<div class="line"><a name="l00285"></a><span class="lineno"> 285</span>&#160; <span class="comment">// case it will return false.</span></div>
<div class="line"><a name="l00286"></a><span class="lineno"> 286</span>&#160; <span class="keywordtype">bool</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#ac714aeb75f0f6dd87e52e5d1a0d6edc7">RestoreSolverToAssumptionLevel</a>();</div>
<div class="line"><a name="l00287"></a><span class="lineno"> 287</span>&#160; </div>
<div class="line"><a name="l00288"></a><span class="lineno"> 288</span>&#160; <span class="comment">// Advanced usage. Finish the progation if it was interupted. Note that this</span></div>
<div class="line"><a name="l00289"></a><span class="lineno"> 289</span>&#160; <span class="comment">// might run into conflict and will propagate again until a fixed point is</span></div>
<div class="line"><a name="l00290"></a><span class="lineno"> 290</span>&#160; <span class="comment">// reached or the model was proven UNSAT. Returns IsModelUnsat().</span></div>
<div class="line"><a name="l00291"></a><span class="lineno"> 291</span>&#160; <span class="keywordtype">bool</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a607d97ccada862073f297bc2d495124d">FinishPropagation</a>();</div>
<div class="line"><a name="l00292"></a><span class="lineno"> 292</span>&#160; </div>
<div class="line"><a name="l00293"></a><span class="lineno"> 293</span>&#160; <span class="comment">// Like Backtrack(0) but make sure the propagation is finished and return</span></div>
<div class="line"><a name="l00294"></a><span class="lineno"> 294</span>&#160; <span class="comment">// false if unsat was detected. This also removes any assumptions level.</span></div>
<div class="line"><a name="l00295"></a><span class="lineno"> 295</span>&#160; <span class="keywordtype">bool</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a9da38c8d2910442d551db5e360423029">ResetToLevelZero</a>();</div>
<div class="line"><a name="l00296"></a><span class="lineno"> 296</span>&#160; </div>
<div class="line"><a name="l00297"></a><span class="lineno"> 297</span>&#160; <span class="comment">// Changes the assumptions level and the current solver assumptions. Returns</span></div>
<div class="line"><a name="l00298"></a><span class="lineno"> 298</span>&#160; <span class="comment">// false if the model is UNSAT or ASSUMPTION_UNSAT, true otherwise.</span></div>
<div class="line"><a name="l00299"></a><span class="lineno"> 299</span>&#160; <span class="keywordtype">bool</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#ad4494c6831942d344ed1d9758f0e6cd9">ResetWithGivenAssumptions</a>(<span class="keyword">const</span> std::vector&lt;Literal&gt;&amp; assumptions);</div>
<div class="line"><a name="l00300"></a><span class="lineno"> 300</span>&#160; </div>
<div class="line"><a name="l00301"></a><span class="lineno"> 301</span>&#160; <span class="comment">// Advanced usage. If the decision level is smaller than the assumption level,</span></div>
<div class="line"><a name="l00302"></a><span class="lineno"> 302</span>&#160; <span class="comment">// this will try to reapply all assumptions. Returns true if this was doable,</span></div>
<div class="line"><a name="l00303"></a><span class="lineno"> 303</span>&#160; <span class="comment">// otherwise returns false in which case the model is either UNSAT or</span></div>
<div class="line"><a name="l00304"></a><span class="lineno"> 304</span>&#160; <span class="comment">// ASSUMPTION_UNSAT.</span></div>
<div class="line"><a name="l00305"></a><span class="lineno"> 305</span>&#160; <span class="keywordtype">bool</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#ad28cbdd5735a0c111a642f39524d969e">ReapplyAssumptionsIfNeeded</a>();</div>
<div class="line"><a name="l00306"></a><span class="lineno"> 306</span>&#160; </div>
<div class="line"><a name="l00307"></a><span class="lineno"> 307</span>&#160; <span class="comment">// Helper functions to get the correct status when one of the functions above</span></div>
<div class="line"><a name="l00308"></a><span class="lineno"> 308</span>&#160; <span class="comment">// returns false.</span></div>
<div class="line"><a name="l00309"></a><span class="lineno"><a class="line" href="classoperations__research_1_1sat_1_1_sat_solver.html#a5bbe13ebae8aa11a8a4ac1cb01bc66ad"> 309</a></span>&#160; <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a67a0db04d321a74b7e7fcfd3f1a3f70b">Status</a> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a5bbe13ebae8aa11a8a4ac1cb01bc66ad">UnsatStatus</a>()<span class="keyword"> const </span>{</div>
<div class="line"><a name="l00310"></a><span class="lineno"> 310</span>&#160; <span class="keywordflow">return</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#ad2a33e1d9335cce63548abed6b5c8aab">IsModelUnsat</a>() ? <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a67a0db04d321a74b7e7fcfd3f1a3f70ba2884fa43446c0cbc9c7a9b74d41d7483">INFEASIBLE</a> : <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a67a0db04d321a74b7e7fcfd3f1a3f70bae5ba802809eb747ea486ca3fae32a885">ASSUMPTIONS_UNSAT</a>;</div>
<div class="line"><a name="l00311"></a><span class="lineno"> 311</span>&#160; }</div>
<div class="line"><a name="l00312"></a><span class="lineno"> 312</span>&#160; </div>
<div class="line"><a name="l00313"></a><span class="lineno"> 313</span>&#160; <span class="comment">// Extract the current problem clauses. The Output type must support the two</span></div>
<div class="line"><a name="l00314"></a><span class="lineno"> 314</span>&#160; <span class="comment">// functions:</span></div>
<div class="line"><a name="l00315"></a><span class="lineno"> 315</span>&#160; <span class="comment">// - void AddBinaryClause(Literal a, Literal b);</span></div>
<div class="line"><a name="l00316"></a><span class="lineno"> 316</span>&#160; <span class="comment">// - void AddClause(absl::Span&lt;const Literal&gt; clause);</span></div>
<div class="line"><a name="l00317"></a><span class="lineno"> 317</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00318"></a><span class="lineno"> 318</span>&#160; <span class="comment">// TODO(user): also copy the removable clauses?</span></div>
<div class="line"><a name="l00319"></a><span class="lineno"> 319</span>&#160; <span class="keyword">template</span> &lt;<span class="keyword">typename</span> Output&gt;</div>
<div class="line"><a name="l00320"></a><span class="lineno"><a class="line" href="classoperations__research_1_1sat_1_1_sat_solver.html#ab5bc2f86603d9fdb9a51305ab431530d"> 320</a></span>&#160; <span class="keywordtype">void</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#ab5bc2f86603d9fdb9a51305ab431530d">ExtractClauses</a>(Output* out) {</div>
<div class="line"><a name="l00321"></a><span class="lineno"> 321</span>&#160; <a class="code" href="base_2logging_8h.html#a3e1cfef60e774a81f30eaddf26a3a274">CHECK</a>(!<a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#ad2a33e1d9335cce63548abed6b5c8aab">IsModelUnsat</a>());</div>
<div class="line"><a name="l00322"></a><span class="lineno"> 322</span>&#160; <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#ac035378cea0ed7b0978105547402faa8">Backtrack</a>(0);</div>
<div class="line"><a name="l00323"></a><span class="lineno"> 323</span>&#160; <span class="keywordflow">if</span> (!<a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a607d97ccada862073f297bc2d495124d">FinishPropagation</a>()) <span class="keywordflow">return</span>;</div>
<div class="line"><a name="l00324"></a><span class="lineno"> 324</span>&#160; </div>
<div class="line"><a name="l00325"></a><span class="lineno"> 325</span>&#160; <span class="comment">// It is important to process the newly fixed variables, so they are not</span></div>
<div class="line"><a name="l00326"></a><span class="lineno"> 326</span>&#160; <span class="comment">// present in the clauses we export.</span></div>
<div class="line"><a name="l00327"></a><span class="lineno"> 327</span>&#160; <span class="keywordflow">if</span> (num_processed_fixed_variables_ &lt; trail_-&gt;<a class="code" href="namespaceoperations__research_1_1glop.html#abec9e934a51aa2ab519684cc0f446a41">Index</a>()) {</div>
<div class="line"><a name="l00328"></a><span class="lineno"> 328</span>&#160; <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a2aafb0d6bd7d95f183e87866d0ade374">ProcessNewlyFixedVariables</a>();</div>
<div class="line"><a name="l00329"></a><span class="lineno"> 329</span>&#160; }</div>
<div class="line"><a name="l00330"></a><span class="lineno"> 330</span>&#160; clauses_propagator_-&gt;<a class="code" href="classoperations__research_1_1sat_1_1_literal_watchers.html#ae234022ee7c496416290d1946f56e1ad">DeleteRemovedClauses</a>();</div>
<div class="line"><a name="l00331"></a><span class="lineno"> 331</span>&#160; </div>
<div class="line"><a name="l00332"></a><span class="lineno"> 332</span>&#160; <span class="comment">// Note(user): Putting the binary clauses first help because the presolver</span></div>
<div class="line"><a name="l00333"></a><span class="lineno"> 333</span>&#160; <span class="comment">// currently process the clauses in order.</span></div>
<div class="line"><a name="l00334"></a><span class="lineno"> 334</span>&#160; out-&gt;SetNumVariables(<a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a9d3beb2afe4ae647674b054bf29290e2">NumVariables</a>());</div>
<div class="line"><a name="l00335"></a><span class="lineno"> 335</span>&#160; binary_implication_graph_-&gt;<a class="code" href="classoperations__research_1_1sat_1_1_binary_implication_graph.html#a558f9dd435d1f46d7408d60d0e9969f1">ExtractAllBinaryClauses</a>(out);</div>
<div class="line"><a name="l00336"></a><span class="lineno"> 336</span>&#160; <span class="keywordflow">for</span> (<a class="code" href="classoperations__research_1_1sat_1_1_sat_clause.html">SatClause</a>* clause : clauses_propagator_-&gt;<a class="code" href="classoperations__research_1_1sat_1_1_literal_watchers.html#a0569d77056e622964bd02dd901950ede">AllClausesInCreationOrder</a>()) {</div>
<div class="line"><a name="l00337"></a><span class="lineno"> 337</span>&#160; <span class="keywordflow">if</span> (!clauses_propagator_-&gt;<a class="code" href="classoperations__research_1_1sat_1_1_literal_watchers.html#ab054db78fc1b1e1681d2fc4e9fd1ca45">IsRemovable</a>(clause)) {</div>
<div class="line"><a name="l00338"></a><span class="lineno"> 338</span>&#160; out-&gt;AddClause(clause-&gt;AsSpan());</div>
<div class="line"><a name="l00339"></a><span class="lineno"> 339</span>&#160; }</div>
<div class="line"><a name="l00340"></a><span class="lineno"> 340</span>&#160; }</div>
<div class="line"><a name="l00341"></a><span class="lineno"> 341</span>&#160; }</div>
<div class="line"><a name="l00342"></a><span class="lineno"> 342</span>&#160; </div>
<div class="line"><a name="l00343"></a><span class="lineno"> 343</span>&#160; <span class="comment">// Functions to manage the set of learned binary clauses.</span></div>
<div class="line"><a name="l00344"></a><span class="lineno"> 344</span>&#160; <span class="comment">// Only clauses added/learned when TrackBinaryClause() is true are managed.</span></div>
<div class="line"><a name="l00345"></a><span class="lineno"><a class="line" href="classoperations__research_1_1sat_1_1_sat_solver.html#aa5e0514942c20e89148448f4d0572cd0"> 345</a></span>&#160; <span class="keywordtype">void</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#aa5e0514942c20e89148448f4d0572cd0">TrackBinaryClauses</a>(<span class="keywordtype">bool</span> <a class="code" href="demon__profiler_8cc.html#a21edc7ca4cc5802c8779d68556bc09cf">value</a>) { track_binary_clauses_ = <a class="code" href="demon__profiler_8cc.html#a21edc7ca4cc5802c8779d68556bc09cf">value</a>; }</div>
<div class="line"><a name="l00346"></a><span class="lineno"> 346</span>&#160; <span class="keywordtype">bool</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a5a9a59c0a2f7fcec81cc44b1aa159186">AddBinaryClauses</a>(<span class="keyword">const</span> std::vector&lt;BinaryClause&gt;&amp; clauses);</div>
<div class="line"><a name="l00347"></a><span class="lineno"> 347</span>&#160; <span class="keyword">const</span> std::vector&lt;BinaryClause&gt;&amp; <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a4e9c1f685afe26db1566eaa65724b40b">NewlyAddedBinaryClauses</a>();</div>
<div class="line"><a name="l00348"></a><span class="lineno"> 348</span>&#160; <span class="keywordtype">void</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#afdb0cc1ac877cd981dcd3f0b0763e644">ClearNewlyAddedBinaryClauses</a>();</div>
<div class="line"><a name="l00349"></a><span class="lineno"> 349</span>&#160; </div>
<div class="line"><a name="l00350"></a><span class="lineno"><a class="line" href="structoperations__research_1_1sat_1_1_sat_solver_1_1_decision.html"> 350</a></span>&#160; <span class="keyword">struct </span><a class="code" href="structoperations__research_1_1sat_1_1_sat_solver_1_1_decision.html">Decision</a> {</div>
<div class="line"><a name="l00351"></a><span class="lineno"><a class="line" href="structoperations__research_1_1sat_1_1_sat_solver_1_1_decision.html#abd62b993702516d946bdbef25f6d29b0"> 351</a></span>&#160; <a class="code" href="structoperations__research_1_1sat_1_1_sat_solver_1_1_decision.html#abd62b993702516d946bdbef25f6d29b0">Decision</a>() {}</div>
<div class="line"><a name="l00352"></a><span class="lineno"><a class="line" href="structoperations__research_1_1sat_1_1_sat_solver_1_1_decision.html#a2949c912240ff8a61f4a6751250bba27"> 352</a></span>&#160; <a class="code" href="structoperations__research_1_1sat_1_1_sat_solver_1_1_decision.html#a2949c912240ff8a61f4a6751250bba27">Decision</a>(<span class="keywordtype">int</span> i, <a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> l) : <a class="code" href="structoperations__research_1_1sat_1_1_sat_solver_1_1_decision.html#a84b0a5cf3a019584a6f21ec98136c60a">trail_index</a>(i), <a class="code" href="structoperations__research_1_1sat_1_1_sat_solver_1_1_decision.html#af63dcc00f2023fdf498e0829e6fb8a6b">literal</a>(l) {}</div>
<div class="line"><a name="l00353"></a><span class="lineno"><a class="line" href="structoperations__research_1_1sat_1_1_sat_solver_1_1_decision.html#a84b0a5cf3a019584a6f21ec98136c60a"> 353</a></span>&#160; <span class="keywordtype">int</span> <a class="code" href="structoperations__research_1_1sat_1_1_sat_solver_1_1_decision.html#a84b0a5cf3a019584a6f21ec98136c60a">trail_index</a> = 0;</div>
<div class="line"><a name="l00354"></a><span class="lineno"><a class="line" href="structoperations__research_1_1sat_1_1_sat_solver_1_1_decision.html#af63dcc00f2023fdf498e0829e6fb8a6b"> 354</a></span>&#160; <a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> <a class="code" href="structoperations__research_1_1sat_1_1_sat_solver_1_1_decision.html#af63dcc00f2023fdf498e0829e6fb8a6b">literal</a>;</div>
<div class="line"><a name="l00355"></a><span class="lineno"> 355</span>&#160; };</div>
<div class="line"><a name="l00356"></a><span class="lineno"> 356</span>&#160; </div>
<div class="line"><a name="l00357"></a><span class="lineno"> 357</span>&#160; <span class="comment">// Note that the Decisions() vector is always of size NumVariables(), and that</span></div>
<div class="line"><a name="l00358"></a><span class="lineno"> 358</span>&#160; <span class="comment">// only the first CurrentDecisionLevel() entries have a meaning.</span></div>
<div class="line"><a name="l00359"></a><span class="lineno"><a class="line" href="classoperations__research_1_1sat_1_1_sat_solver.html#afb267fc6b043c4e4a15bf0bddd0aaf3f"> 359</a></span>&#160; <span class="keyword">const</span> std::vector&lt;Decision&gt;&amp; <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#afb267fc6b043c4e4a15bf0bddd0aaf3f">Decisions</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> decisions_; }</div>
<div class="line"><a name="l00360"></a><span class="lineno"><a class="line" href="classoperations__research_1_1sat_1_1_sat_solver.html#ad63c4461a1384629cb99413c6df8b9ca"> 360</a></span>&#160; <span class="keywordtype">int</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#ad63c4461a1384629cb99413c6df8b9ca">CurrentDecisionLevel</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> current_decision_level_; }</div>
<div class="line"><a name="l00361"></a><span class="lineno"><a class="line" href="classoperations__research_1_1sat_1_1_sat_solver.html#a01fd4c9f5286534866c6c5ee2c160fe9"> 361</a></span>&#160; <span class="keyword">const</span> <a class="code" href="classoperations__research_1_1sat_1_1_trail.html">Trail</a>&amp; <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a01fd4c9f5286534866c6c5ee2c160fe9">LiteralTrail</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> *trail_; }</div>
<div class="line"><a name="l00362"></a><span class="lineno"><a class="line" href="classoperations__research_1_1sat_1_1_sat_solver.html#a9789bf03dba611e9be5679d6e902d0c8"> 362</a></span>&#160; <span class="keyword">const</span> <a class="code" href="classoperations__research_1_1sat_1_1_variables_assignment.html">VariablesAssignment</a>&amp; <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a9789bf03dba611e9be5679d6e902d0c8">Assignment</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> trail_-&gt;<a class="code" href="classoperations__research_1_1sat_1_1_trail.html#a9789bf03dba611e9be5679d6e902d0c8">Assignment</a>(); }</div>
<div class="line"><a name="l00363"></a><span class="lineno"> 363</span>&#160; </div>
<div class="line"><a name="l00364"></a><span class="lineno"> 364</span>&#160; <span class="comment">// Some statistics since the creation of the solver.</span></div>
<div class="line"><a name="l00365"></a><span class="lineno"> 365</span>&#160; <a class="code" href="integral__types_8h.html#a7cde0074dfd288f2d70c0e035dacb28a">int64</a> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a4fbc93ff66f372e1b604609fe5b45557">num_branches</a>() <span class="keyword">const</span>;</div>
<div class="line"><a name="l00366"></a><span class="lineno"> 366</span>&#160; <a class="code" href="integral__types_8h.html#a7cde0074dfd288f2d70c0e035dacb28a">int64</a> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a42c1fced0014f47ce16a512d454cee0f">num_failures</a>() <span class="keyword">const</span>;</div>
<div class="line"><a name="l00367"></a><span class="lineno"> 367</span>&#160; <a class="code" href="integral__types_8h.html#a7cde0074dfd288f2d70c0e035dacb28a">int64</a> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a7b5f3592cdf12c0df22b6583b3e9ed61">num_propagations</a>() <span class="keyword">const</span>;</div>
<div class="line"><a name="l00368"></a><span class="lineno"> 368</span>&#160; </div>
<div class="line"><a name="l00369"></a><span class="lineno"> 369</span>&#160; <span class="comment">// Note that we count the number of backtrack to level zero from a positive</span></div>
<div class="line"><a name="l00370"></a><span class="lineno"> 370</span>&#160; <span class="comment">// level. Those can corresponds to actual restarts, or conflicts that learn</span></div>
<div class="line"><a name="l00371"></a><span class="lineno"> 371</span>&#160; <span class="comment">// unit clauses or any other reason that trigger such backtrack.</span></div>
<div class="line"><a name="l00372"></a><span class="lineno"> 372</span>&#160; <a class="code" href="integral__types_8h.html#a7cde0074dfd288f2d70c0e035dacb28a">int64</a> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a943e1a6b169c75c35c1f596b11fe4fc4">num_restarts</a>() <span class="keyword">const</span>;</div>
<div class="line"><a name="l00373"></a><span class="lineno"> 373</span>&#160; </div>
<div class="line"><a name="l00374"></a><span class="lineno"> 374</span>&#160; <span class="comment">// A deterministic number that should be correlated with the time spent in</span></div>
<div class="line"><a name="l00375"></a><span class="lineno"> 375</span>&#160; <span class="comment">// the Solve() function. The order of magnitude should be close to the time</span></div>
<div class="line"><a name="l00376"></a><span class="lineno"> 376</span>&#160; <span class="comment">// in seconds.</span></div>
<div class="line"><a name="l00377"></a><span class="lineno"> 377</span>&#160; <span class="keywordtype">double</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#ae525d235b02bcfc962d845e28f5f0125">deterministic_time</a>() <span class="keyword">const</span>;</div>
<div class="line"><a name="l00378"></a><span class="lineno"> 378</span>&#160; </div>
<div class="line"><a name="l00379"></a><span class="lineno"> 379</span>&#160; <span class="comment">// Only used for debugging. Save the current assignment in debug_assignment_.</span></div>
<div class="line"><a name="l00380"></a><span class="lineno"> 380</span>&#160; <span class="comment">// The idea is that if we know that a given assignment is satisfiable, then</span></div>
<div class="line"><a name="l00381"></a><span class="lineno"> 381</span>&#160; <span class="comment">// all the learned clauses or PB constraints must be satisfiable by it. In</span></div>
<div class="line"><a name="l00382"></a><span class="lineno"> 382</span>&#160; <span class="comment">// debug mode, and after this is called, all the learned clauses are tested to</span></div>
<div class="line"><a name="l00383"></a><span class="lineno"> 383</span>&#160; <span class="comment">// satisfy this saved assignement.</span></div>
<div class="line"><a name="l00384"></a><span class="lineno"> 384</span>&#160; <span class="keywordtype">void</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a68050818df324a24e6309055e857b955">SaveDebugAssignment</a>();</div>
<div class="line"><a name="l00385"></a><span class="lineno"> 385</span>&#160; </div>
<div class="line"><a name="l00386"></a><span class="lineno"> 386</span>&#160; <span class="comment">// Returns true iff the loaded problem only contains clauses.</span></div>
<div class="line"><a name="l00387"></a><span class="lineno"><a class="line" href="classoperations__research_1_1sat_1_1_sat_solver.html#a678cca4fb095d5dee896dd687649a5de"> 387</a></span>&#160; <span class="keywordtype">bool</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a678cca4fb095d5dee896dd687649a5de">ProblemIsPureSat</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> problem_is_pure_sat_; }</div>
<div class="line"><a name="l00388"></a><span class="lineno"> 388</span>&#160; </div>
<div class="line"><a name="l00389"></a><span class="lineno"><a class="line" href="classoperations__research_1_1sat_1_1_sat_solver.html#a75f1d17f36330a1c8a96e43fe8805598"> 389</a></span>&#160; <span class="keywordtype">void</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a75f1d17f36330a1c8a96e43fe8805598">SetDratProofHandler</a>(<a class="code" href="classoperations__research_1_1sat_1_1_drat_proof_handler.html">DratProofHandler</a>* drat_proof_handler) {</div>
<div class="line"><a name="l00390"></a><span class="lineno"> 390</span>&#160; drat_proof_handler_ = drat_proof_handler;</div>
<div class="line"><a name="l00391"></a><span class="lineno"> 391</span>&#160; clauses_propagator_-&gt;<a class="code" href="classoperations__research_1_1sat_1_1_literal_watchers.html#a75f1d17f36330a1c8a96e43fe8805598">SetDratProofHandler</a>(drat_proof_handler_);</div>
<div class="line"><a name="l00392"></a><span class="lineno"> 392</span>&#160; binary_implication_graph_-&gt;<a class="code" href="classoperations__research_1_1sat_1_1_binary_implication_graph.html#a75f1d17f36330a1c8a96e43fe8805598">SetDratProofHandler</a>(drat_proof_handler_);</div>
<div class="line"><a name="l00393"></a><span class="lineno"> 393</span>&#160; }</div>
<div class="line"><a name="l00394"></a><span class="lineno"> 394</span>&#160; </div>
<div class="line"><a name="l00395"></a><span class="lineno"> 395</span>&#160; <span class="comment">// This function is here to deal with the case where a SAT/CP model is found</span></div>
<div class="line"><a name="l00396"></a><span class="lineno"> 396</span>&#160; <span class="comment">// to be trivially UNSAT while the user is constructing the model. Instead of</span></div>
<div class="line"><a name="l00397"></a><span class="lineno"> 397</span>&#160; <span class="comment">// having to test the status of all the lines adding a constraint, one can</span></div>
<div class="line"><a name="l00398"></a><span class="lineno"> 398</span>&#160; <span class="comment">// just check if the solver is not UNSAT once the model is constructed. Note</span></div>
<div class="line"><a name="l00399"></a><span class="lineno"> 399</span>&#160; <span class="comment">// that we usually log a warning on the first constraint that caused a</span></div>
<div class="line"><a name="l00400"></a><span class="lineno"> 400</span>&#160; <span class="comment">// &quot;trival&quot; unsatisfiability.</span></div>
<div class="line"><a name="l00401"></a><span class="lineno"><a class="line" href="classoperations__research_1_1sat_1_1_sat_solver.html#a4f7251fc4692363cf55796a6f3e267ea"> 401</a></span>&#160; <span class="keywordtype">void</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a4f7251fc4692363cf55796a6f3e267ea">NotifyThatModelIsUnsat</a>() { model_is_unsat_ = <span class="keyword">true</span>; }</div>
<div class="line"><a name="l00402"></a><span class="lineno"> 402</span>&#160; </div>
<div class="line"><a name="l00403"></a><span class="lineno"> 403</span>&#160; <span class="comment">// Adds a clause at any level of the tree and propagate any new deductions.</span></div>
<div class="line"><a name="l00404"></a><span class="lineno"> 404</span>&#160; <span class="comment">// Returns false if the model becomes UNSAT. Important: We currently do not</span></div>
<div class="line"><a name="l00405"></a><span class="lineno"> 405</span>&#160; <span class="comment">// support adding a clause that is already falsified at a positive decision</span></div>
<div class="line"><a name="l00406"></a><span class="lineno"> 406</span>&#160; <span class="comment">// level. Doing that will cause a check fail.</span></div>
<div class="line"><a name="l00407"></a><span class="lineno"> 407</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00408"></a><span class="lineno"> 408</span>&#160; <span class="comment">// TODO(user): Backjump and propagate on a falsified clause? this is currently</span></div>
<div class="line"><a name="l00409"></a><span class="lineno"> 409</span>&#160; <span class="comment">// not needed.</span></div>
<div class="line"><a name="l00410"></a><span class="lineno"> 410</span>&#160; <span class="keywordtype">bool</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a25eb4ef5875f4884226251b66eb61bc0">AddClauseDuringSearch</a>(absl::Span&lt;const Literal&gt; literals);</div>
<div class="line"><a name="l00411"></a><span class="lineno"> 411</span>&#160; </div>
<div class="line"><a name="l00412"></a><span class="lineno"> 412</span>&#160; <span class="comment">// Performs propagation of the recently enqueued elements.</span></div>
<div class="line"><a name="l00413"></a><span class="lineno"> 413</span>&#160; <span class="comment">// Mainly visible for testing.</span></div>
<div class="line"><a name="l00414"></a><span class="lineno"> 414</span>&#160; <span class="keywordtype">bool</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#adadc001cbdc7263b106fc5886b60ff39">Propagate</a>();</div>
<div class="line"><a name="l00415"></a><span class="lineno"> 415</span>&#160; </div>
<div class="line"><a name="l00416"></a><span class="lineno"> 416</span>&#160; <span class="comment">// This must be called at level zero. It will spend the given num decision and</span></div>
<div class="line"><a name="l00417"></a><span class="lineno"> 417</span>&#160; <span class="comment">// use propagation to try to minimize some clauses from the database.</span></div>
<div class="line"><a name="l00418"></a><span class="lineno"> 418</span>&#160; <span class="keywordtype">void</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a8f1f9030283b2fa93b2353ab260ebe1e">MinimizeSomeClauses</a>(<span class="keywordtype">int</span> decisions_budget);</div>
<div class="line"><a name="l00419"></a><span class="lineno"> 419</span>&#160; </div>
<div class="line"><a name="l00420"></a><span class="lineno"> 420</span>&#160; <span class="comment">// Advance the given time limit with all the deterministic time that was</span></div>
<div class="line"><a name="l00421"></a><span class="lineno"> 421</span>&#160; <span class="comment">// elapsed since last call.</span></div>
<div class="line"><a name="l00422"></a><span class="lineno"><a class="line" href="classoperations__research_1_1sat_1_1_sat_solver.html#a705eddd5baee23097daf34b73e66eae3"> 422</a></span>&#160; <span class="keywordtype">void</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a705eddd5baee23097daf34b73e66eae3">AdvanceDeterministicTime</a>(<a class="code" href="classoperations__research_1_1_time_limit.html">TimeLimit</a>* limit) {</div>
<div class="line"><a name="l00423"></a><span class="lineno"> 423</span>&#160; <span class="keyword">const</span> <span class="keywordtype">double</span> current = <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#ae525d235b02bcfc962d845e28f5f0125">deterministic_time</a>();</div>
<div class="line"><a name="l00424"></a><span class="lineno"> 424</span>&#160; limit-&gt;<a class="code" href="classoperations__research_1_1_time_limit.html#af90cfd1fc238433fc303ee28c5914eb9">AdvanceDeterministicTime</a>(</div>
<div class="line"><a name="l00425"></a><span class="lineno"> 425</span>&#160; current - deterministic_time_at_last_advanced_time_limit_);</div>
<div class="line"><a name="l00426"></a><span class="lineno"> 426</span>&#160; deterministic_time_at_last_advanced_time_limit_ = current;</div>
<div class="line"><a name="l00427"></a><span class="lineno"> 427</span>&#160; }</div>
<div class="line"><a name="l00428"></a><span class="lineno"> 428</span>&#160; </div>
<div class="line"><a name="l00429"></a><span class="lineno"> 429</span>&#160; <span class="comment">// Simplifies the problem when new variables are assigned at level 0.</span></div>
<div class="line"><a name="l00430"></a><span class="lineno"> 430</span>&#160; <span class="keywordtype">void</span> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a2aafb0d6bd7d95f183e87866d0ade374">ProcessNewlyFixedVariables</a>();</div>
<div class="line"><a name="l00431"></a><span class="lineno"> 431</span>&#160; </div>
<div class="line"><a name="l00432"></a><span class="lineno"><a class="line" href="classoperations__research_1_1sat_1_1_sat_solver.html#a3cce11fce89a849b4224eb83e217abd0"> 432</a></span>&#160; <a class="code" href="integral__types_8h.html#a7cde0074dfd288f2d70c0e035dacb28a">int64</a> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a3cce11fce89a849b4224eb83e217abd0">NumFixedVariables</a>()<span class="keyword"> const </span>{</div>
<div class="line"><a name="l00433"></a><span class="lineno"> 433</span>&#160; <span class="keywordflow">if</span> (!decisions_.empty()) <span class="keywordflow">return</span> decisions_[0].trail_index;</div>
<div class="line"><a name="l00434"></a><span class="lineno"> 434</span>&#160; <a class="code" href="base_2logging_8h.html#a7c0ce053b28d53aa4eaf3eb7fb71663b">CHECK_EQ</a>(<a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#ad63c4461a1384629cb99413c6df8b9ca">CurrentDecisionLevel</a>(), 0);</div>
<div class="line"><a name="l00435"></a><span class="lineno"> 435</span>&#160; <span class="keywordflow">return</span> trail_-&gt;<a class="code" href="classoperations__research_1_1sat_1_1_trail.html#a8ef12397d1682615bc3108c397734179">Index</a>();</div>
<div class="line"><a name="l00436"></a><span class="lineno"> 436</span>&#160; }</div>
<div class="line"><a name="l00437"></a><span class="lineno"> 437</span>&#160; </div>
<div class="line"><a name="l00438"></a><span class="lineno"> 438</span>&#160; <span class="keyword">private</span>:</div>
<div class="line"><a name="l00439"></a><span class="lineno"> 439</span>&#160; <span class="comment">// Calls Propagate() and returns true if no conflict occurred. Otherwise,</span></div>
<div class="line"><a name="l00440"></a><span class="lineno"> 440</span>&#160; <span class="comment">// learns the conflict, backtracks, enqueues the consequence of the learned</span></div>
<div class="line"><a name="l00441"></a><span class="lineno"> 441</span>&#160; <span class="comment">// conflict and returns false.</span></div>
<div class="line"><a name="l00442"></a><span class="lineno"> 442</span>&#160; <span class="keywordtype">bool</span> PropagateAndStopAfterOneConflictResolution();</div>
<div class="line"><a name="l00443"></a><span class="lineno"> 443</span>&#160; </div>
<div class="line"><a name="l00444"></a><span class="lineno"> 444</span>&#160; <span class="comment">// All Solve() functions end up calling this one.</span></div>
<div class="line"><a name="l00445"></a><span class="lineno"> 445</span>&#160; <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a67a0db04d321a74b7e7fcfd3f1a3f70b">Status</a> SolveInternal(<a class="code" href="classoperations__research_1_1_time_limit.html">TimeLimit</a>* <a class="code" href="cp__model__solver_8cc.html#ac3cf9db02b23ea1455b5ae6955d03e47">time_limit</a>);</div>
<div class="line"><a name="l00446"></a><span class="lineno"> 446</span>&#160; </div>
<div class="line"><a name="l00447"></a><span class="lineno"> 447</span>&#160; <span class="comment">// Adds a binary clause to the BinaryImplicationGraph and to the</span></div>
<div class="line"><a name="l00448"></a><span class="lineno"> 448</span>&#160; <span class="comment">// BinaryClauseManager when track_binary_clauses_ is true.</span></div>
<div class="line"><a name="l00449"></a><span class="lineno"> 449</span>&#160; <span class="keywordtype">void</span> AddBinaryClauseInternal(<a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> <a class="code" href="constraint__solver_2table_8cc.html#af730895c6c6ef6e03caaf6251192dfd2">a</a>, <a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> <a class="code" href="constraint__solver_2table_8cc.html#a344010e26426d6a13411648d988bc9b6">b</a>);</div>
<div class="line"><a name="l00450"></a><span class="lineno"> 450</span>&#160; </div>
<div class="line"><a name="l00451"></a><span class="lineno"> 451</span>&#160; <span class="comment">// See SaveDebugAssignment(). Note that these functions only consider the</span></div>
<div class="line"><a name="l00452"></a><span class="lineno"> 452</span>&#160; <span class="comment">// variables at the time the debug_assignment_ was saved. If new variables</span></div>
<div class="line"><a name="l00453"></a><span class="lineno"> 453</span>&#160; <span class="comment">// were added since that time, they will be considered unassigned.</span></div>
<div class="line"><a name="l00454"></a><span class="lineno"> 454</span>&#160; <span class="keywordtype">bool</span> ClauseIsValidUnderDebugAssignement(</div>
<div class="line"><a name="l00455"></a><span class="lineno"> 455</span>&#160; <span class="keyword">const</span> std::vector&lt;Literal&gt;&amp; clause) <span class="keyword">const</span>;</div>
<div class="line"><a name="l00456"></a><span class="lineno"> 456</span>&#160; <span class="keywordtype">bool</span> PBConstraintIsValidUnderDebugAssignment(</div>
<div class="line"><a name="l00457"></a><span class="lineno"> 457</span>&#160; <span class="keyword">const</span> std::vector&lt;LiteralWithCoeff&gt;&amp; cst, <span class="keyword">const</span> Coefficient rhs) <span class="keyword">const</span>;</div>
<div class="line"><a name="l00458"></a><span class="lineno"> 458</span>&#160; </div>
<div class="line"><a name="l00459"></a><span class="lineno"> 459</span>&#160; <span class="comment">// Logs the given status if parameters_.log_search_progress() is true.</span></div>
<div class="line"><a name="l00460"></a><span class="lineno"> 460</span>&#160; <span class="comment">// Also returns it.</span></div>
<div class="line"><a name="l00461"></a><span class="lineno"> 461</span>&#160; <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a67a0db04d321a74b7e7fcfd3f1a3f70b">Status</a> StatusWithLog(<a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a67a0db04d321a74b7e7fcfd3f1a3f70b">Status</a> status);</div>
<div class="line"><a name="l00462"></a><span class="lineno"> 462</span>&#160; </div>
<div class="line"><a name="l00463"></a><span class="lineno"> 463</span>&#160; <span class="comment">// Main function called from SolveWithAssumptions() or from Solve() with an</span></div>
<div class="line"><a name="l00464"></a><span class="lineno"> 464</span>&#160; <span class="comment">// assumption_level of 0 (meaning no assumptions).</span></div>
<div class="line"><a name="l00465"></a><span class="lineno"> 465</span>&#160; <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a67a0db04d321a74b7e7fcfd3f1a3f70b">Status</a> SolveInternal(<span class="keywordtype">int</span> assumption_level);</div>
<div class="line"><a name="l00466"></a><span class="lineno"> 466</span>&#160; </div>
<div class="line"><a name="l00467"></a><span class="lineno"> 467</span>&#160; <span class="comment">// Applies the previous decisions (which are still on decisions_), in order,</span></div>
<div class="line"><a name="l00468"></a><span class="lineno"> 468</span>&#160; <span class="comment">// starting from the one at the current decision level. Stops at the one at</span></div>
<div class="line"><a name="l00469"></a><span class="lineno"> 469</span>&#160; <span class="comment">// decisions_[level] or on the first decision already propagated to &quot;false&quot;</span></div>
<div class="line"><a name="l00470"></a><span class="lineno"> 470</span>&#160; <span class="comment">// and thus incompatible.</span></div>
<div class="line"><a name="l00471"></a><span class="lineno"> 471</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00472"></a><span class="lineno"> 472</span>&#160; <span class="comment">// Note that during this process, conflicts may arise which will lead to</span></div>
<div class="line"><a name="l00473"></a><span class="lineno"> 473</span>&#160; <span class="comment">// backjumps. In this case, we will simply keep reapplying decisions from the</span></div>
<div class="line"><a name="l00474"></a><span class="lineno"> 474</span>&#160; <span class="comment">// last one backtracked over and so on.</span></div>
<div class="line"><a name="l00475"></a><span class="lineno"> 475</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00476"></a><span class="lineno"> 476</span>&#160; <span class="comment">// Returns FEASIBLE if no conflict occurred, INFEASIBLE if the model was</span></div>
<div class="line"><a name="l00477"></a><span class="lineno"> 477</span>&#160; <span class="comment">// proven unsat and ASSUMPTION_UNSAT otherwise. In the last case the first non</span></div>
<div class="line"><a name="l00478"></a><span class="lineno"> 478</span>&#160; <span class="comment">// taken old decision will be propagated to false by the ones before.</span></div>
<div class="line"><a name="l00479"></a><span class="lineno"> 479</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00480"></a><span class="lineno"> 480</span>&#160; <span class="comment">// first_propagation_index will be filled with the trail index of the first</span></div>
<div class="line"><a name="l00481"></a><span class="lineno"> 481</span>&#160; <span class="comment">// newly propagated literal, or with -1 if INFEASIBLE is returned.</span></div>
<div class="line"><a name="l00482"></a><span class="lineno"> 482</span>&#160; <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a67a0db04d321a74b7e7fcfd3f1a3f70b">Status</a> ReapplyDecisionsUpTo(<span class="keywordtype">int</span> level, <span class="keywordtype">int</span>* first_propagation_index);</div>
<div class="line"><a name="l00483"></a><span class="lineno"> 483</span>&#160; </div>
<div class="line"><a name="l00484"></a><span class="lineno"> 484</span>&#160; <span class="comment">// Returns false if the thread memory is over the limit.</span></div>
<div class="line"><a name="l00485"></a><span class="lineno"> 485</span>&#160; <span class="keywordtype">bool</span> IsMemoryLimitReached() <span class="keyword">const</span>;</div>
<div class="line"><a name="l00486"></a><span class="lineno"> 486</span>&#160; </div>
<div class="line"><a name="l00487"></a><span class="lineno"> 487</span>&#160; <span class="comment">// Sets model_is_unsat_ to true and return false.</span></div>
<div class="line"><a name="l00488"></a><span class="lineno"> 488</span>&#160; <span class="keywordtype">bool</span> SetModelUnsat();</div>
<div class="line"><a name="l00489"></a><span class="lineno"> 489</span>&#160; </div>
<div class="line"><a name="l00490"></a><span class="lineno"> 490</span>&#160; <span class="comment">// Returns the decision level of a given variable.</span></div>
<div class="line"><a name="l00491"></a><span class="lineno"> 491</span>&#160; <span class="keywordtype">int</span> DecisionLevel(BooleanVariable <a class="code" href="expr__array_8cc.html#a472a99923cbe11ae7b5a5d157d9ad465">var</a>)<span class="keyword"> const </span>{</div>
<div class="line"><a name="l00492"></a><span class="lineno"> 492</span>&#160; <span class="keywordflow">return</span> trail_-&gt;<a class="code" href="classoperations__research_1_1sat_1_1_trail.html#a29be1a6b9ba823a6fffb927609d18599">Info</a>(<a class="code" href="expr__array_8cc.html#a472a99923cbe11ae7b5a5d157d9ad465">var</a>).<a class="code" href="structoperations__research_1_1sat_1_1_assignment_info.html#afefd28242df91e46e762af1f7eaf623f">level</a>;</div>
<div class="line"><a name="l00493"></a><span class="lineno"> 493</span>&#160; }</div>
<div class="line"><a name="l00494"></a><span class="lineno"> 494</span>&#160; </div>
<div class="line"><a name="l00495"></a><span class="lineno"> 495</span>&#160; <span class="comment">// Returns the relevant pointer if the given variable was propagated by the</span></div>
<div class="line"><a name="l00496"></a><span class="lineno"> 496</span>&#160; <span class="comment">// constraint in question. This is used to bump the activity of the learned</span></div>
<div class="line"><a name="l00497"></a><span class="lineno"> 497</span>&#160; <span class="comment">// clauses or pb constraints.</span></div>
<div class="line"><a name="l00498"></a><span class="lineno"> 498</span>&#160; SatClause* ReasonClauseOrNull(BooleanVariable <a class="code" href="expr__array_8cc.html#a472a99923cbe11ae7b5a5d157d9ad465">var</a>) <span class="keyword">const</span>;</div>
<div class="line"><a name="l00499"></a><span class="lineno"> 499</span>&#160; UpperBoundedLinearConstraint* ReasonPbConstraintOrNull(</div>
<div class="line"><a name="l00500"></a><span class="lineno"> 500</span>&#160; BooleanVariable <a class="code" href="expr__array_8cc.html#a472a99923cbe11ae7b5a5d157d9ad465">var</a>) <span class="keyword">const</span>;</div>
<div class="line"><a name="l00501"></a><span class="lineno"> 501</span>&#160; </div>
<div class="line"><a name="l00502"></a><span class="lineno"> 502</span>&#160; <span class="comment">// This does one step of a pseudo-Boolean resolution:</span></div>
<div class="line"><a name="l00503"></a><span class="lineno"> 503</span>&#160; <span class="comment">// - The variable var has been assigned to l at a given trail_index.</span></div>
<div class="line"><a name="l00504"></a><span class="lineno"> 504</span>&#160; <span class="comment">// - The reason for var propagates it to l.</span></div>
<div class="line"><a name="l00505"></a><span class="lineno"> 505</span>&#160; <span class="comment">// - The conflict propagates it to not(l)</span></div>
<div class="line"><a name="l00506"></a><span class="lineno"> 506</span>&#160; <span class="comment">// The goal of the operation is to combine the two constraints in order to</span></div>
<div class="line"><a name="l00507"></a><span class="lineno"> 507</span>&#160; <span class="comment">// have a new conflict at a lower trail_index.</span></div>
<div class="line"><a name="l00508"></a><span class="lineno"> 508</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00509"></a><span class="lineno"> 509</span>&#160; <span class="comment">// Returns true if the reason for var was a normal clause. In this case,</span></div>
<div class="line"><a name="l00510"></a><span class="lineno"> 510</span>&#160; <span class="comment">// the *slack is updated to its new value.</span></div>
<div class="line"><a name="l00511"></a><span class="lineno"> 511</span>&#160; <span class="keywordtype">bool</span> ResolvePBConflict(BooleanVariable <a class="code" href="expr__array_8cc.html#a472a99923cbe11ae7b5a5d157d9ad465">var</a>,</div>
<div class="line"><a name="l00512"></a><span class="lineno"> 512</span>&#160; MutableUpperBoundedLinearConstraint* conflict,</div>
<div class="line"><a name="l00513"></a><span class="lineno"> 513</span>&#160; Coefficient* slack);</div>
<div class="line"><a name="l00514"></a><span class="lineno"> 514</span>&#160; </div>
<div class="line"><a name="l00515"></a><span class="lineno"> 515</span>&#160; <span class="comment">// Returns true iff the clause is the reason for an assigned variable.</span></div>
<div class="line"><a name="l00516"></a><span class="lineno"> 516</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00517"></a><span class="lineno"> 517</span>&#160; <span class="comment">// TODO(user): With our current data structures, we could also return true</span></div>
<div class="line"><a name="l00518"></a><span class="lineno"> 518</span>&#160; <span class="comment">// for clauses that were just used as a reason (like just before an untrail).</span></div>
<div class="line"><a name="l00519"></a><span class="lineno"> 519</span>&#160; <span class="comment">// This may be beneficial, but should properly be defined so that we can</span></div>
<div class="line"><a name="l00520"></a><span class="lineno"> 520</span>&#160; <span class="comment">// have the same behavior if we change the implementation.</span></div>
<div class="line"><a name="l00521"></a><span class="lineno"> 521</span>&#160; <span class="keywordtype">bool</span> ClauseIsUsedAsReason(SatClause* clause)<span class="keyword"> const </span>{</div>
<div class="line"><a name="l00522"></a><span class="lineno"> 522</span>&#160; <span class="keyword">const</span> BooleanVariable <a class="code" href="expr__array_8cc.html#a472a99923cbe11ae7b5a5d157d9ad465">var</a> = clause-&gt;PropagatedLiteral().Variable();</div>
<div class="line"><a name="l00523"></a><span class="lineno"> 523</span>&#160; <span class="keywordflow">return</span> trail_-&gt;<a class="code" href="classoperations__research_1_1sat_1_1_trail.html#a29be1a6b9ba823a6fffb927609d18599">Info</a>(<a class="code" href="expr__array_8cc.html#a472a99923cbe11ae7b5a5d157d9ad465">var</a>).<a class="code" href="structoperations__research_1_1sat_1_1_assignment_info.html#a8843d978bef78a2392a908bd07fffb8e">trail_index</a> &lt; trail_-&gt;<a class="code" href="classoperations__research_1_1sat_1_1_trail.html#a8ef12397d1682615bc3108c397734179">Index</a>() &amp;&amp;</div>
<div class="line"><a name="l00524"></a><span class="lineno"> 524</span>&#160; (*trail_)[trail_-&gt;<a class="code" href="classoperations__research_1_1sat_1_1_trail.html#a29be1a6b9ba823a6fffb927609d18599">Info</a>(<a class="code" href="expr__array_8cc.html#a472a99923cbe11ae7b5a5d157d9ad465">var</a>).<a class="code" href="structoperations__research_1_1sat_1_1_assignment_info.html#a8843d978bef78a2392a908bd07fffb8e">trail_index</a>].Variable() == <a class="code" href="expr__array_8cc.html#a472a99923cbe11ae7b5a5d157d9ad465">var</a> &amp;&amp;</div>
<div class="line"><a name="l00525"></a><span class="lineno"> 525</span>&#160; ReasonClauseOrNull(<a class="code" href="expr__array_8cc.html#a472a99923cbe11ae7b5a5d157d9ad465">var</a>) == clause;</div>
<div class="line"><a name="l00526"></a><span class="lineno"> 526</span>&#160; }</div>
<div class="line"><a name="l00527"></a><span class="lineno"> 527</span>&#160; </div>
<div class="line"><a name="l00528"></a><span class="lineno"> 528</span>&#160; <span class="comment">// Add a problem clause. The clause is assumed to be &quot;cleaned&quot;, that is no</span></div>
<div class="line"><a name="l00529"></a><span class="lineno"> 529</span>&#160; <span class="comment">// duplicate variables (not strictly required) and not empty.</span></div>
<div class="line"><a name="l00530"></a><span class="lineno"> 530</span>&#160; <span class="keywordtype">bool</span> AddProblemClauseInternal(absl::Span&lt;const Literal&gt; literals);</div>
<div class="line"><a name="l00531"></a><span class="lineno"> 531</span>&#160; </div>
<div class="line"><a name="l00532"></a><span class="lineno"> 532</span>&#160; <span class="comment">// This is used by all the Add*LinearConstraint() functions. It detects</span></div>
<div class="line"><a name="l00533"></a><span class="lineno"> 533</span>&#160; <span class="comment">// infeasible/trivial constraints or clause constraints and takes the proper</span></div>
<div class="line"><a name="l00534"></a><span class="lineno"> 534</span>&#160; <span class="comment">// action.</span></div>
<div class="line"><a name="l00535"></a><span class="lineno"> 535</span>&#160; <span class="keywordtype">bool</span> AddLinearConstraintInternal(<span class="keyword">const</span> std::vector&lt;LiteralWithCoeff&gt;&amp; cst,</div>
<div class="line"><a name="l00536"></a><span class="lineno"> 536</span>&#160; Coefficient rhs, Coefficient max_value);</div>
<div class="line"><a name="l00537"></a><span class="lineno"> 537</span>&#160; </div>
<div class="line"><a name="l00538"></a><span class="lineno"> 538</span>&#160; <span class="comment">// Adds a learned clause to the problem. This should be called after</span></div>
<div class="line"><a name="l00539"></a><span class="lineno"> 539</span>&#160; <span class="comment">// Backtrack(). The backtrack is such that after it is applied, all the</span></div>
<div class="line"><a name="l00540"></a><span class="lineno"> 540</span>&#160; <span class="comment">// literals of the learned close except one will be false. Thus the last one</span></div>
<div class="line"><a name="l00541"></a><span class="lineno"> 541</span>&#160; <span class="comment">// will be implied True. This function also Enqueue() the implied literal.</span></div>
<div class="line"><a name="l00542"></a><span class="lineno"> 542</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00543"></a><span class="lineno"> 543</span>&#160; <span class="comment">// Returns the LBD of the clause.</span></div>
<div class="line"><a name="l00544"></a><span class="lineno"> 544</span>&#160; <span class="keywordtype">int</span> AddLearnedClauseAndEnqueueUnitPropagation(</div>
<div class="line"><a name="l00545"></a><span class="lineno"> 545</span>&#160; <span class="keyword">const</span> std::vector&lt;Literal&gt;&amp; literals, <span class="keywordtype">bool</span> is_redundant);</div>
<div class="line"><a name="l00546"></a><span class="lineno"> 546</span>&#160; </div>
<div class="line"><a name="l00547"></a><span class="lineno"> 547</span>&#160; <span class="comment">// Creates a new decision which corresponds to setting the given literal to</span></div>
<div class="line"><a name="l00548"></a><span class="lineno"> 548</span>&#160; <span class="comment">// True and Enqueue() this change.</span></div>
<div class="line"><a name="l00549"></a><span class="lineno"> 549</span>&#160; <span class="keywordtype">void</span> EnqueueNewDecision(Literal <a class="code" href="optimization_8cc.html#af63dcc00f2023fdf498e0829e6fb8a6b">literal</a>);</div>
<div class="line"><a name="l00550"></a><span class="lineno"> 550</span>&#160; </div>
<div class="line"><a name="l00551"></a><span class="lineno"> 551</span>&#160; <span class="comment">// Returns true if everything has been propagated.</span></div>
<div class="line"><a name="l00552"></a><span class="lineno"> 552</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00553"></a><span class="lineno"> 553</span>&#160; <span class="comment">// TODO(user): This test is fast but not exhaustive, especially regarding the</span></div>
<div class="line"><a name="l00554"></a><span class="lineno"> 554</span>&#160; <span class="comment">// integer propagators. Fix.</span></div>
<div class="line"><a name="l00555"></a><span class="lineno"> 555</span>&#160; <span class="keywordtype">bool</span> PropagationIsDone() <span class="keyword">const</span>;</div>
<div class="line"><a name="l00556"></a><span class="lineno"> 556</span>&#160; </div>
<div class="line"><a name="l00557"></a><span class="lineno"> 557</span>&#160; <span class="comment">// Update the propagators_ list with the relevant propagators.</span></div>
<div class="line"><a name="l00558"></a><span class="lineno"> 558</span>&#160; <span class="keywordtype">void</span> InitializePropagators();</div>
<div class="line"><a name="l00559"></a><span class="lineno"> 559</span>&#160; </div>
<div class="line"><a name="l00560"></a><span class="lineno"> 560</span>&#160; <span class="comment">// Unrolls the trail until a given point. This unassign the assigned variables</span></div>
<div class="line"><a name="l00561"></a><span class="lineno"> 561</span>&#160; <span class="comment">// and add them to the priority queue with the correct weight.</span></div>
<div class="line"><a name="l00562"></a><span class="lineno"> 562</span>&#160; <span class="keywordtype">void</span> Untrail(<span class="keywordtype">int</span> target_trail_index);</div>
<div class="line"><a name="l00563"></a><span class="lineno"> 563</span>&#160; </div>
<div class="line"><a name="l00564"></a><span class="lineno"> 564</span>&#160; <span class="comment">// Output to the DRAT proof handler any newly fixed variables.</span></div>
<div class="line"><a name="l00565"></a><span class="lineno"> 565</span>&#160; <span class="keywordtype">void</span> ProcessNewlyFixedVariablesForDratProof();</div>
<div class="line"><a name="l00566"></a><span class="lineno"> 566</span>&#160; </div>
<div class="line"><a name="l00567"></a><span class="lineno"> 567</span>&#160; <span class="comment">// Returns the maximum trail_index of the literals in the given clause.</span></div>
<div class="line"><a name="l00568"></a><span class="lineno"> 568</span>&#160; <span class="comment">// All the literals must be assigned. Returns -1 if the clause is empty.</span></div>
<div class="line"><a name="l00569"></a><span class="lineno"> 569</span>&#160; <span class="keywordtype">int</span> ComputeMaxTrailIndex(absl::Span&lt;const Literal&gt; clause) <span class="keyword">const</span>;</div>
<div class="line"><a name="l00570"></a><span class="lineno"> 570</span>&#160; </div>
<div class="line"><a name="l00571"></a><span class="lineno"> 571</span>&#160; <span class="comment">// Computes what is known as the first UIP (Unique implication point) conflict</span></div>
<div class="line"><a name="l00572"></a><span class="lineno"> 572</span>&#160; <span class="comment">// clause starting from the failing clause. For a definition of UIP and a</span></div>
<div class="line"><a name="l00573"></a><span class="lineno"> 573</span>&#160; <span class="comment">// comparison of the different possible conflict clause computation, see the</span></div>
<div class="line"><a name="l00574"></a><span class="lineno"> 574</span>&#160; <span class="comment">// reference below.</span></div>
<div class="line"><a name="l00575"></a><span class="lineno"> 575</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00576"></a><span class="lineno"> 576</span>&#160; <span class="comment">// The conflict will have only one literal at the highest decision level, and</span></div>
<div class="line"><a name="l00577"></a><span class="lineno"> 577</span>&#160; <span class="comment">// this literal will always be the first in the conflict vector.</span></div>
<div class="line"><a name="l00578"></a><span class="lineno"> 578</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00579"></a><span class="lineno"> 579</span>&#160; <span class="comment">// L Zhang, CF Madigan, MH Moskewicz, S Malik, &quot;Efficient conflict driven</span></div>
<div class="line"><a name="l00580"></a><span class="lineno"> 580</span>&#160; <span class="comment">// learning in a boolean satisfiability solver&quot; Proceedings of the 2001</span></div>
<div class="line"><a name="l00581"></a><span class="lineno"> 581</span>&#160; <span class="comment">// IEEE/ACM international conference on Computer-aided design, Pages 279-285.</span></div>
<div class="line"><a name="l00582"></a><span class="lineno"> 582</span>&#160; <span class="comment">// http://www.cs.tau.ac.il/~msagiv/courses/ATP/iccad2001_final.pdf</span></div>
<div class="line"><a name="l00583"></a><span class="lineno"> 583</span>&#160; <span class="keywordtype">void</span> ComputeFirstUIPConflict(</div>
<div class="line"><a name="l00584"></a><span class="lineno"> 584</span>&#160; <span class="keywordtype">int</span> max_trail_index, std::vector&lt;Literal&gt;* conflict,</div>
<div class="line"><a name="l00585"></a><span class="lineno"> 585</span>&#160; std::vector&lt;Literal&gt;* reason_used_to_infer_the_conflict,</div>
<div class="line"><a name="l00586"></a><span class="lineno"> 586</span>&#160; std::vector&lt;SatClause*&gt;* subsumed_clauses);</div>
<div class="line"><a name="l00587"></a><span class="lineno"> 587</span>&#160; </div>
<div class="line"><a name="l00588"></a><span class="lineno"> 588</span>&#160; <span class="comment">// Fills literals with all the literals in the reasons of the literals in the</span></div>
<div class="line"><a name="l00589"></a><span class="lineno"> 589</span>&#160; <span class="comment">// given input. The output vector will have no duplicates and will not contain</span></div>
<div class="line"><a name="l00590"></a><span class="lineno"> 590</span>&#160; <span class="comment">// the literals already present in the input.</span></div>
<div class="line"><a name="l00591"></a><span class="lineno"> 591</span>&#160; <span class="keywordtype">void</span> ComputeUnionOfReasons(<span class="keyword">const</span> std::vector&lt;Literal&gt;&amp; <a class="code" href="parser_8yy_8cc.html#a5a634cf4429798b1c921a81de8250051">input</a>,</div>
<div class="line"><a name="l00592"></a><span class="lineno"> 592</span>&#160; std::vector&lt;Literal&gt;* literals);</div>
<div class="line"><a name="l00593"></a><span class="lineno"> 593</span>&#160; </div>
<div class="line"><a name="l00594"></a><span class="lineno"> 594</span>&#160; <span class="comment">// Given an assumption (i.e. literal) currently assigned to false, this will</span></div>
<div class="line"><a name="l00595"></a><span class="lineno"> 595</span>&#160; <span class="comment">// returns the set of all assumptions that caused this particular assignment.</span></div>
<div class="line"><a name="l00596"></a><span class="lineno"> 596</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00597"></a><span class="lineno"> 597</span>&#160; <span class="comment">// This is useful to get a small set of assumptions that can&#39;t be all</span></div>
<div class="line"><a name="l00598"></a><span class="lineno"> 598</span>&#160; <span class="comment">// satisfied together.</span></div>
<div class="line"><a name="l00599"></a><span class="lineno"> 599</span>&#160; <span class="keywordtype">void</span> FillUnsatAssumptions(Literal false_assumption,</div>
<div class="line"><a name="l00600"></a><span class="lineno"> 600</span>&#160; std::vector&lt;Literal&gt;* unsat_assumptions);</div>
<div class="line"><a name="l00601"></a><span class="lineno"> 601</span>&#160; </div>
<div class="line"><a name="l00602"></a><span class="lineno"> 602</span>&#160; <span class="comment">// Do the full pseudo-Boolean constraint analysis. This calls multiple</span></div>
<div class="line"><a name="l00603"></a><span class="lineno"> 603</span>&#160; <span class="comment">// time ResolvePBConflict() on the current conflict until we have a conflict</span></div>
<div class="line"><a name="l00604"></a><span class="lineno"> 604</span>&#160; <span class="comment">// that allow us to propagate more at a lower decision level. This level</span></div>
<div class="line"><a name="l00605"></a><span class="lineno"> 605</span>&#160; <span class="comment">// is the one returned in backjump_level.</span></div>
<div class="line"><a name="l00606"></a><span class="lineno"> 606</span>&#160; <span class="keywordtype">void</span> ComputePBConflict(<span class="keywordtype">int</span> max_trail_index, Coefficient initial_slack,</div>
<div class="line"><a name="l00607"></a><span class="lineno"> 607</span>&#160; MutableUpperBoundedLinearConstraint* conflict,</div>
<div class="line"><a name="l00608"></a><span class="lineno"> 608</span>&#160; <span class="keywordtype">int</span>* backjump_level);</div>
<div class="line"><a name="l00609"></a><span class="lineno"> 609</span>&#160; </div>
<div class="line"><a name="l00610"></a><span class="lineno"> 610</span>&#160; <span class="comment">// Applies some heuristics to a conflict in order to minimize its size and/or</span></div>
<div class="line"><a name="l00611"></a><span class="lineno"> 611</span>&#160; <span class="comment">// replace literals by other literals from lower decision levels. The first</span></div>
<div class="line"><a name="l00612"></a><span class="lineno"> 612</span>&#160; <span class="comment">// function choose which one of the other functions to call depending on the</span></div>
<div class="line"><a name="l00613"></a><span class="lineno"> 613</span>&#160; <span class="comment">// parameters.</span></div>
<div class="line"><a name="l00614"></a><span class="lineno"> 614</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00615"></a><span class="lineno"> 615</span>&#160; <span class="comment">// Precondidtion: is_marked_ should be set to true for all the variables of</span></div>
<div class="line"><a name="l00616"></a><span class="lineno"> 616</span>&#160; <span class="comment">// the conflict. It can also contains false non-conflict variables that</span></div>
<div class="line"><a name="l00617"></a><span class="lineno"> 617</span>&#160; <span class="comment">// are implied by the negation of the 1-UIP conflict literal.</span></div>
<div class="line"><a name="l00618"></a><span class="lineno"> 618</span>&#160; <span class="keywordtype">void</span> MinimizeConflict(</div>
<div class="line"><a name="l00619"></a><span class="lineno"> 619</span>&#160; std::vector&lt;Literal&gt;* conflict,</div>
<div class="line"><a name="l00620"></a><span class="lineno"> 620</span>&#160; std::vector&lt;Literal&gt;* reason_used_to_infer_the_conflict);</div>
<div class="line"><a name="l00621"></a><span class="lineno"> 621</span>&#160; <span class="keywordtype">void</span> MinimizeConflictExperimental(std::vector&lt;Literal&gt;* conflict);</div>
<div class="line"><a name="l00622"></a><span class="lineno"> 622</span>&#160; <span class="keywordtype">void</span> MinimizeConflictSimple(std::vector&lt;Literal&gt;* conflict);</div>
<div class="line"><a name="l00623"></a><span class="lineno"> 623</span>&#160; <span class="keywordtype">void</span> MinimizeConflictRecursively(std::vector&lt;Literal&gt;* conflict);</div>
<div class="line"><a name="l00624"></a><span class="lineno"> 624</span>&#160; </div>
<div class="line"><a name="l00625"></a><span class="lineno"> 625</span>&#160; <span class="comment">// Utility function used by MinimizeConflictRecursively().</span></div>
<div class="line"><a name="l00626"></a><span class="lineno"> 626</span>&#160; <span class="keywordtype">bool</span> CanBeInferedFromConflictVariables(BooleanVariable variable);</div>
<div class="line"><a name="l00627"></a><span class="lineno"> 627</span>&#160; </div>
<div class="line"><a name="l00628"></a><span class="lineno"> 628</span>&#160; <span class="comment">// To be used in DCHECK(). Verifies some property of the conflict clause:</span></div>
<div class="line"><a name="l00629"></a><span class="lineno"> 629</span>&#160; <span class="comment">// - There is an unique literal with the highest decision level.</span></div>
<div class="line"><a name="l00630"></a><span class="lineno"> 630</span>&#160; <span class="comment">// - This literal appears in the first position.</span></div>
<div class="line"><a name="l00631"></a><span class="lineno"> 631</span>&#160; <span class="comment">// - All the other literals are of smaller decision level.</span></div>
<div class="line"><a name="l00632"></a><span class="lineno"> 632</span>&#160; <span class="comment">// - Ther is no literal with a decision level of zero.</span></div>
<div class="line"><a name="l00633"></a><span class="lineno"> 633</span>&#160; <span class="keywordtype">bool</span> IsConflictValid(<span class="keyword">const</span> std::vector&lt;Literal&gt;&amp; literals);</div>
<div class="line"><a name="l00634"></a><span class="lineno"> 634</span>&#160; </div>
<div class="line"><a name="l00635"></a><span class="lineno"> 635</span>&#160; <span class="comment">// Given the learned clause after a conflict, this computes the correct</span></div>
<div class="line"><a name="l00636"></a><span class="lineno"> 636</span>&#160; <span class="comment">// backtrack level to call Backtrack() with.</span></div>
<div class="line"><a name="l00637"></a><span class="lineno"> 637</span>&#160; <span class="keywordtype">int</span> ComputeBacktrackLevel(<span class="keyword">const</span> std::vector&lt;Literal&gt;&amp; literals);</div>
<div class="line"><a name="l00638"></a><span class="lineno"> 638</span>&#160; </div>
<div class="line"><a name="l00639"></a><span class="lineno"> 639</span>&#160; <span class="comment">// The LBD (Literal Blocks Distance) is the number of different decision</span></div>
<div class="line"><a name="l00640"></a><span class="lineno"> 640</span>&#160; <span class="comment">// levels at which the literals of the clause were assigned. Note that we</span></div>
<div class="line"><a name="l00641"></a><span class="lineno"> 641</span>&#160; <span class="comment">// ignore the decision level 0 whereas the definition in the paper below</span></div>
<div class="line"><a name="l00642"></a><span class="lineno"> 642</span>&#160; <span class="comment">// doesn&#39;t:</span></div>
<div class="line"><a name="l00643"></a><span class="lineno"> 643</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00644"></a><span class="lineno"> 644</span>&#160; <span class="comment">// G. Audemard, L. Simon, &quot;Predicting Learnt Clauses Quality in Modern SAT</span></div>
<div class="line"><a name="l00645"></a><span class="lineno"> 645</span>&#160; <span class="comment">// Solver&quot; in Twenty-first International Joint Conference on Artificial</span></div>
<div class="line"><a name="l00646"></a><span class="lineno"> 646</span>&#160; <span class="comment">// Intelligence (IJCAI&#39;09), july 2009.</span></div>
<div class="line"><a name="l00647"></a><span class="lineno"> 647</span>&#160; <span class="comment">// http://www.ijcai.org/papers09/Papers/IJCAI09-074.pdf</span></div>
<div class="line"><a name="l00648"></a><span class="lineno"> 648</span>&#160; <span class="comment">//</span></div>
<div class="line"><a name="l00649"></a><span class="lineno"> 649</span>&#160; <span class="comment">// IMPORTANT: All the literals of the clause must be assigned, and the first</span></div>
<div class="line"><a name="l00650"></a><span class="lineno"> 650</span>&#160; <span class="comment">// literal must be of the highest decision level. This will be the case for</span></div>
<div class="line"><a name="l00651"></a><span class="lineno"> 651</span>&#160; <span class="comment">// all the reason clauses.</span></div>
<div class="line"><a name="l00652"></a><span class="lineno"> 652</span>&#160; <span class="keyword">template</span> &lt;<span class="keyword">typename</span> LiteralList&gt;</div>
<div class="line"><a name="l00653"></a><span class="lineno"> 653</span>&#160; <span class="keywordtype">int</span> ComputeLbd(<span class="keyword">const</span> LiteralList&amp; literals);</div>
<div class="line"><a name="l00654"></a><span class="lineno"> 654</span>&#160; </div>
<div class="line"><a name="l00655"></a><span class="lineno"> 655</span>&#160; <span class="comment">// Checks if we need to reduce the number of learned clauses and do</span></div>
<div class="line"><a name="l00656"></a><span class="lineno"> 656</span>&#160; <span class="comment">// it if needed. Also updates the learned clause limit for the next cleanup.</span></div>
<div class="line"><a name="l00657"></a><span class="lineno"> 657</span>&#160; <span class="keywordtype">void</span> CleanClauseDatabaseIfNeeded();</div>
<div class="line"><a name="l00658"></a><span class="lineno"> 658</span>&#160; </div>
<div class="line"><a name="l00659"></a><span class="lineno"> 659</span>&#160; <span class="comment">// Activity management for clauses. This work the same way at the ones for</span></div>
<div class="line"><a name="l00660"></a><span class="lineno"> 660</span>&#160; <span class="comment">// variables, but with different parameters.</span></div>
<div class="line"><a name="l00661"></a><span class="lineno"> 661</span>&#160; <span class="keywordtype">void</span> BumpReasonActivities(<span class="keyword">const</span> std::vector&lt;Literal&gt;&amp; literals);</div>
<div class="line"><a name="l00662"></a><span class="lineno"> 662</span>&#160; <span class="keywordtype">void</span> BumpClauseActivity(SatClause* clause);</div>
<div class="line"><a name="l00663"></a><span class="lineno"> 663</span>&#160; <span class="keywordtype">void</span> RescaleClauseActivities(<span class="keywordtype">double</span> scaling_factor);</div>
<div class="line"><a name="l00664"></a><span class="lineno"> 664</span>&#160; <span class="keywordtype">void</span> UpdateClauseActivityIncrement();</div>
<div class="line"><a name="l00665"></a><span class="lineno"> 665</span>&#160; </div>
<div class="line"><a name="l00666"></a><span class="lineno"> 666</span>&#160; std::string DebugString(<span class="keyword">const</span> SatClause&amp; clause) <span class="keyword">const</span>;</div>
<div class="line"><a name="l00667"></a><span class="lineno"> 667</span>&#160; std::string StatusString(<a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a67a0db04d321a74b7e7fcfd3f1a3f70b">Status</a> status) <span class="keyword">const</span>;</div>
<div class="line"><a name="l00668"></a><span class="lineno"> 668</span>&#160; std::string RunningStatisticsString() <span class="keyword">const</span>;</div>
<div class="line"><a name="l00669"></a><span class="lineno"> 669</span>&#160; </div>
<div class="line"><a name="l00670"></a><span class="lineno"> 670</span>&#160; <span class="comment">// Marks as &quot;non-deletable&quot; all clauses that were used to infer the given</span></div>
<div class="line"><a name="l00671"></a><span class="lineno"> 671</span>&#160; <span class="comment">// variable. The variable must be currently assigned.</span></div>
<div class="line"><a name="l00672"></a><span class="lineno"> 672</span>&#160; <span class="keywordtype">void</span> KeepAllClauseUsedToInfer(BooleanVariable variable);</div>
<div class="line"><a name="l00673"></a><span class="lineno"> 673</span>&#160; </div>
<div class="line"><a name="l00674"></a><span class="lineno"> 674</span>&#160; <span class="comment">// Use propagation to try to minimize the given clause. This is really similar</span></div>
<div class="line"><a name="l00675"></a><span class="lineno"> 675</span>&#160; <span class="comment">// to MinimizeCoreWithPropagation(). It must be called when the current</span></div>
<div class="line"><a name="l00676"></a><span class="lineno"> 676</span>&#160; <span class="comment">// decision level is zero. Note that because this do a small tree search, it</span></div>
<div class="line"><a name="l00677"></a><span class="lineno"> 677</span>&#160; <span class="comment">// will impact the variable/clauses activities and may add new conflicts.</span></div>
<div class="line"><a name="l00678"></a><span class="lineno"> 678</span>&#160; <span class="keywordtype">void</span> TryToMinimizeClause(SatClause* clause);</div>
<div class="line"><a name="l00679"></a><span class="lineno"> 679</span>&#160; </div>
<div class="line"><a name="l00680"></a><span class="lineno"> 680</span>&#160; <span class="comment">// This is used by the old non-model constructor.</span></div>
<div class="line"><a name="l00681"></a><span class="lineno"> 681</span>&#160; Model* model_;</div>
<div class="line"><a name="l00682"></a><span class="lineno"> 682</span>&#160; std::unique_ptr&lt;Model&gt; owned_model_;</div>
<div class="line"><a name="l00683"></a><span class="lineno"> 683</span>&#160; </div>
<div class="line"><a name="l00684"></a><span class="lineno"> 684</span>&#160; BooleanVariable num_variables_ = BooleanVariable(0);</div>
<div class="line"><a name="l00685"></a><span class="lineno"> 685</span>&#160; </div>
<div class="line"><a name="l00686"></a><span class="lineno"> 686</span>&#160; <span class="comment">// Internal propagators. We keep them here because we need more than the</span></div>
<div class="line"><a name="l00687"></a><span class="lineno"> 687</span>&#160; <span class="comment">// SatPropagator interface for them.</span></div>
<div class="line"><a name="l00688"></a><span class="lineno"> 688</span>&#160; BinaryImplicationGraph* binary_implication_graph_;</div>
<div class="line"><a name="l00689"></a><span class="lineno"> 689</span>&#160; LiteralWatchers* clauses_propagator_;</div>
<div class="line"><a name="l00690"></a><span class="lineno"> 690</span>&#160; PbConstraints* pb_constraints_;</div>
<div class="line"><a name="l00691"></a><span class="lineno"> 691</span>&#160; </div>
<div class="line"><a name="l00692"></a><span class="lineno"> 692</span>&#160; <span class="comment">// Ordered list of propagators used by Propagate()/Untrail().</span></div>
<div class="line"><a name="l00693"></a><span class="lineno"> 693</span>&#160; std::vector&lt;SatPropagator*&gt; propagators_;</div>
<div class="line"><a name="l00694"></a><span class="lineno"> 694</span>&#160; </div>
<div class="line"><a name="l00695"></a><span class="lineno"> 695</span>&#160; <span class="comment">// Ordered list of propagators added with AddPropagator().</span></div>
<div class="line"><a name="l00696"></a><span class="lineno"> 696</span>&#160; std::vector&lt;SatPropagator*&gt; external_propagators_;</div>
<div class="line"><a name="l00697"></a><span class="lineno"> 697</span>&#160; SatPropagator* last_propagator_ = <span class="keyword">nullptr</span>;</div>
<div class="line"><a name="l00698"></a><span class="lineno"> 698</span>&#160; </div>
<div class="line"><a name="l00699"></a><span class="lineno"> 699</span>&#160; <span class="comment">// For the old, non-model interface.</span></div>
<div class="line"><a name="l00700"></a><span class="lineno"> 700</span>&#160; std::vector&lt;std::unique_ptr&lt;SatPropagator&gt;&gt; owned_propagators_;</div>
<div class="line"><a name="l00701"></a><span class="lineno"> 701</span>&#160; </div>
<div class="line"><a name="l00702"></a><span class="lineno"> 702</span>&#160; <span class="comment">// Keep track of all binary clauses so they can be exported.</span></div>
<div class="line"><a name="l00703"></a><span class="lineno"> 703</span>&#160; <span class="keywordtype">bool</span> track_binary_clauses_;</div>
<div class="line"><a name="l00704"></a><span class="lineno"> 704</span>&#160; BinaryClauseManager binary_clauses_;</div>
<div class="line"><a name="l00705"></a><span class="lineno"> 705</span>&#160; </div>
<div class="line"><a name="l00706"></a><span class="lineno"> 706</span>&#160; <span class="comment">// Pointers to singleton Model objects.</span></div>
<div class="line"><a name="l00707"></a><span class="lineno"> 707</span>&#160; Trail* trail_;</div>
<div class="line"><a name="l00708"></a><span class="lineno"> 708</span>&#160; TimeLimit* time_limit_;</div>
<div class="line"><a name="l00709"></a><span class="lineno"> 709</span>&#160; SatParameters* parameters_;</div>
<div class="line"><a name="l00710"></a><span class="lineno"> 710</span>&#160; RestartPolicy* restart_;</div>
<div class="line"><a name="l00711"></a><span class="lineno"> 711</span>&#160; SatDecisionPolicy* decision_policy_;</div>
<div class="line"><a name="l00712"></a><span class="lineno"> 712</span>&#160; </div>
<div class="line"><a name="l00713"></a><span class="lineno"> 713</span>&#160; <span class="comment">// Used for debugging only. See SaveDebugAssignment().</span></div>
<div class="line"><a name="l00714"></a><span class="lineno"> 714</span>&#160; VariablesAssignment debug_assignment_;</div>
<div class="line"><a name="l00715"></a><span class="lineno"> 715</span>&#160; </div>
<div class="line"><a name="l00716"></a><span class="lineno"> 716</span>&#160; <span class="comment">// The stack of decisions taken by the solver. They are stored in [0,</span></div>
<div class="line"><a name="l00717"></a><span class="lineno"> 717</span>&#160; <span class="comment">// current_decision_level_). The vector is of size num_variables_ so it can</span></div>
<div class="line"><a name="l00718"></a><span class="lineno"> 718</span>&#160; <span class="comment">// store all the decisions. This is done this way because in some situation we</span></div>
<div class="line"><a name="l00719"></a><span class="lineno"> 719</span>&#160; <span class="comment">// need to remember the previously taken decisions after a backtrack.</span></div>
<div class="line"><a name="l00720"></a><span class="lineno"> 720</span>&#160; <span class="keywordtype">int</span> current_decision_level_ = 0;</div>
<div class="line"><a name="l00721"></a><span class="lineno"> 721</span>&#160; std::vector&lt;Decision&gt; decisions_;</div>
<div class="line"><a name="l00722"></a><span class="lineno"> 722</span>&#160; </div>
<div class="line"><a name="l00723"></a><span class="lineno"> 723</span>&#160; <span class="comment">// The trail index after the last Backtrack() call or before the last</span></div>
<div class="line"><a name="l00724"></a><span class="lineno"> 724</span>&#160; <span class="comment">// EnqueueNewDecision() call.</span></div>
<div class="line"><a name="l00725"></a><span class="lineno"> 725</span>&#160; <span class="keywordtype">int</span> last_decision_or_backtrack_trail_index_ = 0;</div>
<div class="line"><a name="l00726"></a><span class="lineno"> 726</span>&#160; </div>
<div class="line"><a name="l00727"></a><span class="lineno"> 727</span>&#160; <span class="comment">// The assumption level. See SolveWithAssumptions().</span></div>
<div class="line"><a name="l00728"></a><span class="lineno"> 728</span>&#160; <span class="keywordtype">int</span> assumption_level_ = 0;</div>
<div class="line"><a name="l00729"></a><span class="lineno"> 729</span>&#160; </div>
<div class="line"><a name="l00730"></a><span class="lineno"> 730</span>&#160; <span class="comment">// The size of the trail when ProcessNewlyFixedVariables() was last called.</span></div>
<div class="line"><a name="l00731"></a><span class="lineno"> 731</span>&#160; <span class="comment">// Note that the trail contains only fixed literals (that is literals of</span></div>
<div class="line"><a name="l00732"></a><span class="lineno"> 732</span>&#160; <span class="comment">// decision levels 0) before this point.</span></div>
<div class="line"><a name="l00733"></a><span class="lineno"> 733</span>&#160; <span class="keywordtype">int</span> num_processed_fixed_variables_ = 0;</div>
<div class="line"><a name="l00734"></a><span class="lineno"> 734</span>&#160; <span class="keywordtype">double</span> deterministic_time_of_last_fixed_variables_cleanup_ = 0.0;</div>
<div class="line"><a name="l00735"></a><span class="lineno"> 735</span>&#160; </div>
<div class="line"><a name="l00736"></a><span class="lineno"> 736</span>&#160; <span class="comment">// Used in ProcessNewlyFixedVariablesForDratProof().</span></div>
<div class="line"><a name="l00737"></a><span class="lineno"> 737</span>&#160; <span class="keywordtype">int</span> drat_num_processed_fixed_variables_ = 0;</div>
<div class="line"><a name="l00738"></a><span class="lineno"> 738</span>&#160; </div>
<div class="line"><a name="l00739"></a><span class="lineno"> 739</span>&#160; <span class="comment">// Tracks various information about the solver progress.</span></div>
<div class="line"><a name="l00740"></a><span class="lineno"> 740</span>&#160; <span class="keyword">struct </span>Counters {</div>
<div class="line"><a name="l00741"></a><span class="lineno"> 741</span>&#160; <a class="code" href="integral__types_8h.html#a7cde0074dfd288f2d70c0e035dacb28a">int64</a> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a4fbc93ff66f372e1b604609fe5b45557">num_branches</a> = 0;</div>
<div class="line"><a name="l00742"></a><span class="lineno"> 742</span>&#160; <a class="code" href="integral__types_8h.html#a7cde0074dfd288f2d70c0e035dacb28a">int64</a> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a42c1fced0014f47ce16a512d454cee0f">num_failures</a> = 0;</div>
<div class="line"><a name="l00743"></a><span class="lineno"> 743</span>&#160; <a class="code" href="integral__types_8h.html#a7cde0074dfd288f2d70c0e035dacb28a">int64</a> <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a943e1a6b169c75c35c1f596b11fe4fc4">num_restarts</a> = 0;</div>
<div class="line"><a name="l00744"></a><span class="lineno"> 744</span>&#160; </div>
<div class="line"><a name="l00745"></a><span class="lineno"> 745</span>&#160; <span class="comment">// Minimization stats.</span></div>
<div class="line"><a name="l00746"></a><span class="lineno"> 746</span>&#160; <a class="code" href="integral__types_8h.html#a7cde0074dfd288f2d70c0e035dacb28a">int64</a> num_minimizations = 0;</div>
<div class="line"><a name="l00747"></a><span class="lineno"> 747</span>&#160; <a class="code" href="integral__types_8h.html#a7cde0074dfd288f2d70c0e035dacb28a">int64</a> num_literals_removed = 0;</div>
<div class="line"><a name="l00748"></a><span class="lineno"> 748</span>&#160; </div>
<div class="line"><a name="l00749"></a><span class="lineno"> 749</span>&#160; <span class="comment">// PB constraints.</span></div>
<div class="line"><a name="l00750"></a><span class="lineno"> 750</span>&#160; <a class="code" href="integral__types_8h.html#a7cde0074dfd288f2d70c0e035dacb28a">int64</a> num_learned_pb_literals = 0;</div>
<div class="line"><a name="l00751"></a><span class="lineno"> 751</span>&#160; </div>
<div class="line"><a name="l00752"></a><span class="lineno"> 752</span>&#160; <span class="comment">// Clause learning /deletion stats.</span></div>
<div class="line"><a name="l00753"></a><span class="lineno"> 753</span>&#160; <a class="code" href="integral__types_8h.html#a7cde0074dfd288f2d70c0e035dacb28a">int64</a> num_literals_learned = 0;</div>
<div class="line"><a name="l00754"></a><span class="lineno"> 754</span>&#160; <a class="code" href="integral__types_8h.html#a7cde0074dfd288f2d70c0e035dacb28a">int64</a> num_literals_forgotten = 0;</div>
<div class="line"><a name="l00755"></a><span class="lineno"> 755</span>&#160; <a class="code" href="integral__types_8h.html#a7cde0074dfd288f2d70c0e035dacb28a">int64</a> num_subsumed_clauses = 0;</div>
<div class="line"><a name="l00756"></a><span class="lineno"> 756</span>&#160; </div>
<div class="line"><a name="l00757"></a><span class="lineno"> 757</span>&#160; <span class="comment">// TryToMinimizeClause() stats.</span></div>
<div class="line"><a name="l00758"></a><span class="lineno"> 758</span>&#160; <a class="code" href="integral__types_8h.html#a7cde0074dfd288f2d70c0e035dacb28a">int64</a> minimization_num_clauses = 0;</div>
<div class="line"><a name="l00759"></a><span class="lineno"> 759</span>&#160; <a class="code" href="integral__types_8h.html#a7cde0074dfd288f2d70c0e035dacb28a">int64</a> minimization_num_decisions = 0;</div>
<div class="line"><a name="l00760"></a><span class="lineno"> 760</span>&#160; <a class="code" href="integral__types_8h.html#a7cde0074dfd288f2d70c0e035dacb28a">int64</a> minimization_num_true = 0;</div>
<div class="line"><a name="l00761"></a><span class="lineno"> 761</span>&#160; <a class="code" href="integral__types_8h.html#a7cde0074dfd288f2d70c0e035dacb28a">int64</a> minimization_num_subsumed = 0;</div>
<div class="line"><a name="l00762"></a><span class="lineno"> 762</span>&#160; <a class="code" href="integral__types_8h.html#a7cde0074dfd288f2d70c0e035dacb28a">int64</a> minimization_num_removed_literals = 0;</div>
<div class="line"><a name="l00763"></a><span class="lineno"> 763</span>&#160; };</div>
<div class="line"><a name="l00764"></a><span class="lineno"> 764</span>&#160; Counters counters_;</div>
<div class="line"><a name="l00765"></a><span class="lineno"> 765</span>&#160; </div>
<div class="line"><a name="l00766"></a><span class="lineno"> 766</span>&#160; <span class="comment">// Solver information.</span></div>
<div class="line"><a name="l00767"></a><span class="lineno"> 767</span>&#160; <a class="code" href="class_wall_timer.html">WallTimer</a> timer_;</div>
<div class="line"><a name="l00768"></a><span class="lineno"> 768</span>&#160; </div>
<div class="line"><a name="l00769"></a><span class="lineno"> 769</span>&#160; <span class="comment">// This is set to true if the model is found to be UNSAT when adding new</span></div>
<div class="line"><a name="l00770"></a><span class="lineno"> 770</span>&#160; <span class="comment">// constraints.</span></div>
<div class="line"><a name="l00771"></a><span class="lineno"> 771</span>&#160; <span class="keywordtype">bool</span> model_is_unsat_ = <span class="keyword">false</span>;</div>
<div class="line"><a name="l00772"></a><span class="lineno"> 772</span>&#160; </div>
<div class="line"><a name="l00773"></a><span class="lineno"> 773</span>&#160; <span class="comment">// Increment used to bump the variable activities.</span></div>
<div class="line"><a name="l00774"></a><span class="lineno"> 774</span>&#160; <span class="keywordtype">double</span> clause_activity_increment_;</div>
<div class="line"><a name="l00775"></a><span class="lineno"> 775</span>&#160; </div>
<div class="line"><a name="l00776"></a><span class="lineno"> 776</span>&#160; <span class="comment">// This counter is decremented each time we learn a clause that can be</span></div>
<div class="line"><a name="l00777"></a><span class="lineno"> 777</span>&#160; <span class="comment">// deleted. When it reaches zero, a clause cleanup is triggered.</span></div>
<div class="line"><a name="l00778"></a><span class="lineno"> 778</span>&#160; <span class="keywordtype">int</span> num_learned_clause_before_cleanup_ = 0;</div>
<div class="line"><a name="l00779"></a><span class="lineno"> 779</span>&#160; </div>
<div class="line"><a name="l00780"></a><span class="lineno"> 780</span>&#160; <span class="comment">// Temporary members used during conflict analysis.</span></div>
<div class="line"><a name="l00781"></a><span class="lineno"> 781</span>&#160; SparseBitset&lt;BooleanVariable&gt; is_marked_;</div>
<div class="line"><a name="l00782"></a><span class="lineno"> 782</span>&#160; SparseBitset&lt;BooleanVariable&gt; is_independent_;</div>
<div class="line"><a name="l00783"></a><span class="lineno"> 783</span>&#160; SparseBitset&lt;BooleanVariable&gt; tmp_mark_;</div>
<div class="line"><a name="l00784"></a><span class="lineno"> 784</span>&#160; std::vector&lt;int&gt; min_trail_index_per_level_;</div>
<div class="line"><a name="l00785"></a><span class="lineno"> 785</span>&#160; </div>
<div class="line"><a name="l00786"></a><span class="lineno"> 786</span>&#160; <span class="comment">// Temporary members used by CanBeInferedFromConflictVariables().</span></div>
<div class="line"><a name="l00787"></a><span class="lineno"> 787</span>&#160; std::vector&lt;BooleanVariable&gt; dfs_stack_;</div>
<div class="line"><a name="l00788"></a><span class="lineno"> 788</span>&#160; std::vector&lt;BooleanVariable&gt; variable_to_process_;</div>
<div class="line"><a name="l00789"></a><span class="lineno"> 789</span>&#160; </div>
<div class="line"><a name="l00790"></a><span class="lineno"> 790</span>&#160; <span class="comment">// Temporary member used by AddLinearConstraintInternal().</span></div>
<div class="line"><a name="l00791"></a><span class="lineno"> 791</span>&#160; std::vector&lt;Literal&gt; literals_scratchpad_;</div>
<div class="line"><a name="l00792"></a><span class="lineno"> 792</span>&#160; </div>
<div class="line"><a name="l00793"></a><span class="lineno"> 793</span>&#160; <span class="comment">// A boolean vector used to temporarily mark decision levels.</span></div>
<div class="line"><a name="l00794"></a><span class="lineno"> 794</span>&#160; DEFINE_INT_TYPE(SatDecisionLevel, <span class="keywordtype">int</span>);</div>
<div class="line"><a name="l00795"></a><span class="lineno"> 795</span>&#160; SparseBitset&lt;SatDecisionLevel&gt; is_level_marked_;</div>
<div class="line"><a name="l00796"></a><span class="lineno"> 796</span>&#160; </div>
<div class="line"><a name="l00797"></a><span class="lineno"> 797</span>&#160; <span class="comment">// Temporary vectors used by EnqueueDecisionAndBackjumpOnConflict().</span></div>
<div class="line"><a name="l00798"></a><span class="lineno"> 798</span>&#160; std::vector&lt;Literal&gt; learned_conflict_;</div>
<div class="line"><a name="l00799"></a><span class="lineno"> 799</span>&#160; std::vector&lt;Literal&gt; reason_used_to_infer_the_conflict_;</div>
<div class="line"><a name="l00800"></a><span class="lineno"> 800</span>&#160; std::vector&lt;Literal&gt; extra_reason_literals_;</div>
<div class="line"><a name="l00801"></a><span class="lineno"> 801</span>&#160; std::vector&lt;SatClause*&gt; subsumed_clauses_;</div>
<div class="line"><a name="l00802"></a><span class="lineno"> 802</span>&#160; </div>
<div class="line"><a name="l00803"></a><span class="lineno"> 803</span>&#160; <span class="comment">// When true, temporarily disable the deletion of clauses that are not needed</span></div>
<div class="line"><a name="l00804"></a><span class="lineno"> 804</span>&#160; <span class="comment">// anymore. This is a hack for TryToMinimizeClause() because we use</span></div>
<div class="line"><a name="l00805"></a><span class="lineno"> 805</span>&#160; <span class="comment">// propagation in this function which might trigger a clause database</span></div>
<div class="line"><a name="l00806"></a><span class="lineno"> 806</span>&#160; <span class="comment">// deletion, but we still want the pointer to the clause we wants to minimize</span></div>
<div class="line"><a name="l00807"></a><span class="lineno"> 807</span>&#160; <span class="comment">// to be valid until the end of that function.</span></div>
<div class="line"><a name="l00808"></a><span class="lineno"> 808</span>&#160; <span class="keywordtype">bool</span> block_clause_deletion_ = <span class="keyword">false</span>;</div>
<div class="line"><a name="l00809"></a><span class="lineno"> 809</span>&#160; </div>
<div class="line"><a name="l00810"></a><span class="lineno"> 810</span>&#160; <span class="comment">// &quot;cache&quot; to avoid inspecting many times the same reason during conflict</span></div>
<div class="line"><a name="l00811"></a><span class="lineno"> 811</span>&#160; <span class="comment">// analysis.</span></div>
<div class="line"><a name="l00812"></a><span class="lineno"> 812</span>&#160; VariableWithSameReasonIdentifier same_reason_identifier_;</div>
<div class="line"><a name="l00813"></a><span class="lineno"> 813</span>&#160; </div>
<div class="line"><a name="l00814"></a><span class="lineno"> 814</span>&#160; <span class="comment">// Temporary vector used by AddProblemClause().</span></div>
<div class="line"><a name="l00815"></a><span class="lineno"> 815</span>&#160; std::vector&lt;LiteralWithCoeff&gt; tmp_pb_constraint_;</div>
<div class="line"><a name="l00816"></a><span class="lineno"> 816</span>&#160; </div>
<div class="line"><a name="l00817"></a><span class="lineno"> 817</span>&#160; <span class="comment">// Boolean used to include/exclude constraints from the core computation.</span></div>
<div class="line"><a name="l00818"></a><span class="lineno"> 818</span>&#160; <span class="keywordtype">bool</span> is_relevant_for_core_computation_;</div>
<div class="line"><a name="l00819"></a><span class="lineno"> 819</span>&#160; </div>
<div class="line"><a name="l00820"></a><span class="lineno"> 820</span>&#160; <span class="comment">// The current pseudo-Boolean conflict used in PB conflict analysis.</span></div>
<div class="line"><a name="l00821"></a><span class="lineno"> 821</span>&#160; MutableUpperBoundedLinearConstraint pb_conflict_;</div>
<div class="line"><a name="l00822"></a><span class="lineno"> 822</span>&#160; </div>
<div class="line"><a name="l00823"></a><span class="lineno"> 823</span>&#160; <span class="comment">// The deterministic time when the time limit was updated.</span></div>
<div class="line"><a name="l00824"></a><span class="lineno"> 824</span>&#160; <span class="comment">// As the deterministic time in the time limit has to be advanced manually,</span></div>
<div class="line"><a name="l00825"></a><span class="lineno"> 825</span>&#160; <span class="comment">// it is necessary to keep track of the last time the time was advanced.</span></div>
<div class="line"><a name="l00826"></a><span class="lineno"> 826</span>&#160; <span class="keywordtype">double</span> deterministic_time_at_last_advanced_time_limit_ = 0;</div>
<div class="line"><a name="l00827"></a><span class="lineno"> 827</span>&#160; </div>
<div class="line"><a name="l00828"></a><span class="lineno"> 828</span>&#160; <span class="comment">// This is true iff the loaded problem only contains clauses.</span></div>
<div class="line"><a name="l00829"></a><span class="lineno"> 829</span>&#160; <span class="keywordtype">bool</span> problem_is_pure_sat_;</div>
<div class="line"><a name="l00830"></a><span class="lineno"> 830</span>&#160; </div>
<div class="line"><a name="l00831"></a><span class="lineno"> 831</span>&#160; DratProofHandler* drat_proof_handler_;</div>
<div class="line"><a name="l00832"></a><span class="lineno"> 832</span>&#160; </div>
<div class="line"><a name="l00833"></a><span class="lineno"> 833</span>&#160; <span class="keyword">mutable</span> StatsGroup stats_;</div>
<div class="line"><a name="l00834"></a><span class="lineno"> 834</span>&#160; DISALLOW_COPY_AND_ASSIGN(<a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#adc7569321b063bae82803229623c8f4f">SatSolver</a>);</div>
<div class="line"><a name="l00835"></a><span class="lineno"> 835</span>&#160;};</div>
<div class="line"><a name="l00836"></a><span class="lineno"> 836</span>&#160; </div>
<div class="line"><a name="l00837"></a><span class="lineno"> 837</span>&#160;<span class="comment">// Tries to minimize the given UNSAT core with a really simple heuristic.</span></div>
<div class="line"><a name="l00838"></a><span class="lineno"> 838</span>&#160;<span class="comment">// The idea is to remove literals that are consequences of others in the core.</span></div>
<div class="line"><a name="l00839"></a><span class="lineno"> 839</span>&#160;<span class="comment">// We already know that in the initial order, no literal is propagated by the</span></div>
<div class="line"><a name="l00840"></a><span class="lineno"> 840</span>&#160;<span class="comment">// one before it, so we just look for propagation in the reverse order.</span></div>
<div class="line"><a name="l00841"></a><span class="lineno"> 841</span>&#160;<span class="comment">//</span></div>
<div class="line"><a name="l00842"></a><span class="lineno"> 842</span>&#160;<span class="comment">// Important: The given SatSolver must be the one that just produced the given</span></div>
<div class="line"><a name="l00843"></a><span class="lineno"> 843</span>&#160;<span class="comment">// core.</span></div>
<div class="line"><a name="l00844"></a><span class="lineno"> 844</span>&#160;<span class="keywordtype">void</span> <a class="code" href="namespaceoperations__research_1_1sat.html#a6fb8349259fa849de0789a4ec58a8492">MinimizeCore</a>(SatSolver* solver, std::vector&lt;Literal&gt;* core);</div>
<div class="line"><a name="l00845"></a><span class="lineno"> 845</span>&#160; </div>
<div class="line"><a name="l00846"></a><span class="lineno"> 846</span>&#160;<span class="comment">// ============================================================================</span></div>
<div class="line"><a name="l00847"></a><span class="lineno"> 847</span>&#160;<span class="comment">// Model based functions.</span></div>
<div class="line"><a name="l00848"></a><span class="lineno"> 848</span>&#160;<span class="comment">//</span></div>
<div class="line"><a name="l00849"></a><span class="lineno"> 849</span>&#160;<span class="comment">// TODO(user): move them in another file, and unit-test them.</span></div>
<div class="line"><a name="l00850"></a><span class="lineno"> 850</span>&#160;<span class="comment">// ============================================================================</span></div>
<div class="line"><a name="l00851"></a><span class="lineno"> 851</span>&#160; </div>
<div class="line"><a name="l00852"></a><span class="lineno"><a class="line" href="namespaceoperations__research_1_1sat.html#a5671353b0876a1d63e61414bd02f1081"> 852</a></span>&#160;<span class="keyword">inline</span> std::function&lt;void(<a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>*)&gt; <a class="code" href="namespaceoperations__research_1_1sat.html#a5671353b0876a1d63e61414bd02f1081">BooleanLinearConstraint</a>(</div>
<div class="line"><a name="l00853"></a><span class="lineno"> 853</span>&#160; <a class="code" href="integral__types_8h.html#a7cde0074dfd288f2d70c0e035dacb28a">int64</a> lower_bound, <a class="code" href="integral__types_8h.html#a7cde0074dfd288f2d70c0e035dacb28a">int64</a> upper_bound, std::vector&lt;LiteralWithCoeff&gt;* cst) {</div>
<div class="line"><a name="l00854"></a><span class="lineno"> 854</span>&#160; <span class="keywordflow">return</span> [=](<a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>* <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>) {</div>
<div class="line"><a name="l00855"></a><span class="lineno"> 855</span>&#160; <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>-&gt;GetOrCreate&lt;<a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html">SatSolver</a>&gt;()-&gt;AddLinearConstraint(</div>
<div class="line"><a name="l00856"></a><span class="lineno"> 856</span>&#160; <span class="comment">/*use_lower_bound=*/</span><span class="keyword">true</span>, Coefficient(lower_bound),</div>
<div class="line"><a name="l00857"></a><span class="lineno"> 857</span>&#160; <span class="comment">/*use_upper_bound=*/</span><span class="keyword">true</span>, Coefficient(upper_bound), cst);</div>
<div class="line"><a name="l00858"></a><span class="lineno"> 858</span>&#160; };</div>
<div class="line"><a name="l00859"></a><span class="lineno"> 859</span>&#160;}</div>
<div class="line"><a name="l00860"></a><span class="lineno"> 860</span>&#160; </div>
<div class="line"><a name="l00861"></a><span class="lineno"><a class="line" href="namespaceoperations__research_1_1sat.html#ae51e64bd361f6b51d7d35a62aad28f03"> 861</a></span>&#160;<span class="keyword">inline</span> std::function&lt;void(<a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>*)&gt; <a class="code" href="namespaceoperations__research_1_1sat.html#ae51e64bd361f6b51d7d35a62aad28f03">CardinalityConstraint</a>(</div>
<div class="line"><a name="l00862"></a><span class="lineno"> 862</span>&#160; <a class="code" href="integral__types_8h.html#a7cde0074dfd288f2d70c0e035dacb28a">int64</a> lower_bound, <a class="code" href="integral__types_8h.html#a7cde0074dfd288f2d70c0e035dacb28a">int64</a> upper_bound,</div>
<div class="line"><a name="l00863"></a><span class="lineno"> 863</span>&#160; <span class="keyword">const</span> std::vector&lt;Literal&gt;&amp; literals) {</div>
<div class="line"><a name="l00864"></a><span class="lineno"> 864</span>&#160; <span class="keywordflow">return</span> [=](<a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>* <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>) {</div>
<div class="line"><a name="l00865"></a><span class="lineno"> 865</span>&#160; std::vector&lt;LiteralWithCoeff&gt; cst;</div>
<div class="line"><a name="l00866"></a><span class="lineno"> 866</span>&#160; cst.reserve(literals.size());</div>
<div class="line"><a name="l00867"></a><span class="lineno"> 867</span>&#160; <span class="keywordflow">for</span> (<span class="keywordtype">int</span> i = 0; i &lt; literals.size(); ++i) {</div>
<div class="line"><a name="l00868"></a><span class="lineno"> 868</span>&#160; cst.emplace_back(literals[i], 1);</div>
<div class="line"><a name="l00869"></a><span class="lineno"> 869</span>&#160; }</div>
<div class="line"><a name="l00870"></a><span class="lineno"> 870</span>&#160; <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>-&gt;GetOrCreate&lt;<a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html">SatSolver</a>&gt;()-&gt;AddLinearConstraint(</div>
<div class="line"><a name="l00871"></a><span class="lineno"> 871</span>&#160; <span class="comment">/*use_lower_bound=*/</span><span class="keyword">true</span>, Coefficient(lower_bound),</div>
<div class="line"><a name="l00872"></a><span class="lineno"> 872</span>&#160; <span class="comment">/*use_upper_bound=*/</span><span class="keyword">true</span>, Coefficient(upper_bound), &amp;cst);</div>
<div class="line"><a name="l00873"></a><span class="lineno"> 873</span>&#160; };</div>
<div class="line"><a name="l00874"></a><span class="lineno"> 874</span>&#160;}</div>
<div class="line"><a name="l00875"></a><span class="lineno"> 875</span>&#160; </div>
<div class="line"><a name="l00876"></a><span class="lineno"><a class="line" href="namespaceoperations__research_1_1sat.html#a1b1462c55662c1263c0e1f54ed6e06cd"> 876</a></span>&#160;<span class="keyword">inline</span> std::function&lt;void(<a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>*)&gt; <a class="code" href="namespaceoperations__research_1_1sat.html#a1b1462c55662c1263c0e1f54ed6e06cd">ExactlyOneConstraint</a>(</div>
<div class="line"><a name="l00877"></a><span class="lineno"> 877</span>&#160; <span class="keyword">const</span> std::vector&lt;Literal&gt;&amp; literals) {</div>
<div class="line"><a name="l00878"></a><span class="lineno"> 878</span>&#160; <span class="keywordflow">return</span> [=](<a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>* <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>) {</div>
<div class="line"><a name="l00879"></a><span class="lineno"> 879</span>&#160; std::vector&lt;LiteralWithCoeff&gt; cst;</div>
<div class="line"><a name="l00880"></a><span class="lineno"> 880</span>&#160; cst.reserve(literals.size());</div>
<div class="line"><a name="l00881"></a><span class="lineno"> 881</span>&#160; <span class="keywordflow">for</span> (<span class="keyword">const</span> <a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> l : literals) {</div>
<div class="line"><a name="l00882"></a><span class="lineno"> 882</span>&#160; cst.emplace_back(l, Coefficient(1));</div>
<div class="line"><a name="l00883"></a><span class="lineno"> 883</span>&#160; }</div>
<div class="line"><a name="l00884"></a><span class="lineno"> 884</span>&#160; <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>-&gt;GetOrCreate&lt;<a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html">SatSolver</a>&gt;()-&gt;AddLinearConstraint(</div>
<div class="line"><a name="l00885"></a><span class="lineno"> 885</span>&#160; <span class="comment">/*use_lower_bound=*/</span><span class="keyword">true</span>, Coefficient(1),</div>
<div class="line"><a name="l00886"></a><span class="lineno"> 886</span>&#160; <span class="comment">/*use_upper_bound=*/</span><span class="keyword">true</span>, Coefficient(1), &amp;cst);</div>
<div class="line"><a name="l00887"></a><span class="lineno"> 887</span>&#160; };</div>
<div class="line"><a name="l00888"></a><span class="lineno"> 888</span>&#160;}</div>
<div class="line"><a name="l00889"></a><span class="lineno"> 889</span>&#160; </div>
<div class="line"><a name="l00890"></a><span class="lineno"><a class="line" href="namespaceoperations__research_1_1sat.html#ab8221efb0cc3dd5059674845b4db7fed"> 890</a></span>&#160;<span class="keyword">inline</span> std::function&lt;void(<a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>*)&gt; <a class="code" href="namespaceoperations__research_1_1sat.html#ab8221efb0cc3dd5059674845b4db7fed">AtMostOneConstraint</a>(</div>
<div class="line"><a name="l00891"></a><span class="lineno"> 891</span>&#160; <span class="keyword">const</span> std::vector&lt;Literal&gt;&amp; literals) {</div>
<div class="line"><a name="l00892"></a><span class="lineno"> 892</span>&#160; <span class="keywordflow">return</span> [=](<a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>* <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>) {</div>
<div class="line"><a name="l00893"></a><span class="lineno"> 893</span>&#160; std::vector&lt;LiteralWithCoeff&gt; cst;</div>
<div class="line"><a name="l00894"></a><span class="lineno"> 894</span>&#160; cst.reserve(literals.size());</div>
<div class="line"><a name="l00895"></a><span class="lineno"> 895</span>&#160; <span class="keywordflow">for</span> (<span class="keyword">const</span> <a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> l : literals) {</div>
<div class="line"><a name="l00896"></a><span class="lineno"> 896</span>&#160; cst.emplace_back(l, Coefficient(1));</div>
<div class="line"><a name="l00897"></a><span class="lineno"> 897</span>&#160; }</div>
<div class="line"><a name="l00898"></a><span class="lineno"> 898</span>&#160; <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>-&gt;GetOrCreate&lt;<a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html">SatSolver</a>&gt;()-&gt;AddLinearConstraint(</div>
<div class="line"><a name="l00899"></a><span class="lineno"> 899</span>&#160; <span class="comment">/*use_lower_bound=*/</span><span class="keyword">false</span>, Coefficient(0),</div>
<div class="line"><a name="l00900"></a><span class="lineno"> 900</span>&#160; <span class="comment">/*use_upper_bound=*/</span><span class="keyword">true</span>, Coefficient(1), &amp;cst);</div>
<div class="line"><a name="l00901"></a><span class="lineno"> 901</span>&#160; };</div>
<div class="line"><a name="l00902"></a><span class="lineno"> 902</span>&#160;}</div>
<div class="line"><a name="l00903"></a><span class="lineno"> 903</span>&#160; </div>
<div class="line"><a name="l00904"></a><span class="lineno"><a class="line" href="namespaceoperations__research_1_1sat.html#a1655a9b9673e7c4de940ca6e5e3cf936"> 904</a></span>&#160;<span class="keyword">inline</span> std::function&lt;void(<a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>*)&gt; <a class="code" href="namespaceoperations__research_1_1sat.html#a1655a9b9673e7c4de940ca6e5e3cf936">ClauseConstraint</a>(</div>
<div class="line"><a name="l00905"></a><span class="lineno"> 905</span>&#160; absl::Span&lt;const Literal&gt; literals) {</div>
<div class="line"><a name="l00906"></a><span class="lineno"> 906</span>&#160; <span class="keywordflow">return</span> [=](<a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>* <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>) {</div>
<div class="line"><a name="l00907"></a><span class="lineno"> 907</span>&#160; std::vector&lt;LiteralWithCoeff&gt; cst;</div>
<div class="line"><a name="l00908"></a><span class="lineno"> 908</span>&#160; cst.reserve(literals.size());</div>
<div class="line"><a name="l00909"></a><span class="lineno"> 909</span>&#160; <span class="keywordflow">for</span> (<span class="keyword">const</span> <a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> l : literals) {</div>
<div class="line"><a name="l00910"></a><span class="lineno"> 910</span>&#160; cst.emplace_back(l, Coefficient(1));</div>
<div class="line"><a name="l00911"></a><span class="lineno"> 911</span>&#160; }</div>
<div class="line"><a name="l00912"></a><span class="lineno"> 912</span>&#160; <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>-&gt;GetOrCreate&lt;<a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html">SatSolver</a>&gt;()-&gt;AddLinearConstraint(</div>
<div class="line"><a name="l00913"></a><span class="lineno"> 913</span>&#160; <span class="comment">/*use_lower_bound=*/</span><span class="keyword">true</span>, Coefficient(1),</div>
<div class="line"><a name="l00914"></a><span class="lineno"> 914</span>&#160; <span class="comment">/*use_upper_bound=*/</span><span class="keyword">false</span>, Coefficient(1), &amp;cst);</div>
<div class="line"><a name="l00915"></a><span class="lineno"> 915</span>&#160; };</div>
<div class="line"><a name="l00916"></a><span class="lineno"> 916</span>&#160;}</div>
<div class="line"><a name="l00917"></a><span class="lineno"> 917</span>&#160; </div>
<div class="line"><a name="l00918"></a><span class="lineno"> 918</span>&#160;<span class="comment">// a =&gt; b.</span></div>
<div class="line"><a name="l00919"></a><span class="lineno"><a class="line" href="namespaceoperations__research_1_1sat.html#af84263389dc692dc91b26e4c28193344"> 919</a></span>&#160;<span class="keyword">inline</span> std::function&lt;void(<a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>*)&gt; <a class="code" href="namespaceoperations__research_1_1sat.html#a8a0620c105ec05f1b42bcde3a9380872">Implication</a>(<a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> <a class="code" href="constraint__solver_2table_8cc.html#af730895c6c6ef6e03caaf6251192dfd2">a</a>, <a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> <a class="code" href="constraint__solver_2table_8cc.html#a344010e26426d6a13411648d988bc9b6">b</a>) {</div>
<div class="line"><a name="l00920"></a><span class="lineno"> 920</span>&#160; <span class="keywordflow">return</span> [=](<a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>* <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>) {</div>
<div class="line"><a name="l00921"></a><span class="lineno"> 921</span>&#160; <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>-&gt;GetOrCreate&lt;<a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html">SatSolver</a>&gt;()-&gt;AddBinaryClause(<a class="code" href="constraint__solver_2table_8cc.html#af730895c6c6ef6e03caaf6251192dfd2">a</a>.Negated(), <a class="code" href="constraint__solver_2table_8cc.html#a344010e26426d6a13411648d988bc9b6">b</a>);</div>
<div class="line"><a name="l00922"></a><span class="lineno"> 922</span>&#160; };</div>
<div class="line"><a name="l00923"></a><span class="lineno"> 923</span>&#160;}</div>
<div class="line"><a name="l00924"></a><span class="lineno"> 924</span>&#160; </div>
<div class="line"><a name="l00925"></a><span class="lineno"> 925</span>&#160;<span class="comment">// a == b.</span></div>
<div class="line"><a name="l00926"></a><span class="lineno"><a class="line" href="namespaceoperations__research_1_1sat.html#a1908a0387e0ab86d63d3f08f32f7dc8f"> 926</a></span>&#160;<span class="keyword">inline</span> std::function&lt;void(<a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>*)&gt; <a class="code" href="namespaceoperations__research_1_1sat.html#a607ba8d18e00b2e6dbdc8622bb74fdf5">Equality</a>(<a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> <a class="code" href="constraint__solver_2table_8cc.html#af730895c6c6ef6e03caaf6251192dfd2">a</a>, <a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> <a class="code" href="constraint__solver_2table_8cc.html#a344010e26426d6a13411648d988bc9b6">b</a>) {</div>
<div class="line"><a name="l00927"></a><span class="lineno"> 927</span>&#160; <span class="keywordflow">return</span> [=](<a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>* <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>) {</div>
<div class="line"><a name="l00928"></a><span class="lineno"> 928</span>&#160; <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>-&gt;GetOrCreate&lt;<a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html">SatSolver</a>&gt;()-&gt;AddBinaryClause(<a class="code" href="constraint__solver_2table_8cc.html#af730895c6c6ef6e03caaf6251192dfd2">a</a>.Negated(), <a class="code" href="constraint__solver_2table_8cc.html#a344010e26426d6a13411648d988bc9b6">b</a>);</div>
<div class="line"><a name="l00929"></a><span class="lineno"> 929</span>&#160; <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>-&gt;GetOrCreate&lt;<a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html">SatSolver</a>&gt;()-&gt;AddBinaryClause(<a class="code" href="constraint__solver_2table_8cc.html#af730895c6c6ef6e03caaf6251192dfd2">a</a>, <a class="code" href="constraint__solver_2table_8cc.html#a344010e26426d6a13411648d988bc9b6">b</a>.Negated());</div>
<div class="line"><a name="l00930"></a><span class="lineno"> 930</span>&#160; };</div>
<div class="line"><a name="l00931"></a><span class="lineno"> 931</span>&#160;}</div>
<div class="line"><a name="l00932"></a><span class="lineno"> 932</span>&#160; </div>
<div class="line"><a name="l00933"></a><span class="lineno"> 933</span>&#160;<span class="comment">// r &lt;=&gt; (at least one literal is true). This is a reified clause.</span></div>
<div class="line"><a name="l00934"></a><span class="lineno"><a class="line" href="namespaceoperations__research_1_1sat.html#affc20db163dca7cacfb4aa97cf8d72b9"> 934</a></span>&#160;<span class="keyword">inline</span> std::function&lt;void(<a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>*)&gt; <a class="code" href="namespaceoperations__research_1_1sat.html#affc20db163dca7cacfb4aa97cf8d72b9">ReifiedBoolOr</a>(</div>
<div class="line"><a name="l00935"></a><span class="lineno"> 935</span>&#160; <span class="keyword">const</span> std::vector&lt;Literal&gt;&amp; literals, <a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> r) {</div>
<div class="line"><a name="l00936"></a><span class="lineno"> 936</span>&#160; <span class="keywordflow">return</span> [=](<a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>* <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>) {</div>
<div class="line"><a name="l00937"></a><span class="lineno"> 937</span>&#160; std::vector&lt;Literal&gt; clause;</div>
<div class="line"><a name="l00938"></a><span class="lineno"> 938</span>&#160; <span class="keywordflow">for</span> (<span class="keyword">const</span> <a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> l : literals) {</div>
<div class="line"><a name="l00939"></a><span class="lineno"> 939</span>&#160; <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>-&gt;Add(<a class="code" href="namespaceoperations__research_1_1sat.html#a8a0620c105ec05f1b42bcde3a9380872">Implication</a>(l, r)); <span class="comment">// l =&gt; r.</span></div>
<div class="line"><a name="l00940"></a><span class="lineno"> 940</span>&#160; clause.push_back(l);</div>
<div class="line"><a name="l00941"></a><span class="lineno"> 941</span>&#160; }</div>
<div class="line"><a name="l00942"></a><span class="lineno"> 942</span>&#160; </div>
<div class="line"><a name="l00943"></a><span class="lineno"> 943</span>&#160; <span class="comment">// All false =&gt; r false.</span></div>
<div class="line"><a name="l00944"></a><span class="lineno"> 944</span>&#160; clause.push_back(r.<a class="code" href="classoperations__research_1_1sat_1_1_literal.html#a886e9c024f7209181c0a850b6e90c644">Negated</a>());</div>
<div class="line"><a name="l00945"></a><span class="lineno"> 945</span>&#160; <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>-&gt;Add(<a class="code" href="namespaceoperations__research_1_1sat.html#a1655a9b9673e7c4de940ca6e5e3cf936">ClauseConstraint</a>(clause));</div>
<div class="line"><a name="l00946"></a><span class="lineno"> 946</span>&#160; };</div>
<div class="line"><a name="l00947"></a><span class="lineno"> 947</span>&#160;}</div>
<div class="line"><a name="l00948"></a><span class="lineno"> 948</span>&#160; </div>
<div class="line"><a name="l00949"></a><span class="lineno"> 949</span>&#160;<span class="comment">// enforcement_literals =&gt; clause.</span></div>
<div class="line"><a name="l00950"></a><span class="lineno"><a class="line" href="namespaceoperations__research_1_1sat.html#a64b1b8d5018080ad3e7dd7eb6df42274"> 950</a></span>&#160;<span class="keyword">inline</span> std::function&lt;void(<a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>*)&gt; <a class="code" href="namespaceoperations__research_1_1sat.html#a64b1b8d5018080ad3e7dd7eb6df42274">EnforcedClause</a>(</div>
<div class="line"><a name="l00951"></a><span class="lineno"> 951</span>&#160; absl::Span&lt;const Literal&gt; enforcement_literals,</div>
<div class="line"><a name="l00952"></a><span class="lineno"> 952</span>&#160; absl::Span&lt;const Literal&gt; clause) {</div>
<div class="line"><a name="l00953"></a><span class="lineno"> 953</span>&#160; <span class="keywordflow">return</span> [=](<a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>* <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>) {</div>
<div class="line"><a name="l00954"></a><span class="lineno"> 954</span>&#160; std::vector&lt;Literal&gt; tmp;</div>
<div class="line"><a name="l00955"></a><span class="lineno"> 955</span>&#160; <span class="keywordflow">for</span> (<span class="keyword">const</span> <a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> l : enforcement_literals) {</div>
<div class="line"><a name="l00956"></a><span class="lineno"> 956</span>&#160; tmp.push_back(l.Negated());</div>
<div class="line"><a name="l00957"></a><span class="lineno"> 957</span>&#160; }</div>
<div class="line"><a name="l00958"></a><span class="lineno"> 958</span>&#160; <span class="keywordflow">for</span> (<span class="keyword">const</span> <a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> l : clause) {</div>
<div class="line"><a name="l00959"></a><span class="lineno"> 959</span>&#160; tmp.push_back(l);</div>
<div class="line"><a name="l00960"></a><span class="lineno"> 960</span>&#160; }</div>
<div class="line"><a name="l00961"></a><span class="lineno"> 961</span>&#160; <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>-&gt;Add(<a class="code" href="namespaceoperations__research_1_1sat.html#a1655a9b9673e7c4de940ca6e5e3cf936">ClauseConstraint</a>(tmp));</div>
<div class="line"><a name="l00962"></a><span class="lineno"> 962</span>&#160; };</div>
<div class="line"><a name="l00963"></a><span class="lineno"> 963</span>&#160;}</div>
<div class="line"><a name="l00964"></a><span class="lineno"> 964</span>&#160; </div>
<div class="line"><a name="l00965"></a><span class="lineno"> 965</span>&#160;<span class="comment">// r &lt;=&gt; (all literals are true).</span></div>
<div class="line"><a name="l00966"></a><span class="lineno"> 966</span>&#160;<span class="comment">//</span></div>
<div class="line"><a name="l00967"></a><span class="lineno"> 967</span>&#160;<span class="comment">// Note(user): we could have called ReifiedBoolOr() with everything negated.</span></div>
<div class="line"><a name="l00968"></a><span class="lineno"><a class="line" href="namespaceoperations__research_1_1sat.html#aa874aee040980146062498b87e8fb956"> 968</a></span>&#160;<span class="keyword">inline</span> std::function&lt;void(<a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>*)&gt; <a class="code" href="namespaceoperations__research_1_1sat.html#aa874aee040980146062498b87e8fb956">ReifiedBoolAnd</a>(</div>
<div class="line"><a name="l00969"></a><span class="lineno"> 969</span>&#160; <span class="keyword">const</span> std::vector&lt;Literal&gt;&amp; literals, <a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> r) {</div>
<div class="line"><a name="l00970"></a><span class="lineno"> 970</span>&#160; <span class="keywordflow">return</span> [=](<a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>* <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>) {</div>
<div class="line"><a name="l00971"></a><span class="lineno"> 971</span>&#160; std::vector&lt;Literal&gt; clause;</div>
<div class="line"><a name="l00972"></a><span class="lineno"> 972</span>&#160; <span class="keywordflow">for</span> (<span class="keyword">const</span> <a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> l : literals) {</div>
<div class="line"><a name="l00973"></a><span class="lineno"> 973</span>&#160; <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>-&gt;Add(<a class="code" href="namespaceoperations__research_1_1sat.html#a8a0620c105ec05f1b42bcde3a9380872">Implication</a>(r, l)); <span class="comment">// r =&gt; l.</span></div>
<div class="line"><a name="l00974"></a><span class="lineno"> 974</span>&#160; clause.push_back(l.Negated());</div>
<div class="line"><a name="l00975"></a><span class="lineno"> 975</span>&#160; }</div>
<div class="line"><a name="l00976"></a><span class="lineno"> 976</span>&#160; </div>
<div class="line"><a name="l00977"></a><span class="lineno"> 977</span>&#160; <span class="comment">// All true =&gt; r true.</span></div>
<div class="line"><a name="l00978"></a><span class="lineno"> 978</span>&#160; clause.push_back(r);</div>
<div class="line"><a name="l00979"></a><span class="lineno"> 979</span>&#160; <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>-&gt;Add(<a class="code" href="namespaceoperations__research_1_1sat.html#a1655a9b9673e7c4de940ca6e5e3cf936">ClauseConstraint</a>(clause));</div>
<div class="line"><a name="l00980"></a><span class="lineno"> 980</span>&#160; };</div>
<div class="line"><a name="l00981"></a><span class="lineno"> 981</span>&#160;}</div>
<div class="line"><a name="l00982"></a><span class="lineno"> 982</span>&#160; </div>
<div class="line"><a name="l00983"></a><span class="lineno"> 983</span>&#160;<span class="comment">// r &lt;=&gt; (a &lt;= b).</span></div>
<div class="line"><a name="l00984"></a><span class="lineno"><a class="line" href="namespaceoperations__research_1_1sat.html#a0435d9a6682ddb54c3942024ede20346"> 984</a></span>&#160;<span class="keyword">inline</span> std::function&lt;void(<a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>*)&gt; <a class="code" href="namespaceoperations__research_1_1sat.html#a0435d9a6682ddb54c3942024ede20346">ReifiedBoolLe</a>(<a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> <a class="code" href="constraint__solver_2table_8cc.html#af730895c6c6ef6e03caaf6251192dfd2">a</a>, <a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> <a class="code" href="constraint__solver_2table_8cc.html#a344010e26426d6a13411648d988bc9b6">b</a>,</div>
<div class="line"><a name="l00985"></a><span class="lineno"> 985</span>&#160; <a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> r) {</div>
<div class="line"><a name="l00986"></a><span class="lineno"> 986</span>&#160; <span class="keywordflow">return</span> [=](<a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>* <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>) {</div>
<div class="line"><a name="l00987"></a><span class="lineno"> 987</span>&#160; <span class="comment">// r &lt;=&gt; (a &lt;= b) is the same as r &lt;=&gt; not(a=1 and b=0).</span></div>
<div class="line"><a name="l00988"></a><span class="lineno"> 988</span>&#160; <span class="comment">// So r &lt;=&gt; a=0 OR b=1.</span></div>
<div class="line"><a name="l00989"></a><span class="lineno"> 989</span>&#160; <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>-&gt;Add(<a class="code" href="namespaceoperations__research_1_1sat.html#affc20db163dca7cacfb4aa97cf8d72b9">ReifiedBoolOr</a>({<a class="code" href="constraint__solver_2table_8cc.html#af730895c6c6ef6e03caaf6251192dfd2">a</a>.Negated(), <a class="code" href="constraint__solver_2table_8cc.html#a344010e26426d6a13411648d988bc9b6">b</a>}, r));</div>
<div class="line"><a name="l00990"></a><span class="lineno"> 990</span>&#160; };</div>
<div class="line"><a name="l00991"></a><span class="lineno"> 991</span>&#160;}</div>
<div class="line"><a name="l00992"></a><span class="lineno"> 992</span>&#160; </div>
<div class="line"><a name="l00993"></a><span class="lineno"> 993</span>&#160;<span class="comment">// This checks that the variable is fixed.</span></div>
<div class="line"><a name="l00994"></a><span class="lineno"><a class="line" href="namespaceoperations__research_1_1sat.html#aa151820d71fb7d412c8e2a46ea2d6256"> 994</a></span>&#160;<span class="keyword">inline</span> std::function&lt;<a class="code" href="integral__types_8h.html#a7cde0074dfd288f2d70c0e035dacb28a">int64</a>(<span class="keyword">const</span> <a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>&amp;)&gt; <a class="code" href="namespaceoperations__research_1_1sat.html#a3f1a1b8a7a1a488e263a2e74f45d2a59">Value</a>(<a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a> l) {</div>
<div class="line"><a name="l00995"></a><span class="lineno"> 995</span>&#160; <span class="keywordflow">return</span> [=](<span class="keyword">const</span> <a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>&amp; <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>) {</div>
<div class="line"><a name="l00996"></a><span class="lineno"> 996</span>&#160; <span class="keyword">const</span> <a class="code" href="classoperations__research_1_1sat_1_1_trail.html">Trail</a>* trail = <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>.Get&lt;<a class="code" href="classoperations__research_1_1sat_1_1_trail.html">Trail</a>&gt;();</div>
<div class="line"><a name="l00997"></a><span class="lineno"> 997</span>&#160; <a class="code" href="base_2logging_8h.html#a3e1cfef60e774a81f30eaddf26a3a274">CHECK</a>(trail-&gt;<a class="code" href="classoperations__research_1_1sat_1_1_trail.html#a9789bf03dba611e9be5679d6e902d0c8">Assignment</a>().<a class="code" href="classoperations__research_1_1sat_1_1_variables_assignment.html#a49e751eb6f0e9babd957889bb8e7472d">VariableIsAssigned</a>(l.<a class="code" href="classoperations__research_1_1sat_1_1_literal.html#a6a5dcff82096cd7a7147bf996dbaa5a8">Variable</a>()));</div>
<div class="line"><a name="l00998"></a><span class="lineno"> 998</span>&#160; <span class="keywordflow">return</span> trail-&gt;<a class="code" href="classoperations__research_1_1sat_1_1_trail.html#a9789bf03dba611e9be5679d6e902d0c8">Assignment</a>().<a class="code" href="classoperations__research_1_1sat_1_1_variables_assignment.html#a5300129913f51dcb0b1c531e3248490e">LiteralIsTrue</a>(l);</div>
<div class="line"><a name="l00999"></a><span class="lineno"> 999</span>&#160; };</div>
<div class="line"><a name="l01000"></a><span class="lineno"> 1000</span>&#160;}</div>
<div class="line"><a name="l01001"></a><span class="lineno"> 1001</span>&#160; </div>
<div class="line"><a name="l01002"></a><span class="lineno"> 1002</span>&#160;<span class="comment">// This checks that the variable is fixed.</span></div>
<div class="line"><a name="l01003"></a><span class="lineno"><a class="line" href="namespaceoperations__research_1_1sat.html#a63ce4e5357af736d38ff8571ba32225c"> 1003</a></span>&#160;<span class="keyword">inline</span> std::function&lt;<a class="code" href="integral__types_8h.html#a7cde0074dfd288f2d70c0e035dacb28a">int64</a>(<span class="keyword">const</span> <a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>&amp;)&gt; <a class="code" href="namespaceoperations__research_1_1sat.html#a3f1a1b8a7a1a488e263a2e74f45d2a59">Value</a>(BooleanVariable <a class="code" href="constraint__solver_2table_8cc.html#a344010e26426d6a13411648d988bc9b6">b</a>) {</div>
<div class="line"><a name="l01004"></a><span class="lineno"> 1004</span>&#160; <span class="keywordflow">return</span> [=](<span class="keyword">const</span> <a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>&amp; <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>) {</div>
<div class="line"><a name="l01005"></a><span class="lineno"> 1005</span>&#160; <span class="keyword">const</span> <a class="code" href="classoperations__research_1_1sat_1_1_trail.html">Trail</a>* trail = <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>.Get&lt;<a class="code" href="classoperations__research_1_1sat_1_1_trail.html">Trail</a>&gt;();</div>
<div class="line"><a name="l01006"></a><span class="lineno"> 1006</span>&#160; <a class="code" href="base_2logging_8h.html#a3e1cfef60e774a81f30eaddf26a3a274">CHECK</a>(trail-&gt;<a class="code" href="classoperations__research_1_1sat_1_1_trail.html#a9789bf03dba611e9be5679d6e902d0c8">Assignment</a>().<a class="code" href="classoperations__research_1_1sat_1_1_variables_assignment.html#a49e751eb6f0e9babd957889bb8e7472d">VariableIsAssigned</a>(<a class="code" href="constraint__solver_2table_8cc.html#a344010e26426d6a13411648d988bc9b6">b</a>));</div>
<div class="line"><a name="l01007"></a><span class="lineno"> 1007</span>&#160; <span class="keywordflow">return</span> trail-&gt;<a class="code" href="classoperations__research_1_1sat_1_1_trail.html#a9789bf03dba611e9be5679d6e902d0c8">Assignment</a>().<a class="code" href="classoperations__research_1_1sat_1_1_variables_assignment.html#a5300129913f51dcb0b1c531e3248490e">LiteralIsTrue</a>(<a class="code" href="classoperations__research_1_1sat_1_1_literal.html">Literal</a>(<a class="code" href="constraint__solver_2table_8cc.html#a344010e26426d6a13411648d988bc9b6">b</a>, <span class="keyword">true</span>));</div>
<div class="line"><a name="l01008"></a><span class="lineno"> 1008</span>&#160; };</div>
<div class="line"><a name="l01009"></a><span class="lineno"> 1009</span>&#160;}</div>
<div class="line"><a name="l01010"></a><span class="lineno"> 1010</span>&#160; </div>
<div class="line"><a name="l01011"></a><span class="lineno"> 1011</span>&#160;<span class="comment">// This can be used to enumerate all the solutions. After each SAT call to</span></div>
<div class="line"><a name="l01012"></a><span class="lineno"> 1012</span>&#160;<span class="comment">// Solve(), calling this will reset the solver and exclude the current solution</span></div>
<div class="line"><a name="l01013"></a><span class="lineno"> 1013</span>&#160;<span class="comment">// so that the next call to Solve() will give a new solution or UNSAT is there</span></div>
<div class="line"><a name="l01014"></a><span class="lineno"> 1014</span>&#160;<span class="comment">// is no more new solutions.</span></div>
<div class="line"><a name="l01015"></a><span class="lineno"><a class="line" href="namespaceoperations__research_1_1sat.html#a111954e38f31aadd4d5bd3e41741bfce"> 1015</a></span>&#160;<span class="keyword">inline</span> std::function&lt;void(<a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>*)&gt; <a class="code" href="namespaceoperations__research_1_1sat.html#a111954e38f31aadd4d5bd3e41741bfce">ExcludeCurrentSolutionAndBacktrack</a>() {</div>
<div class="line"><a name="l01016"></a><span class="lineno"> 1016</span>&#160; <span class="keywordflow">return</span> [=](<a class="code" href="classoperations__research_1_1sat_1_1_model.html">Model</a>* <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>) {</div>
<div class="line"><a name="l01017"></a><span class="lineno"> 1017</span>&#160; <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html">SatSolver</a>* sat_solver = <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>-&gt;GetOrCreate&lt;<a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html">SatSolver</a>&gt;();</div>
<div class="line"><a name="l01018"></a><span class="lineno"> 1018</span>&#160; </div>
<div class="line"><a name="l01019"></a><span class="lineno"> 1019</span>&#160; <span class="comment">// Note that we only exclude the current decisions, which is an efficient</span></div>
<div class="line"><a name="l01020"></a><span class="lineno"> 1020</span>&#160; <span class="comment">// way to not get the same SAT assignment.</span></div>
<div class="line"><a name="l01021"></a><span class="lineno"> 1021</span>&#160; <span class="keyword">const</span> <span class="keywordtype">int</span> current_level = sat_solver-&gt;<a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#ad63c4461a1384629cb99413c6df8b9ca">CurrentDecisionLevel</a>();</div>
<div class="line"><a name="l01022"></a><span class="lineno"> 1022</span>&#160; std::vector&lt;Literal&gt; clause_to_exclude_solution;</div>
<div class="line"><a name="l01023"></a><span class="lineno"> 1023</span>&#160; clause_to_exclude_solution.reserve(current_level);</div>
<div class="line"><a name="l01024"></a><span class="lineno"> 1024</span>&#160; <span class="keywordflow">for</span> (<span class="keywordtype">int</span> i = 0; i &lt; current_level; ++i) {</div>
<div class="line"><a name="l01025"></a><span class="lineno"> 1025</span>&#160; clause_to_exclude_solution.push_back(</div>
<div class="line"><a name="l01026"></a><span class="lineno"> 1026</span>&#160; sat_solver-&gt;<a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#afb267fc6b043c4e4a15bf0bddd0aaf3f">Decisions</a>()[i].literal.Negated());</div>
<div class="line"><a name="l01027"></a><span class="lineno"> 1027</span>&#160; }</div>
<div class="line"><a name="l01028"></a><span class="lineno"> 1028</span>&#160; sat_solver-&gt;<a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#ac035378cea0ed7b0978105547402faa8">Backtrack</a>(0);</div>
<div class="line"><a name="l01029"></a><span class="lineno"> 1029</span>&#160; <a class="code" href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a>-&gt;Add(<a class="code" href="namespaceoperations__research_1_1sat.html#a1655a9b9673e7c4de940ca6e5e3cf936">ClauseConstraint</a>(clause_to_exclude_solution));</div>
<div class="line"><a name="l01030"></a><span class="lineno"> 1030</span>&#160; };</div>
<div class="line"><a name="l01031"></a><span class="lineno"> 1031</span>&#160;}</div>
<div class="line"><a name="l01032"></a><span class="lineno"> 1032</span>&#160; </div>
<div class="line"><a name="l01033"></a><span class="lineno"> 1033</span>&#160;<span class="comment">// Returns a string representation of a SatSolver::Status.</span></div>
<div class="line"><a name="l01034"></a><span class="lineno"> 1034</span>&#160;std::string <a class="code" href="namespaceoperations__research_1_1sat.html#a762ee6abbb57f9f730df6033aafdf4fc">SatStatusString</a>(<a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a67a0db04d321a74b7e7fcfd3f1a3f70b">SatSolver::Status</a> status);</div>
<div class="line"><a name="l01035"></a><span class="lineno"><a class="line" href="namespaceoperations__research_1_1sat.html#ac9056651d162a99763fc16f98eaf690f"> 1035</a></span>&#160;<span class="keyword">inline</span> std::ostream&amp; <a class="code" href="namespaceoperations__research_1_1sat.html#a15ca399ada8a279dc92f693ede7e4004">operator&lt;&lt;</a>(std::ostream&amp; os, <a class="code" href="classoperations__research_1_1sat_1_1_sat_solver.html#a67a0db04d321a74b7e7fcfd3f1a3f70b">SatSolver::Status</a> status) {</div>
<div class="line"><a name="l01036"></a><span class="lineno"> 1036</span>&#160; os &lt;&lt; <a class="code" href="namespaceoperations__research_1_1sat.html#a762ee6abbb57f9f730df6033aafdf4fc">SatStatusString</a>(status);</div>
<div class="line"><a name="l01037"></a><span class="lineno"> 1037</span>&#160; <span class="keywordflow">return</span> os;</div>
<div class="line"><a name="l01038"></a><span class="lineno"> 1038</span>&#160;}</div>
<div class="line"><a name="l01039"></a><span class="lineno"> 1039</span>&#160; </div>
<div class="line"><a name="l01040"></a><span class="lineno"> 1040</span>&#160;} <span class="comment">// namespace sat</span></div>
<div class="line"><a name="l01041"></a><span class="lineno"> 1041</span>&#160;} <span class="comment">// namespace operations_research</span></div>
<div class="line"><a name="l01042"></a><span class="lineno"> 1042</span>&#160; </div>
<div class="line"><a name="l01043"></a><span class="lineno"> 1043</span>&#160;<span class="preprocessor">#endif </span><span class="comment">// OR_TOOLS_SAT_SAT_SOLVER_H_</span></div>
<div class="ttc" id="aalldiff__cst_8cc_html_a9d0c202d5fdd62f4fa2c613339ff168a"><div class="ttname"><a href="alldiff__cst_8cc.html#a9d0c202d5fdd62f4fa2c613339ff168a">max</a></div><div class="ttdeci">int64 max</div><div class="ttdef"><b>Definition:</b> <a href="alldiff__cst_8cc_source.html#l00139">alldiff_cst.cc:139</a></div></div>
<div class="ttc" id="abase_2logging_8h_html"><div class="ttname"><a href="base_2logging_8h.html">logging.h</a></div></div>
<div class="ttc" id="abase_2logging_8h_html_a3e1cfef60e774a81f30eaddf26a3a274"><div class="ttname"><a href="base_2logging_8h.html#a3e1cfef60e774a81f30eaddf26a3a274">CHECK</a></div><div class="ttdeci">#define CHECK(condition)</div><div class="ttdef"><b>Definition:</b> <a href="base_2logging_8h_source.html#l00495">base/logging.h:495</a></div></div>
<div class="ttc" id="abase_2logging_8h_html_a4bd2e815ca2f702a4b6aa744b1ff3b82"><div class="ttname"><a href="base_2logging_8h.html#a4bd2e815ca2f702a4b6aa744b1ff3b82">CHECK_LT</a></div><div class="ttdeci">#define CHECK_LT(val1, val2)</div><div class="ttdef"><b>Definition:</b> <a href="base_2logging_8h_source.html#l00700">base/logging.h:700</a></div></div>
<div class="ttc" id="abase_2logging_8h_html_a7c0ce053b28d53aa4eaf3eb7fb71663b"><div class="ttname"><a href="base_2logging_8h.html#a7c0ce053b28d53aa4eaf3eb7fb71663b">CHECK_EQ</a></div><div class="ttdeci">#define CHECK_EQ(val1, val2)</div><div class="ttdef"><b>Definition:</b> <a href="base_2logging_8h_source.html#l00697">base/logging.h:697</a></div></div>
<div class="ttc" id="aclass_wall_timer_html"><div class="ttname"><a href="class_wall_timer.html">WallTimer</a></div><div class="ttdef"><b>Definition:</b> <a href="timer_8h_source.html#l00023">timer.h:23</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1_time_limit_html"><div class="ttname"><a href="classoperations__research_1_1_time_limit.html">operations_research::TimeLimit</a></div><div class="ttdoc">A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...</div><div class="ttdef"><b>Definition:</b> <a href="time__limit_8h_source.html#l00105">time_limit.h:105</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1_time_limit_html_af90cfd1fc238433fc303ee28c5914eb9"><div class="ttname"><a href="classoperations__research_1_1_time_limit.html#af90cfd1fc238433fc303ee28c5914eb9">operations_research::TimeLimit::AdvanceDeterministicTime</a></div><div class="ttdeci">void AdvanceDeterministicTime(double deterministic_duration)</div><div class="ttdoc">Advances the deterministic time.</div><div class="ttdef"><b>Definition:</b> <a href="time__limit_8h_source.html#l00226">time_limit.h:226</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_binary_implication_graph_html_a558f9dd435d1f46d7408d60d0e9969f1"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_binary_implication_graph.html#a558f9dd435d1f46d7408d60d0e9969f1">operations_research::sat::BinaryImplicationGraph::ExtractAllBinaryClauses</a></div><div class="ttdeci">void ExtractAllBinaryClauses(Output *out) const</div><div class="ttdef"><b>Definition:</b> <a href="clause_8h_source.html#l00646">clause.h:646</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_binary_implication_graph_html_a75f1d17f36330a1c8a96e43fe8805598"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_binary_implication_graph.html#a75f1d17f36330a1c8a96e43fe8805598">operations_research::sat::BinaryImplicationGraph::SetDratProofHandler</a></div><div class="ttdeci">void SetDratProofHandler(DratProofHandler *drat_proof_handler)</div><div class="ttdef"><b>Definition:</b> <a href="clause_8h_source.html#l00667">clause.h:667</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_drat_proof_handler_html"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_drat_proof_handler.html">operations_research::sat::DratProofHandler</a></div><div class="ttdef"><b>Definition:</b> <a href="drat__proof__handler_8h_source.html#l00040">drat_proof_handler.h:40</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_literal_html"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_literal.html">operations_research::sat::Literal</a></div><div class="ttdef"><b>Definition:</b> <a href="sat__base_8h_source.html#l00064">sat_base.h:64</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_literal_html_a6a5dcff82096cd7a7147bf996dbaa5a8"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_literal.html#a6a5dcff82096cd7a7147bf996dbaa5a8">operations_research::sat::Literal::Variable</a></div><div class="ttdeci">BooleanVariable Variable() const</div><div class="ttdef"><b>Definition:</b> <a href="sat__base_8h_source.html#l00080">sat_base.h:80</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_literal_html_a886e9c024f7209181c0a850b6e90c644"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_literal.html#a886e9c024f7209181c0a850b6e90c644">operations_research::sat::Literal::Negated</a></div><div class="ttdeci">Literal Negated() const</div><div class="ttdef"><b>Definition:</b> <a href="sat__base_8h_source.html#l00091">sat_base.h:91</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_literal_watchers_html_a0569d77056e622964bd02dd901950ede"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_literal_watchers.html#a0569d77056e622964bd02dd901950ede">operations_research::sat::LiteralWatchers::AllClausesInCreationOrder</a></div><div class="ttdeci">const std::vector&lt; SatClause * &gt; &amp; AllClausesInCreationOrder() const</div><div class="ttdef"><b>Definition:</b> <a href="clause_8h_source.html#l00211">clause.h:211</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_literal_watchers_html_a75f1d17f36330a1c8a96e43fe8805598"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_literal_watchers.html#a75f1d17f36330a1c8a96e43fe8805598">operations_research::sat::LiteralWatchers::SetDratProofHandler</a></div><div class="ttdeci">void SetDratProofHandler(DratProofHandler *drat_proof_handler)</div><div class="ttdef"><b>Definition:</b> <a href="clause_8h_source.html#l00239">clause.h:239</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_literal_watchers_html_ab054db78fc1b1e1681d2fc4e9fd1ca45"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_literal_watchers.html#ab054db78fc1b1e1681d2fc4e9fd1ca45">operations_research::sat::LiteralWatchers::IsRemovable</a></div><div class="ttdeci">bool IsRemovable(SatClause *const clause) const</div><div class="ttdef"><b>Definition:</b> <a href="clause_8h_source.html#l00219">clause.h:219</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_literal_watchers_html_ae234022ee7c496416290d1946f56e1ad"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_literal_watchers.html#ae234022ee7c496416290d1946f56e1ad">operations_research::sat::LiteralWatchers::DeleteRemovedClauses</a></div><div class="ttdeci">void DeleteRemovedClauses()</div><div class="ttdef"><b>Definition:</b> <a href="clause_8cc_source.html#l00454">clause.cc:454</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_model_html"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_model.html">operations_research::sat::Model</a></div><div class="ttdoc">Class that owns everything related to a particular optimization model.</div><div class="ttdef"><b>Definition:</b> <a href="sat_2model_8h_source.html#l00038">sat/model.h:38</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_clause_html"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_clause.html">operations_research::sat::SatClause</a></div><div class="ttdef"><b>Definition:</b> <a href="clause_8h_source.html#l00051">clause.h:51</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_decision_policy_html_a0b5d7f31620ad7b364e7415c47ee5e0d"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_decision_policy.html#a0b5d7f31620ad7b364e7415c47ee5e0d">operations_research::sat::SatDecisionPolicy::AllPreferences</a></div><div class="ttdeci">std::vector&lt; std::pair&lt; Literal, double &gt; &gt; AllPreferences() const</div><div class="ttdef"><b>Definition:</b> <a href="sat__decision_8cc_source.html#l00263">sat_decision.cc:263</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_decision_policy_html_a1dc177ee88f0a7ce2e46a032e5c3cf02"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_decision_policy.html#a1dc177ee88f0a7ce2e46a032e5c3cf02">operations_research::sat::SatDecisionPolicy::ResetDecisionHeuristic</a></div><div class="ttdeci">void ResetDecisionHeuristic()</div><div class="ttdef"><b>Definition:</b> <a href="sat__decision_8cc_source.html#l00126">sat_decision.cc:126</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_decision_policy_html_a955786dcbe82b7c4dc9924a5473ac1e8"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_decision_policy.html#a955786dcbe82b7c4dc9924a5473ac1e8">operations_research::sat::SatDecisionPolicy::SetAssignmentPreference</a></div><div class="ttdeci">void SetAssignmentPreference(Literal literal, double weight)</div><div class="ttdef"><b>Definition:</b> <a href="sat__decision_8cc_source.html#l00248">sat_decision.cc:248</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_propagator_html"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_propagator.html">operations_research::sat::SatPropagator</a></div><div class="ttdef"><b>Definition:</b> <a href="sat__base_8h_source.html#l00445">sat_base.h:445</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html">operations_research::sat::SatSolver</a></div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00057">sat_solver.h:57</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a01fd4c9f5286534866c6c5ee2c160fe9"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a01fd4c9f5286534866c6c5ee2c160fe9">operations_research::sat::SatSolver::LiteralTrail</a></div><div class="ttdeci">const Trail &amp; LiteralTrail() const</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00361">sat_solver.h:361</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a05725f6398ef1b0d50c87c4d9e719260"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a05725f6398ef1b0d50c87c4d9e719260">operations_research::sat::SatSolver::AllPreferences</a></div><div class="ttdeci">std::vector&lt; std::pair&lt; Literal, double &gt; &gt; AllPreferences() const</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00153">sat_solver.h:153</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a05c49a95f6af6f8d873c96cae6ab6653"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a05c49a95f6af6f8d873c96cae6ab6653">operations_research::sat::SatSolver::AddLinearConstraint</a></div><div class="ttdeci">bool AddLinearConstraint(bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, std::vector&lt; LiteralWithCoeff &gt; *cst)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00299">sat_solver.cc:299</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a093c00c2bd81c8ec7a5f86a4466fa7d5"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a093c00c2bd81c8ec7a5f86a4466fa7d5">operations_research::sat::SatSolver::EnqueueDecisionIfNotConflicting</a></div><div class="ttdeci">bool EnqueueDecisionIfNotConflicting(Literal true_literal)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00873">sat_solver.cc:873</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a0b58ef3a397720b272662f8bc45585cb"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a0b58ef3a397720b272662f8bc45585cb">operations_research::sat::SatSolver::SetNumVariables</a></div><div class="ttdeci">void SetNumVariables(int num_variables)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00064">sat_solver.cc:64</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a0e8b0117614d340615ab66abec430d78"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a0e8b0117614d340615ab66abec430d78">operations_research::sat::SatSolver::AddTernaryClause</a></div><div class="ttdeci">bool AddTernaryClause(Literal a, Literal b, Literal c)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00191">sat_solver.cc:191</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a17c09186d8dd4922296e97185f685c97"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a17c09186d8dd4922296e97185f685c97">operations_research::sat::SatSolver::AddLastPropagator</a></div><div class="ttdeci">void AddLastPropagator(SatPropagator *propagator)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00413">sat_solver.cc:413</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a1a5e26554d014197de9434d2c39e07e9"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a1a5e26554d014197de9434d2c39e07e9">operations_research::sat::SatSolver::parameters</a></div><div class="ttdeci">const SatParameters &amp; parameters() const</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00110">sat_solver.cc:110</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a1cf106c907fb0a4114a08a76ae2e874f"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a1cf106c907fb0a4114a08a76ae2e874f">operations_research::sat::SatSolver::ResetDecisionHeuristicAndSetAllPreferences</a></div><div class="ttdeci">void ResetDecisionHeuristicAndSetAllPreferences(const std::vector&lt; std::pair&lt; Literal, double &gt;&gt; &amp;prefs)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00159">sat_solver.h:159</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a1dc177ee88f0a7ce2e46a032e5c3cf02"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a1dc177ee88f0a7ce2e46a032e5c3cf02">operations_research::sat::SatSolver::ResetDecisionHeuristic</a></div><div class="ttdeci">void ResetDecisionHeuristic()</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00156">sat_solver.h:156</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a25eb4ef5875f4884226251b66eb61bc0"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a25eb4ef5875f4884226251b66eb61bc0">operations_research::sat::SatSolver::AddClauseDuringSearch</a></div><div class="ttdeci">bool AddClauseDuringSearch(absl::Span&lt; const Literal &gt; literals)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00134">sat_solver.cc:134</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a27e14216f4d9330375fc0089a1919f20"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a27e14216f4d9330375fc0089a1919f20">operations_research::sat::SatSolver::SolveWithTimeLimit</a></div><div class="ttdeci">Status SolveWithTimeLimit(TimeLimit *time_limit)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00968">sat_solver.cc:968</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a2aafb0d6bd7d95f183e87866d0ade374"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a2aafb0d6bd7d95f183e87866d0ade374">operations_research::sat::SatSolver::ProcessNewlyFixedVariables</a></div><div class="ttdeci">void ProcessNewlyFixedVariables()</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l01563">sat_solver.cc:1563</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a2abca6db0c780a4482d1ac9eb6365057"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a2abca6db0c780a4482d1ac9eb6365057">operations_research::sat::SatSolver::ResetAndSolveWithGivenAssumptions</a></div><div class="ttdeci">Status ResetAndSolveWithGivenAssumptions(const std::vector&lt; Literal &gt; &amp;assumptions)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00947">sat_solver.cc:947</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a2b006481369eb4f4cb7f3037dfdd8404"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a2b006481369eb4f4cb7f3037dfdd8404">operations_research::sat::SatSolver::Solve</a></div><div class="ttdeci">Status Solve()</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00972">sat_solver.cc:972</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a2d1cea64152ca53ac5df160b48059800"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a2d1cea64152ca53ac5df160b48059800">operations_research::sat::SatSolver::AddPropagator</a></div><div class="ttdeci">void AddPropagator(SatPropagator *propagator)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00405">sat_solver.cc:405</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a3cce11fce89a849b4224eb83e217abd0"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a3cce11fce89a849b4224eb83e217abd0">operations_research::sat::SatSolver::NumFixedVariables</a></div><div class="ttdeci">int64 NumFixedVariables() const</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00432">sat_solver.h:432</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a42c1fced0014f47ce16a512d454cee0f"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a42c1fced0014f47ce16a512d454cee0f">operations_research::sat::SatSolver::num_failures</a></div><div class="ttdeci">int64 num_failures() const</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00084">sat_solver.cc:84</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a43684a0a8ef85b1cea0076dba3fb271d"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a43684a0a8ef85b1cea0076dba3fb271d">operations_research::sat::SatSolver::NewBooleanVariable</a></div><div class="ttdeci">BooleanVariable NewBooleanVariable()</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00083">sat_solver.h:83</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a4e9c1f685afe26db1566eaa65724b40b"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a4e9c1f685afe26db1566eaa65724b40b">operations_research::sat::SatSolver::NewlyAddedBinaryClauses</a></div><div class="ttdeci">const std::vector&lt; BinaryClause &gt; &amp; NewlyAddedBinaryClauses()</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00932">sat_solver.cc:932</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a4f7251fc4692363cf55796a6f3e267ea"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a4f7251fc4692363cf55796a6f3e267ea">operations_research::sat::SatSolver::NotifyThatModelIsUnsat</a></div><div class="ttdeci">void NotifyThatModelIsUnsat()</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00401">sat_solver.h:401</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a4fbc93ff66f372e1b604609fe5b45557"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a4fbc93ff66f372e1b604609fe5b45557">operations_research::sat::SatSolver::num_branches</a></div><div class="ttdeci">int64 num_branches() const</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00082">sat_solver.cc:82</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a5a9a59c0a2f7fcec81cc44b1aa159186"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a5a9a59c0a2f7fcec81cc44b1aa159186">operations_research::sat::SatSolver::AddBinaryClauses</a></div><div class="ttdeci">bool AddBinaryClauses(const std::vector&lt; BinaryClause &gt; &amp;clauses)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00918">sat_solver.cc:918</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a5bbe13ebae8aa11a8a4ac1cb01bc66ad"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a5bbe13ebae8aa11a8a4ac1cb01bc66ad">operations_research::sat::SatSolver::UnsatStatus</a></div><div class="ttdeci">Status UnsatStatus() const</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00309">sat_solver.h:309</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a5ca47674a4a0b5e7f40eb430ab474440"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a5ca47674a4a0b5e7f40eb430ab474440">operations_research::sat::SatSolver::SetAssumptionLevel</a></div><div class="ttdeci">void SetAssumptionLevel(int assumption_level)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00962">sat_solver.cc:962</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a607d97ccada862073f297bc2d495124d"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a607d97ccada862073f297bc2d495124d">operations_research::sat::SatSolver::FinishPropagation</a></div><div class="ttdeci">bool FinishPropagation()</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00521">sat_solver.cc:521</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a678cca4fb095d5dee896dd687649a5de"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a678cca4fb095d5dee896dd687649a5de">operations_research::sat::SatSolver::ProblemIsPureSat</a></div><div class="ttdeci">bool ProblemIsPureSat() const</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00387">sat_solver.h:387</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a67a0db04d321a74b7e7fcfd3f1a3f70b"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a67a0db04d321a74b7e7fcfd3f1a3f70b">operations_research::sat::SatSolver::Status</a></div><div class="ttdeci">Status</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00180">sat_solver.h:180</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a67a0db04d321a74b7e7fcfd3f1a3f70ba03f919221217f95d21a593a7120165e1"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a67a0db04d321a74b7e7fcfd3f1a3f70ba03f919221217f95d21a593a7120165e1">operations_research::sat::SatSolver::FEASIBLE</a></div><div class="ttdeci">@ FEASIBLE</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00183">sat_solver.h:183</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a67a0db04d321a74b7e7fcfd3f1a3f70ba2884fa43446c0cbc9c7a9b74d41d7483"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a67a0db04d321a74b7e7fcfd3f1a3f70ba2884fa43446c0cbc9c7a9b74d41d7483">operations_research::sat::SatSolver::INFEASIBLE</a></div><div class="ttdeci">@ INFEASIBLE</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00182">sat_solver.h:182</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a67a0db04d321a74b7e7fcfd3f1a3f70ba72c2402449caa8f3edc8aa0a3816baed"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a67a0db04d321a74b7e7fcfd3f1a3f70ba72c2402449caa8f3edc8aa0a3816baed">operations_research::sat::SatSolver::LIMIT_REACHED</a></div><div class="ttdeci">@ LIMIT_REACHED</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00184">sat_solver.h:184</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a67a0db04d321a74b7e7fcfd3f1a3f70bae5ba802809eb747ea486ca3fae32a885"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a67a0db04d321a74b7e7fcfd3f1a3f70bae5ba802809eb747ea486ca3fae32a885">operations_research::sat::SatSolver::ASSUMPTIONS_UNSAT</a></div><div class="ttdeci">@ ASSUMPTIONS_UNSAT</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00181">sat_solver.h:181</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a68050818df324a24e6309055e857b955"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a68050818df324a24e6309055e857b955">operations_research::sat::SatSolver::SaveDebugAssignment</a></div><div class="ttdeci">void SaveDebugAssignment()</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00442">sat_solver.cc:442</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a6ce6ed209f0abff6cdbf46e2de1c8a48"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a6ce6ed209f0abff6cdbf46e2de1c8a48">operations_research::sat::SatSolver::model</a></div><div class="ttdeci">Model * model()</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00065">sat_solver.h:65</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a705eddd5baee23097daf34b73e66eae3"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a705eddd5baee23097daf34b73e66eae3">operations_research::sat::SatSolver::AdvanceDeterministicTime</a></div><div class="ttdeci">void AdvanceDeterministicTime(TimeLimit *limit)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00422">sat_solver.h:422</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a75f1d17f36330a1c8a96e43fe8805598"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a75f1d17f36330a1c8a96e43fe8805598">operations_research::sat::SatSolver::SetDratProofHandler</a></div><div class="ttdeci">void SetDratProofHandler(DratProofHandler *drat_proof_handler)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00389">sat_solver.h:389</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a7b5f3592cdf12c0df22b6583b3e9ed61"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a7b5f3592cdf12c0df22b6583b3e9ed61">operations_research::sat::SatSolver::num_propagations</a></div><div class="ttdeci">int64 num_propagations() const</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00086">sat_solver.cc:86</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a88dcaf0cf27bb4991376ed54d8f2698f"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a88dcaf0cf27bb4991376ed54d8f2698f">operations_research::sat::SatSolver::AssumptionLevel</a></div><div class="ttdeci">int AssumptionLevel() const</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00220">sat_solver.h:220</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a8c6812e05685c0b43d4dd8efaf68aa23"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a8c6812e05685c0b43d4dd8efaf68aa23">operations_research::sat::SatSolver::~SatSolver</a></div><div class="ttdeci">~SatSolver()</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00062">sat_solver.cc:62</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a8f1f9030283b2fa93b2353ab260ebe1e"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a8f1f9030283b2fa93b2353ab260ebe1e">operations_research::sat::SatSolver::MinimizeSomeClauses</a></div><div class="ttdeci">void MinimizeSomeClauses(int decisions_budget)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l01247">sat_solver.cc:1247</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a943e1a6b169c75c35c1f596b11fe4fc4"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a943e1a6b169c75c35c1f596b11fe4fc4">operations_research::sat::SatSolver::num_restarts</a></div><div class="ttdeci">int64 num_restarts() const</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00090">sat_solver.cc:90</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a955786dcbe82b7c4dc9924a5473ac1e8"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a955786dcbe82b7c4dc9924a5473ac1e8">operations_research::sat::SatSolver::SetAssignmentPreference</a></div><div class="ttdeci">void SetAssignmentPreference(Literal literal, double weight)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00150">sat_solver.h:150</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a9789bf03dba611e9be5679d6e902d0c8"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a9789bf03dba611e9be5679d6e902d0c8">operations_research::sat::SatSolver::Assignment</a></div><div class="ttdeci">const VariablesAssignment &amp; Assignment() const</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00362">sat_solver.h:362</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a9ae69b015a43c1a94e8815ab0dd8189c"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a9ae69b015a43c1a94e8815ab0dd8189c">operations_research::sat::SatSolver::EnqueueDecisionAndBackjumpOnConflict</a></div><div class="ttdeci">int EnqueueDecisionAndBackjumpOnConflict(Literal true_literal)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00499">sat_solver.cc:499</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a9d3beb2afe4ae647674b054bf29290e2"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a9d3beb2afe4ae647674b054bf29290e2">operations_research::sat::SatSolver::NumVariables</a></div><div class="ttdeci">int NumVariables() const</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00082">sat_solver.h:82</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a9d584b84d7b882a6017b072b33475172"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a9d584b84d7b882a6017b072b33475172">operations_research::sat::SatSolver::SetParameters</a></div><div class="ttdeci">void SetParameters(const SatParameters &amp;parameters)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00115">sat_solver.cc:115</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_a9da38c8d2910442d551db5e360423029"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#a9da38c8d2910442d551db5e360423029">operations_research::sat::SatSolver::ResetToLevelZero</a></div><div class="ttdeci">bool ResetToLevelZero()</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00529">sat_solver.cc:529</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_aa5e0514942c20e89148448f4d0572cd0"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#aa5e0514942c20e89148448f4d0572cd0">operations_research::sat::SatSolver::TrackBinaryClauses</a></div><div class="ttdeci">void TrackBinaryClauses(bool value)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00345">sat_solver.h:345</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_aac912e9410b8989493f492fcbb2d9094"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#aac912e9410b8989493f492fcbb2d9094">operations_research::sat::SatSolver::AddBinaryClause</a></div><div class="ttdeci">bool AddBinaryClause(Literal a, Literal b)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00180">sat_solver.cc:180</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_ab5bc2f86603d9fdb9a51305ab431530d"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#ab5bc2f86603d9fdb9a51305ab431530d">operations_research::sat::SatSolver::ExtractClauses</a></div><div class="ttdeci">void ExtractClauses(Output *out)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00320">sat_solver.h:320</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_ab63a08713131e63e9cc4109f98ecf859"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#ab63a08713131e63e9cc4109f98ecf859">operations_research::sat::SatSolver::EnqueueDecisionAndBacktrackOnConflict</a></div><div class="ttdeci">int EnqueueDecisionAndBacktrackOnConflict(Literal true_literal)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00861">sat_solver.cc:861</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_ac035378cea0ed7b0978105547402faa8"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#ac035378cea0ed7b0978105547402faa8">operations_research::sat::SatSolver::Backtrack</a></div><div class="ttdeci">void Backtrack(int target_level)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00888">sat_solver.cc:888</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_ac714aeb75f0f6dd87e52e5d1a0d6edc7"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#ac714aeb75f0f6dd87e52e5d1a0d6edc7">operations_research::sat::SatSolver::RestoreSolverToAssumptionLevel</a></div><div class="ttdeci">bool RestoreSolverToAssumptionLevel()</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00511">sat_solver.cc:511</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_acfbfa9df611cb625ff79785c05784580"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#acfbfa9df611cb625ff79785c05784580">operations_research::sat::SatSolver::GetLastIncompatibleDecisions</a></div><div class="ttdeci">std::vector&lt; Literal &gt; GetLastIncompatibleDecisions()</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l01272">sat_solver.cc:1272</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_ad085476234b92559b93383f9e1264af6"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#ad085476234b92559b93383f9e1264af6">operations_research::sat::SatSolver::TakePropagatorOwnership</a></div><div class="ttdeci">void TakePropagatorOwnership(std::unique_ptr&lt; SatPropagator &gt; propagator)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00142">sat_solver.h:142</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_ad28cbdd5735a0c111a642f39524d969e"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#ad28cbdd5735a0c111a642f39524d969e">operations_research::sat::SatSolver::ReapplyAssumptionsIfNeeded</a></div><div class="ttdeci">bool ReapplyAssumptionsIfNeeded()</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00554">sat_solver.cc:554</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_ad2a33e1d9335cce63548abed6b5c8aab"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#ad2a33e1d9335cce63548abed6b5c8aab">operations_research::sat::SatSolver::IsModelUnsat</a></div><div class="ttdeci">bool IsModelUnsat() const</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00136">sat_solver.h:136</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_ad4494c6831942d344ed1d9758f0e6cd9"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#ad4494c6831942d344ed1d9758f0e6cd9">operations_research::sat::SatSolver::ResetWithGivenAssumptions</a></div><div class="ttdeci">bool ResetWithGivenAssumptions(const std::vector&lt; Literal &gt; &amp;assumptions)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00536">sat_solver.cc:536</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_ad63c4461a1384629cb99413c6df8b9ca"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#ad63c4461a1384629cb99413c6df8b9ca">operations_research::sat::SatSolver::CurrentDecisionLevel</a></div><div class="ttdeci">int CurrentDecisionLevel() const</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00360">sat_solver.h:360</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_adadc001cbdc7263b106fc5886b60ff39"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#adadc001cbdc7263b106fc5886b60ff39">operations_research::sat::SatSolver::Propagate</a></div><div class="ttdeci">bool Propagate()</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l01622">sat_solver.cc:1622</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_adc7569321b063bae82803229623c8f4f"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#adc7569321b063bae82803229623c8f4f">operations_research::sat::SatSolver::SatSolver</a></div><div class="ttdeci">SatSolver()</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00037">sat_solver.cc:37</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_ae525d235b02bcfc962d845e28f5f0125"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#ae525d235b02bcfc962d845e28f5f0125">operations_research::sat::SatSolver::deterministic_time</a></div><div class="ttdeci">double deterministic_time() const</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00092">sat_solver.cc:92</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_af67fe279478772a6d1492a7f673bda5d"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#af67fe279478772a6d1492a7f673bda5d">operations_research::sat::SatSolver::AddProblemClause</a></div><div class="ttdeci">bool AddProblemClause(absl::Span&lt; const Literal &gt; literals)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00203">sat_solver.cc:203</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_afb267fc6b043c4e4a15bf0bddd0aaf3f"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#afb267fc6b043c4e4a15bf0bddd0aaf3f">operations_research::sat::SatSolver::Decisions</a></div><div class="ttdeci">const std::vector&lt; Decision &gt; &amp; Decisions() const</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00359">sat_solver.h:359</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_afbbbc2f0845a82a5a5cfb3f00a61abe9"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#afbbbc2f0845a82a5a5cfb3f00a61abe9">operations_research::sat::SatSolver::AddUnitClause</a></div><div class="ttdeci">bool AddUnitClause(Literal true_literal)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00164">sat_solver.cc:164</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_sat_solver_html_afdb0cc1ac877cd981dcd3f0b0763e644"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_solver.html#afdb0cc1ac877cd981dcd3f0b0763e644">operations_research::sat::SatSolver::ClearNewlyAddedBinaryClauses</a></div><div class="ttdeci">void ClearNewlyAddedBinaryClauses()</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l00936">sat_solver.cc:936</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_trail_html"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_trail.html">operations_research::sat::Trail</a></div><div class="ttdef"><b>Definition:</b> <a href="sat__base_8h_source.html#l00233">sat_base.h:233</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_trail_html_a29be1a6b9ba823a6fffb927609d18599"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_trail.html#a29be1a6b9ba823a6fffb927609d18599">operations_research::sat::Trail::Info</a></div><div class="ttdeci">const AssignmentInfo &amp; Info(BooleanVariable var) const</div><div class="ttdef"><b>Definition:</b> <a href="sat__base_8h_source.html#l00381">sat_base.h:381</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_trail_html_a8ef12397d1682615bc3108c397734179"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_trail.html#a8ef12397d1682615bc3108c397734179">operations_research::sat::Trail::Index</a></div><div class="ttdeci">int Index() const</div><div class="ttdef"><b>Definition:</b> <a href="sat__base_8h_source.html#l00378">sat_base.h:378</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_trail_html_a9789bf03dba611e9be5679d6e902d0c8"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_trail.html#a9789bf03dba611e9be5679d6e902d0c8">operations_research::sat::Trail::Assignment</a></div><div class="ttdeci">const VariablesAssignment &amp; Assignment() const</div><div class="ttdef"><b>Definition:</b> <a href="sat__base_8h_source.html#l00380">sat_base.h:380</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_variables_assignment_html"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_variables_assignment.html">operations_research::sat::VariablesAssignment</a></div><div class="ttdef"><b>Definition:</b> <a href="sat__base_8h_source.html#l00122">sat_base.h:122</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_variables_assignment_html_a49e751eb6f0e9babd957889bb8e7472d"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_variables_assignment.html#a49e751eb6f0e9babd957889bb8e7472d">operations_research::sat::VariablesAssignment::VariableIsAssigned</a></div><div class="ttdeci">bool VariableIsAssigned(BooleanVariable var) const</div><div class="ttdef"><b>Definition:</b> <a href="sat__base_8h_source.html#l00158">sat_base.h:158</a></div></div>
<div class="ttc" id="aclassoperations__research_1_1sat_1_1_variables_assignment_html_a5300129913f51dcb0b1c531e3248490e"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_variables_assignment.html#a5300129913f51dcb0b1c531e3248490e">operations_research::sat::VariablesAssignment::LiteralIsTrue</a></div><div class="ttdeci">bool LiteralIsTrue(Literal literal) const</div><div class="ttdef"><b>Definition:</b> <a href="sat__base_8h_source.html#l00150">sat_base.h:150</a></div></div>
<div class="ttc" id="aclause_8h_html"><div class="ttname"><a href="clause_8h.html">clause.h</a></div></div>
<div class="ttc" id="aconstraint__solver_2table_8cc_html_a344010e26426d6a13411648d988bc9b6"><div class="ttname"><a href="constraint__solver_2table_8cc.html#a344010e26426d6a13411648d988bc9b6">b</a></div><div class="ttdeci">int64 b</div><div class="ttdef"><b>Definition:</b> <a href="constraint__solver_2table_8cc_source.html#l00043">constraint_solver/table.cc:43</a></div></div>
<div class="ttc" id="aconstraint__solver_2table_8cc_html_af730895c6c6ef6e03caaf6251192dfd2"><div class="ttname"><a href="constraint__solver_2table_8cc.html#af730895c6c6ef6e03caaf6251192dfd2">a</a></div><div class="ttdeci">int64 a</div><div class="ttdef"><b>Definition:</b> <a href="constraint__solver_2table_8cc_source.html#l00042">constraint_solver/table.cc:42</a></div></div>
<div class="ttc" id="acp__model__solver_8cc_html_ac3cf9db02b23ea1455b5ae6955d03e47"><div class="ttname"><a href="cp__model__solver_8cc.html#ac3cf9db02b23ea1455b5ae6955d03e47">time_limit</a></div><div class="ttdeci">SharedTimeLimit * time_limit</div><div class="ttdef"><b>Definition:</b> <a href="cp__model__solver_8cc_source.html#l02106">cp_model_solver.cc:2106</a></div></div>
<div class="ttc" id="ademon__profiler_8cc_html_a21edc7ca4cc5802c8779d68556bc09cf"><div class="ttname"><a href="demon__profiler_8cc.html#a21edc7ca4cc5802c8779d68556bc09cf">value</a></div><div class="ttdeci">int64 value</div><div class="ttdef"><b>Definition:</b> <a href="demon__profiler_8cc_source.html#l00043">demon_profiler.cc:43</a></div></div>
<div class="ttc" id="adrat__proof__handler_8h_html"><div class="ttname"><a href="drat__proof__handler_8h.html">drat_proof_handler.h</a></div></div>
<div class="ttc" id="aexpr__array_8cc_html_a472a99923cbe11ae7b5a5d157d9ad465"><div class="ttname"><a href="expr__array_8cc.html#a472a99923cbe11ae7b5a5d157d9ad465">var</a></div><div class="ttdeci">IntVar * var</div><div class="ttdef"><b>Definition:</b> <a href="expr__array_8cc_source.html#l01858">expr_array.cc:1858</a></div></div>
<div class="ttc" id="agurobi__interface_8cc_html_a0728f23c9a47655d38e0bf1a2f200bcf"><div class="ttname"><a href="gurobi__interface_8cc.html#a0728f23c9a47655d38e0bf1a2f200bcf">model</a></div><div class="ttdeci">GRBmodel * model</div><div class="ttdef"><b>Definition:</b> <a href="gurobi__interface_8cc_source.html#l00272">gurobi_interface.cc:272</a></div></div>
<div class="ttc" id="ahash_8h_html"><div class="ttname"><a href="hash_8h.html">hash.h</a></div></div>
<div class="ttc" id="aint__type_8h_html"><div class="ttname"><a href="int__type_8h.html">int_type.h</a></div></div>
<div class="ttc" id="aintegral__types_8h_html"><div class="ttname"><a href="integral__types_8h.html">integral_types.h</a></div></div>
<div class="ttc" id="aintegral__types_8h_html_a7cde0074dfd288f2d70c0e035dacb28a"><div class="ttname"><a href="integral__types_8h.html#a7cde0074dfd288f2d70c0e035dacb28a">int64</a></div><div class="ttdeci">int64_t int64</div><div class="ttdef"><b>Definition:</b> <a href="integral__types_8h_source.html#l00034">integral_types.h:34</a></div></div>
<div class="ttc" id="amacros_8h_html"><div class="ttname"><a href="macros_8h.html">macros.h</a></div></div>
<div class="ttc" id="anamespaceoperations__research_1_1glop_html_abec9e934a51aa2ab519684cc0f446a41"><div class="ttname"><a href="namespaceoperations__research_1_1glop.html#abec9e934a51aa2ab519684cc0f446a41">operations_research::glop::Index</a></div><div class="ttdeci">int32 Index</div><div class="ttdef"><b>Definition:</b> <a href="lp__types_8h_source.html#l00037">lp_types.h:37</a></div></div>
<div class="ttc" id="anamespaceoperations__research_1_1sat_html_a0435d9a6682ddb54c3942024ede20346"><div class="ttname"><a href="namespaceoperations__research_1_1sat.html#a0435d9a6682ddb54c3942024ede20346">operations_research::sat::ReifiedBoolLe</a></div><div class="ttdeci">std::function&lt; void(Model *)&gt; ReifiedBoolLe(Literal a, Literal b, Literal r)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00984">sat_solver.h:984</a></div></div>
<div class="ttc" id="anamespaceoperations__research_1_1sat_html_a111954e38f31aadd4d5bd3e41741bfce"><div class="ttname"><a href="namespaceoperations__research_1_1sat.html#a111954e38f31aadd4d5bd3e41741bfce">operations_research::sat::ExcludeCurrentSolutionAndBacktrack</a></div><div class="ttdeci">std::function&lt; void(Model *)&gt; ExcludeCurrentSolutionAndBacktrack()</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l01015">sat_solver.h:1015</a></div></div>
<div class="ttc" id="anamespaceoperations__research_1_1sat_html_a15ca399ada8a279dc92f693ede7e4004"><div class="ttname"><a href="namespaceoperations__research_1_1sat.html#a15ca399ada8a279dc92f693ede7e4004">operations_research::sat::operator&lt;&lt;</a></div><div class="ttdeci">std::ostream &amp; operator&lt;&lt;(std::ostream &amp;os, const BoolVar &amp;var)</div><div class="ttdef"><b>Definition:</b> <a href="cp__model_8cc_source.html#l00065">cp_model.cc:65</a></div></div>
<div class="ttc" id="anamespaceoperations__research_1_1sat_html_a1655a9b9673e7c4de940ca6e5e3cf936"><div class="ttname"><a href="namespaceoperations__research_1_1sat.html#a1655a9b9673e7c4de940ca6e5e3cf936">operations_research::sat::ClauseConstraint</a></div><div class="ttdeci">std::function&lt; void(Model *)&gt; ClauseConstraint(absl::Span&lt; const Literal &gt; literals)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00904">sat_solver.h:904</a></div></div>
<div class="ttc" id="anamespaceoperations__research_1_1sat_html_a1b1462c55662c1263c0e1f54ed6e06cd"><div class="ttname"><a href="namespaceoperations__research_1_1sat.html#a1b1462c55662c1263c0e1f54ed6e06cd">operations_research::sat::ExactlyOneConstraint</a></div><div class="ttdeci">std::function&lt; void(Model *)&gt; ExactlyOneConstraint(const std::vector&lt; Literal &gt; &amp;literals)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00876">sat_solver.h:876</a></div></div>
<div class="ttc" id="anamespaceoperations__research_1_1sat_html_a3f1a1b8a7a1a488e263a2e74f45d2a59"><div class="ttname"><a href="namespaceoperations__research_1_1sat.html#a3f1a1b8a7a1a488e263a2e74f45d2a59">operations_research::sat::Value</a></div><div class="ttdeci">std::function&lt; int64(const Model &amp;)&gt; Value(IntegerVariable v)</div><div class="ttdef"><b>Definition:</b> <a href="integer_8h_source.html#l01487">integer.h:1487</a></div></div>
<div class="ttc" id="anamespaceoperations__research_1_1sat_html_a5671353b0876a1d63e61414bd02f1081"><div class="ttname"><a href="namespaceoperations__research_1_1sat.html#a5671353b0876a1d63e61414bd02f1081">operations_research::sat::BooleanLinearConstraint</a></div><div class="ttdeci">std::function&lt; void(Model *)&gt; BooleanLinearConstraint(int64 lower_bound, int64 upper_bound, std::vector&lt; LiteralWithCoeff &gt; *cst)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00852">sat_solver.h:852</a></div></div>
<div class="ttc" id="anamespaceoperations__research_1_1sat_html_a607ba8d18e00b2e6dbdc8622bb74fdf5"><div class="ttname"><a href="namespaceoperations__research_1_1sat.html#a607ba8d18e00b2e6dbdc8622bb74fdf5">operations_research::sat::Equality</a></div><div class="ttdeci">std::function&lt; void(Model *)&gt; Equality(IntegerVariable v, int64 value)</div><div class="ttdef"><b>Definition:</b> <a href="integer_8h_source.html#l01524">integer.h:1524</a></div></div>
<div class="ttc" id="anamespaceoperations__research_1_1sat_html_a64b1b8d5018080ad3e7dd7eb6df42274"><div class="ttname"><a href="namespaceoperations__research_1_1sat.html#a64b1b8d5018080ad3e7dd7eb6df42274">operations_research::sat::EnforcedClause</a></div><div class="ttdeci">std::function&lt; void(Model *)&gt; EnforcedClause(absl::Span&lt; const Literal &gt; enforcement_literals, absl::Span&lt; const Literal &gt; clause)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00950">sat_solver.h:950</a></div></div>
<div class="ttc" id="anamespaceoperations__research_1_1sat_html_a6fb8349259fa849de0789a4ec58a8492"><div class="ttname"><a href="namespaceoperations__research_1_1sat.html#a6fb8349259fa849de0789a4ec58a8492">operations_research::sat::MinimizeCore</a></div><div class="ttdeci">void MinimizeCore(SatSolver *solver, std::vector&lt; Literal &gt; *core)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l02547">sat_solver.cc:2547</a></div></div>
<div class="ttc" id="anamespaceoperations__research_1_1sat_html_a762ee6abbb57f9f730df6033aafdf4fc"><div class="ttname"><a href="namespaceoperations__research_1_1sat.html#a762ee6abbb57f9f730df6033aafdf4fc">operations_research::sat::SatStatusString</a></div><div class="ttdeci">std::string SatStatusString(SatSolver::Status status)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8cc_source.html#l02530">sat_solver.cc:2530</a></div></div>
<div class="ttc" id="anamespaceoperations__research_1_1sat_html_a8a0620c105ec05f1b42bcde3a9380872"><div class="ttname"><a href="namespaceoperations__research_1_1sat.html#a8a0620c105ec05f1b42bcde3a9380872">operations_research::sat::Implication</a></div><div class="ttdeci">std::function&lt; void(Model *)&gt; Implication(const std::vector&lt; Literal &gt; &amp;enforcement_literals, IntegerLiteral i)</div><div class="ttdef"><b>Definition:</b> <a href="integer_8h_source.html#l01537">integer.h:1537</a></div></div>
<div class="ttc" id="anamespaceoperations__research_1_1sat_html_aa874aee040980146062498b87e8fb956"><div class="ttname"><a href="namespaceoperations__research_1_1sat.html#aa874aee040980146062498b87e8fb956">operations_research::sat::ReifiedBoolAnd</a></div><div class="ttdeci">std::function&lt; void(Model *)&gt; ReifiedBoolAnd(const std::vector&lt; Literal &gt; &amp;literals, Literal r)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00968">sat_solver.h:968</a></div></div>
<div class="ttc" id="anamespaceoperations__research_1_1sat_html_ab8221efb0cc3dd5059674845b4db7fed"><div class="ttname"><a href="namespaceoperations__research_1_1sat.html#ab8221efb0cc3dd5059674845b4db7fed">operations_research::sat::AtMostOneConstraint</a></div><div class="ttdeci">std::function&lt; void(Model *)&gt; AtMostOneConstraint(const std::vector&lt; Literal &gt; &amp;literals)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00890">sat_solver.h:890</a></div></div>
<div class="ttc" id="anamespaceoperations__research_1_1sat_html_ae51e64bd361f6b51d7d35a62aad28f03"><div class="ttname"><a href="namespaceoperations__research_1_1sat.html#ae51e64bd361f6b51d7d35a62aad28f03">operations_research::sat::CardinalityConstraint</a></div><div class="ttdeci">std::function&lt; void(Model *)&gt; CardinalityConstraint(int64 lower_bound, int64 upper_bound, const std::vector&lt; Literal &gt; &amp;literals)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00861">sat_solver.h:861</a></div></div>
<div class="ttc" id="anamespaceoperations__research_1_1sat_html_aed3a7826cb80e5dfe7cadb141fde73f2"><div class="ttname"><a href="namespaceoperations__research_1_1sat.html#aed3a7826cb80e5dfe7cadb141fde73f2">operations_research::sat::kUnsatTrailIndex</a></div><div class="ttdeci">const int kUnsatTrailIndex</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00052">sat_solver.h:52</a></div></div>
<div class="ttc" id="anamespaceoperations__research_1_1sat_html_affc20db163dca7cacfb4aa97cf8d72b9"><div class="ttname"><a href="namespaceoperations__research_1_1sat.html#affc20db163dca7cacfb4aa97cf8d72b9">operations_research::sat::ReifiedBoolOr</a></div><div class="ttdeci">std::function&lt; void(Model *)&gt; ReifiedBoolOr(const std::vector&lt; Literal &gt; &amp;literals, Literal r)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00934">sat_solver.h:934</a></div></div>
<div class="ttc" id="anamespaceoperations__research_html"><div class="ttname"><a href="namespaceoperations__research.html">operations_research</a></div><div class="ttdoc">The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...</div><div class="ttdef"><b>Definition:</b> <a href="dense__doubly__linked__list_8h_source.html#l00021">dense_doubly_linked_list.h:21</a></div></div>
<div class="ttc" id="aoptimization_8cc_html_af63dcc00f2023fdf498e0829e6fb8a6b"><div class="ttname"><a href="optimization_8cc.html#af63dcc00f2023fdf498e0829e6fb8a6b">literal</a></div><div class="ttdeci">Literal literal</div><div class="ttdef"><b>Definition:</b> <a href="optimization_8cc_source.html#l00084">optimization.cc:84</a></div></div>
<div class="ttc" id="apack_8cc_html_ae42ca38a167164c07831993889216903"><div class="ttname"><a href="pack_8cc.html#ae42ca38a167164c07831993889216903">weight</a></div><div class="ttdeci">int64 weight</div><div class="ttdef"><b>Definition:</b> <a href="pack_8cc_source.html#l00509">pack.cc:509</a></div></div>
<div class="ttc" id="aparser_8yy_8cc_html_a5a634cf4429798b1c921a81de8250051"><div class="ttname"><a href="parser_8yy_8cc.html#a5a634cf4429798b1c921a81de8250051">input</a></div><div class="ttdeci">static int input(yyscan_t yyscanner)</div></div>
<div class="ttc" id="apb__constraint_8h_html"><div class="ttname"><a href="pb__constraint_8h.html">pb_constraint.h</a></div></div>
<div class="ttc" id="arestart_8h_html"><div class="ttname"><a href="restart_8h.html">restart.h</a></div></div>
<div class="ttc" id="asat_2model_8h_html"><div class="ttname"><a href="sat_2model_8h.html">model.h</a></div></div>
<div class="ttc" id="asat__base_8h_html"><div class="ttname"><a href="sat__base_8h.html">sat_base.h</a></div></div>
<div class="ttc" id="asat__decision_8h_html"><div class="ttname"><a href="sat__decision_8h.html">sat_decision.h</a></div></div>
<div class="ttc" id="asat__parameters_8pb_8h_html"><div class="ttname"><a href="sat__parameters_8pb_8h.html">sat_parameters.pb.h</a></div></div>
<div class="ttc" id="astats_8h_html"><div class="ttname"><a href="stats_8h.html">stats.h</a></div></div>
<div class="ttc" id="astructoperations__research_1_1sat_1_1_assignment_info_html_a8843d978bef78a2392a908bd07fffb8e"><div class="ttname"><a href="structoperations__research_1_1sat_1_1_assignment_info.html#a8843d978bef78a2392a908bd07fffb8e">operations_research::sat::AssignmentInfo::trail_index</a></div><div class="ttdeci">int32 trail_index</div><div class="ttdef"><b>Definition:</b> <a href="sat__base_8h_source.html#l00208">sat_base.h:208</a></div></div>
<div class="ttc" id="astructoperations__research_1_1sat_1_1_assignment_info_html_afefd28242df91e46e762af1f7eaf623f"><div class="ttname"><a href="structoperations__research_1_1sat_1_1_assignment_info.html#afefd28242df91e46e762af1f7eaf623f">operations_research::sat::AssignmentInfo::level</a></div><div class="ttdeci">uint32 level</div><div class="ttdef"><b>Definition:</b> <a href="sat__base_8h_source.html#l00199">sat_base.h:199</a></div></div>
<div class="ttc" id="astructoperations__research_1_1sat_1_1_sat_solver_1_1_decision_html"><div class="ttname"><a href="structoperations__research_1_1sat_1_1_sat_solver_1_1_decision.html">operations_research::sat::SatSolver::Decision</a></div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00350">sat_solver.h:350</a></div></div>
<div class="ttc" id="astructoperations__research_1_1sat_1_1_sat_solver_1_1_decision_html_a2949c912240ff8a61f4a6751250bba27"><div class="ttname"><a href="structoperations__research_1_1sat_1_1_sat_solver_1_1_decision.html#a2949c912240ff8a61f4a6751250bba27">operations_research::sat::SatSolver::Decision::Decision</a></div><div class="ttdeci">Decision(int i, Literal l)</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00352">sat_solver.h:352</a></div></div>
<div class="ttc" id="astructoperations__research_1_1sat_1_1_sat_solver_1_1_decision_html_a84b0a5cf3a019584a6f21ec98136c60a"><div class="ttname"><a href="structoperations__research_1_1sat_1_1_sat_solver_1_1_decision.html#a84b0a5cf3a019584a6f21ec98136c60a">operations_research::sat::SatSolver::Decision::trail_index</a></div><div class="ttdeci">int trail_index</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00353">sat_solver.h:353</a></div></div>
<div class="ttc" id="astructoperations__research_1_1sat_1_1_sat_solver_1_1_decision_html_abd62b993702516d946bdbef25f6d29b0"><div class="ttname"><a href="structoperations__research_1_1sat_1_1_sat_solver_1_1_decision.html#abd62b993702516d946bdbef25f6d29b0">operations_research::sat::SatSolver::Decision::Decision</a></div><div class="ttdeci">Decision()</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00351">sat_solver.h:351</a></div></div>
<div class="ttc" id="astructoperations__research_1_1sat_1_1_sat_solver_1_1_decision_html_af63dcc00f2023fdf498e0829e6fb8a6b"><div class="ttname"><a href="structoperations__research_1_1sat_1_1_sat_solver_1_1_decision.html#af63dcc00f2023fdf498e0829e6fb8a6b">operations_research::sat::SatSolver::Decision::literal</a></div><div class="ttdeci">Literal literal</div><div class="ttdef"><b>Definition:</b> <a href="sat__solver_8h_source.html#l00354">sat_solver.h:354</a></div></div>
<div class="ttc" id="atime__limit_8h_html"><div class="ttname"><a href="time__limit_8h.html">time_limit.h</a></div></div>
<div class="ttc" id="atimer_8h_html"><div class="ttname"><a href="timer_8h.html">timer.h</a></div></div>
</div><!-- fragment --></div><!-- contents -->
</div><!-- doc-content -->
<!-- HTML footer for doxygen 1.8.18-->
<!-- start footer part -->
<div id="nav-path" class="navpath"><!-- id is needed for treeview function! -->
<ul>
<li class="navelem"><a class="el" href="dir_a7cc1eeded8f693d0da6c729bc88c45a.html">ortools</a></li><li class="navelem"><a class="el" href="dir_dddac007a45022d9da6ea1dee012c3b9.html">sat</a></li><li class="navelem"><a class="el" href="sat__solver_8h.html">sat_solver.h</a></li>
<li class="footer">Generated by
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.9.1 </li>
</ul>
</div>
</body>
</html>