OR-Tools  8.1
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"
26 #include "ortools/sat/sat_base.h"
27 
28 namespace operations_research {
29 namespace 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.
34 std::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.
45 std::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.
58 std::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;
69  void RegisterWith(GenericLiteralWatcher* watcher);
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_
operations_research::sat::AllDifferentConstraint::Propagate
bool Propagate() final
Definition: all_different.cc:237
var
IntVar * var
Definition: expr_array.cc:1858
operations_research::sat::AllDifferentBoundsPropagator::RegisterWith
void RegisterWith(GenericLiteralWatcher *watcher)
Definition: all_different.cc:635
integral_types.h
DCHECK_LT
#define DCHECK_LT(val1, val2)
Definition: base/logging.h:888
operations_research::sat::IntegerTrail
Definition: integer.h:533
operations_research::sat::kNoIntegerVariable
const IntegerVariable kNoIntegerVariable(-1)
operations_research::sat::AllDifferentConstraint::RegisterWith
void RegisterWith(GenericLiteralWatcher *watcher)
Definition: all_different.cc:148
operations_research::sat::AllDifferentAC
std::function< void(Model *)> AllDifferentAC(const std::vector< IntegerVariable > &variables)
Definition: all_different.cc:76
operations_research::sat::PropagatorInterface
Definition: integer.h:1043
value
int64 value
Definition: demon_profiler.cc:43
model.h
operations_research::sat::AllDifferentBoundsPropagator::Propagate
bool Propagate() final
Definition: all_different.cc:435
macros.h
operations_research
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Definition: dense_doubly_linked_list.h:21
int64
int64_t int64
Definition: integral_types.h:34
index
int index
Definition: pack.cc:508
sat_base.h
operations_research::sat::GenericLiteralWatcher
Definition: integer.h:1091
operations_research::sat::AllDifferentBoundsPropagator::AllDifferentBoundsPropagator
AllDifferentBoundsPropagator(const std::vector< IntegerVariable > &vars, IntegerTrail *integer_trail)
Definition: all_different.cc:418
operations_research::sat::AllDifferentOnBounds
std::function< void(Model *)> AllDifferentOnBounds(const std::vector< IntegerVariable > &vars)
Definition: all_different.cc:65
DCHECK_GE
#define DCHECK_GE(val1, val2)
Definition: base/logging.h:889
operations_research::sat::AllDifferentBinary
std::function< void(Model *)> AllDifferentBinary(const std::vector< IntegerVariable > &vars)
Definition: all_different.cc:31
operations_research::sat::AllDifferentBoundsPropagator
Definition: all_different.h:147
operations_research::sat::AllDifferentConstraint::AllDifferentConstraint
AllDifferentConstraint(std::vector< IntegerVariable > variables, IntegerEncoder *encoder, Trail *trail, IntegerTrail *integer_trail)
Definition: all_different.cc:89
operations_research::sat::IntegerEncoder
Definition: integer.h:276
integer.h
operations_research::sat::Trail
Definition: sat_base.h:233
operations_research::sat::AllDifferentConstraint
Definition: all_different.h:62