Google OR-Tools v9.14
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
cp_model_symmetries.cc
Go to the documentation of this file.
1// Copyright 2010-2025 Google LLC
2// Licensed under the Apache License, Version 2.0 (the "License");
3// you may not use this file except in compliance with the License.
4// You may obtain a copy of the License at
5//
6// http://www.apache.org/licenses/LICENSE-2.0
7//
8// Unless required by applicable law or agreed to in writing, software
9// distributed under the License is distributed on an "AS IS" BASIS,
10// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11// See the License for the specific language governing permissions and
12// limitations under the License.
13
15
16#include <stddef.h>
17
18#include <algorithm>
19#include <cstdint>
20#include <cstdlib>
21#include <functional>
22#include <limits>
23#include <memory>
24#include <utility>
25#include <vector>
26
27#include "absl/algorithm/container.h"
28#include "absl/container/btree_map.h"
29#include "absl/container/flat_hash_map.h"
30#include "absl/container/flat_hash_set.h"
31#include "absl/log/check.h"
32#include "absl/meta/type_traits.h"
33#include "absl/status/status.h"
34#include "absl/strings/str_cat.h"
35#include "absl/strings/str_join.h"
36#include "absl/types/span.h"
37#include "google/protobuf/message.h"
41#include "ortools/base/hash.h"
43#include "ortools/graph/graph.h"
48#include "ortools/sat/model.h"
55#include "ortools/sat/util.h"
61
62namespace operations_research {
63namespace sat {
64
65namespace {
66struct VectorHash {
67 std::size_t operator()(absl::Span<const int64_t> values) const {
68 size_t hash = 0;
69 for (const int64_t value : values) {
70 hash = util_hash::Hash(value, hash);
71 }
72 return hash;
73 }
74};
75
76struct NodeExprCompare {
77 bool operator()(const LinearExpressionProto& a,
78 const LinearExpressionProto& b) const {
79 if (a.offset() != b.offset()) return a.offset() < b.offset();
80 if (a.vars_size() != b.vars_size()) return a.vars_size() < b.vars_size();
81 for (int i = 0; i < a.vars_size(); ++i) {
82 if (a.vars(i) != b.vars(i)) return a.vars(i) < b.vars(i);
83 if (a.coeffs(i) != b.coeffs(i)) return a.coeffs(i) < b.coeffs(i);
84 }
85 return false;
86 }
87};
88
89// A simple class to generate equivalence class number for
90// GenerateGraphForSymmetryDetection().
91class IdGenerator {
92 public:
93 IdGenerator() = default;
94
95 // If the color was never seen before, then generate a new id, otherwise
96 // return the previously generated id.
97 int GetId(const std::vector<int64_t>& color) {
98 // Do not use try_emplace. It breaks with gcc13 on or-tools.
99 return id_map_.insert({color, id_map_.size()}).first->second;
100 }
101
102 int NextFreeId() const { return id_map_.size(); }
103
104 private:
105 absl::flat_hash_map<std::vector<int64_t>, int, VectorHash> id_map_;
106};
107
108// Appends values in `repeated_field` to `vector`.
109//
110// We use a template as proto int64_t != C++ int64_t in open source.
111template <typename FieldInt64Type>
112void Append(
113 const google::protobuf::RepeatedField<FieldInt64Type>& repeated_field,
114 std::vector<int64_t>* vector) {
115 CHECK(vector != nullptr);
116 for (const FieldInt64Type value : repeated_field) {
117 vector->push_back(value);
118 }
119}
120
121bool IsIntervalFixedSize(const IntervalConstraintProto& interval) {
122 if (!interval.size().vars().empty()) {
123 return false;
124 }
125 if (interval.start().vars().size() != interval.end().vars().size()) {
126 return false;
127 }
128 for (int i = 0; i < interval.start().vars().size(); ++i) {
129 if (interval.start().coeffs(i) != interval.end().coeffs(i)) {
130 return false;
131 }
132 if (interval.start().vars(i) != interval.end().vars(i)) {
133 return false;
134 }
135 }
136 if (interval.end().offset() !=
137 interval.start().offset() + interval.size().offset()) {
138 return false;
139 }
140 return true;
141}
142
143// Returns a graph whose automorphisms can be mapped back to the symmetries of
144// the model described in the given CpModelProto.
145//
146// Any permutation of the graph that respects the initial_equivalence_classes
147// output can be mapped to a symmetry of the given problem simply by taking its
148// restriction on the first num_variables nodes and interpreting its index as a
149// variable index. In a sense, a node with a low enough index #i is in
150// one-to-one correspondence with the variable #i (using the index
151// representation of variables).
152//
153// The format of the initial_equivalence_classes is the same as the one
154// described in GraphSymmetryFinder::FindSymmetries(). The classes must be dense
155// in [0, num_classes) and any symmetry will only map nodes with the same class
156// between each other.
157template <typename Graph>
158std::unique_ptr<Graph> GenerateGraphForSymmetryDetection(
159 const CpModelProto& problem, std::vector<int>* initial_equivalence_classes,
160 SolverLogger* logger) {
161 CHECK(initial_equivalence_classes != nullptr);
162
163 const int num_variables = problem.variables_size();
164 auto graph = std::make_unique<Graph>();
165
166 // Each node will be created with a given color. Two nodes of different color
167 // can never be send one into another by a symmetry. The first element of
168 // the color vector will always be the NodeType.
169 //
170 // TODO(user): Using a full int64_t for storing 3 values is not great. We
171 // can optimize this at the price of a bit more code.
172 enum NodeType {
173 VARIABLE_NODE,
174 VAR_COEFFICIENT_NODE,
175 CONSTRAINT_NODE,
176 VAR_LIN_EXPR_NODE,
177 };
178 IdGenerator color_id_generator;
179 initial_equivalence_classes->clear();
180 auto new_node_from_id = [&initial_equivalence_classes, &graph](int color_id) {
181 // Since we add nodes one by one, initial_equivalence_classes->size() gives
182 // the number of nodes at any point, which we use as the next node index.
183 const int node = initial_equivalence_classes->size();
184 initial_equivalence_classes->push_back(color_id);
185
186 // In some corner cases, we create a node but never uses it. We still
187 // want it to be there.
188 graph->AddNode(node);
189 return node;
190 };
191 auto new_node = [&new_node_from_id,
192 &color_id_generator](const std::vector<int64_t>& color) {
193 return new_node_from_id(color_id_generator.GetId(color));
194 };
195 // For two variables to be in the same equivalence class, they need to have
196 // the same objective coefficient, and the same possible bounds.
197 //
198 // TODO(user): We could ignore the objective coefficients, and just make sure
199 // that when we break symmetry amongst variables, we choose the possibility
200 // with the smallest cost?
201 std::vector<int64_t> objective_by_var(num_variables, 0);
202 for (int i = 0; i < problem.objective().vars_size(); ++i) {
203 const int ref = problem.objective().vars(i);
204 const int var = PositiveRef(ref);
205 const int64_t coeff = problem.objective().coeffs(i);
206 objective_by_var[var] = RefIsPositive(ref) ? coeff : -coeff;
207 }
208
209 // Create one node for each variable. Note that the code rely on the fact that
210 // the index of a VARIABLE_NODE type is the same as the variable index.
211 std::vector<int64_t> tmp_color;
212 for (int v = 0; v < num_variables; ++v) {
213 tmp_color = {VARIABLE_NODE, objective_by_var[v]};
214 Append(problem.variables(v).domain(), &tmp_color);
215 CHECK_EQ(v, new_node(tmp_color));
216 }
217
218 const int color_id_for_coeff_one =
219 color_id_generator.GetId({VAR_COEFFICIENT_NODE, 1});
220 const int color_id_for_coeff_minus_one =
221 color_id_generator.GetId({VAR_COEFFICIENT_NODE, -1});
222
223 // We will lazily create "coefficient nodes" that correspond to a variable
224 // with a given coefficient.
225 absl::flat_hash_map<std::pair<int64_t, int64_t>, int> coefficient_nodes;
226 auto get_coefficient_node =
227 [&new_node_from_id, &graph, &coefficient_nodes, &color_id_generator,
228 &tmp_color, color_id_for_coeff_minus_one](int var, int64_t coeff) {
229 const int var_node = var;
230 DCHECK(RefIsPositive(var));
231
232 // For a coefficient of one, which are the most common, we can optimize
233 // the size of the graph by omitting the coefficient node altogether and
234 // using directly the var_node in this case.
235 if (coeff == 1) return var_node;
236
237 const auto insert =
238 coefficient_nodes.insert({std::make_pair(var, coeff), 0});
239 if (!insert.second) return insert.first->second;
240
241 int color_id;
242 // Because -1 is really common (also used for negated literal), we have
243 // a fast path for it.
244 if (coeff == -1) {
245 color_id = color_id_for_coeff_minus_one;
246 } else {
247 tmp_color = {VAR_COEFFICIENT_NODE, coeff};
248 color_id = color_id_generator.GetId(tmp_color);
249 }
250 const int secondary_node = new_node_from_id(color_id);
251 graph->AddArc(var_node, secondary_node);
252 insert.first->second = secondary_node;
253 return secondary_node;
254 };
255
256 // For a literal we use the same as a coefficient 1 or -1. We can do that
257 // because literal and (var, coefficient) never appear together in the same
258 // constraint.
259 auto get_literal_node = [&get_coefficient_node](int ref) {
260 return get_coefficient_node(PositiveRef(ref), RefIsPositive(ref) ? 1 : -1);
261 };
262
263 // Because the implications can be numerous, we encode them without
264 // constraints node by using an arc from the lhs to the rhs. Note that we also
265 // always add the other direction. We use a set to remove duplicates both for
266 // efficiency and to not artificially break symmetries by using multi-arcs.
267 //
268 // Tricky: We cannot use the base variable node here to avoid situation like
269 // both a variable a and b having the same children (not(a), not(b)) in the
270 // graph. Because if that happen, we can permute a and b without permuting
271 // their associated not(a) and not(b) node! To be sure this cannot happen, a
272 // variable node can not have as children a VAR_COEFFICIENT_NODE from another
273 // node. This makes sure that any permutation that touch a variable, must
274 // permute its coefficient nodes accordingly.
275 absl::flat_hash_set<std::pair<int, int>> implications;
276 auto get_implication_node = [&new_node_from_id, &graph, &coefficient_nodes,
277 color_id_for_coeff_one,
278 color_id_for_coeff_minus_one](int ref) {
279 const int var = PositiveRef(ref);
280 const int64_t coeff = RefIsPositive(ref) ? 1 : -1;
281 const auto insert =
282 coefficient_nodes.insert({std::make_pair(var, coeff), 0});
283 if (!insert.second) return insert.first->second;
284 const int secondary_node = new_node_from_id(
285 coeff == 1 ? color_id_for_coeff_one : color_id_for_coeff_minus_one);
286 graph->AddArc(var, secondary_node);
287 insert.first->second = secondary_node;
288 return secondary_node;
289 };
290 auto add_implication = [&get_implication_node, &graph, &implications](
291 int ref_a, int ref_b) {
292 const auto insert = implications.insert({ref_a, ref_b});
293 if (!insert.second) return;
294 graph->AddArc(get_implication_node(ref_a), get_implication_node(ref_b));
295
296 // Always add the other side.
297 implications.insert({NegatedRef(ref_b), NegatedRef(ref_a)});
298 graph->AddArc(get_implication_node(NegatedRef(ref_b)),
299 get_implication_node(NegatedRef(ref_a)));
300 };
301
302 auto make_linear_expr_node = [&new_node, &graph, &get_coefficient_node](
303 const LinearExpressionProto& expr,
304 const std::vector<int64_t>& color) {
305 std::vector<int64_t> local_color = color;
306 local_color.push_back(expr.offset());
307 const int local_node = new_node(local_color);
308
309 for (int i = 0; i < expr.vars().size(); ++i) {
310 const int ref = expr.vars(i);
311 const int var_node = PositiveRef(ref);
312 const int64_t coeff =
313 RefIsPositive(ref) ? expr.coeffs(i) : -expr.coeffs(i);
314 graph->AddArc(get_coefficient_node(var_node, coeff), local_node);
315 }
316 return local_node;
317 };
318
319 absl::btree_map<LinearExpressionProto, int, NodeExprCompare> expr_nodes;
320 auto shared_linear_expr_node =
321 [&make_linear_expr_node, &expr_nodes](const LinearExpressionProto& expr) {
322 const auto [it, inserted] = expr_nodes.insert({expr, 0});
323 if (inserted) {
324 const std::vector<int64_t> local_color = {VAR_LIN_EXPR_NODE,
325 expr.offset()};
326 it->second = make_linear_expr_node(expr, local_color);
327 }
328 return it->second;
329 };
330
331 // We need to keep track of this for scheduling constraints.
332 absl::flat_hash_map<int, int> interval_constraint_index_to_node;
333
334 // Add constraints to the graph.
335 for (int constraint_index = 0; constraint_index < problem.constraints_size();
336 ++constraint_index) {
337 const ConstraintProto& constraint = problem.constraints(constraint_index);
338 const int constraint_node = initial_equivalence_classes->size();
339 std::vector<int64_t> color = {CONSTRAINT_NODE,
340 constraint.constraint_case()};
341
342 switch (constraint.constraint_case()) {
344 // TODO(user): We continue for the corner case of a constraint not set
345 // with enforcement literal. We should probably clear this constraint
346 // before reaching here.
347 continue;
349 // TODO(user): We can use the same trick as for the implications to
350 // encode relations of the form coeff * var_a <= coeff * var_b without
351 // creating a constraint node by directly adding an arc between the two
352 // var coefficient nodes.
353 Append(constraint.linear().domain(), &color);
354 CHECK_EQ(constraint_node, new_node(color));
355 for (int i = 0; i < constraint.linear().vars_size(); ++i) {
356 const int ref = constraint.linear().vars(i);
357 const int variable_node = PositiveRef(ref);
358 const int64_t coeff = RefIsPositive(ref)
359 ? constraint.linear().coeffs(i)
360 : -constraint.linear().coeffs(i);
361 graph->AddArc(get_coefficient_node(variable_node, coeff),
362 constraint_node);
363 }
364 break;
365 }
367 CHECK_EQ(constraint_node, new_node(color));
368 for (const LinearExpressionProto& expr :
369 constraint.all_diff().exprs()) {
370 graph->AddArc(shared_linear_expr_node(expr), constraint_node);
371 }
372 break;
373 }
375 CHECK_EQ(constraint_node, new_node(color));
376 for (const int ref : constraint.bool_or().literals()) {
377 graph->AddArc(get_literal_node(ref), constraint_node);
378 }
379 break;
380 }
382 if (constraint.at_most_one().literals().size() == 2) {
383 // Treat it as an implication to avoid creating a node.
384 add_implication(constraint.at_most_one().literals(0),
385 NegatedRef(constraint.at_most_one().literals(1)));
386 break;
387 }
388
389 CHECK_EQ(constraint_node, new_node(color));
390 for (const int ref : constraint.at_most_one().literals()) {
391 graph->AddArc(get_literal_node(ref), constraint_node);
392 }
393 break;
394 }
396 CHECK_EQ(constraint_node, new_node(color));
397 for (const int ref : constraint.exactly_one().literals()) {
398 graph->AddArc(get_literal_node(ref), constraint_node);
399 }
400 break;
401 }
403 CHECK_EQ(constraint_node, new_node(color));
404 for (const int ref : constraint.bool_xor().literals()) {
405 graph->AddArc(get_literal_node(ref), constraint_node);
406 }
407 break;
408 }
410 if (constraint.enforcement_literal_size() > 1) {
411 CHECK_EQ(constraint_node, new_node(color));
412 for (const int ref : constraint.bool_and().literals()) {
413 graph->AddArc(get_literal_node(ref), constraint_node);
414 }
415 break;
416 }
417
418 CHECK_EQ(constraint.enforcement_literal_size(), 1);
419 const int ref_a = constraint.enforcement_literal(0);
420 for (const int ref_b : constraint.bool_and().literals()) {
421 add_implication(ref_a, ref_b);
422 }
423 break;
424 }
426 const LinearExpressionProto& target_expr =
427 constraint.lin_max().target();
428
429 const int target_node = make_linear_expr_node(target_expr, color);
430
431 for (int i = 0; i < constraint.lin_max().exprs_size(); ++i) {
432 const LinearExpressionProto& expr = constraint.lin_max().exprs(i);
433 graph->AddArc(shared_linear_expr_node(expr), target_node);
434 }
435
436 break;
437 }
439 static constexpr int kFixedIntervalColor = 0;
440 static constexpr int kNonFixedIntervalColor = 1;
441 if (IsIntervalFixedSize(constraint.interval())) {
442 std::vector<int64_t> local_color = color;
443 local_color.push_back(kFixedIntervalColor);
444 local_color.push_back(constraint.interval().size().offset());
445 const int full_node =
446 make_linear_expr_node(constraint.interval().start(), local_color);
447 CHECK_EQ(full_node, constraint_node);
448 } else {
449 // We create 3 constraint nodes (for start, size and end) including
450 // the offset. We connect these to their terms like for a linear
451 // constraint.
452 std::vector<int64_t> local_color = color;
453 local_color.push_back(kNonFixedIntervalColor);
454
455 local_color.push_back(0);
456 const int start_node =
457 make_linear_expr_node(constraint.interval().start(), local_color);
458 local_color.pop_back();
459 CHECK_EQ(start_node, constraint_node);
460
461 // We can use a shared node for one of the three. Let's use the size
462 // since it has the most chance of being reused.
463 const int size_node =
464 shared_linear_expr_node(constraint.interval().size());
465
466 local_color.push_back(1);
467 const int end_node =
468 make_linear_expr_node(constraint.interval().end(), local_color);
469 local_color.pop_back();
470
471 // Make sure that if one node is mapped to another one, its other two
472 // components are the same.
473 graph->AddArc(start_node, end_node);
474 graph->AddArc(end_node, size_node);
475 }
476 interval_constraint_index_to_node[constraint_index] = constraint_node;
477 break;
478 }
480 // Note(user): This require that intervals appear before they are used.
481 // We currently enforce this at validation, otherwise we need two passes
482 // here and in a bunch of other places.
483 CHECK_EQ(constraint_node, new_node(color));
484 for (const int interval : constraint.no_overlap().intervals()) {
485 graph->AddArc(interval_constraint_index_to_node.at(interval),
486 constraint_node);
487 }
488 break;
489 }
491 // Note(user): This require that intervals appear before they are used.
492 // We currently enforce this at validation, otherwise we need two passes
493 // here and in a bunch of other places.
494 CHECK_EQ(constraint_node, new_node(color));
495 std::vector<int64_t> local_color = color;
496 local_color.push_back(0);
497 const int size = constraint.no_overlap_2d().x_intervals().size();
498 const int node_x = new_node(local_color);
499 const int node_y = new_node(local_color);
500 local_color.pop_back();
501 graph->AddArc(constraint_node, node_x);
502 graph->AddArc(constraint_node, node_y);
503 local_color.push_back(1);
504 for (int i = 0; i < size; ++i) {
505 const int box_node = new_node(local_color);
506 graph->AddArc(box_node, constraint_node);
507 const int x = constraint.no_overlap_2d().x_intervals(i);
508 const int y = constraint.no_overlap_2d().y_intervals(i);
509 graph->AddArc(interval_constraint_index_to_node.at(x), node_x);
510 graph->AddArc(interval_constraint_index_to_node.at(x), box_node);
511 graph->AddArc(interval_constraint_index_to_node.at(y), node_y);
512 graph->AddArc(interval_constraint_index_to_node.at(y), box_node);
513 }
514 break;
515 }
517 // Note(user): This require that intervals appear before they are used.
518 // We currently enforce this at validation, otherwise we need two passes
519 // here and in a bunch of other places.
520 const CumulativeConstraintProto& ct = constraint.cumulative();
521 std::vector<int64_t> capacity_color = color;
522 capacity_color.push_back(0);
523 CHECK_EQ(constraint_node, new_node(capacity_color));
524 graph->AddArc(constraint_node,
525 make_linear_expr_node(ct.capacity(), capacity_color));
526
527 std::vector<int64_t> task_color = color;
528 task_color.push_back(1);
529 for (int i = 0; i < ct.intervals().size(); ++i) {
530 const int task_node =
531 make_linear_expr_node(ct.demands(i), task_color);
532 graph->AddArc(task_node, constraint_node);
533 graph->AddArc(task_node,
534 interval_constraint_index_to_node.at(ct.intervals(i)));
535 }
536 break;
537 }
539 // Note that this implementation will generate the same graph for a
540 // circuit constraint with two disconnected components and two circuit
541 // constraints with one component each.
542 const int num_arcs = constraint.circuit().literals().size();
543 absl::flat_hash_map<int, int> circuit_node_to_symmetry_node;
544 std::vector<int64_t> arc_color = color;
545 arc_color.push_back(1);
546 for (int i = 0; i < num_arcs; ++i) {
547 const int literal = constraint.circuit().literals(i);
548 const int tail = constraint.circuit().tails(i);
549 const int head = constraint.circuit().heads(i);
550 const int arc_node = new_node(arc_color);
551 if (!circuit_node_to_symmetry_node.contains(head)) {
552 circuit_node_to_symmetry_node[head] = new_node(color);
553 }
554 const int head_node = circuit_node_to_symmetry_node[head];
555 if (!circuit_node_to_symmetry_node.contains(tail)) {
556 circuit_node_to_symmetry_node[tail] = new_node(color);
557 }
558 const int tail_node = circuit_node_to_symmetry_node[tail];
559 // To make the graph directed, we add two arcs on the head but not on
560 // the tail.
561 graph->AddArc(tail_node, arc_node);
562 graph->AddArc(arc_node, get_literal_node(literal));
563 graph->AddArc(arc_node, head_node);
564 }
565 break;
566 }
567 default: {
568 // If the model contains any non-supported constraints, return an empty
569 // graph.
570 //
571 // TODO(user): support other types of constraints. Or at least, we
572 // could associate to them an unique node so that their variables can
573 // appear in no symmetry.
574 VLOG(1) << "Unsupported constraint type "
575 << ConstraintCaseName(constraint.constraint_case());
576 return nullptr;
577 }
578 }
579
580 // For enforcement, we use a similar trick than for the implications.
581 // Because all our constraint arcs are in the direction var_node to
582 // constraint_node, we just use the reverse direction for the enforcement
583 // part. This way we can reuse the same get_literal_node() function.
584 if (constraint.constraint_case() != ConstraintProto::kBoolAnd ||
585 constraint.enforcement_literal().size() > 1) {
586 for (const int ref : constraint.enforcement_literal()) {
587 graph->AddArc(constraint_node, get_literal_node(ref));
588 }
589 }
590 }
591
592 graph->Build();
593 DCHECK_EQ(graph->num_nodes(), initial_equivalence_classes->size());
594
595 // TODO(user): The symmetry code does not officially support multi-arcs. And
596 // we shouldn't have any as long as there is no duplicates variable in our
597 // constraints (but of course, we can't always guarantee that). That said,
598 // because the symmetry code really only look at the degree, it works as long
599 // as the maximum degree is bounded by num_nodes.
600 const int num_nodes = graph->num_nodes();
601 std::vector<int> in_degree(num_nodes, 0);
602 std::vector<int> out_degree(num_nodes, 0);
603 for (int i = 0; i < num_nodes; ++i) {
604 out_degree[i] = graph->OutDegree(i);
605 for (const int head : (*graph)[i]) {
606 in_degree[head]++;
607 }
608 }
609 for (int i = 0; i < num_nodes; ++i) {
610 if (in_degree[i] >= num_nodes || out_degree[i] >= num_nodes) {
611 SOLVER_LOG(logger, "[Symmetry] Too many multi-arcs in symmetry code.");
612 return nullptr;
613 }
614 }
615
616 // Because this code is running during presolve, a lot a variable might have
617 // no edges. We do not want to detect symmetries between these.
618 //
619 // Note that this code forces us to "densify" the ids afterwards because the
620 // symmetry detection code relies on that.
621 //
622 // TODO(user): It will probably be more efficient to not even create these
623 // nodes, but we will need a mapping to know the variable <-> node index.
624 int next_id = color_id_generator.NextFreeId();
625 for (int i = 0; i < num_variables; ++i) {
626 if ((*graph)[i].empty()) {
627 (*initial_equivalence_classes)[i] = next_id++;
628 }
629 }
630
631 // Densify ids.
632 int id = 0;
633 std::vector<int> mapping(next_id, -1);
634 for (int& ref : *initial_equivalence_classes) {
635 if (mapping[ref] == -1) {
636 ref = mapping[ref] = id++;
637 } else {
638 ref = mapping[ref];
639 }
640 }
641
642 return graph;
643}
644} // namespace
645
647 const SatParameters& params, const CpModelProto& problem,
648 std::vector<std::unique_ptr<SparsePermutation>>* generators,
649 SolverLogger* logger, TimeLimit* solver_time_limit) {
650 CHECK(generators != nullptr);
651 generators->clear();
652
653 if (params.symmetry_level() < 3 && problem.variables().size() > 1e6 &&
654 problem.constraints().size() > 1e6) {
655 SOLVER_LOG(logger,
656 "[Symmetry] Problem too large. Skipping. You can use "
657 "symmetry_level:3 or more to force it.");
658 return;
659 }
660
662
663 std::vector<int> equivalence_classes;
664 std::unique_ptr<Graph> graph(GenerateGraphForSymmetryDetection<Graph>(
665 problem, &equivalence_classes, logger));
666 if (graph == nullptr) return;
667
668 SOLVER_LOG(logger, "[Symmetry] Graph for symmetry has ",
669 FormatCounter(graph->num_nodes()), " nodes and ",
670 FormatCounter(graph->num_arcs()), " arcs.");
671 if (graph->num_nodes() == 0) return;
672
673 if (params.symmetry_level() < 3 && graph->num_nodes() > 1e6 &&
674 graph->num_arcs() > 1e6) {
675 SOLVER_LOG(logger,
676 "[Symmetry] Graph too large. Skipping. You can use "
677 "symmetry_level:3 or more to force it.");
678 return;
679 }
680
681 std::unique_ptr<TimeLimit> time_limit = TimeLimit::FromDeterministicTime(
683 time_limit->MergeWithGlobalTimeLimit(solver_time_limit);
684 GraphSymmetryFinder symmetry_finder(*graph, /*is_undirected=*/false);
685 std::vector<int> factorized_automorphism_group_size;
686 const absl::Status status = symmetry_finder.FindSymmetries(
687 &equivalence_classes, generators, &factorized_automorphism_group_size,
688 time_limit.get());
689
690 // TODO(user): Change the API to not return an error when the time limit is
691 // reached.
692 if (!status.ok()) {
693 SOLVER_LOG(logger,
694 "[Symmetry] GraphSymmetryFinder error: ", status.message());
695 }
696
697 // Remove from the permutations the part not concerning the variables.
698 // Note that some permutations may become empty, which means that we had
699 // duplicate constraints.
700 double average_support_size = 0.0;
701 int num_generators = 0;
702 int num_duplicate_constraints = 0;
703 for (int i = 0; i < generators->size(); ++i) {
704 SparsePermutation* permutation = (*generators)[i].get();
705 std::vector<int> to_delete;
706 for (int j = 0; j < permutation->NumCycles(); ++j) {
707 // Because variable nodes are in a separate equivalence class than any
708 // other node, a cycle can either contain only variable nodes or none, so
709 // we just need to check one element of the cycle.
710 if (*(permutation->Cycle(j).begin()) >= problem.variables_size()) {
711 to_delete.push_back(j);
712 if (DEBUG_MODE) {
713 // Verify that the cycle's entire support does not touch any variable.
714 for (const int node : permutation->Cycle(j)) {
715 DCHECK_GE(node, problem.variables_size());
716 }
717 }
718 }
719 }
720
721 permutation->RemoveCycles(to_delete);
722 if (!permutation->Support().empty()) {
723 average_support_size += permutation->Support().size();
724 swap((*generators)[num_generators], (*generators)[i]);
725 ++num_generators;
726 } else {
727 ++num_duplicate_constraints;
728 }
729 }
730 generators->resize(num_generators);
731 SOLVER_LOG(logger, "[Symmetry] Symmetry computation done. time: ",
732 time_limit->GetElapsedTime(),
733 " dtime: ", time_limit->GetElapsedDeterministicTime());
734 if (num_generators > 0) {
735 average_support_size /= num_generators;
736 SOLVER_LOG(logger, "[Symmetry] #generators: ", num_generators,
737 ", average support size: ", average_support_size);
738 if (num_duplicate_constraints > 0) {
739 SOLVER_LOG(logger, "[Symmetry] The model contains ",
740 num_duplicate_constraints, " duplicate constraints !");
741 }
742 }
743}
744
745namespace {
746
747void LogOrbitInformation(absl::Span<const int> var_to_orbit_index,
748 SolverLogger* logger) {
749 if (logger == nullptr || !logger->LoggingIsEnabled()) return;
750
751 int num_touched_vars = 0;
752 std::vector<int> orbit_sizes;
753 for (int var = 0; var < var_to_orbit_index.size(); ++var) {
754 const int rep = var_to_orbit_index[var];
755 if (rep == -1) continue;
756 if (rep >= orbit_sizes.size()) orbit_sizes.resize(rep + 1, 0);
757 ++num_touched_vars;
758 orbit_sizes[rep]++;
759 }
760 std::sort(orbit_sizes.begin(), orbit_sizes.end(), std::greater<int>());
761 const int num_orbits = orbit_sizes.size();
762 if (num_orbits > 10) orbit_sizes.resize(10);
763 SOLVER_LOG(logger, "[Symmetry] ", num_orbits, " orbits on ", num_touched_vars,
764 " variables with sizes: ", absl::StrJoin(orbit_sizes, ","),
765 (num_orbits > orbit_sizes.size() ? ",..." : ""));
766}
767
768} // namespace
769
771 CpModelProto* proto, SolverLogger* logger,
773 SymmetryProto* symmetry = proto->mutable_symmetry();
774 symmetry->Clear();
775
776 std::vector<std::unique_ptr<SparsePermutation>> generators;
777 FindCpModelSymmetries(params, *proto, &generators, logger, time_limit);
778 if (generators.empty()) {
779 proto->clear_symmetry();
780 return;
781 }
782
783 // Log orbit information.
784 //
785 // TODO(user): It might be nice to just add this to the proto rather than
786 // re-reading the generators and recomputing this in a few places.
787 const int num_vars = proto->variables().size();
788 const std::vector<int> orbits = GetOrbits(num_vars, generators);
789 LogOrbitInformation(orbits, logger);
790
791 for (const std::unique_ptr<SparsePermutation>& perm : generators) {
792 SparsePermutationProto* perm_proto = symmetry->add_permutations();
793 const int num_cycle = perm->NumCycles();
794 for (int i = 0; i < num_cycle; ++i) {
795 const int old_size = perm_proto->support().size();
796 for (const int var : perm->Cycle(i)) {
797 perm_proto->add_support(var);
798 }
799 perm_proto->add_cycle_sizes(perm_proto->support().size() - old_size);
800 }
801 }
802
803 std::vector<std::vector<int>> orbitope = BasicOrbitopeExtraction(generators);
804 if (orbitope.empty()) return;
805 SOLVER_LOG(logger, "[Symmetry] Found orbitope of size ", orbitope.size(),
806 " x ", orbitope[0].size());
807 DenseMatrixProto* matrix = symmetry->add_orbitopes();
808 matrix->set_num_rows(orbitope.size());
809 matrix->set_num_cols(orbitope[0].size());
810 for (const std::vector<int>& row : orbitope) {
811 for (const int entry : row) {
812 matrix->add_entries(entry);
813 }
814 }
815}
816
817namespace {
818
819// Given one Boolean orbit under symmetry, if there is a Boolean at one in this
820// orbit, then we can always move it to a fixed position (i.e. the given
821// variable var). Moreover, any variable implied to zero in this orbit by var
822// being at one can be fixed to zero. This is because, after symmetry breaking,
823// either var is one, or all the orbit is zero. We also add implications to
824// enforce this fact, but this is not done in this function.
825//
826// TODO(user): If an exactly one / at least one is included in the orbit, then
827// we can set a given variable to one directly. We can also detect this by
828// trying to propagate the orbit to all false.
829//
830// TODO(user): The same reasonning can be done if fixing the variable to
831// zero leads to many propagations at one. For general variables, we might be
832// able to do something too.
833void OrbitAndPropagation(absl::Span<const int> orbits, int var,
834 std::vector<int>* can_be_fixed_to_false,
835 PresolveContext* context) {
836 // Note that if a variable is fixed in the orbit, then everything should be
837 // fixed.
838 if (context->IsFixed(var)) return;
839 if (!context->CanBeUsedAsLiteral(var)) return;
840
841 // Lets fix var to true and see what is propagated.
842 //
843 // TODO(user): Ideally we should have a propagator ready for this. Right now
844 // we load the full model if we detected symmetries. We should really combine
845 // this with probing even though this is "breaking" the symmetry so it cannot
846 // be applied as generally as probing.
847 //
848 // TODO(user): Note that probing can also benefit from symmetry, since in
849 // each orbit, only one variable needs to be probed, and any conclusion can
850 // be duplicated to all the variables from an orbit! It is also why we just
851 // need to propagate one variable here.
852 Model model;
853 if (!LoadModelForProbing(context, &model)) return;
854
855 auto* sat_solver = model.GetOrCreate<SatSolver>();
856 auto* mapping = model.GetOrCreate<CpModelMapping>();
857 const Literal to_propagate = mapping->Literal(var);
858
859 const VariablesAssignment& assignment = sat_solver->Assignment();
860 if (assignment.LiteralIsAssigned(to_propagate)) return;
861 sat_solver->EnqueueDecisionAndBackjumpOnConflict(to_propagate);
862 if (sat_solver->CurrentDecisionLevel() != 1) return;
863
864 // We can fix to false any variable that is in the orbit and set to false!
865 can_be_fixed_to_false->clear();
866 int orbit_size = 0;
867 const int orbit_index = orbits[var];
868 const int num_variables = orbits.size();
869 for (int var = 0; var < num_variables; ++var) {
870 if (orbits[var] != orbit_index) continue;
871 ++orbit_size;
872
873 // By symmetry since same orbit.
874 DCHECK(!context->IsFixed(var));
875 DCHECK(context->CanBeUsedAsLiteral(var));
876
877 if (assignment.LiteralIsFalse(mapping->Literal(var))) {
878 can_be_fixed_to_false->push_back(var);
879 }
880 }
881 if (!can_be_fixed_to_false->empty()) {
882 SOLVER_LOG(context->logger(),
883 "[Symmetry] Num fixable by binary propagation in orbit: ",
884 can_be_fixed_to_false->size(), " / ", orbit_size);
885 }
886}
887
888std::vector<int64_t> BuildInequalityCoeffsForOrbitope(
889 absl::Span<const int64_t> maximum_values, int64_t max_linear_size,
890 bool* is_approximated) {
891 std::vector<int64_t> out(maximum_values.size());
892 int64_t range_product = 1;
893 uint64_t greatest_coeff = 0;
894 for (int i = 0; i < maximum_values.size(); ++i) {
895 out[i] = range_product;
896 greatest_coeff =
897 std::max(greatest_coeff, static_cast<uint64_t>(maximum_values[i]));
898 range_product = CapProd(range_product, 1 + maximum_values[i]);
899 }
900
901 if (range_product <= max_linear_size) {
902 // The product of all ranges fit in a int64_t. This is good news, that
903 // means we can interpret each row of the matrix as an integer in a
904 // mixed-radix representation and impose row[i] <= row[i+1].
905 *is_approximated = false;
906 return out;
907 }
908 *is_approximated = true;
909
910 const auto compute_approximate_coeffs =
911 [max_linear_size, maximum_values](double scaling_factor,
912 std::vector<int64_t>* coeffs) -> bool {
913 int64_t max_size = 0;
914 double cumulative_product_double = 1.0;
915 for (int i = 0; i < maximum_values.size(); ++i) {
916 const int64_t max = maximum_values[i];
917 const int64_t coeff = static_cast<int64_t>(cumulative_product_double);
918 (*coeffs)[i] = coeff;
919 cumulative_product_double *= scaling_factor * max + 1;
920 max_size = CapAdd(max_size, CapProd(max, coeff));
921 if (max_size > max_linear_size) return false;
922 }
923 return true;
924 };
925
926 const double scaling = BinarySearch<double>(
927 0.0, 1.0, [&compute_approximate_coeffs, &out](double scaling_factor) {
928 return compute_approximate_coeffs(scaling_factor, &out);
929 });
930 CHECK(compute_approximate_coeffs(scaling, &out));
931 return out;
932}
933
934} // namespace
935
937 const SatParameters& params = context->params();
938 const CpModelProto& proto = *context->working_model;
939
940 // We need to make sure the proto is up to date before computing symmetries!
941 if (context->working_model->has_objective()) {
942 context->WriteObjectiveToProto();
943 }
945
946 // Tricky: the equivalence relation are not part of the proto.
947 // We thus add them temporarily to compute the symmetry.
948 int64_t num_added = 0;
949 const int initial_ct_index = proto.constraints().size();
950 const int num_vars = proto.variables_size();
951 for (int var = 0; var < num_vars; ++var) {
952 if (context->IsFixed(var)) continue;
953 if (context->VariableWasRemoved(var)) continue;
954 if (context->VariableIsNotUsedAnymore(var)) continue;
955
956 const AffineRelation::Relation r = context->GetAffineRelation(var);
957 if (r.representative == var) continue;
958
959 ++num_added;
961 auto* arg = ct->mutable_linear();
962 arg->add_vars(var);
963 arg->add_coeffs(1);
964 arg->add_vars(r.representative);
965 arg->add_coeffs(-r.coeff);
966 arg->add_domain(r.offset);
967 arg->add_domain(r.offset);
968 }
969
970 std::vector<std::unique_ptr<SparsePermutation>> generators;
971 FindCpModelSymmetries(params, proto, &generators, context->logger(),
972 context->time_limit());
973
974 // Remove temporary affine relation.
975 context->working_model->mutable_constraints()->DeleteSubrange(
976 initial_ct_index, num_added);
977
978 if (generators.empty()) return true;
979
980 // Collect the at most ones.
981 //
982 // Note(user): This relies on the fact that the pointers remain stable when
983 // we adds new constraints. It should be the case, but it is a bit unsafe.
984 // On the other hand it is annoying to deal with both cases below.
985 std::vector<const google::protobuf::RepeatedField<int32_t>*> at_most_ones;
986 for (int i = 0; i < proto.constraints_size(); ++i) {
988 at_most_ones.push_back(&proto.constraints(i).at_most_one().literals());
989 }
990 if (proto.constraints(i).constraint_case() ==
992 at_most_ones.push_back(&proto.constraints(i).exactly_one().literals());
993 }
994 }
995
996 // We have a few heuristics. The first only look at the global orbits under
997 // the symmetry group and try to infer Boolean variable fixing via symmetry
998 // breaking. Note that nothing is fixed yet, we will decide later if we fix
999 // these Booleans or not.
1000 int distinguished_var = -1;
1001 std::vector<int> can_be_fixed_to_false;
1002
1003 // Get the global orbits and their size.
1004 const std::vector<int> orbits = GetOrbits(num_vars, generators);
1005 std::vector<int> orbit_sizes;
1006 int max_orbit_size = 0;
1007 int sum_of_orbit_sizes = 0;
1008 for (int var = 0; var < num_vars; ++var) {
1009 const int rep = orbits[var];
1010 if (rep == -1) continue;
1011 if (rep >= orbit_sizes.size()) orbit_sizes.resize(rep + 1, 0);
1012 ++sum_of_orbit_sizes;
1013 orbit_sizes[rep]++;
1014 if (orbit_sizes[rep] > max_orbit_size) {
1015 distinguished_var = var;
1016 max_orbit_size = orbit_sizes[rep];
1017 }
1018 }
1019
1020 // Log orbit info.
1021 LogOrbitInformation(orbits, context->logger());
1022
1023 // First heuristic based on propagation, see the function comment.
1024 if (max_orbit_size > 2) {
1025 OrbitAndPropagation(orbits, distinguished_var, &can_be_fixed_to_false,
1026 context);
1027 }
1028 const int first_heuristic_size = can_be_fixed_to_false.size();
1029
1030 // If an at most one intersect with one or more orbit, in each intersection,
1031 // we can fix all but one variable to zero. For now we only test positive
1032 // literal, and maximize the number of fixing.
1033 //
1034 // TODO(user): Doing that is not always good, on cod105.mps, fixing variables
1035 // instead of letting the inner solver handle Boolean symmetries make the
1036 // problem unsolvable instead of easily solved. This is probably because this
1037 // fixing do not exploit the full structure of these symmetries. Note
1038 // however that the fixing via propagation above close cod105 even more
1039 // efficiently.
1040 std::vector<int> var_can_be_true_per_orbit(num_vars, -1);
1041 {
1042 std::vector<int> tmp_to_clear;
1043 std::vector<int> tmp_sizes(num_vars, 0);
1044 for (const google::protobuf::RepeatedField<int32_t>* literals :
1045 at_most_ones) {
1046 tmp_to_clear.clear();
1047
1048 // Compute how many variables we can fix with this at most one.
1049 int num_fixable = 0;
1050 for (const int literal : *literals) {
1051 if (!RefIsPositive(literal)) continue;
1052 if (context->IsFixed(literal)) continue;
1053
1054 const int var = PositiveRef(literal);
1055 const int rep = orbits[var];
1056 if (rep == -1) continue;
1057
1058 // We count all but the first one in each orbit.
1059 if (tmp_sizes[rep] == 0) tmp_to_clear.push_back(rep);
1060 if (tmp_sizes[rep] > 0) ++num_fixable;
1061 tmp_sizes[rep]++;
1062 }
1063
1064 // Redo a pass to copy the intersection.
1065 if (num_fixable > can_be_fixed_to_false.size()) {
1066 distinguished_var = -1;
1067 can_be_fixed_to_false.clear();
1068 for (const int literal : *literals) {
1069 if (!RefIsPositive(literal)) continue;
1070 if (context->IsFixed(literal)) continue;
1071
1072 const int var = PositiveRef(literal);
1073 const int rep = orbits[var];
1074 if (rep == -1) continue;
1075 if (distinguished_var == -1 ||
1076 orbit_sizes[rep] > orbit_sizes[orbits[distinguished_var]]) {
1077 distinguished_var = var;
1078 }
1079
1080 // We push all but the first one in each orbit.
1081 if (tmp_sizes[rep] == 0) {
1082 can_be_fixed_to_false.push_back(var);
1083 } else {
1084 var_can_be_true_per_orbit[rep] = var;
1085 }
1086 tmp_sizes[rep] = 0;
1087 }
1088 } else {
1089 // Sparse clean up.
1090 for (const int rep : tmp_to_clear) tmp_sizes[rep] = 0;
1091 }
1092 }
1093
1094 if (can_be_fixed_to_false.size() > first_heuristic_size) {
1095 SOLVER_LOG(
1096 context->logger(),
1097 "[Symmetry] Num fixable by intersecting at_most_one with orbits: ",
1098 can_be_fixed_to_false.size(), " largest_orbit: ", max_orbit_size);
1099 }
1100 }
1101
1102 // Orbitope approach.
1103 //
1104 // This is basically the same as the generic approach, but because of the
1105 // extra structure, computing the orbit of any stabilizer subgroup is easy.
1106 // We look for orbits intersecting at most one constraints, so we can break
1107 // symmetry by fixing variables.
1108 //
1109 // TODO(user): The same effect could be achieved by adding symmetry breaking
1110 // constraints of the form "a >= b " between Booleans and let the presolve do
1111 // the reduction. This might be less code, but it is also less efficient.
1112 // Similarly, when we cannot just fix variables to break symmetries, we could
1113 // add these constraints, but it is unclear if we should do it all the time or
1114 // not.
1115 //
1116 // TODO(user): code the generic approach with orbits and stabilizer.
1117 std::vector<std::vector<int>> orbitope = BasicOrbitopeExtraction(generators);
1118 if (!orbitope.empty()) {
1119 SOLVER_LOG(context->logger(), "[Symmetry] Found orbitope of size ",
1120 orbitope.size(), " x ", orbitope[0].size());
1121 }
1122
1123 // HACK for flatzinc wordpress* problem.
1124 //
1125 // If we have a large orbitope, with one objective term by column, we break
1126 // the symmetry by ordering the objective terms. This usually increase
1127 // drastically the objective lower bounds we can discover.
1128 //
1129 // TODO(user): generalize somehow. See if we can exploit this in
1130 // lb_tree_search directly. We also have a lot more structure than just the
1131 // objective can be ordered. Like if the objective is a max, we can still do
1132 // that.
1133 //
1134 // TODO(user): Actually the constraint we add is really just breaking the
1135 // orbitope symmetry on one line. But this line being the objective is key. We
1136 // can also explicitly look for a full permutation group of the objective
1137 // terms directly instead of finding the largest orbitope first.
1138 if (!orbitope.empty() && context->working_model->has_objective()) {
1139 const int num_objective_terms = context->ObjectiveMap().size();
1140 if (orbitope[0].size() == num_objective_terms) {
1141 int num_in_column = 0;
1142 for (const std::vector<int>& row : orbitope) {
1143 if (context->ObjectiveMap().contains(row[0])) ++num_in_column;
1144 }
1145 if (num_in_column == 1) {
1146 context->WriteObjectiveToProto();
1147 const auto& obj = context->working_model->objective();
1148 CHECK_EQ(num_objective_terms, obj.vars().size());
1149 for (int i = 1; i < num_objective_terms; ++i) {
1150 auto* new_ct =
1152 new_ct->add_vars(obj.vars(i - 1));
1153 new_ct->add_vars(obj.vars(i));
1154 new_ct->add_coeffs(1);
1155 new_ct->add_coeffs(-1);
1156 new_ct->add_domain(0);
1157 new_ct->add_domain(std::numeric_limits<int64_t>::max());
1158 }
1160 context->UpdateRuleStats("symmetry: objective is one orbitope row.");
1161 return true;
1162 }
1163 }
1164 }
1165
1166 // Super simple heuristic to use the orbitope or not.
1167 //
1168 // In an orbitope with an at most one on each row, we can fix the upper right
1169 // triangle. We could use a formula, but the loop is fast enough.
1170 //
1171 // TODO(user): Compute the stabilizer under the only non-fixed element and
1172 // iterate!
1173 int max_num_fixed_in_orbitope = 0;
1174 if (!orbitope.empty()) {
1175 int size_left = orbitope[0].size();
1176 for (int col = 0; size_left > 1 && col < orbitope.size(); ++col) {
1177 max_num_fixed_in_orbitope += size_left - 1;
1178 --size_left;
1179 }
1180 }
1181
1182 // Fixing just a few variables to break large symmetry can be really bad. See
1183 // for example cdc7-4-3-2.pb.gz where we don't find solution if we do that. On
1184 // the other hand, enabling this make it worse on neos-3083784-nive.pb.gz.
1185 //
1186 // In general, enabling this works better in single thread with max_lp_sym,
1187 // but worse in multi-thread, where less workers are using symmetries, and so
1188 // it is better to fix more stuff.
1189 //
1190 // TODO(user): Tune more, especially as we handle symmetry better. Also the
1191 // estimate is pretty bad, we should probably compute stabilizer and decide
1192 // when we actually know how much we can fix compared to how many symmetry we
1193 // lose.
1194 const int num_fixable =
1195 std::max<int>(max_num_fixed_in_orbitope, can_be_fixed_to_false.size());
1196 if (/* DISABLES CODE */ (false) && !can_be_fixed_to_false.empty() &&
1197 100 * num_fixable < sum_of_orbit_sizes) {
1198 SOLVER_LOG(context->logger(),
1199 "[Symmetry] Not fixing anything as gain seems too small.");
1200 return true;
1201 }
1202
1203 // Fix "can_be_fixed_to_false" instead of the orbitope if it is larger.
1204 if (max_num_fixed_in_orbitope < can_be_fixed_to_false.size()) {
1205 const int orbit_index = orbits[distinguished_var];
1206 int num_in_orbit = 0;
1207 for (int i = 0; i < can_be_fixed_to_false.size(); ++i) {
1208 const int var = can_be_fixed_to_false[i];
1209 if (orbits[var] == orbit_index) ++num_in_orbit;
1210 context->UpdateRuleStats("symmetry: fixed to false in general orbit");
1211 if (var_can_be_true_per_orbit[orbits[var]] != -1) {
1212 // We are breaking the symmetry in a way that makes the hint invalid.
1213 // We want `var` to be false, so we would naively pick a symmetry to
1214 // enforce that. But that will be wrong if we do this twice: after we
1215 // permute the hint to fix the first one we would look for a symmetry
1216 // group element that fixes the second one to false. But there are many
1217 // of those, and picking the wrong one would risk making the first one
1218 // true again. Since this is a AMO, fixing the one that is true doesn't
1219 // have this problem.
1221 var_can_be_true_per_orbit[orbits[var]], true, generators);
1222 }
1223 if (!context->SetLiteralToFalse(var)) return false;
1224 }
1225
1226 // Moreover, we can add the implication that in the orbit of
1227 // distinguished_var, either everything is false, or var is at one.
1228 if (orbit_sizes[orbit_index] > num_in_orbit + 1) {
1229 context->UpdateRuleStats(
1230 "symmetry: added orbit symmetry breaking implications");
1231 auto* ct = context->working_model->add_constraints();
1232 auto* bool_and = ct->mutable_bool_and();
1233 ct->add_enforcement_literal(NegatedRef(distinguished_var));
1234 for (int var = 0; var < num_vars; ++var) {
1235 if (orbits[var] != orbit_index) continue;
1236 if (var == distinguished_var) continue;
1237 if (context->IsFixed(var)) continue;
1238 bool_and->add_literals(NegatedRef(var));
1239 }
1241 }
1242 return true;
1243 }
1244 if (orbitope.empty()) return true;
1245
1246 // This will always be kept all zero after usage.
1247 std::vector<int> tmp_to_clear;
1248 std::vector<int> tmp_sizes(num_vars, 0);
1249 std::vector<int> tmp_num_positive(num_vars, 0);
1250
1251 // TODO(user): The code below requires that no variable appears twice in the
1252 // same at most one. In particular lit and not(lit) cannot appear in the same
1253 // at most one.
1254 for (const google::protobuf::RepeatedField<int32_t>* literals :
1255 at_most_ones) {
1256 for (const int lit : *literals) {
1257 const int var = PositiveRef(lit);
1258 CHECK_NE(tmp_sizes[var], 1);
1259 tmp_sizes[var] = 1;
1260 }
1261 for (const int lit : *literals) {
1262 tmp_sizes[PositiveRef(lit)] = 0;
1263 }
1264 }
1265
1266 if (!orbitope.empty() && orbitope[0].size() > 1) {
1267 const int num_cols = orbitope[0].size();
1268 const std::vector<int> orbitope_orbits =
1269 GetOrbitopeOrbits(num_vars, orbitope);
1270
1271 // Using the orbitope orbits and intersecting at most ones, we will be able
1272 // in some case to derive a property of the literals of one row of the
1273 // orbitope. Namely that:
1274 // - All literals of that row take the same value.
1275 // - At most one literal can be true.
1276 // - At most one literal can be false.
1277 //
1278 // See the comment below for how we can infer this.
1279 const int num_rows = orbitope.size();
1280 std::vector<bool> row_is_all_equivalent(num_rows, false);
1281 std::vector<bool> row_has_at_most_one_true(num_rows, false);
1282 std::vector<bool> row_has_at_most_one_false(num_rows, false);
1283
1284 // Because in the orbitope case, we have a full symmetry group of the
1285 // columns, we can infer more than just using the orbits under a general
1286 // permutation group. If an at most one contains two variables from the
1287 // row, we can infer:
1288 // 1/ If the two variables appear positively, then there is an at most one
1289 // on the full row, and we can set n - 1 variables to zero to break the
1290 // symmetry.
1291 // 2/ If the two variables appear negatively, then the opposite situation
1292 // arise and there is at most one zero on the row, we can set n - 1
1293 // variables to one.
1294 // 3/ If two literals of opposite sign appear, then the only possibility
1295 // for the row are all at one or all at zero, thus we can mark all
1296 // variables as equivalent.
1297 //
1298 // These property comes from the fact that when we permute a line of the
1299 // orbitope in any way, then the position than ends up in the at most one
1300 // must never be both at one.
1301 //
1302 // Note that 3/ can be done without breaking any symmetry, but for 1/ and 2/
1303 // by choosing which variable is not fixed, we will break some symmetry.
1304 //
1305 // TODO(user): for 1/ and 2/ we could add an at most one constraint on the
1306 // full row if it is not already there!
1307 //
1308 // Note(user): On the miplib, only 1/ and 2/ happens currently. Not sure
1309 // with LNS though.
1310 for (const google::protobuf::RepeatedField<int32_t>* literals :
1311 at_most_ones) {
1312 tmp_to_clear.clear();
1313 for (const int literal : *literals) {
1314 if (context->IsFixed(literal)) continue;
1315 const int var = PositiveRef(literal);
1316 const int row = orbitope_orbits[var];
1317 if (row == -1) continue;
1318
1319 if (tmp_sizes[row] == 0) tmp_to_clear.push_back(row);
1320 tmp_sizes[row]++;
1321 if (RefIsPositive(literal)) tmp_num_positive[row]++;
1322 }
1323
1324 // An at most one touching two positions in an orbitope row can be
1325 // extended to include the full row.
1326 //
1327 // Note(user): I am not sure we care about that here. By symmetry, if we
1328 // have an at most one touching two positions, then we should have others
1329 // touching all pair of positions. And the at most one expansion would
1330 // already have extended it. So this is more FYI.
1331 bool possible_extension = false;
1332
1333 // TODO(user): if the same at most one touch more than one row, we can
1334 // deduce more. It is a bit tricky and maybe not frequent enough to make a
1335 // big difference. Also, as we start to fix things, at most one might
1336 // propagate by themselves.
1337 for (const int row : tmp_to_clear) {
1338 const int size = tmp_sizes[row];
1339 const int num_positive = tmp_num_positive[row];
1340 const int num_negative = tmp_sizes[row] - tmp_num_positive[row];
1341 tmp_sizes[row] = 0;
1342 tmp_num_positive[row] = 0;
1343
1344 if (num_positive > 0 && num_negative > 0) {
1345 row_is_all_equivalent[row] = true;
1346 }
1347 if (num_positive > 1 && num_negative == 0) {
1348 if (size < num_cols) possible_extension = true;
1349 row_has_at_most_one_true[row] = true;
1350 } else if (num_positive == 0 && num_negative > 1) {
1351 if (size < num_cols) possible_extension = true;
1352 row_has_at_most_one_false[row] = true;
1353 }
1354 }
1355
1356 if (possible_extension) {
1357 context->UpdateRuleStats(
1358 "TODO symmetry: possible at most one extension.");
1359 }
1360 }
1361
1362 // List the row in "at most one" by score. We will be able to fix a
1363 // "triangle" of literals in order to break some of the symmetry.
1364 std::vector<std::pair<int, int64_t>> rows_by_score;
1365
1366 // Mark all the equivalence or fixed rows.
1367 // Note that this operation do not change the symmetry group.
1368 //
1369 // TODO(user): We could remove these rows from the orbitope. Note that
1370 // currently this never happen on the miplib (maybe in LNS though).
1371 for (int i = 0; i < num_rows; ++i) {
1372 if (row_has_at_most_one_true[i] && row_has_at_most_one_false[i]) {
1373 // If we have both property, it means we have
1374 // - sum_j orbitope[row][j] <= 1
1375 // - sum_j not(orbitope[row][j]) <= 1 which is the same as
1376 // sum_j orbitope[row][j] >= num_cols - 1.
1377 // This is only possible if we have two elements and we don't have
1378 // row_is_all_equivalent.
1379 if (num_cols == 2 && !row_is_all_equivalent[i]) {
1380 // We have [1, 0] or [0, 1].
1381 context->UpdateRuleStats("symmetry: equivalence in orbitope row");
1382 if (!context->StoreBooleanEqualityRelation(
1383 orbitope[i][0], NegatedRef(orbitope[i][1]))) {
1384 return false;
1385 }
1386 if (context->ModelIsUnsat()) return false;
1387 } else {
1388 // No solution.
1389 return context->NotifyThatModelIsUnsat("orbitope and at most one");
1390 }
1391 continue;
1392 }
1393
1394 if (row_is_all_equivalent[i]) {
1395 // Here we proved that the row is either all ones or all zeros.
1396 // This was because we had:
1397 // at_most_one = [x, ~y, ...]
1398 // orbitope = [x, y, ...]
1399 // and by symmetry we have
1400 // at_most_one = [~x, y, ...]
1401 // This for all pairs of positions in that row.
1402 if (row_has_at_most_one_false[i]) {
1403 context->UpdateRuleStats("symmetry: all true in orbitope row");
1404 for (int j = 0; j < num_cols; ++j) {
1405 if (!context->SetLiteralToTrue(orbitope[i][j])) return false;
1406 }
1407 } else if (row_has_at_most_one_true[i]) {
1408 context->UpdateRuleStats("symmetry: all false in orbitope row");
1409 for (int j = 0; j < num_cols; ++j) {
1410 if (!context->SetLiteralToFalse(orbitope[i][j])) return false;
1411 }
1412 } else {
1413 context->UpdateRuleStats("symmetry: all equivalent in orbitope row");
1414 for (int j = 1; j < num_cols; ++j) {
1415 if (!context->StoreBooleanEqualityRelation(orbitope[i][0],
1416 orbitope[i][j])) {
1417 return false;
1418 }
1419 if (context->ModelIsUnsat()) return false;
1420 }
1421 }
1422 continue;
1423 }
1424
1425 // We use as the score the number of constraint in which variables from
1426 // this row participate.
1427 const int64_t score =
1428 context->VarToConstraints(PositiveRef(orbitope[i][0])).size();
1429 if (row_has_at_most_one_true[i]) {
1430 rows_by_score.push_back({i, score});
1431 } else if (row_has_at_most_one_false[i]) {
1432 rows_by_score.push_back({i, score});
1433 }
1434 }
1435
1436 // Break the symmetry by fixing at each step all but one literal to true or
1437 // false. Note that each time we do that for a row, we need to exclude the
1438 // non-fixed column from the rest of the row processing. We thus fix a
1439 // "triangle" of literals.
1440 //
1441 // This is the same as ordering the columns in some lexicographic order and
1442 // using the at_most_ones to fix known position. Note that we can still add
1443 // lexicographic symmetry breaking inequality on the columns as long as we
1444 // do that in the same order as these fixing.
1445 absl::c_stable_sort(rows_by_score, [](const std::pair<int, int64_t>& p1,
1446 const std::pair<int, int64_t>& p2) {
1447 return p1.second > p2.second;
1448 });
1449 int num_processed_rows = 0;
1450 for (const auto [row, score] : rows_by_score) {
1451 if (num_processed_rows + 1 >= num_cols) break;
1452 ++num_processed_rows;
1453 if (row_has_at_most_one_true[row]) {
1454 context->UpdateRuleStats(
1455 "symmetry: fixed all but one to false in orbitope row");
1456 for (int j = num_processed_rows; j < num_cols; ++j) {
1457 if (!context->SetLiteralToFalse(orbitope[row][j])) return false;
1458 }
1459 } else {
1460 CHECK(row_has_at_most_one_false[row]);
1461 context->UpdateRuleStats(
1462 "symmetry: fixed all but one to true in orbitope row");
1463 for (int j = num_processed_rows; j < num_cols; ++j) {
1464 if (!context->SetLiteralToTrue(orbitope[row][j])) return false;
1465 }
1466 }
1467 }
1468
1469 // For correctness of the code below, reduce the orbitope.
1470 //
1471 // TODO(user): This is probably not needed if we add lexicographic
1472 // constraint instead of just breaking a single row below.
1473 if (num_processed_rows > 0) {
1474 // Remove the first num_processed_rows.
1475 int new_size = 0;
1476 for (int i = num_processed_rows; i < orbitope.size(); ++i) {
1477 orbitope[new_size++] = std::move(orbitope[i]);
1478 }
1479 CHECK_LT(new_size, orbitope.size());
1480 orbitope.resize(new_size);
1481
1482 // For each of them remove the first num_processed_rows entries.
1483 for (int i = 0; i < orbitope.size(); ++i) {
1484 CHECK_LT(num_processed_rows, orbitope[i].size());
1485 orbitope[i].erase(orbitope[i].begin(),
1486 orbitope[i].begin() + num_processed_rows);
1487 }
1488 }
1489 }
1490
1491 // The transformations below seems to hurt more than what they help.
1492 // Especially when we handle symmetry during the search like with max_lp_sym
1493 // worker. See for instance neos-948346.pb or map06.pb.gz.
1494 if (params.symmetry_level() <= 3) return true;
1495
1496 // If we are left with a set of variable than can all be permuted, lets
1497 // break the symmetry by ordering them.
1498 if (orbitope.size() == 1) {
1499 const int num_cols = orbitope[0].size();
1500 for (int i = 0; i + 1 < num_cols; ++i) {
1501 // Add orbitope[0][i] >= orbitope[0][i+1].
1502 if (context->CanBeUsedAsLiteral(orbitope[0][i]) &&
1503 context->CanBeUsedAsLiteral(orbitope[0][i + 1])) {
1504 context->AddImplication(orbitope[0][i + 1], orbitope[0][i]);
1505 context->UpdateRuleStats(
1506 "symmetry: added symmetry breaking implication");
1507 continue;
1508 }
1509
1511 ct->mutable_linear()->add_coeffs(1);
1512 ct->mutable_linear()->add_vars(orbitope[0][i]);
1513 ct->mutable_linear()->add_coeffs(-1);
1514 ct->mutable_linear()->add_vars(orbitope[0][i + 1]);
1515 ct->mutable_linear()->add_domain(0);
1516 ct->mutable_linear()->add_domain(std::numeric_limits<int64_t>::max());
1517 context->UpdateRuleStats("symmetry: added symmetry breaking inequality");
1518 }
1520 } else if (orbitope.size() > 1) {
1521 std::vector<int64_t> max_values(orbitope.size());
1522 for (int i = 0; i < orbitope.size(); ++i) {
1523 const int var = orbitope[i][0];
1524 const int64_t max = std::max(std::abs(context->MaxOf(var)),
1525 std::abs(context->MinOf(var)));
1526 max_values[i] = max;
1527 }
1528 constexpr int kMaxBits = 60;
1529 bool is_approximated;
1530 const std::vector<int64_t> coeffs = BuildInequalityCoeffsForOrbitope(
1531 max_values, (int64_t{1} << kMaxBits), &is_approximated);
1532 for (int i = 0; i + 1 < orbitope[0].size(); ++i) {
1534 auto* arg = ct->mutable_linear();
1535 for (int j = 0; j < orbitope.size(); ++j) {
1536 const int64_t coeff = coeffs[j];
1537 arg->add_vars(orbitope[j][i + 1]);
1538 arg->add_coeffs(coeff);
1539 arg->add_vars(orbitope[j][i]);
1540 arg->add_coeffs(-coeff);
1541 DCHECK_EQ(context->MaxOf(orbitope[j][i + 1]),
1542 context->MaxOf(orbitope[j][i]));
1543 DCHECK_EQ(context->MinOf(orbitope[j][i + 1]),
1544 context->MinOf(orbitope[j][i]));
1545 }
1546 arg->add_domain(0);
1547 arg->add_domain(std::numeric_limits<int64_t>::max());
1548 DCHECK(!PossibleIntegerOverflow(*context->working_model, arg->vars(),
1549 arg->coeffs()));
1550 }
1551 context->UpdateRuleStats(
1552 absl::StrCat("symmetry: added linear ",
1553 is_approximated ? "approximated " : "",
1554 "inequality ordering orbitope columns"),
1555 orbitope[0].size());
1557 return true;
1558 }
1559
1560 return true;
1561}
1562
1563namespace {
1564
1565std::vector<absl::Span<int>> GetCyclesAsSpan(
1566 SparsePermutationProto& permutation) {
1567 std::vector<absl::Span<int>> result;
1568 int start = 0;
1569 const int num_cycles = permutation.cycle_sizes().size();
1570 for (int i = 0; i < num_cycles; ++i) {
1571 const int size = permutation.cycle_sizes(i);
1572 result.push_back(
1573 absl::MakeSpan(&permutation.mutable_support()->at(start), size));
1574 start += size;
1575 }
1576 return result;
1577}
1578
1579} // namespace
1580
1582 PresolveContext* context) {
1583 std::vector<absl::Span<int>> cycles;
1584 int num_problematic_generators = 0;
1585 for (SparsePermutationProto& generator : *symmetry->mutable_permutations()) {
1586 // We process each cycle at once.
1587 // If all variables from a cycle are fixed to the same value, this is
1588 // fine and we can just remove the cycle.
1589 //
1590 // TODO(user): These are just basic checks and do not guarantee that we
1591 // properly kept this symmetry in the presolve.
1592 //
1593 // TODO(user): Deal with case where all variable in an orbit has been found
1594 // to be equivalent to each other. Or all variables have affine
1595 // representative, like if all domains where [0][2], we should have remapped
1596 // all such variable to Booleans.
1597 cycles = GetCyclesAsSpan(generator);
1598 bool problematic = false;
1599
1600 int new_num_cycles = 0;
1601 const int old_num_cycles = cycles.size();
1602 for (int i = 0; i < old_num_cycles; ++i) {
1603 if (cycles[i].empty()) continue;
1604 const int reference_var = cycles[i][0];
1605 const Domain reference_domain = context->DomainOf(reference_var);
1606 const AffineRelation::Relation reference_relation =
1607 context->GetAffineRelation(reference_var);
1608
1609 int num_affine_relations = 0;
1610 int num_with_same_representative = 0;
1611
1612 int num_fixed = 0;
1613 int num_unused = 0;
1614 for (const int var : cycles[i]) {
1615 CHECK(RefIsPositive(var));
1616 if (context->DomainOf(var) != reference_domain) {
1617 context->UpdateRuleStats(
1618 "TODO symmetry: different domain in symmetric variables");
1619 problematic = true;
1620 break;
1621 }
1622
1623 if (context->DomainOf(var).IsFixed()) {
1624 ++num_fixed;
1625 continue;
1626 }
1627
1628 // If we have affine relation, we only support the case where they
1629 // are all the same.
1630 const auto affine_relation = context->GetAffineRelation(var);
1631 if (affine_relation == reference_relation) {
1632 ++num_with_same_representative;
1633 }
1634 if (affine_relation.representative != var) {
1635 ++num_affine_relations;
1636 }
1637
1638 if (context->VariableIsNotUsedAnymore(var)) {
1639 ++num_unused;
1640 continue;
1641 }
1642 }
1643
1644 if (problematic) break;
1645
1646 if (num_fixed > 0) {
1647 if (num_fixed != cycles[i].size()) {
1648 context->UpdateRuleStats(
1649 "TODO symmetry: not all variables fixed in cycle");
1650 problematic = true;
1651 break;
1652 }
1653 continue; // We can skip this cycle
1654 }
1655
1656 if (num_affine_relations > 0) {
1657 if (num_with_same_representative != cycles[i].size()) {
1658 context->UpdateRuleStats(
1659 "TODO symmetry: not all variables have same representative");
1660 problematic = true;
1661 break;
1662 }
1663 continue; // We can skip this cycle
1664 }
1665
1666 // Note that the order matter.
1667 // If all have the same representative, we don't care about this one.
1668 if (num_unused > 0) {
1669 if (num_unused != cycles[i].size()) {
1670 context->UpdateRuleStats(
1671 "TODO symmetry: not all variables unused in cycle");
1672 problematic = true;
1673 break;
1674 }
1675 continue; // We can skip this cycle
1676 }
1677
1678 // Lets keep this cycle.
1679 cycles[new_num_cycles++] = cycles[i];
1680 }
1681
1682 if (problematic) {
1683 ++num_problematic_generators;
1684 generator.clear_support();
1685 generator.clear_cycle_sizes();
1686 continue;
1687 }
1688
1689 if (new_num_cycles < old_num_cycles) {
1690 cycles.resize(new_num_cycles);
1691 generator.clear_cycle_sizes();
1692 int new_support_size = 0;
1693 for (const absl::Span<int> cycle : cycles) {
1694 for (const int var : cycle) {
1695 generator.set_support(new_support_size++, var);
1696 }
1697 generator.add_cycle_sizes(cycle.size());
1698 }
1699 generator.mutable_support()->Truncate(new_support_size);
1700 }
1701 }
1702
1703 if (num_problematic_generators > 0) {
1704 SOLVER_LOG(context->logger(), "[Symmetry] ", num_problematic_generators,
1705 " generators where problematic !! Fix.");
1706 }
1707
1708 // Lets remove empty generators.
1709 int new_size = 0;
1710 const int old_size = symmetry->permutations().size();
1711 for (int i = 0; i < old_size; ++i) {
1712 if (symmetry->permutations(i).support().empty()) continue;
1713 if (new_size != i) {
1714 symmetry->mutable_permutations()->SwapElements(new_size, i);
1715 }
1716 ++new_size;
1717 }
1718 if (new_size != old_size) {
1719 symmetry->mutable_permutations()->DeleteSubrange(new_size,
1720 old_size - new_size);
1721 }
1722
1723 // Lets output the new statistics.
1724 // TODO(user): Avoid the reconvertion.
1725 {
1726 const int num_vars = context->working_model->variables().size();
1727 std::vector<std::unique_ptr<SparsePermutation>> generators;
1728 for (const SparsePermutationProto& perm : symmetry->permutations()) {
1729 generators.emplace_back(CreateSparsePermutationFromProto(num_vars, perm));
1730 }
1731 SOLVER_LOG(context->logger(),
1732 "[Symmetry] final processing #generators:", generators.size());
1733 const std::vector<int> orbits = GetOrbits(num_vars, generators);
1734 LogOrbitInformation(orbits, context->logger());
1735 }
1736
1737 return true;
1738}
1739
1740} // namespace sat
1741} // namespace operations_research
Definition model.h:341
absl::Status FindSymmetries(std::vector< int > *node_equivalence_classes_io, std::vector< std::unique_ptr< SparsePermutation > > *generators, std::vector< int > *factorized_automorphism_group_size, TimeLimit *time_limit=nullptr)
bool LoggingIsEnabled() const
Returns true iff logging is enabled.
Definition logging.h:50
void RemoveCycles(absl::Span< const int > cycle_indices)
const std::vector< int > & Support() const
static std::unique_ptr< TimeLimit > FromDeterministicTime(double deterministic_limit)
Definition time_limit.h:128
::operations_research::sat::BoolArgumentProto *PROTOBUF_NONNULL mutable_bool_and()
const ::operations_research::sat::BoolArgumentProto & exactly_one() const
const ::operations_research::sat::BoolArgumentProto & at_most_one() const
::operations_research::sat::LinearConstraintProto *PROTOBUF_NONNULL mutable_linear()
::operations_research::sat::ConstraintProto *PROTOBUF_NONNULL mutable_constraints(int index)
const ::operations_research::sat::IntegerVariableProto & variables(int index) const
const ::operations_research::sat::ConstraintProto & constraints(int index) const
bool has_objective() const
.operations_research.sat.CpObjectiveProto objective = 4;
int constraints_size() const
repeated .operations_research.sat.ConstraintProto constraints = 3;
::operations_research::sat::SymmetryProto *PROTOBUF_NONNULL mutable_symmetry()
::operations_research::sat::ConstraintProto *PROTOBUF_NONNULL add_constraints()
int variables_size() const
repeated .operations_research.sat.IntegerVariableProto variables = 2;
const ::operations_research::sat::CpObjectiveProto & objective() const
ABSL_MUST_USE_RESULT bool SetLiteralToTrue(int lit)
ABSL_MUST_USE_RESULT bool SetLiteralToFalse(int lit)
Returns false if the 'lit' doesn't have the desired value in the domain.
ABSL_MUST_USE_RESULT bool NotifyThatModelIsUnsat(absl::string_view message="")
bool StoreBooleanEqualityRelation(int ref_a, int ref_b)
bool VariableIsNotUsedAnymore(int ref) const
Returns true if this ref no longer appears in the model.
void UpdateRuleStats(const std::string &name, int num_times=1)
AffineRelation::Relation GetAffineRelation(int ref) const
Returns the representative of ref under the affine relations.
const absl::flat_hash_set< int > & VarToConstraints(int var) const
void UpdateNewConstraintsVariableUsage()
Calls UpdateConstraintVariableUsage() on all newly created constraints.
const absl::flat_hash_map< int, int64_t > & ObjectiveMap() const
void MaybeUpdateVarWithSymmetriesToValue(int var, bool value, absl::Span< const std::unique_ptr< SparsePermutation > > generators)
const ::operations_research::sat::SparsePermutationProto & permutations(int index) const
::operations_research::sat::SparsePermutationProto *PROTOBUF_NONNULL mutable_permutations(int index)
::operations_research::sat::SparsePermutationProto *PROTOBUF_NONNULL add_permutations()
::operations_research::sat::DenseMatrixProto *PROTOBUF_NONNULL add_orbitopes()
ABSL_ATTRIBUTE_REINITIALIZES void Clear() PROTOBUF_FINAL
time_limit
Definition solve.cc:22
std::vector< int > GetOrbitopeOrbits(int n, absl::Span< const std::vector< int > > orbitope)
bool LoadModelForProbing(PresolveContext *context, Model *local_model)
bool DetectAndExploitSymmetriesInPresolve(PresolveContext *context)
void FindCpModelSymmetries(const SatParameters &params, const CpModelProto &problem, std::vector< std::unique_ptr< SparsePermutation > > *generators, SolverLogger *logger, TimeLimit *solver_time_limit)
bool PossibleIntegerOverflow(const CpModelProto &model, absl::Span< const int > vars, absl::Span< const int64_t > coeffs, int64_t offset, std::pair< int64_t, int64_t > *implied_domain)
bool FilterOrbitOnUnusedOrFixedVariables(SymmetryProto *symmetry, PresolveContext *context)
std::string FormatCounter(int64_t num)
Prints a positive number with separators for easier reading (ex: 1'348'065).
Definition util.cc:44
std::vector< int > GetOrbits(int n, absl::Span< const std::unique_ptr< SparsePermutation > > generators)
absl::string_view ConstraintCaseName(ConstraintProto::ConstraintCase constraint_case)
void DetectAndAddSymmetryToProto(const SatParameters &params, CpModelProto *proto, SolverLogger *logger, TimeLimit *time_limit)
Detects symmetries and fill the symmetry field.
std::unique_ptr< SparsePermutation > CreateSparsePermutationFromProto(int n, const SparsePermutationProto &proto)
Creates a SparsePermutation on [0, n) from its proto representation.
int NegatedRef(int ref)
Small utility functions to deal with negative variable/literal references.
std::vector< std::vector< int > > BasicOrbitopeExtraction(absl::Span< const std::unique_ptr< SparsePermutation > > generators)
Graph * GenerateGraphForSymmetryDetection(const LinearBooleanProblem &problem, std::vector< int > *initial_equivalence_classes)
In SWIG mode, we don't want anything besides these top-level includes.
int64_t CapAdd(int64_t x, int64_t y)
const bool DEBUG_MODE
Definition radix_sort.h:266
Point BinarySearch(Point x_true, Point x_false, std::function< bool(Point)> f)
int64_t CapProd(int64_t x, int64_t y)
util::ReverseArcStaticGraph Graph
Type of graph to use.
ClosedInterval::Iterator begin(ClosedInterval interval)
uint64_t Hash(uint64_t num, uint64_t c)
Definition hash.h:73
std::vector< int >::const_iterator begin() const
#define SOLVER_LOG(logger,...)
Definition logging.h:110