OR-Tools  8.1
circuit.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_CIRCUIT_H_
15 #define OR_TOOLS_SAT_CIRCUIT_H_
16 
17 #include <functional>
18 #include <memory>
19 #include <vector>
20 
21 #include "absl/container/flat_hash_map.h"
22 #include "ortools/base/int_type.h"
24 #include "ortools/base/logging.h"
25 #include "ortools/base/macros.h"
26 #include "ortools/sat/integer.h"
27 #include "ortools/sat/model.h"
28 #include "ortools/sat/sat_base.h"
29 #include "ortools/util/rev.h"
30 
31 namespace operations_research {
32 namespace sat {
33 
34 // Circuit/sub-circuit constraint.
35 //
36 // Nodes that are not in the unique allowed sub-circuit must point to themseves.
37 // A nodes that has no self-arc must thus be inside the sub-circuit. If there is
38 // no self-arc at all, then this constaint forces the circuit to go through all
39 // the nodes. Multi-arcs are NOT supported.
40 //
41 // Important: for correctness, this constraint requires that "exactly one"
42 // constraints have been added for all the incoming (resp. outgoing) arcs of
43 // each node. Also, such constraint must propagate before this one.
45  public:
46  struct Options {
47  // Hack for the VRP to allow for more than one sub-circuit and forces all
48  // the subcircuits to go through the node zero.
50  };
51 
52  // The constraints take a sparse representation of a graph on [0, n). Each arc
53  // being present when the given literal is true.
54  CircuitPropagator(int num_nodes, const std::vector<int>& tails,
55  const std::vector<int>& heads,
56  const std::vector<Literal>& literals, Options options,
57  Model* model);
58 
59  void SetLevel(int level) final;
60  bool Propagate() final;
61  bool IncrementalPropagate(const std::vector<int>& watch_indices) final;
62  void RegisterWith(GenericLiteralWatcher* watcher);
63 
64  private:
65  // Updates the structures when the given arc is added to the paths.
66  void AddArc(int tail, int head, LiteralIndex literal_index);
67 
68  // Clears and fills reason with the literals of the arcs that form a path from
69  // the given node. The path can be a cycle, but in this case it must end at
70  // start (not like a rho shape).
71  void FillReasonForPath(int start_node, std::vector<Literal>* reason) const;
72 
73  const int num_nodes_;
74  const Options options_;
75  Trail* trail_;
76  const VariablesAssignment& assignment_;
77 
78  // We use this to query in O(1) for an arc existence. The self-arcs are
79  // accessed often, so we use a more efficient std::vector<> for them. Note
80  // that we do not add self-arcs to graph_.
81  //
82  // TODO(user): for large dense graph, using a matrix is faster and uses less
83  // memory. If the need arise we can have the two implementations.
84  std::vector<Literal> self_arcs_;
85  absl::flat_hash_map<std::pair<int, int>, Literal> graph_;
86 
87  // Data used to interpret the watch indices passed to IncrementalPropagate().
88  struct Arc {
89  int tail;
90  int head;
91  };
92  std::vector<Literal> watch_index_to_literal_;
93  std::vector<std::vector<Arc>> watch_index_to_arcs_;
94 
95  // Index in trail_ up to which we propagated all the assigned Literals.
96  int propagation_trail_index_ = 0;
97 
98  // Current partial chains of arc that are present.
99  std::vector<int> next_; // -1 if not assigned yet.
100  std::vector<int> prev_; // -1 if not assigned yet.
101  std::vector<LiteralIndex> next_literal_;
102 
103  // Backtrack support for the partial chains of arcs, level_ends_[level] is an
104  // index in added_arcs_;
105  std::vector<int> level_ends_;
106  std::vector<Arc> added_arcs_;
107 
108  // Reversible list of node that must be in a cycle. A node must be in a cycle
109  // iff self_arcs_[node] is false. This graph entry can be used as a reason.
110  int rev_must_be_in_cycle_size_ = 0;
111  std::vector<int> must_be_in_cycle_;
112 
113  // Temporary vectors.
114  std::vector<bool> processed_;
115  std::vector<bool> in_current_path_;
116 
117  DISALLOW_COPY_AND_ASSIGN(CircuitPropagator);
118 };
119 
120 // This constraint ensures that the graph is a covering of all nodes by
121 // circuits and loops, such that all circuits contain exactly one distinguished
122 // node. Those distinguished nodes are meant to be depots.
123 //
124 // This constraint does not need ExactlyOnePerRowAndPerColumn() to be correct,
125 // but it does not propagate degree deductions (only fails if a node has more
126 // than one outgoing arc or more than one incoming arc), so that adding
127 // ExactlyOnePerRowAndPerColumn() should work better.
128 //
129 // TODO(user): Make distinguished nodes an array of Boolean variables,
130 // so this can be used for facility location problems.
132  public:
133  CircuitCoveringPropagator(std::vector<std::vector<Literal>> graph,
134  const std::vector<int>& distinguished_nodes,
135  Model* model);
136 
137  void SetLevel(int level) final;
138  bool Propagate() final;
139  bool IncrementalPropagate(const std::vector<int>& watch_indices) final;
140  void RegisterWith(GenericLiteralWatcher* watcher);
141 
142  private:
143  // Adds all literals on the path/circuit from tail to head in the graph of
144  // literals set to true.
145  // next_[i] should be filled with a node j s.t. graph_[i][j] is true, or -1.
146  void FillFixedPathInReason(int start, int end, std::vector<Literal>* reason);
147 
148  // Input data.
149  const std::vector<std::vector<Literal>> graph_;
150  const int num_nodes_;
151  std::vector<bool> node_is_distinguished_;
152 
153  // SAT incremental state.
154  Trail* trail_;
155  std::vector<std::pair<int, int>> watch_index_to_arc_;
156  std::vector<std::pair<int, int>> fixed_arcs_;
157  std::vector<int> level_ends_;
158 
159  // Used in Propagate() to represent paths and circuits.
160  std::vector<int> next_;
161  std::vector<int> prev_;
162  std::vector<bool> visited_;
163 };
164 
165 // Changes the node indices so that we get a graph in [0, num_nodes) where every
166 // node has at least one incoming or outgoing arc. Returns the number of nodes.
167 template <class IntContainer>
168 int ReindexArcs(IntContainer* tails, IntContainer* heads) {
169  const int num_arcs = tails->size();
170  if (num_arcs == 0) return 0;
171 
172  // Put all nodes in a set.
173  std::set<int> nodes;
174  for (int arc = 0; arc < num_arcs; ++arc) {
175  nodes.insert((*tails)[arc]);
176  nodes.insert((*heads)[arc]);
177  }
178 
179  // Compute the new indices while keeping a stable order.
180  int new_index = 0;
181  absl::flat_hash_map<int, int> mapping;
182  for (const int node : nodes) {
183  mapping[node] = new_index++;
184  }
185 
186  // Remap the arcs.
187  for (int arc = 0; arc < num_arcs; ++arc) {
188  (*tails)[arc] = mapping[(*tails)[arc]];
189  (*heads)[arc] = mapping[(*heads)[arc]];
190  }
191  return nodes.size();
192 }
193 
194 // ============================================================================
195 // Model based functions.
196 // ============================================================================
197 
198 // This just wraps CircuitPropagator. See the comment there to see what this
199 // does. Note that any nodes with no outoing or no incoming arc will cause the
200 // problem to be UNSAT. One can call ReindexArcs() first to ignore such nodes.
201 std::function<void(Model*)> SubcircuitConstraint(
202  int num_nodes, const std::vector<int>& tails, const std::vector<int>& heads,
203  const std::vector<Literal>& literals,
204  bool multiple_subcircuit_through_zero = false);
205 
206 // TODO(user): Change to a sparse API like for the function above.
207 std::function<void(Model*)> ExactlyOnePerRowAndPerColumn(
208  const std::vector<std::vector<Literal>>& graph);
209 std::function<void(Model*)> CircuitCovering(
210  const std::vector<std::vector<Literal>>& graph,
211  const std::vector<int>& distinguished_nodes);
212 
213 } // namespace sat
214 } // namespace operations_research
215 
216 #endif // OR_TOOLS_SAT_CIRCUIT_H_
tail
int64 tail
Definition: routing_flow.cc:127
integral_types.h
operations_research::Arc
std::pair< int64, int64 > Arc
Definition: search.cc:3361
operations_research::sat::CircuitCoveringPropagator::SetLevel
void SetLevel(int level) final
Definition: circuit.cc:340
logging.h
operations_research::sat::PropagatorInterface
Definition: integer.h:1043
operations_research::sat::ExactlyOnePerRowAndPerColumn
std::function< void(Model *)> ExactlyOnePerRowAndPerColumn(const std::vector< std::vector< Literal >> &graph)
Definition: circuit.cc:452
model.h
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
operations_research::sat::CircuitPropagator::IncrementalPropagate
bool IncrementalPropagate(const std::vector< int > &watch_indices) final
Definition: circuit.cc:153
operations_research::sat::CircuitCoveringPropagator::CircuitCoveringPropagator
CircuitCoveringPropagator(std::vector< std::vector< Literal >> graph, const std::vector< int > &distinguished_nodes, Model *model)
Definition: circuit.cc:308
operations_research::sat::CircuitPropagator
Definition: circuit.h:44
sat_base.h
operations_research::sat::GenericLiteralWatcher
Definition: integer.h:1091
operations_research::sat::SubcircuitConstraint
std::function< void(Model *)> SubcircuitConstraint(int num_nodes, const std::vector< int > &tails, const std::vector< int > &heads, const std::vector< Literal > &literals, bool multiple_subcircuit_through_zero)
Definition: circuit.cc:471
operations_research::sat::CircuitPropagator::RegisterWith
void RegisterWith(GenericLiteralWatcher *watcher)
Definition: circuit.cc:92
int_type.h
operations_research::sat::Model
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
operations_research::sat::CircuitCoveringPropagator::Propagate
bool Propagate() final
Definition: circuit.cc:374
operations_research::sat::CircuitCovering
std::function< void(Model *)> CircuitCovering(const std::vector< std::vector< Literal >> &graph, const std::vector< int > &distinguished_nodes)
Definition: circuit.cc:513
rev.h
operations_research::sat::CircuitCoveringPropagator
Definition: circuit.h:131
model
GRBmodel * model
Definition: gurobi_interface.cc:269
operations_research::sat::Literal
Definition: sat_base.h:64
operations_research::sat::CircuitPropagator::SetLevel
void SetLevel(int level) final
Definition: circuit.cc:108
operations_research::ReversibleInterface
Definition: rev.h:29
operations_research::sat::CircuitCoveringPropagator::RegisterWith
void RegisterWith(GenericLiteralWatcher *watcher)
Definition: circuit.cc:320
operations_research::sat::CircuitPropagator::Options::multiple_subcircuit_through_zero
bool multiple_subcircuit_through_zero
Definition: circuit.h:49
operations_research::sat::ReindexArcs
int ReindexArcs(IntContainer *tails, IntContainer *heads)
Definition: circuit.h:168
operations_research::sat::CircuitPropagator::CircuitPropagator
CircuitPropagator(int num_nodes, const std::vector< int > &tails, const std::vector< int > &heads, const std::vector< Literal > &literals, Options options, Model *model)
Definition: circuit.cc:25
operations_research::sat::CircuitPropagator::Options
Definition: circuit.h:46
absl
Definition: cleanup.h:22
operations_research::sat::CircuitPropagator::Propagate
bool Propagate() final
Definition: circuit.cc:197
head
int64 head
Definition: routing_flow.cc:128
operations_research::sat::VariablesAssignment
Definition: sat_base.h:122
operations_research::sat::CircuitCoveringPropagator::IncrementalPropagate
bool IncrementalPropagate(const std::vector< int > &watch_indices) final
Definition: circuit.cc:353
integer.h
operations_research::sat::Trail
Definition: sat_base.h:233