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