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