Google OR-Tools v9.14
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
all_different.h
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
14#ifndef OR_TOOLS_SAT_ALL_DIFFERENT_H_
15#define OR_TOOLS_SAT_ALL_DIFFERENT_H_
16
17#include <cstdint>
18#include <functional>
19#include <utility>
20#include <vector>
21
22#include "absl/log/check.h"
23#include "absl/types/span.h"
25#include "ortools/sat/integer.h"
27#include "ortools/sat/model.h"
29#include "ortools/util/bitset.h"
31
32namespace operations_research {
33namespace sat {
34
35// Enforces that the given tuple of variables takes different values. This fully
36// encodes all the variables and simply enforces a <= 1 constraint on each
37// possible values.
38std::function<void(Model*)> AllDifferentBinary(
39 absl::Span<const IntegerVariable> vars);
40
41// Enforces that the given tuple of variables takes different values.
42// Same as AllDifferentBinary() but use a different propagator that only enforce
43// the so called "bound consistency" on the variable domains.
44//
45// Compared to AllDifferentBinary() this doesn't require fully encoding the
46// variables and it is also quite fast. Note that the propagation is different,
47// this will not remove already taken values from inside a domain, but it will
48// propagates more the domain bounds.
49std::function<void(Model*)> AllDifferentOnBounds(
50 absl::Span<const IntegerVariable> vars);
51std::function<void(Model*)> AllDifferentOnBounds(
52 absl::Span<const AffineExpression> expressions);
53
54// This constraint forces all variables to take different values. This is meant
55// to be used as a complement to an alldifferent decomposition like
56// AllDifferentBinary(): DO NOT USE WITHOUT ONE. Doing the filtering that the
57// decomposition can do with an appropriate algorithm should be cheaper and
58// yield more accurate explanations.
59//
60// It uses the matching algorithm described in Regin at AAAI1994:
61// "A filtering algorithm for constraints of difference in CSPs".
62//
63// This will fully encode variables.
64std::function<void(Model*)> AllDifferentAC(
65 absl::Span<const IntegerVariable> variables);
66
67// Implementation of AllDifferentAC().
69 public:
70 AllDifferentConstraint(absl::Span<const IntegerVariable> variables,
71 Model* model);
72
73 // In a circuit, the successor of all node must be "different".
74 // Thus this propagator can also be used in this context.
75 AllDifferentConstraint(int num_nodes, absl::Span<const int> tails,
76 absl::Span<const int> heads,
77 absl::Span<const Literal> literals, Model* model);
78
79 bool Propagate() final;
81
82 private:
83 // MakeAugmentingPath() is a step in Ford-Fulkerson's augmenting path
84 // algorithm. It changes its current internal state (see vectors below)
85 // to assign a value to the start vertex using an augmenting path.
86 // If it is not possible, it keeps variable_to_value_[start] to -1 and returns
87 // false, otherwise it modifies the current assignment and returns true.
88 // It uses value/variable_visited to mark the nodes it visits during its
89 // search: one can use this information to generate an explanation of failure,
90 // or manipulate it to create what-if scenarios without modifying successor_.
91 bool MakeAugmentingPath(int start);
92
93 // This caches all literals of the fully encoded variables.
94 // Values of a given variable are 0-indexed using offsets variable_min_value_,
95 // the set of all values is globally offset using offset min_all_values_.
96 // TODO(user): compare this encoding to a sparser hash_map encoding.
97 const int num_variables_;
98 const std::vector<IntegerVariable> variables_;
99
100 // Note that we remap all value into [0, num_values_) in a "dense" way.
101 std::vector<std::vector<std::pair<int, Literal>>>
102 variable_to_possible_values_;
103 int64_t num_values_;
104
105 // Internal state of MakeAugmentingPath().
106 // value_to_variable_ and variable_to_value_ represent the current assignment;
107 // -1 means not assigned. Otherwise,
108 // variable_to_value_[var] = value <=> value_to_variable_[value] = var.
109 CompactVectorVector<int> successor_;
110 std::vector<bool> value_visited_;
111 std::vector<bool> variable_visited_;
112 std::vector<int> value_to_variable_;
113 std::vector<int> variable_to_value_;
114 std::vector<int> prev_matching_;
115 std::vector<int> visiting_;
116 std::vector<int> variable_visited_from_;
117
118 // Internal state of ComputeSCCs().
119 // Variable nodes are indexed by [0, num_variables_),
120 // value nodes by [num_variables_, num_variables_ + num_all_values_),
121 // and a dummy node with index num_variables_ + num_all_values_ is added.
122 // The graph passed to ComputeSCCs() is the residual of the possible graph
123 // by the current matching, i.e. its arcs are:
124 // _ (var, val) if val \in dom(var) and var not matched to val,
125 // _ (val, var) if var matched to val,
126 // _ (val, dummy) if val not matched to any variable,
127 // _ (dummy, var) for all variables.
128 // In the original paper, forbidden arcs are identified by detecting that they
129 // are not in any alternating cycle or alternating path starting at a
130 // free vertex. Adding the dummy node allows to factor the alternating path
131 // part in the alternating cycle, and filter with only the SCC decomposition.
132 // When num_variables_ == num_all_values_, the dummy node is useless,
133 // we add it anyway to simplify the code.
134 CompactVectorVector<int> residual_graph_successors_;
135 std::vector<int> component_number_;
136
137 Trail* trail_;
138 IntegerTrail* integer_trail_;
139};
140
141// Implements the all different bound consistent propagator with explanation.
142// That is, given n affine expressions that must take different values, this
143// propagates the bounds of each expression as much as possible. The key is to
144// detect the so called Hall interval which are interval of size k that contains
145// the domain of k expressinos. Because all the variables must take different
146// values, we can deduce that the domain of the other variables cannot contains
147// such Hall interval.
148//
149// We use a "fast" O(n log n) algorithm.
150//
151// TODO(user): It might be difficult to find something faster than what is
152// implemented here. Some related reference:
153// https://cs.uwaterloo.ca/~vanbeek/Publications/ijcai03_TR.pdf
155 public:
156 AllDifferentBoundsPropagator(absl::Span<const AffineExpression> expressions,
157 IntegerTrail* integer_trail);
158
159 // This type is neither copyable nor movable.
162 delete;
163
164 bool Propagate() final;
165 void RegisterWith(GenericLiteralWatcher* watcher);
166
167 private:
168 // We locally cache the lb/ub for faster sorting and to guarantee some
169 // invariant when we push bounds.
170 struct CachedBounds {
171 AffineExpression expr;
172 IntegerValue lb;
173 IntegerValue ub;
174 };
175
176 // Fills integer_reason_ with the reason why we have the given hall interval.
177 void FillHallReason(IntegerValue hall_lb, IntegerValue hall_ub);
178
179 // Do half the job of Propagate(). This will split the variable into
180 // independent subset, and call PropagateLowerBoundsInternal() on each of
181 // them.
182 bool PropagateLowerBounds();
183 bool PropagateLowerBoundsInternal(IntegerValue min_lb,
184 absl::Span<CachedBounds> bounds);
185
186 // Internally, we will maintain a set of non-consecutive integer intervals of
187 // the form [start, end]. Each point (i.e. IntegerValue) of such interval will
188 // be associated to an unique input expression and via an union-find algorithm
189 // point to its start. The end only make sense for representative.
190 //
191 // TODO(user): Because we don't use rank, we have a worst case complexity of
192 // O(n log n). We could try a normal Union-find data structure, but then we
193 // also have to maintain a start vector.
194 //
195 // Note that during the execution of the algorithm we start from empty
196 // intervals and finish with a set of points of size num_vars.
197 //
198 // The list of all points are maintained in the dense vectors index_to_*_
199 // where we have remapped values to indices (with GetIndex()) to make sure it
200 // always fall into the correct range.
201 int FindStartIndexAndCompressPath(int index);
202
203 int GetIndex(IntegerValue value) const {
204 DCHECK_GE(value, base_);
205 DCHECK_LT(value - base_, index_to_start_index_.size());
206 return (value - base_).value();
207 }
208
209 IntegerValue GetValue(int index) const { return base_ + IntegerValue(index); }
210
211 IntegerTrail* integer_trail_;
212
213 // These vector will be either sorted by lb or by -ub.
214 std::vector<CachedBounds> bounds_;
215 std::vector<CachedBounds> negated_bounds_;
216
217 // The list of Hall intervalls detected so far, sorted.
218 std::vector<IntegerValue> hall_starts_;
219 std::vector<IntegerValue> hall_ends_;
220
221 // Non-consecutive intervals related data-structures.
222 IntegerValue base_;
223 std::vector<int> index_to_start_index_;
224 std::vector<int> index_to_end_index_;
225 SparseBitset<int> index_is_present_;
226 std::vector<AffineExpression> index_to_expr_;
227
228 // Temporary integer reason.
229 std::vector<IntegerLiteral> integer_reason_;
230};
231
232} // namespace sat
233} // namespace operations_research
234
235#endif // OR_TOOLS_SAT_ALL_DIFFERENT_H_
void RegisterWith(GenericLiteralWatcher *watcher)
AllDifferentBoundsPropagator(const AllDifferentBoundsPropagator &)=delete
This type is neither copyable nor movable.
AllDifferentBoundsPropagator(absl::Span< const AffineExpression > expressions, IntegerTrail *integer_trail)
AllDifferentBoundsPropagator & operator=(const AllDifferentBoundsPropagator &)=delete
AllDifferentConstraint(absl::Span< const IntegerVariable > variables, Model *model)
void RegisterWith(GenericLiteralWatcher *watcher)
std::function< void(Model *)> AllDifferentBinary(absl::Span< const IntegerVariable > vars)
std::function< void(Model *)> AllDifferentOnBounds(absl::Span< const AffineExpression > expressions)
std::function< void(Model *)> AllDifferentAC(absl::Span< const IntegerVariable > variables)
In SWIG mode, we don't want anything besides these top-level includes.