14 #ifndef OR_TOOLS_SAT_CIRCUIT_H_
15 #define OR_TOOLS_SAT_CIRCUIT_H_
21 #include "absl/container/flat_hash_map.h"
55 const std::vector<int>& heads,
56 const std::vector<Literal>& literals,
Options options,
66 void AddArc(
int tail,
int head, LiteralIndex literal_index);
71 void FillReasonForPath(
int start_node, std::vector<
Literal>* reason) const;
84 std::vector<
Literal> self_arcs_;
85 absl::flat_hash_map<std::pair<
int,
int>,
Literal> graph_;
92 std::vector<Literal> watch_index_to_literal_;
93 std::vector<std::vector<Arc>> watch_index_to_arcs_;
96 int propagation_trail_index_ = 0;
99 std::vector<int> next_;
100 std::vector<int> prev_;
101 std::vector<LiteralIndex> next_literal_;
105 std::vector<int> level_ends_;
106 std::vector<Arc> added_arcs_;
110 int rev_must_be_in_cycle_size_ = 0;
111 std::vector<int> must_be_in_cycle_;
114 std::vector<bool> processed_;
115 std::vector<bool> in_current_path_;
134 const std::vector<int>& distinguished_nodes,
146 void FillFixedPathInReason(
int start,
int end, std::vector<Literal>* reason);
149 const std::vector<std::vector<Literal>> graph_;
150 const int num_nodes_;
151 std::vector<bool> node_is_distinguished_;
155 std::vector<std::pair<int, int>> watch_index_to_arc_;
156 std::vector<std::pair<int, int>> fixed_arcs_;
157 std::vector<int> level_ends_;
160 std::vector<int> next_;
161 std::vector<int> prev_;
162 std::vector<bool> visited_;
167 template <
class IntContainer>
169 const int num_arcs = tails->size();
170 if (num_arcs == 0)
return 0;
174 for (
int arc = 0; arc < num_arcs; ++arc) {
175 nodes.insert((*tails)[arc]);
176 nodes.insert((*heads)[arc]);
181 absl::flat_hash_map<int, int> mapping;
182 for (
const int node : nodes) {
183 mapping[node] = new_index++;
187 for (
int arc = 0; arc < num_arcs; ++arc) {
188 (*tails)[arc] = mapping[(*tails)[arc]];
189 (*heads)[arc] = mapping[(*heads)[arc]];
202 int num_nodes,
const std::vector<int>& tails,
const std::vector<int>& heads,
203 const std::vector<Literal>& literals,
204 bool multiple_subcircuit_through_zero =
false);
208 const std::vector<std::vector<Literal>>& graph);
210 const std::vector<std::vector<Literal>>& graph,
211 const std::vector<int>& distinguished_nodes);
216 #endif // OR_TOOLS_SAT_CIRCUIT_H_