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"
27 #include "ortools/sat/sat_base.h"
29 #include "ortools/sat/sat_solver.h"
30 #include "ortools/sat/util.h"
33 
34 namespace operations_research {
35 namespace 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 
50 class StampingSimplifier;
53 
55  // The time budget to spend.
56  double deterministic_time_limit = 30.0;
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.
87 class Inprocessing {
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)