OR-Tools  8.2
symmetry.h
Go to the documentation of this file.
1// Copyright 2010-2018 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
14#ifndef OR_TOOLS_SAT_SYMMETRY_H_
15#define OR_TOOLS_SAT_SYMMETRY_H_
16
17#include <memory>
18#include <vector>
19
20#include "absl/types/span.h"
22#include "ortools/base/macros.h"
25#include "ortools/util/stats.h"
26
27namespace operations_research {
28namespace sat {
29
30// This class implements more or less the strategy described in the paper:
31// Devriendt J., Bogaerts B., De Cat B., Denecker M., Mears C. "Symmetry
32// propagation: Improved Dynamic Symmetry Breaking in SAT", 2012,
33// IEEE 24th International Conference on Tools with Artificial Intelligence.
34//
35// Basically, each time a literal is propagated, this class tries to detect
36// if another literal could also be propagated by symmetry. Note that this uses
37// a heuristic in order to be efficient and that it is not exhaustive in the
38// sense that it doesn't detect all possible propagations.
39//
40// Algorithm details:
41//
42// Given the current solver trail (i.e. the assigned literals and their
43// assignment order) the idea is to compute (as efficiently as possible) for
44// each permutation added to this class what is called the first (under the
45// trail assignment order) non-symmetric literal. A literal 'l' is said to be
46// non-symmetric under a given assignement and for a given permutation 'p' if
47// 'l' is assigned to true but not 'p(l)'.
48//
49// If a first non-symmetric literal 'l' for a permutation 'p' is not a decision,
50// then:
51// - Because it is not a decision, 'l' has been implied by a reason formed by
52// literals assigned to true at lower trail indices.
53// - Because this is the first non-symmetric literal for 'p', the permuted
54// reason only contains literal that are also assigned to true.
55// - Because of this, 'p(l)' is also implied by the current assignment.
56// Of course, this assume that p is a symmetry of the full problem.
57// Note that if it is already assigned to false, then we have a conflict.
58//
59// TODO(user): Implement the optimizations mentioned in the paper?
60// TODO(user): Instrument and see if the code can be optimized.
62 public:
64 ~SymmetryPropagator() override;
65
66 bool Propagate(Trail* trail) final;
67 void Untrail(const Trail& trail, int trail_index) final;
68 absl::Span<const Literal> Reason(const Trail& trail,
69 int trail_index) const final;
70
71 // Adds a new permutation to this symmetry propagator. The ownership is
72 // transferred. This must be an integer permutation such that:
73 // - Its domain is [0, 2 * num_variables) and corresponds to the index
74 // representation of the literals over num_variables variables.
75 // - It must be compatible with the negation, for any literal l; not(p(l))
76 // must be the same as p(not(l)), where p(x) represents the image of x by
77 // the permutation.
78 //
79 // Remark: Any permutation which is a symmetry of the main SAT problem can be
80 // added here. However, since the number of permutations is usually not
81 // manageable, a good alternative is to only add the generators of the
82 // permutation group. It is also important to add permutations with a support
83 // as small as possible.
84 //
85 // TODO(user): Currently this can only be called before PropagateNext() is
86 // called (DCHECKed). Not sure if we need more incrementality though.
87 void AddSymmetry(std::unique_ptr<SparsePermutation> permutation);
88 int num_permutations() const { return permutations_.size(); }
89
90 // Visible for testing.
91 //
92 // Permutes a list of literals from input into output using the permutation
93 // with given index. This uses tmp_literal_mapping_ and has a complexity in
94 // O(permutation_support + input_size).
95 void Permute(int index, absl::Span<const Literal> input,
96 std::vector<Literal>* output) const;
97
98 private:
99 // Propagates the literal at propagation_trail_index_ from the trail.
100 bool PropagateNext(Trail* trail);
101
102 // The permutations.
103 // The index of a permutation is its position in this vector.
104 std::vector<std::unique_ptr<SparsePermutation>> permutations_;
105
106 // Reverse mapping (source literal) -> list of (permutation_index, image).
107 struct ImageInfo {
108 ImageInfo(int p, Literal i) : permutation_index(p), image(i) {}
109
110 int permutation_index;
111 Literal image;
112 };
114
115 // For each permutation p, we maintain the list of all assigned literals
116 // affected by p whose trail index is < propagation_trail_index_; sorted by
117 // trail index. Next to each such literal, we also store:
118 struct AssignedLiteralInfo {
119 AssignedLiteralInfo(Literal l, Literal i, int index)
120 : literal(l), image(i), first_non_symmetric_info_index_so_far(index) {}
121
122 // The literal in question (assigned to true and in the support of p).
123 Literal literal;
124
125 // The image by p of the literal above.
126 Literal image;
127
128 // Previous AssignedLiteralInfos are considered 'symmetric' iff both their
129 // 'literal' and 'image' were assigned to true at the time the current
130 // AssignedLiteralInfo's literal was assigned (i.e. earlier in the trail).
131 int first_non_symmetric_info_index_so_far;
132 };
133 std::vector<std::vector<AssignedLiteralInfo>> permutation_trails_;
134
135 // Adds an AssignedLiteralInfo to the given permutation trail.
136 // Returns false if there is a non-symmetric literal in this trail with its
137 // image not already assigned to true by the solver.
138 bool Enqueue(const Trail& trail, Literal literal, Literal image,
139 std::vector<AssignedLiteralInfo>* p_trail);
140
141 // The identity permutation over all the literals.
142 // This is temporary modified to encode a sparse permutation and then always
143 // restored to the identity.
144 mutable absl::StrongVector<LiteralIndex, Literal> tmp_literal_mapping_;
145
146 // Symmetry reason indexed by trail_index.
147 struct ReasonInfo {
148 int source_trail_index;
149 int symmetry_index;
150 };
151 std::vector<ReasonInfo> reasons_;
152
153 mutable StatsGroup stats_;
154 int num_propagations_;
155 int num_conflicts_;
156 DISALLOW_COPY_AND_ASSIGN(SymmetryPropagator);
157};
158
159} // namespace sat
160} // namespace operations_research
161
162#endif // OR_TOOLS_SAT_SYMMETRY_H_
absl::Span< const Literal > Reason(const Trail &trail, int trail_index) const final
Definition: symmetry.cc:147
void AddSymmetry(std::unique_ptr< SparsePermutation > permutation)
Definition: symmetry.cc:36
void Permute(int index, absl::Span< const Literal > input, std::vector< Literal > *output) const
Definition: symmetry.cc:192
void Untrail(const Trail &trail, int trail_index) final
Definition: symmetry.cc:134
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Literal literal
Definition: optimization.cc:84
int index
Definition: pack.cc:508
static int input(yyscan_t yyscanner)