OR-Tools  8.2
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"
25#include "ortools/base/macros.h"
26#include "ortools/sat/integer.h"
27#include "ortools/sat/model.h"
29#include "ortools/util/rev.h"
30
31namespace operations_research {
32namespace 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;
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.
167template <class IntContainer>
168int 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.
201std::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.
207std::function<void(Model*)> ExactlyOnePerRowAndPerColumn(
208 const std::vector<std::vector<Literal>>& graph);
209std::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_
CircuitCoveringPropagator(std::vector< std::vector< Literal > > graph, const std::vector< int > &distinguished_nodes, Model *model)
Definition: circuit.cc:308
bool IncrementalPropagate(const std::vector< int > &watch_indices) final
Definition: circuit.cc:353
void RegisterWith(GenericLiteralWatcher *watcher)
Definition: circuit.cc:320
bool IncrementalPropagate(const std::vector< int > &watch_indices) final
Definition: circuit.cc:153
void RegisterWith(GenericLiteralWatcher *watcher)
Definition: circuit.cc:92
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
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
GRBmodel * model
Definition: cleanup.h:22
int ReindexArcs(IntContainer *tails, IntContainer *heads)
Definition: circuit.h:168
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
std::function< void(Model *)> CircuitCovering(const std::vector< std::vector< Literal > > &graph, const std::vector< int > &distinguished_nodes)
Definition: circuit.cc:513
std::function< void(Model *)> ExactlyOnePerRowAndPerColumn(const std::vector< std::vector< Literal > > &graph)
Definition: circuit.cc:452
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
std::pair< int64, int64 > Arc
Definition: search.cc:3361
STL namespace.
int64 tail
int64 head