OR-Tools  8.2
simplification.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// Implementation of a pure SAT presolver. This roughly follows the paper:
15//
16// "Effective Preprocessing in SAT through Variable and Clause Elimination",
17// Niklas Een and Armin Biere, published in the SAT 2005 proceedings.
18
19#ifndef OR_TOOLS_SAT_SIMPLIFICATION_H_
20#define OR_TOOLS_SAT_SIMPLIFICATION_H_
21
22#include <deque>
23#include <memory>
24#include <set>
25#include <vector>
26
27#include "absl/types/span.h"
31#include "ortools/base/macros.h"
35#include "ortools/sat/sat_parameters.pb.h"
38
39namespace operations_research {
40namespace sat {
41
42// A simple sat postsolver.
43//
44// The idea is that any presolve algorithm can just update this class, and at
45// the end, this class will recover a solution of the initial problem from a
46// solution of the presolved problem.
48 public:
49 explicit SatPostsolver(int num_variables);
50
51 // The postsolver will process the Add() calls in reverse order. If the given
52 // clause has all its literals at false, it simply sets the literal x to true.
53 // Note that x must be a literal of the given clause.
54 void Add(Literal x, const absl::Span<const Literal> clause);
55
56 // Tells the postsolver that the given literal must be true in any solution.
57 // We currently check that the variable is not already fixed.
58 //
59 // TODO(user): this as almost the same effect as adding an unit clause, and we
60 // should probably remove this to simplify the code.
61 void FixVariable(Literal x);
62
63 // This assumes that the given variable mapping has been applied to the
64 // problem. All the subsequent Add() and FixVariable() will refer to the new
65 // problem. During postsolve, the initial solution must also correspond to
66 // this new problem. Note that if mapping[v] == -1, then the literal v is
67 // assumed to be deleted.
68 //
69 // This can be called more than once. But each call must refer to the current
70 // variables set (after all the previous mapping have been applied).
71 void ApplyMapping(
73
74 // Extracts the current assignment of the given solver and postsolve it.
75 //
76 // Node(fdid): This can currently be called only once (but this is easy to
77 // change since only some CHECK will fail).
78 std::vector<bool> ExtractAndPostsolveSolution(const SatSolver& solver);
79 std::vector<bool> PostsolveSolution(const std::vector<bool>& solution);
80
81 // Getters to the clauses managed by this class.
82 // Important: This will always put the associated literal first.
83 int NumClauses() const { return clauses_start_.size(); }
84 std::vector<Literal> Clause(int i) const {
85 // TODO(user): we could avoid the copy here, but because clauses_literals_
86 // is a deque, we do need a special return class and cannot juste use
87 // absl::Span<Literal> for instance.
88 const int begin = clauses_start_[i];
89 const int end = i + 1 < clauses_start_.size() ? clauses_start_[i + 1]
90 : clauses_literals_.size();
91 std::vector<Literal> result(clauses_literals_.begin() + begin,
92 clauses_literals_.begin() + end);
93 for (int j = 0; j < result.size(); ++j) {
94 if (result[j] == associated_literal_[i]) {
95 std::swap(result[0], result[j]);
96 break;
97 }
98 }
99 return result;
100 }
101
102 private:
103 Literal ApplyReverseMapping(Literal l);
104 void Postsolve(VariablesAssignment* assignment) const;
105
106 // The presolve can add new variables, so we need to store the number of
107 // original variables in order to return a solution with the correct number
108 // of variables.
109 const int initial_num_variables_;
110 int num_variables_;
111
112 // Stores the arguments of the Add() calls: clauses_start_[i] is the index of
113 // the first literal of the clause #i in the clauses_literals_ deque.
114 std::vector<int> clauses_start_;
115 std::deque<Literal> clauses_literals_;
116 std::vector<Literal> associated_literal_;
117
118 // All the added clauses will be mapped back to the initial variables using
119 // this reverse mapping. This way, clauses_ and associated_literal_ are only
120 // in term of the initial problem.
122
123 // This will stores the fixed variables value and later the postsolved
124 // assignment.
125 VariablesAssignment assignment_;
126
127 DISALLOW_COPY_AND_ASSIGN(SatPostsolver);
128};
129
130// This class holds a SAT problem (i.e. a set of clauses) and the logic to
131// presolve it by a series of subsumption, self-subsuming resolution, and
132// variable elimination by clause distribution.
133//
134// Note that this does propagate unit-clauses, but probably much
135// less efficiently than the propagation code in the SAT solver. So it is better
136// to use a SAT solver to fix variables before using this class.
137//
138// TODO(user): Interact more with a SAT solver to reuse its propagation logic.
139//
140// TODO(user): Forbid the removal of some variables. This way we can presolve
141// only the clause part of a general Boolean problem by not removing variables
142// appearing in pseudo-Boolean constraints.
144 public:
145 // TODO(user): use IntType!
147
148 explicit SatPresolver(SatPostsolver* postsolver)
149 : postsolver_(postsolver),
150 num_trivial_clauses_(0),
151 drat_proof_handler_(nullptr) {}
152
153 void SetParameters(const SatParameters& params) { parameters_ = params; }
154 void SetTimeLimit(TimeLimit* time_limit) { time_limit_ = time_limit; }
155
156 // Registers a mapping to encode equivalent literals.
157 // See ProbeAndFindEquivalentLiteral().
160 equiv_mapping_ = mapping;
161 }
162
163 // Adds new clause to the SatPresolver.
164 void SetNumVariables(int num_variables);
166 void AddClause(absl::Span<const Literal> clause);
167
168 // Presolves the problem currently loaded. Returns false if the model is
169 // proven to be UNSAT during the presolving.
170 //
171 // TODO(user): Add support for a time limit and some kind of iterations limit
172 // so that this can never take too much time.
173 bool Presolve();
174
175 // Same as Presolve() but only allow to remove BooleanVariable whose index
176 // is set to true in the given vector.
177 bool Presolve(const std::vector<bool>& var_that_can_be_removed,
178 bool log_info = false);
179
180 // All the clauses managed by this class.
181 // Note that deleted clauses keep their indices (they are just empty).
182 int NumClauses() const { return clauses_.size(); }
183 const std::vector<Literal>& Clause(ClauseIndex ci) const {
184 return clauses_[ci];
185 }
186
187 // The number of variables. This is computed automatically from the clauses
188 // added to the SatPresolver.
189 int NumVariables() const { return literal_to_clause_sizes_.size() / 2; }
190
191 // After presolving, Some variables in [0, NumVariables()) have no longer any
192 // clause pointing to them. This return a mapping that maps this interval to
193 // [0, new_size) such that now all variables are used. The unused variable
194 // will be mapped to BooleanVariable(-1).
196
197 // Loads the current presolved problem in to the given sat solver.
198 // Note that the variables will be re-indexed according to the mapping given
199 // by GetMapping() so that they form a dense set.
200 //
201 // IMPORTANT: This is not const because it deletes the presolver clauses as
202 // they are added to the SatSolver in order to save memory. After this is
203 // called, only VariableMapping() will still works.
205
206 // Visible for Testing. Takes a given clause index and looks for clause that
207 // can be subsumed or strengthened using this clause. Returns false if the
208 // model is proven to be unsat.
210
211 // Visible for testing. Tries to eliminate x by clause distribution.
212 // This is also known as bounded variable elimination.
213 //
214 // It is always possible to remove x by resolving each clause containing x
215 // with all the clauses containing not(x). Hence the cross-product name. Note
216 // that this function only do that if the number of clauses is reduced.
217 bool CrossProduct(Literal x);
218
219 // Visible for testing. Just applies the BVA step of the presolve.
220 void PresolveWithBva();
221
222 void SetDratProofHandler(DratProofHandler* drat_proof_handler) {
223 drat_proof_handler_ = drat_proof_handler;
224 }
225
226 private:
227 // Internal function used by ProcessClauseToSimplifyOthers().
228 bool ProcessClauseToSimplifyOthersUsingLiteral(ClauseIndex clause_index,
229 Literal lit);
230
231 // Internal function to add clauses generated during the presolve. The clause
232 // must already be sorted with the default Literal order and will be cleared
233 // after this call.
234 void AddClauseInternal(std::vector<Literal>* clause);
235
236 // Clause removal function.
237 void Remove(ClauseIndex ci);
238 void RemoveAndRegisterForPostsolve(ClauseIndex ci, Literal x);
239 void RemoveAndRegisterForPostsolveAllClauseContaining(Literal x);
240
241 // Call ProcessClauseToSimplifyOthers() on all the clauses in
242 // clause_to_process_ and empty the list afterwards. Note that while some
243 // clauses are processed, new ones may be added to the list. Returns false if
244 // the problem is shown to be UNSAT.
245 bool ProcessAllClauses();
246
247 // Finds the literal from the clause that occur the less in the clause
248 // database.
249 Literal FindLiteralWithShortestOccurrenceList(
250 const std::vector<Literal>& clause);
251 LiteralIndex FindLiteralWithShortestOccurrenceListExcluding(
252 const std::vector<Literal>& clause, Literal to_exclude);
253
254 // Tests and maybe perform a Simple Bounded Variable addition starting from
255 // the given literal as described in the paper: "Automated Reencoding of
256 // Boolean Formulas", Norbert Manthey, Marijn J. H. Heule, and Armin Biere,
257 // Volume 7857 of the series Lecture Notes in Computer Science pp 102-117,
258 // 2013.
259 // https://www.research.ibm.com/haifa/conferences/hvc2012/papers/paper16.pdf
260 //
261 // This seems to have a mostly positive effect, except on the crafted problem
262 // familly mugrauer_balint--GI.crafted_nxx_d6_cx_numxx where the reduction
263 // is big, but apparently the problem is harder to prove UNSAT for the solver.
264 void SimpleBva(LiteralIndex l);
265
266 // Display some statistics on the current clause database.
267 void DisplayStats(double elapsed_seconds);
268
269 // Returns a hash of the given clause variables (not literal) in such a way
270 // that hash1 & not(hash2) == 0 iff the set of variable of clause 1 is a
271 // subset of the one of clause2.
272 uint64 ComputeSignatureOfClauseVariables(ClauseIndex ci);
273
274 // The "active" variables on which we want to call CrossProduct() are kept
275 // in a priority queue so that we process first the ones that occur the least
276 // often in the clause database.
277 void InitializePriorityQueue();
278 void UpdatePriorityQueue(BooleanVariable var);
279 struct PQElement {
280 PQElement() : heap_index(-1), variable(-1), weight(0.0) {}
281
282 // Interface for the AdjustablePriorityQueue.
283 void SetHeapIndex(int h) { heap_index = h; }
284 int GetHeapIndex() const { return heap_index; }
285
286 // Priority order. The AdjustablePriorityQueue returns the largest element
287 // first, but our weight goes this other way around (smaller is better).
288 bool operator<(const PQElement& other) const {
289 return weight > other.weight;
290 }
291
292 int heap_index;
293 BooleanVariable variable;
294 double weight;
295 };
298
299 // Literal priority queue for BVA. The literals are ordered by descending
300 // number of occurrences in clauses.
301 void InitializeBvaPriorityQueue();
302 void UpdateBvaPriorityQueue(LiteralIndex lit);
303 void AddToBvaPriorityQueue(LiteralIndex lit);
304 struct BvaPqElement {
305 BvaPqElement() : heap_index(-1), literal(-1), weight(0.0) {}
306
307 // Interface for the AdjustablePriorityQueue.
308 void SetHeapIndex(int h) { heap_index = h; }
309 int GetHeapIndex() const { return heap_index; }
310
311 // Priority order.
312 // The AdjustablePriorityQueue returns the largest element first.
313 bool operator<(const BvaPqElement& other) const {
314 return weight < other.weight;
315 }
316
317 int heap_index;
318 LiteralIndex literal;
319 double weight;
320 };
321 std::deque<BvaPqElement> bva_pq_elements_; // deque because we add variables.
323
324 // Temporary data for SimpleBva().
325 std::set<LiteralIndex> m_lit_;
326 std::vector<ClauseIndex> m_cls_;
327 absl::StrongVector<LiteralIndex, int> literal_to_p_size_;
328 std::vector<std::pair<LiteralIndex, ClauseIndex>> flattened_p_;
329 std::vector<Literal> tmp_new_clause_;
330
331 // List of clauses on which we need to call ProcessClauseToSimplifyOthers().
332 // See ProcessAllClauses().
333 std::vector<bool> in_clause_to_process_;
334 std::deque<ClauseIndex> clause_to_process_;
335
336 // The set of all clauses.
337 // An empty clause means that it has been removed.
338 std::vector<std::vector<Literal>> clauses_; // Indexed by ClauseIndex
339
340 // The cached value of ComputeSignatureOfClauseVariables() for each clause.
341 std::vector<uint64> signatures_; // Indexed by ClauseIndex
342 int64 num_inspected_signatures_ = 0;
343 int64 num_inspected_literals_ = 0;
344
345 // Occurrence list. For each literal, contains the ClauseIndex of the clause
346 // that contains it (ordered by clause index).
348 literal_to_clauses_;
349
350 // Because we only lazily clean the occurrence list after clause deletions,
351 // we keep the size of the occurrence list (without the deleted clause) here.
352 absl::StrongVector<LiteralIndex, int> literal_to_clause_sizes_;
353
354 // Used for postsolve.
355 SatPostsolver* postsolver_;
356
357 // Equivalent literal mapping.
359
360 int num_trivial_clauses_;
361 SatParameters parameters_;
362 DratProofHandler* drat_proof_handler_;
363 TimeLimit* time_limit_ = nullptr;
364
365 DISALLOW_COPY_AND_ASSIGN(SatPresolver);
366};
367
368// Visible for testing. Returns true iff:
369// - a subsume b (subsumption): the clause a is a subset of b, in which case
370// opposite_literal is set to -1.
371// - b is strengthened by self-subsumption using a (self-subsuming resolution):
372// the clause a with one of its literal negated is a subset of b, in which
373// case opposite_literal is set to this negated literal index. Moreover, this
374// opposite_literal is then removed from b.
375//
376// If num_inspected_literals_ is not nullptr, the "complexity" of this function
377// will be added to it in order to track the amount of work done.
378//
379// TODO(user): when a.size() << b.size(), we should use binary search instead
380// of scanning b linearly.
381bool SimplifyClause(const std::vector<Literal>& a, std::vector<Literal>* b,
382 LiteralIndex* opposite_literal,
383 int64* num_inspected_literals = nullptr);
384
385// Visible for testing. Returns kNoLiteralIndex except if:
386// - a and b differ in only one literal.
387// - For a it is the given literal l.
388// In which case, returns the LiteralIndex of the literal in b that is not in a.
389LiteralIndex DifferAtGivenLiteral(const std::vector<Literal>& a,
390 const std::vector<Literal>& b, Literal l);
391
392// Visible for testing. Computes the resolvant of 'a' and 'b' obtained by
393// performing the resolution on 'x'. If the resolvant is trivially true this
394// returns false, otherwise it returns true and fill 'out' with the resolvant.
395//
396// Note that the resolvant is just 'a' union 'b' with the literals 'x' and
397// not(x) removed. The two clauses are assumed to be sorted, and the computed
398// resolvant will also be sorted.
399//
400// This is the basic operation when a variable is eliminated by clause
401// distribution.
402bool ComputeResolvant(Literal x, const std::vector<Literal>& a,
403 const std::vector<Literal>& b, std::vector<Literal>* out);
404
405// Same as ComputeResolvant() but just returns the resolvant size.
406// Returns -1 when ComputeResolvant() returns false.
407int ComputeResolvantSize(Literal x, const std::vector<Literal>& a,
408 const std::vector<Literal>& b);
409
410// Presolver that does literals probing and finds equivalent literals by
411// computing the strongly connected components of the graph:
412// literal l -> literals propagated by l.
413//
414// Clears the mapping if there are no equivalent literals. Otherwise, mapping[l]
415// is the representative of the equivalent class of l. Note that mapping[l] may
416// be equal to l.
417//
418// The postsolver will be updated so it can recover a solution of the mapped
419// problem. Note that this works on any problem the SatSolver can handle, not
420// only pure SAT problem, but the returned mapping do need to be applied to all
421// constraints.
423 SatSolver* solver, SatPostsolver* postsolver,
424 DratProofHandler* drat_proof_handler,
426
427// Given a 'solver' with a problem already loaded, this will try to simplify the
428// problem (i.e. presolve it) before calling solver->Solve(). In the process,
429// because of the way the presolve is implemented, the underlying SatSolver may
430// change (it is why we use this unique_ptr interface). In particular, the final
431// variables and 'solver' state may have nothing to do with the problem
432// originaly present in the solver. That said, if the problem is shown to be
433// SAT, then the returned solution will be in term of the original variables.
434//
435// Note that the full presolve is only executed if the problem is a pure SAT
436// problem with only clauses.
438 std::unique_ptr<SatSolver>* solver, TimeLimit* time_limit,
439 std::vector<bool>* solution /* only filled if SAT */,
440 DratProofHandler* drat_proof_handler /* can be nullptr */);
441
442} // namespace sat
443} // namespace operations_research
444
445#endif // OR_TOOLS_SAT_SIMPLIFICATION_H_
size_type size() const
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
Definition: time_limit.h:105
void Add(Literal x, const absl::Span< const Literal > clause)
void ApplyMapping(const absl::StrongVector< BooleanVariable, BooleanVariable > &mapping)
std::vector< bool > PostsolveSolution(const std::vector< bool > &solution)
std::vector< Literal > Clause(int i) const
std::vector< bool > ExtractAndPostsolveSolution(const SatSolver &solver)
void SetNumVariables(int num_variables)
const std::vector< Literal > & Clause(ClauseIndex ci) const
void LoadProblemIntoSatSolver(SatSolver *solver)
void AddBinaryClause(Literal a, Literal b)
void SetEquivalentLiteralMapping(const absl::StrongVector< LiteralIndex, LiteralIndex > &mapping)
void SetParameters(const SatParameters &params)
absl::StrongVector< BooleanVariable, BooleanVariable > VariableMapping() const
void SetDratProofHandler(DratProofHandler *drat_proof_handler)
void AddClause(absl::Span< const Literal > clause)
bool ProcessClauseToSimplifyOthers(ClauseIndex clause_index)
void SetTimeLimit(TimeLimit *time_limit)
SatPresolver(SatPostsolver *postsolver)
SharedTimeLimit * time_limit
IntVar * var
Definition: expr_array.cc:1858
int int32
int64_t int64
uint64_t uint64
int ComputeResolvantSize(Literal x, const std::vector< Literal > &a, const std::vector< Literal > &b)
SatSolver::Status SolveWithPresolve(std::unique_ptr< SatSolver > *solver, TimeLimit *time_limit, std::vector< bool > *solution, DratProofHandler *drat_proof_handler)
LiteralIndex DifferAtGivenLiteral(const std::vector< Literal > &a, const std::vector< Literal > &b, Literal l)
bool ComputeResolvant(Literal x, const std::vector< Literal > &a, const std::vector< Literal > &b, std::vector< Literal > *out)
void ProbeAndFindEquivalentLiteral(SatSolver *solver, SatPostsolver *postsolver, DratProofHandler *drat_proof_handler, absl::StrongVector< LiteralIndex, LiteralIndex > *mapping)
bool SimplifyClause(const std::vector< Literal > &a, std::vector< Literal > *b, LiteralIndex *opposite_literal, int64 *num_inspected_literals)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Literal literal
Definition: optimization.cc:84
int64 weight
Definition: pack.cc:509