OR-Tools  8.2
encoding.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// Algorithms to encode constraints into their SAT representation. Currently,
15// this contains one possible encoding of a cardinality constraint as used by
16// the core-based optimization algorithm in optimization.h.
17
18#ifndef OR_TOOLS_SAT_ENCODING_H_
19#define OR_TOOLS_SAT_ENCODING_H_
20
21#include <deque>
22#include <vector>
23
27#include "ortools/base/macros.h"
28#include "ortools/sat/boolean_problem.pb.h"
32
33namespace operations_research {
34namespace sat {
35
36// This class represents a number in [0, ub]. The encoding uses ub binary
37// variables x_i with i in [0, ub) where x_i means that the number is > i. It is
38// called an EncodingNode, because it represents one node of the tree used to
39// encode a cardinality constraint.
40//
41// In practice, not all literals are explicitly created:
42// - Only the literals in [lb, current_ub) are "active" at a given time.
43// - The represented number is known to be >= lb.
44// - It may be greater than current_ub, but the extra literals will be only
45// created lazily. In all our solves, the literal current_ub - 1, will always
46// be assumed to false (i.e. the number will be <= current_ub - 1).
47// - Note that lb may increase and ub decrease as more information is learned
48// about this node by the sat solver.
49//
50// This is roughly based on the cardinality constraint encoding described in:
51// Bailleux and Yacine Boufkhad, "Efficient CNF Encoding of Boolean Cardinality
52// Constraints", In Proc. of CP 2003, pages 108-122, 2003.
54 public:
56
57 // Constructs a EncodingNode of size one, just formed by the given literal.
58 explicit EncodingNode(Literal l);
59
60 // Creates a "full" encoding node on n new variables, the represented number
61 // beeing in [lb, ub = lb + n). The variables are added to the given solver
62 // with the basic implications linking them:
63 // literal(0) >= ... >= literal(n-1)
65 SatSolver* solver);
66
67 // Creates a "lazy" encoding node representing the sum of a and b.
68 // Only one literals will be created by this operation. Note that no clauses
69 // linking it with a or b are added by this function.
71
72 // Returns a literal with the meaning 'this node number is > i'.
73 // The given i must be in [lb_, current_ub).
74 Literal GreaterThan(int i) const { return literal(i - lb_); }
75
76 // Accessors to size() and literals in [lb, current_ub).
77 int size() const { return literals_.size(); }
78 Literal literal(int i) const {
79 CHECK_GE(i, 0);
80 CHECK_LT(i, literals_.size());
81 return literals_[i];
82 }
83
84 // Sort by decreasing depth first and then by increasing variable index.
85 // This is meant to be used by the priority queue in MergeAllNodesWithPQ().
86 bool operator<(const EncodingNode& other) const {
87 return depth_ > other.depth_ ||
88 (depth_ == other.depth_ && other.for_sorting_ > for_sorting_);
89 }
90
91 // Creates a new literals and increases current_ub.
92 // Returns false if we were already at the upper bound for this node.
93 bool IncreaseCurrentUB(SatSolver* solver);
94
95 // Removes the left-side literals fixed to 1 and returns the number of
96 // literals removed this way. Note that this increases lb_ and reduces the
97 // number of active literals. It also removes any right-side literals fixed to
98 // 0. If such a literal exists, ub is updated accordingly.
99 int Reduce(const SatSolver& solver);
100
101 // Fix the right-side variables with indices >= to the given upper_bound to
102 // false.
103 void ApplyUpperBound(int64 upper_bound, SatSolver* solver);
104
105 void set_weight(Coefficient w) { weight_ = w; }
106 Coefficient weight() const { return weight_; }
107
108 int depth() const { return depth_; }
109 int lb() const { return lb_; }
110 int current_ub() const { return lb_ + literals_.size(); }
111 int ub() const { return ub_; }
112 EncodingNode* child_a() const { return child_a_; }
113 EncodingNode* child_b() const { return child_b_; }
114
115 private:
116 int depth_;
117 int lb_;
118 int ub_;
119 BooleanVariable for_sorting_;
120
121 Coefficient weight_;
122 EncodingNode* child_a_;
123 EncodingNode* child_b_;
124
125 // The literals of this node in order.
126 std::vector<Literal> literals_;
127};
128
129// Note that we use <= because on 32 bits architecture, the size will actually
130// be smaller than 64 bytes. One exception is with visual studio on windows, in
131// debug mode, where the struct is bigger.
132#if defined(_M_X64) && defined(_DEBUG)
133// In debug, with msvc, std::Vector<T> is 32
134static_assert(sizeof(EncodingNode) == 72,
135 "ERROR_EncodingNode_is_not_well_compacted");
136#else
137// Note that we use <= because on 32 bits architecture, the size will actually
138// be smaller than 64 bytes.
139static_assert(sizeof(EncodingNode) <= 64,
140 "ERROR_EncodingNode_is_not_well_compacted");
141#endif
142
143// Merges the two given EncodingNodes by creating a new node that corresponds to
144// the sum of the two given ones. Only the left-most binary variable is created
145// for the parent node, the other ones will be created later when needed.
146EncodingNode LazyMerge(EncodingNode* a, EncodingNode* b, SatSolver* solver);
147
148// Increases the size of the given node by one. To keep all the needed relations
149// with its children, we also need to increase their size by one, and so on
150// recursively. Also adds all the necessary clauses linking the newly added
151// literals.
152void IncreaseNodeSize(EncodingNode* node, SatSolver* solver);
153
154// Merges the two given EncodingNode by creating a new node that corresponds to
155// the sum of the two given ones. The given upper_bound is interpreted as a
156// bound on this sum, and allows creating fewer binary variables.
157EncodingNode FullMerge(Coefficient upper_bound, EncodingNode* a,
158 EncodingNode* b, SatSolver* solver);
159
160// Merges all the given nodes two by two until there is only one left. Returns
161// the final node which encodes the sum of all the given nodes.
162EncodingNode* MergeAllNodesWithDeque(Coefficient upper_bound,
163 const std::vector<EncodingNode*>& nodes,
164 SatSolver* solver,
165 std::deque<EncodingNode>* repository);
166
167// Same as MergeAllNodesWithDeque() but use a priority queue to merge in
168// priority nodes with smaller sizes.
169EncodingNode* LazyMergeAllNodeWithPQ(const std::vector<EncodingNode*>& nodes,
170 SatSolver* solver,
171 std::deque<EncodingNode>* repository);
172
173// Returns a vector with one new EncodingNode by variable in the given
174// objective. Sets the offset to the negated sum of the negative coefficient,
175// because in this case we negate the literals to have only positive
176// coefficients.
177std::vector<EncodingNode*> CreateInitialEncodingNodes(
178 const std::vector<Literal>& literals,
179 const std::vector<Coefficient>& coeffs, Coefficient* offset,
180 std::deque<EncodingNode>* repository);
181std::vector<EncodingNode*> CreateInitialEncodingNodes(
182 const LinearObjective& objective_proto, Coefficient* offset,
183 std::deque<EncodingNode>* repository);
184
185// Reduces the nodes using the now fixed literals, update the lower-bound, and
186// returns the set of assumptions for the next round of the core-based
187// algorithm. Returns an empty set of assumptions if everything is fixed.
188std::vector<Literal> ReduceNodesAndExtractAssumptions(
189 Coefficient upper_bound, Coefficient stratified_lower_bound,
190 Coefficient* lower_bound, std::vector<EncodingNode*>* nodes,
191 SatSolver* solver);
192
193// Returns the minimum weight of the nodes in the core. Note that the literal in
194// the core must appear in the same order as the one in nodes.
195Coefficient ComputeCoreMinWeight(const std::vector<EncodingNode*>& nodes,
196 const std::vector<Literal>& core);
197
198// Returns the maximum node weight under the given upper_bound. Returns zero if
199// no such weight exist (note that a node weight is strictly positive, so this
200// make sense).
201Coefficient MaxNodeWeightSmallerThan(const std::vector<EncodingNode*>& nodes,
202 Coefficient upper_bound);
203
204// Updates the encoding using the given core. The literals in the core must
205// match the order in nodes.
206void ProcessCore(const std::vector<Literal>& core, Coefficient min_weight,
207 std::deque<EncodingNode>* repository,
208 std::vector<EncodingNode*>* nodes, SatSolver* solver);
209
210} // namespace sat
211} // namespace operations_research
212
213#endif // OR_TOOLS_SAT_ENCODING_H_
#define CHECK_LT(val1, val2)
Definition: base/logging.h:700
#define CHECK_GE(val1, val2)
Definition: base/logging.h:701
int Reduce(const SatSolver &solver)
Definition: encoding.cc:81
bool IncreaseCurrentUB(SatSolver *solver)
Definition: encoding.cc:71
EncodingNode * child_b() const
Definition: encoding.h:113
void InitializeLazyNode(EncodingNode *a, EncodingNode *b, SatSolver *solver)
Definition: encoding.cc:55
void InitializeFullNode(int n, EncodingNode *a, EncodingNode *b, SatSolver *solver)
Definition: encoding.cc:35
Literal literal(int i) const
Definition: encoding.h:78
void ApplyUpperBound(int64 upper_bound, SatSolver *solver)
Definition: encoding.cc:97
EncodingNode * child_a() const
Definition: encoding.h:112
Literal GreaterThan(int i) const
Definition: encoding.h:74
bool operator<(const EncodingNode &other) const
Definition: encoding.h:86
int64_t int64
Coefficient ComputeCoreMinWeight(const std::vector< EncodingNode * > &nodes, const std::vector< Literal > &core)
Definition: encoding.cc:418
EncodingNode * MergeAllNodesWithDeque(Coefficient upper_bound, const std::vector< EncodingNode * > &nodes, SatSolver *solver, std::deque< EncodingNode > *repository)
Definition: encoding.cc:263
std::vector< Literal > ReduceNodesAndExtractAssumptions(Coefficient upper_bound, Coefficient stratified_lower_bound, Coefficient *lower_bound, std::vector< EncodingNode * > *nodes, SatSolver *solver)
Definition: encoding.cc:366
EncodingNode * LazyMergeAllNodeWithPQ(const std::vector< EncodingNode * > &nodes, SatSolver *solver, std::deque< EncodingNode > *repository)
Definition: encoding.cc:285
void IncreaseNodeSize(EncodingNode *node, SatSolver *solver)
Definition: encoding.cc:116
EncodingNode LazyMerge(EncodingNode *a, EncodingNode *b, SatSolver *solver)
Definition: encoding.cc:106
EncodingNode FullMerge(Coefficient upper_bound, EncodingNode *a, EncodingNode *b, SatSolver *solver)
Definition: encoding.cc:212
void ProcessCore(const std::vector< Literal > &core, Coefficient min_weight, std::deque< EncodingNode > *repository, std::vector< EncodingNode * > *nodes, SatSolver *solver)
Definition: encoding.cc:445
Coefficient MaxNodeWeightSmallerThan(const std::vector< EncodingNode * > &nodes, Coefficient upper_bound)
Definition: encoding.cc:433
std::vector< EncodingNode * > CreateInitialEncodingNodes(const std::vector< Literal > &literals, const std::vector< Coefficient > &coeffs, Coefficient *offset, std::deque< EncodingNode > *repository)
Definition: encoding.cc:302
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...