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