OR-Tools  8.2
sat_inprocessing.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// This file contains the entry point for our presolve/inprocessing code.
15//
16// TODO(user): for now it is mainly presolve, but the idea is to call these
17// function during the search so they should be as incremental as possible. That
18// is avoid doing work that is not useful because nothing changed or exploring
19// parts that were not done during the last round.
20
21#ifndef OR_TOOLS_SAT_SAT_INPROCESSING_H_
22#define OR_TOOLS_SAT_SAT_INPROCESSING_H_
23
25#include "ortools/sat/clause.h"
26#include "ortools/sat/model.h"
30#include "ortools/sat/util.h"
33
34namespace operations_research {
35namespace sat {
36
37// The order is important and each clauses has a "special" literal that is
38// put first.
39//
40// TODO(user): Use a flat memory structure instead.
42 // Utility function that push back clause but also make sure the given literal
43 // from clause appear first.
45 absl::Span<const Literal> clause);
46
47 std::deque<std::vector<Literal>> clauses;
48};
49
53
55 // The time budget to spend.
57
58 // We assume this is also true if --v 1 is activated and we actually log
59 // even more in --v 1.
60 bool log_info = false;
61
62 // See ProbingOptions in probing.h
64
65 // Whether we perform a transitive reduction of the binary implication graph
66 // after equivalent literal detection and before each probing pass.
67 //
68 // TODO(user): Doing that before the current SAT presolve also change the
69 // possible reduction. This shouldn't matter if we use the binary implication
70 // graph and its reachability instead of just binary clause though.
72};
73
74// We need to keep some information from one call to the next, so we use a
75// class. Note that as this becomes big, we can probably split it.
76//
77// TODO(user): Some algorithms here use the normal SAT propagation engine.
78// However we might want to temporarily disable activities/phase saving and so
79// on if we want to run them as in-processing steps so that they
80// do not "pollute" the normal SAT search.
81//
82// TODO(user): For the propagation, this depends on the SatSolver class, which
83// mean we cannot really use it without some refactoring as an in-processing
84// from the SatSolver::Solve() function. So we do need a special
85// InprocessingSolve() that lives outside SatSolver. Alternatively, we can
86// extract the propagation main loop and conflict analysis from SatSolver.
88 public:
90 : assignment_(model->GetOrCreate<Trail>()->Assignment()),
91 implication_graph_(model->GetOrCreate<BinaryImplicationGraph>()),
92 clause_manager_(model->GetOrCreate<LiteralWatchers>()),
93 trail_(model->GetOrCreate<Trail>()),
94 decision_policy_(model->GetOrCreate<SatDecisionPolicy>()),
95 time_limit_(model->GetOrCreate<TimeLimit>()),
96 sat_solver_(model->GetOrCreate<SatSolver>()),
97 stamping_simplifier_(model->GetOrCreate<StampingSimplifier>()),
98 blocked_clause_simplifier_(
99 model->GetOrCreate<BlockedClauseSimplifier>()),
100 bounded_variable_elimination_(
101 model->GetOrCreate<BoundedVariableElimination>()),
102 model_(model) {}
103
104 // Does some simplifications until a fix point is reached or the given
105 // deterministic time is passed.
106 bool PresolveLoop(SatPresolveOptions options);
107
108 // When the option use_sat_inprocessing is true, then this is called at each
109 // restart. It is up to the heuristics here to decide what inprocessing we
110 // do or if we wait for the next call before doing anything.
111 bool InprocessingRound();
112
113 // Simple wrapper that makes sure all the clauses are attached before a
114 // propagation is performed.
115 bool LevelZeroPropagate();
116
117 // Detects equivalences in the implication graph and propagates any failed
118 // literal found during the process.
119 bool DetectEquivalencesAndStamp(bool use_transitive_reduction, bool log_info);
120
121 // Removes fixed variables and exploit equivalence relations to cleanup the
122 // clauses. Returns false if UNSAT.
123 bool RemoveFixedAndEquivalentVariables(bool log_info);
124
125 // Returns true if there is new fixed variables or new equivalence relations
126 // since RemoveFixedAndEquivalentVariables() was last called.
127 bool MoreFixedVariableToClean() const;
128 bool MoreRedundantVariableToClean() const;
129
130 // Processes all clauses and see if there is any subsumption/strenghtening
131 // reductions that can be performed. Returns false if UNSAT.
132 bool SubsumeAndStrenghtenRound(bool log_info);
133
134 private:
135 const VariablesAssignment& assignment_;
136 BinaryImplicationGraph* implication_graph_;
137 LiteralWatchers* clause_manager_;
138 Trail* trail_;
139 SatDecisionPolicy* decision_policy_;
140 TimeLimit* time_limit_;
141 SatSolver* sat_solver_;
142 StampingSimplifier* stamping_simplifier_;
143 BlockedClauseSimplifier* blocked_clause_simplifier_;
144 BoundedVariableElimination* bounded_variable_elimination_;
145
146 double total_dtime_ = 0.0;
147
148 // TODO(user): This is only used for calling probing. We should probably
149 // create a Probing class to wraps its data. This will also be needed to not
150 // always probe the same variables in each round if the deterministic time
151 // limit is low.
152 Model* model_;
153
154 // Last since clause database was cleaned up.
155 int64 last_num_redundant_literals_ = 0;
156 int64 last_num_fixed_variables_ = 0;
157};
158
159// Implements "stamping" as described in "Efficient CNF Simplification based on
160// Binary Implication Graphs", Marijn Heule, Matti Jarvisalo and Armin Biere.
161//
162// This sample the implications graph with a spanning tree, and then simplify
163// all clauses (subsumption / strengthening) using the implications encoded in
164// this tree. So this allows to consider chain of implications instead of just
165// direct ones, but depending on the problem, only a small fraction of the
166// implication graph will be captured by the tree.
167//
168// Note that we randomize the spanning tree at each call. This can benefit by
169// having the implication graph be transitively reduced before.
171 public:
173 : assignment_(model->GetOrCreate<Trail>()->Assignment()),
174 implication_graph_(model->GetOrCreate<BinaryImplicationGraph>()),
175 clause_manager_(model->GetOrCreate<LiteralWatchers>()),
176 random_(model->GetOrCreate<ModelRandomGenerator>()),
177 time_limit_(model->GetOrCreate<TimeLimit>()) {}
178
179 // This is "fast" (linear scan + sort of all clauses) so we always complete
180 // the full round.
181 //
182 // TODO(user): To save one scan over all the clauses, we could do the fixed
183 // and equivalence variable cleaning here too.
184 bool DoOneRound(bool log_info);
185
186 // When we compute stamps, we might detect fixed variable (via failed literal
187 // probing in the implication graph). So it might make sense to do that until
188 // we have dealt with all fixed literals before calling DoOneRound().
189 bool ComputeStampsForNextRound(bool log_info);
190
191 // Visible for testing.
193
194 // Using a DFS visiting order, we can answer reachability query in O(1) on a
195 // tree, this is well known. ComputeStamps() also detect failed literal in
196 // the tree and fix them. It can return false on UNSAT.
197 bool ComputeStamps();
199 return first_stamps_[a.Index()] < first_stamps_[b.Index()] &&
200 last_stamps_[b.Index()] < last_stamps_[a.Index()];
201 }
202
203 bool ProcessClauses();
204
205 private:
206 const VariablesAssignment& assignment_;
207 BinaryImplicationGraph* implication_graph_;
208 LiteralWatchers* clause_manager_;
209 ModelRandomGenerator* random_;
210 TimeLimit* time_limit_;
211
212 // For ComputeStampsForNextRound().
213 bool stamps_are_already_computed_ = false;
214
215 // Reset at each round.
216 double dtime_ = 0.0;
217 int64 num_subsumed_clauses_ = 0;
218 int64 num_removed_literals_ = 0;
219 int64 num_fixed_ = 0;
220
221 // Encode a spanning tree of the implication graph.
223
224 // Adjacency list representation of the parents_ tree.
227 std::vector<LiteralIndex> children_;
228
229 // Temporary data for the DFS.
231 std::vector<LiteralIndex> dfs_stack_;
232
233 // First/Last visited index in a DFS of the tree above.
236};
237
238// A clause c is "blocked" by a literal l if all clauses containing the
239// negation of l resolve to trivial clause with c. Blocked clause can be
240// simply removed from the problem. At postsolve, if a blocked clause is not
241// satisfied, then l can simply be set to true without breaking any of the
242// clause containing not(l).
243//
244// See the paper "Blocked Clause Elimination", Matti Jarvisalo, Armin Biere,
245// and Marijn Heule.
246//
247// TODO(user): This requires that l only appear in clauses and not in the
248// integer part of CP-SAT.
250 public:
252 : assignment_(model->GetOrCreate<Trail>()->Assignment()),
253 implication_graph_(model->GetOrCreate<BinaryImplicationGraph>()),
254 clause_manager_(model->GetOrCreate<LiteralWatchers>()),
255 postsolve_(model->GetOrCreate<PostsolveClauses>()),
256 time_limit_(model->GetOrCreate<TimeLimit>()) {}
257
258 void DoOneRound(bool log_info);
259
260 private:
261 void InitializeForNewRound();
262 void ProcessLiteral(Literal current_literal);
263 bool ClauseIsBlocked(Literal current_literal,
264 absl::Span<const Literal> clause);
265
266 const VariablesAssignment& assignment_;
267 BinaryImplicationGraph* implication_graph_;
268 LiteralWatchers* clause_manager_;
269 PostsolveClauses* postsolve_;
270 TimeLimit* time_limit_;
271
272 double dtime_ = 0.0;
273 int32 num_blocked_clauses_ = 0;
274 int64 num_inspected_literals_ = 0;
275
276 // Temporary vector to mark literal of a clause.
278
279 // List of literal to process.
280 // TODO(user): use priority queue?
282 std::deque<Literal> queue_;
283
284 // We compute the occurrence graph just once at the beginning of each round
285 // and we do not shrink it as we remove blocked clauses.
286 DEFINE_INT_TYPE(ClauseIndex, int32);
289 literal_to_clauses_;
290};
291
293 public:
295 : parameters_(*model->GetOrCreate<SatParameters>()),
296 assignment_(model->GetOrCreate<Trail>()->Assignment()),
297 implication_graph_(model->GetOrCreate<BinaryImplicationGraph>()),
298 clause_manager_(model->GetOrCreate<LiteralWatchers>()),
299 postsolve_(model->GetOrCreate<PostsolveClauses>()),
300 trail_(model->GetOrCreate<Trail>()),
301 time_limit_(model->GetOrCreate<TimeLimit>()) {}
302
303 bool DoOneRound(bool log_info);
304
305 private:
306 int NumClausesContaining(Literal l);
307 void UpdatePriorityQueue(BooleanVariable var);
308 bool CrossProduct(BooleanVariable var);
309 void DeleteClause(SatClause* sat_clause);
310 void DeleteAllClausesContaining(Literal literal);
311 void AddClause(absl::Span<const Literal> clause);
312 bool RemoveLiteralFromClause(Literal lit, SatClause* sat_clause);
313 bool Propagate();
314
315 // The actual clause elimination algo. We have two versions, one just compute
316 // the "score" of what will be the final state. The other perform the
317 // resolution, remove old clauses and add the new ones.
318 //
319 // Returns false on UNSAT.
320 template <bool score_only, bool with_binary_only>
321 bool ResolveAllClauseContaining(Literal lit);
322
323 const SatParameters& parameters_;
324 const VariablesAssignment& assignment_;
325 BinaryImplicationGraph* implication_graph_;
326 LiteralWatchers* clause_manager_;
327 PostsolveClauses* postsolve_;
328 Trail* trail_;
329 TimeLimit* time_limit_;
330
331 int propagation_index_;
332
333 double dtime_ = 0.0;
334 int64 num_inspected_literals_ = 0;
335 int64 num_simplifications_ = 0;
336 int64 num_blocked_clauses_ = 0;
337 int64 num_eliminated_variables_ = 0;
338 int64 num_literals_diff_ = 0;
339 int64 num_clauses_diff_ = 0;
340
341 int64 new_score_;
342 int64 score_threshold_;
343
344 // Temporary vector to mark literal of a clause and compute its resolvant.
346 std::vector<Literal> resolvant_;
347
348 // Priority queue of variable to process.
349 // We will process highest priority first.
350 struct VariableWithPriority {
351 BooleanVariable var;
352 int32 priority;
353
354 // Interface for the IntegerPriorityQueue.
355 int Index() const { return var.value(); }
356 bool operator<(const VariableWithPriority& o) const {
357 return priority < o.priority;
358 }
359 };
360 IntegerPriorityQueue<VariableWithPriority> queue_;
361
362 // We update the queue_ in batch.
363 absl::StrongVector<BooleanVariable, bool> in_need_to_be_updated_;
364 std::vector<BooleanVariable> need_to_be_updated_;
365
366 // We compute the occurrence graph just once at the beginning of each round.
367 // We maintains the sizes at all time and lazily shrink the graph with deleted
368 // clauses.
369 DEFINE_INT_TYPE(ClauseIndex, int32);
372 literal_to_clauses_;
373 absl::StrongVector<LiteralIndex, int> literal_to_num_clauses_;
374};
375
376} // namespace sat
377} // namespace operations_research
378
379#endif // OR_TOOLS_SAT_SAT_INPROCESSING_H_
An Assignment is a variable -> domains mapping, used to report solutions to the user.
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
Definition: time_limit.h:105
bool PresolveLoop(SatPresolveOptions options)
bool RemoveFixedAndEquivalentVariables(bool log_info)
bool DetectEquivalencesAndStamp(bool use_transitive_reduction, bool log_info)
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
bool ImplicationIsInTree(Literal a, Literal b) const
IntVar * var
Definition: expr_array.cc:1858
GRBmodel * model
int int32
int64_t int64
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Literal literal
Definition: optimization.cc:84
std::deque< std::vector< Literal > > clauses
void AddClauseWithSpecialLiteral(Literal literal, absl::Span< const Literal > clause)