Files
ortools-clone/docs/cpp/sat__inprocessing_8cc_source.html

236 lines
332 KiB
HTML
Raw Normal View History

2020-09-02 09:42:51 +02:00
<!-- 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"/>
2022-01-16 18:02:36 +01:00
<meta name="generator" content="Doxygen 1.8.15"/>
2020-09-02 09:42:51 +02:00
<meta name="viewport" content="width=device-width, initial-scale=1"/>
<title>OR-Tools: sat_inprocessing.cc 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>
2022-01-16 18:02:36 +01:00
<script type="text/javascript">
/* @license magnet:?xt=urn:btih:cf05388f2679ee054f2beb29a391d25f4e673ac3&amp;dn=gpl-2.0.txt GPL-v2 */
$(document).ready(initResizable);
/* @license-end */</script>
2020-09-02 09:42:51 +02:00
<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
2021-12-14 13:41:01 +01:00
&#160;<span id="projectnumber">9.2</span>
2020-09-02 09:42:51 +02:00
</div>
</td>
</tr>
</tbody>
</table>
</div>
<!-- end header part -->
2022-01-16 18:02:36 +01:00
<!-- Generated by Doxygen 1.8.15 -->
2020-09-02 09:42:51 +02:00
<script type="text/javascript">
2022-01-16 18:02:36 +01:00
/* @license magnet:?xt=urn:btih:cf05388f2679ee054f2beb29a391d25f4e673ac3&amp;dn=gpl-2.0.txt GPL-v2 */
var searchBox = new SearchBox("searchBox", "search",false,'Search');
2020-09-02 09:42:51 +02:00
/* @license-end */
</script>
<script type="text/javascript" src="menudata.js"></script>
<script type="text/javascript" src="menu.js"></script>
<script type="text/javascript">
2022-01-16 18:02:36 +01:00
/* @license magnet:?xt=urn:btih:cf05388f2679ee054f2beb29a391d25f4e673ac3&amp;dn=gpl-2.0.txt GPL-v2 */
2020-09-02 09:42:51 +02:00
$(function() {
initMenu('',true,false,'search.php','Search');
$(document).ready(function() { init_search(); });
});
2022-01-16 18:02:36 +01:00
/* @license-end */</script>
2020-09-02 09:42:51 +02:00
<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">
2022-01-16 18:02:36 +01:00
/* @license magnet:?xt=urn:btih:cf05388f2679ee054f2beb29a391d25f4e673ac3&amp;dn=gpl-2.0.txt GPL-v2 */
$(document).ready(function(){initNavTree('sat__inprocessing_8cc_source.html','');});
2020-09-02 09:42:51 +02:00
/* @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">
2022-01-16 18:02:36 +01:00
<div class="headertitle">
<div class="title">sat_inprocessing.cc</div> </div>
2020-09-02 09:42:51 +02:00
</div><!--header-->
<div class="contents">
2022-01-16 18:02:36 +01:00
<a href="sat__inprocessing_8cc.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-2021 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="preprocessor">#include &quot;<a class="code" href="sat__inprocessing_8h.html">ortools/sat/sat_inprocessing.h</a>&quot;</span></div><div class="line"><a name="l00015"></a><span class="lineno"> 15</span>&#160;</div><div class="line"><a name="l00016"></a><span class="lineno"> 16</span>&#160;<span class="preprocessor">#include &lt;cstdint&gt;</span></div><div class="line"><a name="l00017"></a><span class="lineno"> 17</span>&#160;<span class="preprocessor">#include &lt;limits&gt;</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">#include &quot;absl/container/inlined_vector.h&quot;</span></div><div class="line"><a name="l00020"></a><span class="lineno"> 20</span>&#160;<span class="preprocessor">#include &quot;<a class="code" href="stl__util_8h.html">ortools/base/stl_util.h</a>&quot;</span></div><div class="line"><a name="l00021"></a><span class="lineno"> 21</span>&#160;<span class="preprocessor">#include &quot;<a class="code" href="strong__vector_8h.html">ortools/base/strong_vector.h</a>&quot;</span></div><div class="line"><a name="l00022"></a><span class="lineno"> 22</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="l00023"></a><span class="lineno"> 23</span>&#160;<span class="preprocessor">#include &quot;<a class="code" href="probing_8h.html">ortools/sat/probing.h</a>&quot;</span></div><div class="line"><a name="l00024"></a><span class="lineno"> 24</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="l00025"></a><span class="lineno"> 25</span>&#
<div class="ttc" id="base_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="classoperations__research_1_1sat_1_1_inprocessing_html_a33abe26c0696a328c36dd0aa9f0b0f00"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_inprocessing.html#a33abe26c0696a328c36dd0aa9f0b0f00">operations_research::sat::Inprocessing::PresolveLoop</a></div><div class="ttdeci">bool PresolveLoop(SatPresolveOptions options)</div><div class="ttdef"><b>Definition:</b> <a href="sat__inprocessing_8cc_source.html#l00046">sat_inprocessing.cc:46</a></div></div>
<div class="ttc" id="macros_8h_html_a7f536a3b33f9bed8f75734e035d30725"><div class="ttname"><a href="macros_8h.html#a7f536a3b33f9bed8f75734e035d30725">DEBUG_MODE</a></div><div class="ttdeci">const bool DEBUG_MODE</div><div class="ttdef"><b>Definition:</b> <a href="macros_8h_source.html#l00024">macros.h:24</a></div></div>
<div class="ttc" id="class_wall_timer_html_aec56fe080959ecebec3feaed9dafde84"><div class="ttname"><a href="class_wall_timer.html#aec56fe080959ecebec3feaed9dafde84">WallTimer::Get</a></div><div class="ttdeci">double Get() const</div><div class="ttdef"><b>Definition:</b> <a href="timer_8h_source.html#l00045">timer.h:45</a></div></div>
<div class="ttc" id="structoperations__research_1_1sat_1_1_postsolve_clauses_html_a8cc6d9f1059f26a873442045a72e651e"><div class="ttname"><a href="structoperations__research_1_1sat_1_1_postsolve_clauses.html#a8cc6d9f1059f26a873442045a72e651e">operations_research::sat::PostsolveClauses::clauses</a></div><div class="ttdeci">std::deque&lt; std::vector&lt; Literal &gt; &gt; clauses</div><div class="ttdef"><b>Definition:</b> <a href="sat__inprocessing_8h_source.html#l00049">sat_inprocessing.h:49</a></div></div>
<div class="ttc" id="stl__util_8h_html"><div class="ttname"><a href="stl__util_8h.html">stl_util.h</a></div></div>
<div class="ttc" id="classoperations__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#l00052">clause.h:52</a></div></div>
<div class="ttc" id="sat__decision_8h_html"><div class="ttname"><a href="sat__decision_8h.html">sat_decision.h</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_sat_clause_html_a05691332c1a49213875440568a7580aa"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_clause.html#a05691332c1a49213875440568a7580aa">operations_research::sat::SatClause::AsSpan</a></div><div class="ttdeci">absl::Span&lt; const Literal &gt; AsSpan() const</div><div class="ttdef"><b>Definition:</b> <a href="clause_8h_source.html#l00091">clause.h:91</a></div></div>
<div class="ttc" id="structoperations__research_1_1sat_1_1_probing_options_html_a54320231778412ca00e50eb821c95aa6"><div class="ttname"><a href="structoperations__research_1_1sat_1_1_probing_options.html#a54320231778412ca00e50eb821c95aa6">operations_research::sat::ProbingOptions::log_info</a></div><div class="ttdeci">bool log_info</div><div class="ttdef"><b>Definition:</b> <a href="probing_8h_source.html#l00186">probing.h:186</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_binary_implication_graph_html_a1f591be5334541874ba049873235f0a9"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_binary_implication_graph.html#a1f591be5334541874ba049873235f0a9">operations_research::sat::BinaryImplicationGraph::Propagate</a></div><div class="ttdeci">bool Propagate(Trail *trail) final</div><div class="ttdef"><b>Definition:</b> <a href="clause_8cc_source.html#l00759">clause.cc:759</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_variables_assignment_html_acfd1646011e643f58fd7dc66d9cc90a5"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_variables_assignment.html#acfd1646011e643f58fd7dc66d9cc90a5">operations_research::sat::VariablesAssignment::LiteralIsFalse</a></div><div class="ttdeci">bool LiteralIsFalse(Literal literal) const</div><div class="ttdef"><b>Definition:</b> <a href="sat__base_8h_source.html#l00149">sat_base.h:149</a></div></div>
<div class="ttc" id="classabsl_1_1_strong_vector_html_ad69bd11391be1a1dba5c8202259664f8"><div class="ttname"><a href="classabsl_1_1_strong_vector.html#ad69bd11391be1a1dba5c8202259664f8">absl::StrongVector::begin</a></div><div class="ttdeci">iterator begin()</div><div class="ttdef"><b>Definition:</b> <a href="strong__vector_8h_source.html#l00138">strong_vector.h:138</a></div></div>
<div class="ttc" id="namespaceoperations__research_1_1math__opt_html_a5de89a1f6e3f80a49a0d76136d8044e2"><div class="ttname"><a href="namespaceoperations__research_1_1math__opt.html#a5de89a1f6e3f80a49a0d76136d8044e2">operations_research::math_opt::swap</a></div><div class="ttdeci">void swap(IdMap&lt; K, V &gt; &amp;a, IdMap&lt; K, V &gt; &amp;b)</div><div class="ttdef"><b>Definition:</b> <a href="id__map_8h_source.html#l00263">id_map.h:263</a></div></div>
<div class="ttc" id="classoperations__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#l00152">sat_base.h:152</a></div></div>
<div class="ttc" id="classoperations__research_1_1_sparse_bitset_html"><div class="ttname"><a href="classoperations__research_1_1_sparse_bitset.html">operations_research::SparseBitset&lt; LiteralIndex &gt;</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_literal_html_a4a11c7c4d7706c09de5e18707c3b5c62"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_literal.html#a4a11c7c4d7706c09de5e18707c3b5c62">operations_research::sat::Literal::Index</a></div><div class="ttdeci">LiteralIndex Index() const</div><div class="ttdef"><b>Definition:</b> <a href="sat__base_8h_source.html#l00086">sat_base.h:86</a></div></div>
<div class="ttc" id="classoperations__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#l00093">sat_base.h:93</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_binary_implication_graph_html_a6fac58ca16fd746d7488a0a97f6965bd"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_binary_implication_graph.html#a6fac58ca16fd746d7488a0a97f6965bd">operations_research::sat::BinaryImplicationGraph::RepresentativeOf</a></div><div class="ttdeci">Literal RepresentativeOf(Literal l) const</div><div class="ttdef"><b>Definition:</b> <a href="clause_8h_source.html#l00562">clause.h:562</a></div></div>
<div class="ttc" id="structoperations__research_1_1sat_1_1_sat_presolve_options_html_a54320231778412ca00e50eb821c95aa6"><div class="ttname"><a href="structoperations__research_1_1sat_1_1_sat_presolve_options.html#a54320231778412ca00e50eb821c95aa6">operations_research::sat::SatPresolveOptions::log_info</a></div><div class="ttdeci">bool log_info</div><div class="ttdef"><b>Definition:</b> <a href="sat__inprocessing_8h_source.html#l00062">sat_inprocessing.h:62</a></div></div>
<div class="ttc" id="classoperations__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#l00066">sat_base.h:66</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_bounded_variable_elimination_html_a1837f97f35b2db520af88985ea7e5666"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_bounded_variable_elimination.html#a1837f97f35b2db520af88985ea7e5666">operations_research::sat::BoundedVariableElimination::DoOneRound</a></div><div class="ttdeci">bool DoOneRound(bool log_info)</div><div class="ttdef"><b>Definition:</b> <a href="sat__inprocessing_8cc_source.html#l01077">sat_inprocessing.cc:1077</a></div></div>
<div class="ttc" id="classabsl_1_1_strong_vector_html_ac8bb3912a3ce86b15842e79d0b421204"><div class="ttname"><a href="classabsl_1_1_strong_vector.html#ac8bb3912a3ce86b15842e79d0b421204">absl::StrongVector::clear</a></div><div class="ttdeci">void clear()</div><div class="ttdef"><b>Definition:</b> <a href="strong__vector_8h_source.html#l00170">strong_vector.h:170</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_inprocessing_html_a5641f2b95c6ba972fff06ddd6ff5e29b"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_inprocessing.html#a5641f2b95c6ba972fff06ddd6ff5e29b">operations_research::sat::Inprocessing::RemoveFixedAndEquivalentVariables</a></div><div class="ttdeci">bool RemoveFixedAndEquivalentVariables(bool log_info)</div><div class="ttdef"><b>Definition:</b> <a href="sat__inprocessing_8cc_source.html#l00253">sat_inprocessing.cc:253</a></div></div>
<div class="ttc" id="namespacegtl_html_a288a1dc92da5d3ad62d4bc4cec9e8b1d"><div class="ttname"><a href="namespacegtl.html#a288a1dc92da5d3ad62d4bc4cec9e8b1d">gtl::STLSortAndRemoveDuplicates</a></div><div class="ttdeci">void STLSortAndRemoveDuplicates(T *v, const LessFunc &amp;less_func)</div><div class="ttdef"><b>Definition:</b> <a href="stl__util_8h_source.html#l00058">stl_util.h:58</a></div></div>
<div class="ttc" id="structoperations__research_1_1sat_1_1_sat_presolve_options_html_ac68dd5a27fd973b215de47442bacf1ac"><div class="ttname"><a href="structoperations__research_1_1sat_1_1_sat_presolve_options.html#ac68dd5a27fd973b215de47442bacf1ac">operations_research::sat::SatPresolveOptions::extract_binary_clauses_in_probing</a></div><div class="ttdeci">bool extract_binary_clauses_in_probing</div><div class="ttdef"><b>Definition:</b> <a href="sat__inprocessing_8h_source.html#l00065">sat_inprocessing.h:65</a></div></div>
<div class="ttc" id="class_wall_timer_html_a07aaf1227e4d645f15e0a964f54ef291"><div class="ttname"><a href="class_wall_timer.html#a07aaf1227e4d645f15e0a964f54ef291">WallTimer::Start</a></div><div class="ttdeci">void Start()</div><div class="ttdef"><b>Definition:</b> <a href="timer_8h_source.html#l00031">timer.h:31</a></div></div>
<div class="ttc" id="classoperations__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#l00083">sat_solver.h:83</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_literal_watchers_html_a38c7c4ca12035b254d9497a401606e0c"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_literal_watchers.html#a38c7c4ca12035b254d9497a401606e0c">operations_research::sat::LiteralWatchers::DetachAllClauses</a></div><div class="ttdeci">void DetachAllClauses()</div><div class="ttdef"><b>Definition:</b> <a href="clause_8cc_source.html#l00312">clause.cc:312</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_binary_implication_graph_html_a29218ade45d7df87f01459565526cfe2"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_binary_implication_graph.html#a29218ade45d7df87f01459565526cfe2">operations_research::sat::BinaryImplicationGraph::ComputeTransitiveReduction</a></div><div class="ttdeci">bool ComputeTransitiveReduction(bool log_info=false)</div><div class="ttdef"><b>Definition:</b> <a href="clause_8cc_source.html#l01342">clause.cc:1342</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_binary_implication_graph_html_ab64429b401679aee0bbd618449a9152a"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_binary_implication_graph.html#ab64429b401679aee0bbd618449a9152a">operations_research::sat::BinaryImplicationGraph::CleanupAllRemovedVariables</a></div><div class="ttdeci">void CleanupAllRemovedVariables()</div><div class="ttdef"><b>Definition:</b> <a href="clause_8cc_source.html#l01972">clause.cc:1972</a></div></div>
<div class="ttc" id="classoperations__research_1_1_integer_priority_queue_html_a21cecbc35e3da9931f94afa3229354dc"><div class="ttname"><a href="classoperations__research_1_1_integer_priority_queue.html#a21cecbc35e3da9931f94afa3229354dc">operations_research::IntegerPriorityQueue::Reserve</a></div><div class="ttdeci">void Reserve(int n)</div><div class="ttdef"><b>Definition:</b> <a href="integer__pq_8h_source.html#l00048">integer_pq.h:48</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_binary_implication_graph_html_ae9a2f518d6edd64467abcef2c70934ff"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_binary_implication_graph.html#ae9a2f518d6edd64467abcef2c70934ff">operations_research::sat::BinaryImplicationGraph::num_implications</a></div><div class="ttdeci">int64_t num_implications() const</div><div class="ttdef"><b>Definition:</b> <a href="clause_8h_source.html#l00637">clause.h:637</a></div></div>
<div class="ttc" id="constraint__solver_2table_8cc_html_a9293e4d29cac928301645070dd307683"><div class="ttname"><a href="constraint__solver_2table_8cc.html#a9293e4d29cac928301645070dd307683">b</a></div><div class="ttdeci">int64_t b</div><div class="ttdef"><b>Definition:</b> <a href="constraint__solver_2table_8cc_source.html#l00047">constraint_solver/table.cc:47</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_stamping_simplifier_html_a1837f97f35b2db520af88985ea7e5666"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_stamping_simplifier.html#a1837f97f35b2db520af88985ea7e5666">operations_research::sat::StampingSimplifier::DoOneRound</a></div><div class="ttdeci">bool DoOneRound(bool log_info)</div><div class="ttdef"><b>Definition:</b> <a href="sat__inprocessing_8cc_source.html#l00577">sat_inprocessing.cc:577</a></div></div>
<div class="ttc" id="timer_8h_html"><div class="ttname"><a href="timer_8h.html">timer.h</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_binary_implication_graph_html_abcad56047cef75a12528fe99794a6e1e"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_binary_implication_graph.html#abcad56047cef75a12528fe99794a6e1e">operations_research::sat::BinaryImplicationGraph::RemoveFixedVariables</a></div><div class="ttdeci">void RemoveFixedVariables()</div><div class="ttdef"><b>Definition:</b> <a href="clause_8cc_source.html#l00991">clause.cc:991</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_stamping_simplifier_html_a23f1e3b69e90585b8c746ecb2c829d16"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_stamping_simplifier.html#a23f1e3b69e90585b8c746ecb2c829d16">operations_research::sat::StampingSimplifier::ComputeStampsForNextRound</a></div><div class="ttdeci">bool ComputeStampsForNextRound(bool log_info)</div><div class="ttdef"><b>Definition:</b> <a href="sat__inprocessing_8cc_source.html#l00613">sat_inprocessing.cc:613</a></div></div>
<div class="ttc" id="structoperations__research_1_1sat_1_1_postsolve_clauses_html_ae70f41a3895b08dd35056d97eec1800e"><div class="ttname"><a href="structoperations__research_1_1sat_1_1_postsolve_clauses.html#ae70f41a3895b08dd35056d97eec1800e">operations_research::sat::PostsolveClauses::AddClauseWithSpecialLiteral</a></div><div class="ttdeci">void AddClauseWithSpecialLiteral(Literal literal, absl::Span&lt; const Literal &gt; clause)</div><div class="ttdef"><b>Definition:</b> <a href="sat__inprocessing_8cc_source.html#l00029">sat_inprocessing.cc:29</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_stamping_simplifier_html_ad23fe7afc319b790417c946b34c5e40b"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_stamping_simplifier.html#ad23fe7afc319b790417c946b34c5e40b">operations_research::sat::StampingSimplifier::ComputeStamps</a></div><div class="ttdeci">bool ComputeStamps()</div><div class="ttdef"><b>Definition:</b> <a href="sat__inprocessing_8cc_source.html#l00672">sat_inprocessing.cc:672</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_stamping_simplifier_html_a318a00d87baa05fd3e351fa688836de2"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_stamping_simplifier.html#a318a00d87baa05fd3e351fa688836de2">operations_research::sat::StampingSimplifier::ImplicationIsInTree</a></div><div class="ttdeci">bool ImplicationIsInTree(Literal a, Literal b) const</div><div class="ttdef"><b>Definition:</b> <a href="sat__inprocessing_8h_source.html#l00200">sat_inprocessing.h:200</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_literal_watchers_html_a287676c504a640a5569710d352ef6585"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_literal_watchers.html#a287676c504a640a5569710d352ef6585">operations_research::sat::LiteralWatchers::InprocessingRemoveClause</a></div><div class="ttdeci">void InprocessingRemoveClause(SatClause *clause)</div><div class="ttdef"><b>Definition:</b> <a href="clause_8cc_source.html#l00359">clause.cc:359</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_binary_implication_graph_html_a92844929b07caef45924b8c5e3a5a05c"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_binary_implication_graph.html#a92844929b07caef45924b8c5e3a5a05c">operations_research::sat::BinaryImplicationGraph::IsRedundant</a></div><div class="ttdeci">bool IsRedundant(Literal l) const</div><div class="ttdef"><b>Definition:</b> <a href="clause_8h_source.html#l00622">clause.h:622</a></div></div>
<div class="ttc" id="structoperations__research_1_1sat_1_1_probing_options_html"><div class="ttname"><a href="structoperations__research_1_1sat_1_1_probing_options.html">operations_research::sat::ProbingOptions</a></div><div class="ttdef"><b>Definition:</b> <a href="probing_8h_source.html#l00123">probing.h:123</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_sat_clause_html_af9593d4a5ff4274efaf429cb4f9e57cc"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_clause.html#af9593d4a5ff4274efaf429cb4f9e57cc">operations_research::sat::SatClause::size</a></div><div class="ttdeci">int size() const</div><div class="ttdef"><b>Definition:</b> <a href="clause_8h_source.html#l00066">clause.h:66</a></div></div>
<div class="ttc" id="classoperations__research_1_1_integer_priority_queue_html_a06fe50b32a75c0a071b68ebbacb8f681"><div class="ttname"><a href="classoperations__research_1_1_integer_priority_queue.html#a06fe50b32a75c0a071b68ebbacb8f681">operations_research::IntegerPriorityQueue::Contains</a></div><div class="ttdeci">bool Contains(int index) const</div><div class="ttdef"><b>Definition:</b> <a href="integer__pq_8h_source.html#l00067">integer_pq.h:67</a></div></div>
<div class="ttc" id="alldiff__cst_8cc_html_a26e6db9bcc64b584051ecc28171ed11f"><div class="ttname"><a href="alldiff__cst_8cc.html#a26e6db9bcc64b584051ecc28171ed11f">max</a></div><div class="ttdeci">int64_t max</div><div class="ttdef"><b>Definition:</b> <a href="alldiff__cst_8cc_source.html#l00140">alldiff_cst.cc:140</a></div></div>
<div class="ttc" id="strong__vector_8h_html"><div class="ttname"><a href="strong__vector_8h.html">strong_vector.h</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_binary_implication_graph_html_aac261e221628d6a51be7243563659929"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_binary_implication_graph.html#aac261e221628d6a51be7243563659929">operations_research::sat::BinaryImplicationGraph::DetectEquivalences</a></div><div class="ttdeci">bool DetectEquivalences(bool log_info=false)</div><div class="ttdef"><b>Definition:</b> <a href="clause_8cc_source.html#l01155">clause.cc:1155</a></div></div>
<div class="ttc" id="classabsl_1_1_strong_vector_html_a4e3670a285a3642eaa07f66766cffa72"><div class="ttname"><a href="classabsl_1_1_strong_vector.html#a4e3670a285a3642eaa07f66766cffa72">absl::StrongVector::resize</a></div><div class="ttdeci">void resize(size_type new_size)</div><div class="ttdef"><b>Definition:</b> <a href="strong__vector_8h_source.html#l00150">strong_vector.h:150</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_literal_html_a239e1315c4e975a35537790ba0d913a7"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_literal.html#a239e1315c4e975a35537790ba0d913a7">operations_research::sat::Literal::NegatedIndex</a></div><div class="ttdeci">LiteralIndex NegatedIndex() const</div><div class="ttdef"><b>Definition:</b> <a href="sat__base_8h_source.html#l00087">sat_base.h:87</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_sat_parameters_html_a11e0402a63ef761094d58f52b0936ac1"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_parameters.html#a11e0402a63ef761094d58f52b0936ac1">operations_research::sat::SatParameters::presolve_bve_clause_weight</a></div><div class="ttdeci">int32_t presolve_bve_clause_weight() const</div><div class="ttdef"><b>Definition:</b> <a href="sat__parameters_8pb_8h_source.html#l05303">sat_parameters.pb.h:5303</a></div></div>
<div class="ttc" id="classabsl_1_1_strong_vector_html_a644718bb2fb240de962dc3c9a1fdf0dc"><div class="ttname"><a href="classabsl_1_1_strong_vector.html#a644718bb2fb240de962dc3c9a1fdf0dc">absl::StrongVector::empty</a></div><div class="ttdeci">bool empty() const</div><div class="ttdef"><b>Definition:</b> <a href="strong__vector_8h_source.html#l00156">strong_vector.h:156</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_binary_implication_graph_html_af18b28ba180d18c4e4f524d6fde71f28"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_binary_implication_graph.html#af18b28ba180d18c4e4f524d6fde71f28">operations_research::sat::BinaryImplicationGraph::literal_size</a></div><div class="ttdeci">int64_t literal_size() const</div><div class="ttdef"><b>Definition:</b> <a href="clause_8h_source.html#l00638">clause.h:638</a></div></div>
<div class="ttc" id="base_2logging_8h_html_a46e69120fbd3b36e6960e096d23b66f0"><div class="ttname"><a href="base_2logging_8h.html#a46e69120fbd3b36e6960e096d23b66f0">DCHECK_NE</a></div><div class="ttdeci">#define DCHECK_NE(val1, val2)</div><div class="ttdef"><b>Definition:</b> <a href="base_2logging_8h_source.html#l00891">base/logging.h:891</a></div></div>
<div class="ttc" id="classoperations__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#l00380">sat_base.h:380</a></div></div>
<div class="ttc" id="classoperations__research_1_1_integer_priority_queue_html_a260b134ff6e3aa564e8ba1f879aea3d9"><div class="ttname"><a href="classoperations__research_1_1_integer_priority_queue.html#a260b134ff6e3aa564e8ba1f879aea3d9">operations_research::IntegerPriorityQueue::Add</a></div><div class="ttdeci">void Add(Element element)</div><div class="ttdef"><b>Definition:</b> <a href="integer__pq_8h_source.html#l00071">integer_pq.h:71</a></div></div>
<div class="ttc" id="classoperations__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#l00160">sat_base.h:160</a></div></div>
<div class="ttc" id="structoperations__research_1_1sat_1_1_sat_presolve_options_html_a9251c24a19aaef6f5134a615eff02277"><div class="ttname"><a href="structoperations__research_1_1sat_1_1_sat_presolve_options.html#a9251c24a19aaef6f5134a615eff02277">operations_research::sat::SatPresolveOptions::use_transitive_reduction</a></div><div class="ttdeci">bool use_transitive_reduction</div><div class="ttdef"><b>Definition:</b> <a href="sat__inprocessing_8h_source.html#l00073">sat_inprocessing.h:73</a></div></div>
<div class="ttc" id="classabsl_1_1_strong_vector_html_acad38d52497a975bfb6f2f6acd76631f"><div class="ttname"><a href="classabsl_1_1_strong_vector.html#acad38d52497a975bfb6f2f6acd76631f">absl::StrongVector::end</a></div><div class="ttdeci">iterator end()</div><div class="ttdef"><b>Definition:</b> <a href="strong__vector_8h_source.html#l00140">strong_vector.h:140</a></div></div>
<div class="ttc" id="classoperations__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#l01623">sat_solver.cc:1623</a></div></div>
<div class="ttc" id="classoperations__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#l00455">clause.cc:455</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_variables_assignment_html_a142694366986039454f53b38e8378815"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_variables_assignment.html#a142694366986039454f53b38e8378815">operations_research::sat::VariablesAssignment::LiteralIsAssigned</a></div><div class="ttdeci">bool LiteralIsAssigned(Literal literal) const</div><div class="ttdef"><b>Definition:</b> <a href="sat__base_8h_source.html#l00155">sat_base.h:155</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_inprocessing_html_a7fefd67efe60192540adcc4bdea29836"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_inprocessing.html#a7fefd67efe60192540adcc4bdea29836">operations_research::sat::Inprocessing::LevelZeroPropagate</a></div><div class="ttdeci">bool LevelZeroPropagate()</div><div class="ttdef"><b>Definition:</b> <a href="sat__inprocessing_8cc_source.html#l00223">sat_inprocessing.cc:223</a></div></div>
<div class="ttc" id="classabsl_1_1_strong_vector_html_a9263000d449fdccb6cb70b303063e60b"><div class="ttname"><a href="classabsl_1_1_strong_vector.html#a9263000d449fdccb6cb70b303063e60b">absl::StrongVector::push_back</a></div><div class="ttdeci">void push_back(const value_type &amp;x)</div><div class="ttdef"><b>Definition:</b> <a href="strong__vector_8h_source.html#l00158">strong_vector.h:158</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_binary_implication_graph_html_ab95a602604a2056d11cba9119e490236"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_binary_implication_graph.html#ab95a602604a2056d11cba9119e490236">operations_research::sat::BinaryImplicationGraph::RemoveBooleanVariable</a></div><div class="ttdeci">void RemoveBooleanVariable(BooleanVariable var, std::deque&lt; std::vector&lt; Literal &gt;&gt; *postsolve_clauses)</div><div class="ttdef"><b>Definition:</b> <a href="clause_8cc_source.html#l01929">clause.cc:1929</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_stamping_simplifier_html_aaf918948eb5d49c45195671882bbb400"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_stamping_simplifier.html#aaf918948eb5d49c45195671882bbb400">operations_research::sat::StampingSimplifier::SampleTreeAndFillParent</a></div><div class="ttdeci">void SampleTreeAndFillParent()</div><div class="ttdef"><b>Definition:</b> <a href="sat__inprocessing_8cc_source.html#l00637">sat_inprocessing.cc:637</a></div></div>
<div class="ttc" id="pack_8cc_html_a750b5d744c39a06bfb13e6eb010e35d0"><div class="ttname"><a href="pack_8cc.html#a750b5d744c39a06bfb13e6eb010e35d0">index</a></div><div class="ttdeci">int index</div><div class="ttdef"><b>Definition:</b> <a href="pack_8cc_source.html#l00509">pack.cc:509</a></div></div>
<div class="ttc" id="sat__inprocessing_8cc_html_a73c06a952919ea45217c5a8ec59c4088"><div class="ttname"><a href="sat__inprocessing_8cc.html#a73c06a952919ea45217c5a8ec59c4088">RETURN_IF_FALSE</a></div><div class="ttdeci">#define RETURN_IF_FALSE(f)</div><div class="ttdef"><b>Definition:</b> <a href="sat__inprocessing_8cc_source.html#l00043">sat_inprocessing.cc:43</a></div></div>
<div class="ttc" id="classoperations__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#l00220">clause.h:220</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_binary_implication_graph_html_a7eb6126b57ff4ab8246fe54f4e5550f4"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_binary_implication_graph.html#a7eb6126b57ff4ab8246fe54f4e5550f4">operations_research::sat::BinaryImplicationGraph::DirectImplications</a></div><div class="ttdeci">const std::vector&lt; Literal &gt; &amp; DirectImplications(Literal literal)</div><div class="ttdef"><b>Definition:</b> <a href="clause_8cc_source.html#l01841">clause.cc:1841</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_binary_implication_graph_html_ad7144ed926660fe38c0cfbeedbaa8dfc"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_binary_implication_graph.html#ad7144ed926660fe38c0cfbeedbaa8dfc">operations_research::sat::BinaryImplicationGraph::IsDag</a></div><div class="ttdeci">bool IsDag() const</div><div class="ttdef"><b>Definition:</b> <a href="clause_8h_source.html#l00544">clause.h:544</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_inprocessing_html_a55d41aea8582d314b14874b133eb8bcb"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_inprocessing.html#a55d41aea8582d314b14874b133eb8bcb">operations_research::sat::Inprocessing::MoreFixedVariableToClean</a></div><div class="ttdeci">bool MoreFixedVariableToClean() const</div><div class="ttdef"><b>Definition:</b> <a href="sat__inprocessing_8cc_source.html#l00212">sat_inprocessing.cc:212</a></div></div>
<div class="ttc" id="classoperations__research_1_1_integer_priority_queue_html_a8f1cb7a5e2de2945a3dcecd15a09a0a4"><div class="ttname"><a href="classoperations__research_1_1_integer_priority_queue.html#a8f1cb7a5e2de2945a3dcecd15a09a0a4">operations_research::IntegerPriorityQueue::Top</a></div><div class="ttdeci">Element Top() const</div><div class="ttdef"><b>Definition:</b> <a href="integer__pq_8h_source.html#l00078">integer_pq.h:78</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_literal_watchers_html_ab6174cc15ef4df301b31aff43216039e"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_literal_watchers.html#ab6174cc15ef4df301b31aff43216039e">operations_research::sat::LiteralWatchers::num_watched_clauses</a></div><div class="ttdeci">int64_t num_watched_clauses() const</div><div class="ttdef"><b>Definition:</b> <a href="clause_8h_source.html#l00238">clause.h:238</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_inprocessing_html_a2e5437cb35da63545f954a80536023e0"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_inprocessing.html#a2e5437cb35da63545f954a80536023e0">operations_research::sat::Inprocessing::InprocessingRound</a></div><div class="ttdeci">bool InprocessingRound()</div><div class="ttdef"><b>Definition:</b> <a href="sat__inprocessing_8cc_source.html#l00141">sat_inprocessing.cc:141</a></div></div>
<div class="ttc" id="classoperations__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#l01248">sat_solver.cc:1248</a></div></div>
<div class="ttc" id="base_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#l00702">base/logging.h:702</a></div></div>
<div class="ttc" id="classoperations__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#l00212">clause.h:212</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_binary_implication_graph_html_a1858011d343c77f650753e14778c5232"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_binary_implication_graph.html#a1858011d343c77f650753e14778c5232">operations_research::sat::BinaryImplicationGraph::NumImplicationOnVariableRemoval</a></div><div class="ttdeci">int64_t NumImplicationOnVariableRemoval(BooleanVariable var)</div><div class="ttdef"><b>Definition:</b> <a href="clause_8cc_source.html#l01909">clause.cc:1909</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_sat_parameters_html_a10effdf49aaf30adb4b5ce2338be3470"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_parameters.html#a10effdf49aaf30adb4b5ce2338be3470">operations_research::sat::SatParameters::presolve_bve_threshold</a></div><div class="ttdeci">int32_t presolve_bve_threshold() const</div><div class="ttdef"><b>Definition:</b> <a href="sat__parameters_8pb_8h_source.html#l05275">sat_parameters.pb.h:5275</a></div></div>
<div class="ttc" id="namespaceoperations__research_1_1sat_html_a865df3eeca0b96bf7fda22b016b80bc2"><div class="ttname"><a href="namespaceoperations__research_1_1sat.html#a865df3eeca0b96bf7fda22b016b80bc2">operations_research::sat::FailedLiteralProbingRound</a></div><div class="ttdeci">bool FailedLiteralProbingRound(ProbingOptions options, Model *model)</div><div class="ttdef"><b>Definition:</b> <a href="probing_8cc_source.html#l00354">probing.cc:354</a></div></div>
<div class="ttc" id="classoperations__research_1_1_integer_priority_queue_html_a115ac0fc2fcd2f50cf756b94a329fb3c"><div class="ttname"><a href="classoperations__research_1_1_integer_priority_queue.html#a115ac0fc2fcd2f50cf756b94a329fb3c">operations_research::IntegerPriorityQueue::ChangePriority</a></div><div class="ttdeci">void ChangePriority(Element element)</div><div class="ttdef"><b>Definition:</b> <a href="integer__pq_8h_source.html#l00105">integer_pq.h:105</a></div></div>
<div class="ttc" id="base_2logging_8h_html_a09f7d88282cf92c9f231270ac113e5c6"><div class="ttname"><a href="base_2logging_8h.html#a09f7d88282cf92c9f231270ac113e5c6">LOG_IF</a></div><div class="ttdeci">#define LOG_IF(severity, condition)</div><div class="ttdef"><b>Definition:</b> <a href="base_2logging_8h_source.html#l00479">base/logging.h:479</a></div></div>
<div class="ttc" id="classoperations__research_1_1_integer_priority_queue_html_a701a584ce72cccbcce9cb0656b6c898b"><div class="ttname"><a href="classoperations__research_1_1_integer_priority_queue.html#a701a584ce72cccbcce9cb0656b6c898b">operations_research::IntegerPriorityQueue::Pop</a></div><div class="ttdeci">void Pop()</div><div class="ttdef"><b>Definition:</b> <a href="integer__pq_8h_source.html#l00079">integer_pq.h:79</a></div></div>
<div class="ttc" id="base_2logging_8h_html_ae17f8119c108cf3070bad3449c7e0006"><div class="ttname"><a href="base_2logging_8h.html#ae17f8119c108cf3070bad3449c7e0006">DCHECK</a></div><div class="ttdeci">#define DCHECK(condition)</div><div class="ttdef"><b>Definition:</b> <a href="base_2logging_8h_source.html#l00889">base/logging.h:889</a></div></div>
<div class="ttc" id="classoperations__research_1_1_integer_priority_queue_html_a8e12342fc420701fbffd97025421575a"><div class="ttname"><a href="classoperations__research_1_1_integer_priority_queue.html#a8e12342fc420701fbffd97025421575a">operations_research::IntegerPriorityQueue::IsEmpty</a></div><div class="ttdeci">bool IsEmpty() const</div><div class="ttdef"><b>Definition:</b> <a href="integer__pq_8h_source.html#l00057">integer_pq.h:57</a></div></div>
<div class="ttc" id="classoperations__research_1_1_time_limit_html_ac7e861414a70fc937d18bc7ca743fc98"><div class="ttname"><a href="classoperations__research_1_1_time_limit.html#ac7e861414a70fc937d18bc7ca743fc98">operations_research::TimeLimit::GetElapsedDeterministicTime</a></div><div class="ttdeci">double GetElapsedDeterministicTime() const</div><div class="ttdoc">Returns the elapsed deterministic time since the construction of this object.</div><div class="ttdef"><b>Definition:</b> <a href="time__limit_8h_source.html#l00261">time_limit.h:261</a></div></div>
<div class="ttc" id="classabsl_1_1_strong_vector_html"><div class="ttname"><a href="classabsl_1_1_strong_vector.html">absl::StrongVector&lt; LiteralIndex, bool &gt;</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_sat_clause_html_a78c28538faebd5f023cd4511df6ffee4"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_clause.html#a78c28538faebd5f023cd4511df6ffee4">operations_research::sat::SatClause::empty</a></div><div class="ttdeci">int empty() const</div><div class="ttdef"><b>Definition:</b> <a href="clause_8h_source.html#l00067">clause.h:67</a></div></div>
<div class="ttc" id="classoperations__research_1_1_time_limit_html_a810d5f7aaf80cc09cf5a094e20c1aaca"><div class="ttname"><a href="classoperations__research_1_1_time_limit.html#a810d5f7aaf80cc09cf5a094e20c1aaca">operations_research::TimeLimit::LimitReached</a></div><div class="ttdeci">bool LimitReached()</div><div class="ttdoc">Returns true when the external limit is true, or the deterministic time is over the deterministic lim...</div><div class="ttdef"><b>Definition:</b> <a href="time__limit_8h_source.html#l00534">time_limit.h:534</a></div></div>
<div class="ttc" id="base_2logging_8h_html_ae89df3243bbb8341130c7b3f44145ea0"><div class="ttname"><a href="base_2logging_8h.html#ae89df3243bbb8341130c7b3f44145ea0">DCHECK_EQ</a></div><div class="ttdeci">#define DCHECK_EQ(val1, val2)</div><div class="ttdef"><b>Definition:</b> <a href="base_2logging_8h_source.html#l00890">base/logging.h:890</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_sat_decision_policy_html_a9db2d9ca018c68d3f84ee946e3603886"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_sat_decision_policy.html#a9db2d9ca018c68d3f84ee946e3603886">operations_research::sat::SatDecisionPolicy::MaybeEnablePhaseSaving</a></div><div class="ttdeci">void MaybeEnablePhaseSaving(bool save_phase)</div><div class="ttdef"><b>Definition:</b> <a href="sat__decision_8h_source.html#l00086">sat_decision.h:86</a></div></div>
<div class="ttc" id="structoperations__research_1_1sat_1_1_sat_presolve_options_html"><div class="ttname"><a href="structoperations__research_1_1sat_1_1_sat_presolve_options.html">operations_research::sat::SatPresolveOptions</a></div><div class="ttdef"><b>Definition:</b> <a href="sat__inprocessing_8h_source.html#l00056">sat_inprocessing.h:56</a></div></div>
<div class="ttc" id="classoperations__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#l00227">time_limit.h:227</a></div></div>
<div class="ttc" id="structoperations__research_1_1sat_1_1_probing_options_html_a4f572c68b7bf3aac70b3f5292398ff7b"><div class="ttname"><a href="structoperations__research_1_1sat_1_1_probing_options.html#a4f572c68b7bf3aac70b3f5292398ff7b">operations_research::sat::ProbingOptions::deterministic_limit</a></div><div class="ttdeci">double deterministic_limit</div><div class="ttdef"><b>Definition:</b> <a href="probing_8h_source.html#l00144">probing.h:144</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_binary_implication_graph_html_abbf0624c5d966c4dcf29eece343e0592"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_binary_implication_graph.html#abbf0624c5d966c4dcf29eece343e0592">operations_research::sat::BinaryImplicationGraph::FindFailedLiteralAroundVar</a></div><div class="ttdeci">bool FindFailedLiteralAroundVar(BooleanVariable var, bool *is_unsat)</div><div class="ttdef"><b>Definition:</b> <a href="clause_8cc_source.html#l01884">clause.cc:1884</a></div></div>
<div class="ttc" id="classoperations__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#l00361">sat_solver.h:361</a></div></div>
<div class="ttc" id="namespaceoperations__research_html"><div class="ttname"><a href="namespaceoperations__research.html">operations_research</a></div><div class="ttdoc">Collection of objects used to extend the Constraint Solver library.</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="probing_8h_html"><div class="ttname"><a href="probing_8h.html">probing.h</a></div></div>
<div class="ttc" id="structoperations__research_1_1sat_1_1_probing_options_html_a9d4ed6726cbb0ec29c0d62faec4b6405"><div class="ttname"><a href="structoperations__research_1_1sat_1_1_probing_options.html#a9d4ed6726cbb0ec29c0d62faec4b6405">operations_research::sat::ProbingOptions::extract_binary_clauses</a></div><div class="ttdeci">bool extract_binary_clauses</div><div class="ttdef"><b>Definition:</b> <a href="probing_8h_source.html#l00164">probing.h:164</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_stamping_simplifier_html_a5ea60f6738dfbc19da6098ea7e706fae"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_stamping_simplifier.html#a5ea60f6738dfbc19da6098ea7e706fae">operations_research::sat::StampingSimplifier::ProcessClauses</a></div><div class="ttdeci">bool ProcessClauses()</div><div class="ttdef"><b>Definition:</b> <a href="sat__inprocessing_8cc_source.html#l00757">sat_inprocessing.cc:757</a></div></div>
<div class="ttc" id="classabsl_1_1_strong_vector_html_a184fe69018ae421dcf31c964bfe40576"><div class="ttname"><a href="classabsl_1_1_strong_vector.html#a184fe69018ae421dcf31c964bfe40576">absl::StrongVector::assign</a></div><div class="ttdeci">void assign(size_type n, const value_type &amp;val)</div><div class="ttdef"><b>Definition:</b> <a href="strong__vector_8h_source.html#l00131">strong_vector.h:131</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_inprocessing_html_ae07d2afcdeb4149564918774bb584c17"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_inprocessing.html#ae07d2afcdeb4149564918774bb584c17">operations_research::sat::Inprocessing::MoreRedundantVariableToClean</a></div><div class="ttdeci">bool MoreRedundantVariableToClean() const</div><div class="ttdef"><b>Definition:</b> <a href="sat__inprocessing_8cc_source.html#l00217">sat_inprocessing.cc:217</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_inprocessing_html_af933a36985c24ffed84da1ac4f159e43"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_inprocessing.html#af933a36985c24ffed84da1ac4f159e43">operations_research::sat::Inprocessing::DetectEquivalencesAndStamp</a></div><div class="ttdeci">bool DetectEquivalencesAndStamp(bool use_transitive_reduction, bool log_info)</div><div class="ttdef"><b>Definition:</b> <a href="sat__inprocessing_8cc_source.html#l00231">sat_inprocessing.cc:231</a></div></div>
<div class="ttc" id="namespaceoperations__research_1_1sat_html_a2dbcb7017d468a17bdb30252af5c6c31"><div class="ttname"><a href="namespaceoperations__research_1_1sat.html#a2dbcb7017d468a17bdb30252af5c6c31">operations_research::sat::kNoLiteralIndex</a></div><div class="ttdeci">const LiteralIndex kNoLiteralIndex(-1)</div></div>
<div class="ttc" id="expr__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#l01874">expr_array.cc:1874</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_literal_watchers_html_a74971b631e1b357b2f440dff321b5c9b"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_literal_watchers.html#a74971b631e1b357b2f440dff321b5c9b">operations_research::sat::LiteralWatchers::InprocessingAddClause</a></div><div class="ttdeci">SatClause * InprocessingAddClause(absl::Span&lt; const Literal &gt; new_clause)</div><div class="ttdef"><b>Definition:</b> <a href="clause_8cc_source.html#l00416">clause.cc:416</a></div></div>
<div class="ttc" id="vlog__is__on_8h_html_a956152cad330225654d128f35c00efce"><div class="ttname"><a href="vlog__is__on_8h.html#a956152cad330225654d128f35c00efce">VLOG_IS_ON</a></div><div class="ttdeci">#define VLOG_IS_ON(verboselevel)</div><div class="ttdef"><b>Definition:</b> <a href="vlog__is__on_8h_source.html#l00044">vlog_is_on.h:44</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_literal_watchers_html_a56cba28a88a7cffa362a362fdce24dc3"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_literal_watchers.html#a56cba28a88a7cffa362a362fdce24dc3">operations_research::sat::LiteralWatchers::AttachAllClauses</a></div><div class="ttdeci">void AttachAllClauses()</div><div class="ttdef"><b>Definition:</b> <a href="clause_8cc_source.html#l00323">clause.cc:323</a></div></div>
<div class="ttc" id="class_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="classoperations__research_1_1sat_1_1_binary_implication_graph_html_ad2d9e6c6ea7ab13e0d0002a035a6d308"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_binary_implication_graph.html#ad2d9e6c6ea7ab13e0d0002a035a6d308">operations_research::sat::BinaryImplicationGraph::IsRemoved</a></div><div class="ttdeci">bool IsRemoved(Literal l) const</div><div class="ttdef"><b>Definition:</b> <a href="clause_8h_source.html#l00710">clause.h:710</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_literal_watchers_html_a0ddf4dc22639ee58f75985d875d1fd2d"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_literal_watchers.html#a0ddf4dc22639ee58f75985d875d1fd2d">operations_research::sat::LiteralWatchers::InprocessingFixLiteral</a></div><div class="ttdeci">ABSL_MUST_USE_RESULT bool InprocessingFixLiteral(Literal true_literal)</div><div class="ttdef"><b>Definition:</b> <a href="clause_8cc_source.html#l00340">clause.cc:340</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_binary_implication_graph_html_afc581e906dd97aacce13dd14d6a12cf3"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_binary_implication_graph.html#afc581e906dd97aacce13dd14d6a12cf3">operations_research::sat::BinaryImplicationGraph::DirectImplicationsEstimatedSize</a></div><div class="ttdeci">int DirectImplicationsEstimatedSize(Literal literal) const</div><div class="ttdef"><b>Definition:</b> <a href="clause_8h_source.html#l00695">clause.h:695</a></div></div>
<div class="ttc" id="cp__model__solver_8cc_html_ace0951799e72ee99fc07d5e509bc7cbf"><div class="ttname"><a href="cp__model__solver_8cc.html#ace0951799e72ee99fc07d5e509bc7cbf">wall_timer</a></div><div class="ttdeci">WallTimer * wall_timer</div><div class="ttdef"><b>Definition:</b> <a href="cp__model__solver_8cc_source.html#l01950">cp_model_solver.cc:1950</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_blocked_clause_simplifier_html_ad30a040fd97f2cb710bb44c9f048a341"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_blocked_clause_simplifier.html#ad30a040fd97f2cb710bb44c9f048a341">operations_research::sat::BlockedClauseSimplifier::DoOneRound</a></div><div class="ttdeci">void DoOneRound(bool log_info)</div><div class="ttdef"><b>Definition:</b> <a href="sat__inprocessing_8cc_source.html#l00892">sat_inprocessing.cc:892</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_binary_implication_graph_html_a76e3f946eaf9d02fbf3cf8193466e4c7"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_binary_implication_graph.html#a76e3f946eaf9d02fbf3cf8193466e4c7">operations_research::sat::BinaryImplicationGraph::num_redundant_literals</a></div><div class="ttdeci">int64_t num_redundant_literals() const</div><div class="ttdef"><b>Definition:</b> <a href="clause_8h_source.html#l00623">clause.h:623</a></div></div>
<div class="ttc" id="structoperations__research_1_1sat_1_1_sat_presolve_options_html_afac11ce59af8fa30ab784cfa4fb36297"><div class="ttname"><a href="structoperations__research_1_1sat_1_1_sat_presolve_options.html#afac11ce59af8fa30ab784cfa4fb36297">operations_research::sat::SatPresolveOptions::deterministic_time_limit</a></div><div class="ttdeci">double deterministic_time_limit</div><div class="ttdef"><b>Definition:</b> <a href="sat__inprocessing_8h_source.html#l00058">sat_inprocessing.h:58</a></div></div>
<div class="ttc" id="optimization_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#l00085">optimization.cc:85</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_literal_watchers_html_af18b28ba180d18c4e4f524d6fde71f28"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_literal_watchers.html#af18b28ba180d18c4e4f524d6fde71f28">operations_research::sat::LiteralWatchers::literal_size</a></div><div class="ttdeci">int64_t literal_size() const</div><div class="ttdef"><b>Definition:</b> <a href="clause_8h_source.html#l00235">clause.h:235</a></div></div>
<div class="ttc" id="base_2logging_8h_html_ab25e01a2942b821d66371fc68d53f2eb"><div class="ttname"><a href="base_2logging_8h.html#ab25e01a2942b821d66371fc68d53f2eb">CHECK_NE</a></div><div class="ttdeci">#define CHECK_NE(val1, val2)</div><div class="ttdef"><b>Definition:</b> <a href="base_2logging_8h_source.html#l00703">base/logging.h:703</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_literal_watchers_html_ab17b31190c5ab58a1334139848335283"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_literal_watchers.html#ab17b31190c5ab58a1334139848335283">operations_research::sat::LiteralWatchers::InprocessingRewriteClause</a></div><div class="ttdeci">ABSL_MUST_USE_RESULT bool InprocessingRewriteClause(SatClause *clause, absl::Span&lt; const Literal &gt; new_clause)</div><div class="ttdef"><b>Definition:</b> <a href="clause_8cc_source.html#l00368">clause.cc:368</a></div></div>
<div class="ttc" id="log__severity_8h_html_ab4a2cbab234914b320b7fae11b6e8cb9"><div class="ttname"><a href="log__severity_8h.html#ab4a2cbab234914b320b7fae11b6e8cb9">INFO</a></div><div class="ttdeci">const int INFO</div><div class="ttdef"><b>Definition:</b> <a href="log__severity_8h_source.html#l00031">log_severity.h:31</a></div></div>
<div class="ttc" id="constraint__solver_2table_8cc_html_acb18315d548212835cd8ed4287e6c0b6"><div class="ttname"><a href="constraint__solver_2table_8cc.html#acb18315d548212835cd8ed4287e6c0b6">a</a></div><div class="ttdeci">int64_t a</div><div class="ttdef"><b>Definition:</b> <a href="constraint__solver_2table_8cc_source.html#l00046">constraint_solver/table.cc:46</a></div></div>
<div class="ttc" id="classoperations__research_1_1sat_1_1_inprocessing_html_aeb638f5ec6c2dd765d96e06926c4143f"><div class="ttname"><a href="classoperations__research_1_1sat_1_1_inprocessing.html#aeb638f5ec6c2dd765d96e06926c4143f">operations_research::sat::Inprocessing::SubsumeAndStrenghtenRound</a></div><div class="ttdeci">bool SubsumeAndStrenghtenRound(bool log_info)</div><div class="ttdef"><b>Definition:</b> <a href="sat__inprocessing_8cc_source.html#l00362">sat_inprocessing.cc:362</a></div></div>
2021-01-26 11:28:50 +01:00
</div><!-- fragment --></div><!-- contents -->
</div><!-- doc-content -->
2020-09-02 09:42:51 +02:00
<!-- 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__inprocessing_8cc.html">sat_inprocessing.cc</a></li>
<li class="footer">Generated by
<a href="http://www.doxygen.org/index.html">
2022-01-16 18:02:36 +01:00
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.8.15 </li>
2020-09-02 09:42:51 +02:00
</ul>
</div>
</body>
</html>