OR-Tools  8.1
presolve_util.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 #ifndef OR_TOOLS_SAT_PRESOLVE_UTIL_H_
15 #define OR_TOOLS_SAT_PRESOLVE_UTIL_H_
16 
17 #include <algorithm>
18 #include <vector>
19 
20 #include "absl/container/flat_hash_map.h"
21 #include "ortools/base/int_type.h"
23 #include "ortools/base/logging.h"
27 #include "ortools/util/bitset.h"
29 
30 namespace operations_research {
31 namespace sat {
32 
33 // If for each literal of a clause, we can infer a domain on an integer
34 // variable, then we know that this variable domain is included in the union of
35 // such infered domains.
36 //
37 // This allows to propagate "element" like constraints encoded as enforced
38 // linear relations, and other more general reasoning.
39 //
40 // TODO(user): Also use these "deductions" in the solver directly. This is done
41 // in good MIP solvers, and we should exploit them more.
42 //
43 // TODO(user): Also propagate implicit clauses (lit, not(lit)). Maybe merge
44 // that with probing code? it might be costly to store all deduction done by
45 // probing though, but I think this is what MIP solver do.
47  public:
48  // Adds the fact that enforcement => var \in domain.
49  //
50  // Important: No need to store any deductions where the domain is a superset
51  // of the current variable domain.
52  void AddDeduction(int literal_ref, int var, Domain domain);
53 
54  // Returns list of (var, domain) that were deduced because:
55  // 1/ We have a domain deduction for var and all literal from the clause
56  // 2/ So we can take the union of all the deduced domains.
57  //
58  // TODO(user): We could probably be even more efficient. We could also
59  // compute exactly what clauses need to be "waked up" as new deductions are
60  // added.
61  std::vector<std::pair<int, Domain>> ProcessClause(
62  absl::Span<const int> clause);
63 
64  // Optimization. Any following ProcessClause() will be fast if no more
65  // deduction touching that clause are added.
67  something_changed_.ClearAndResize(something_changed_.size());
68  }
69 
70  // Returns the total number of "deductions" stored by this class.
71  int NumDeductions() const { return deductions_.size(); }
72 
73  private:
74  DEFINE_INT_TYPE(Index, int);
75  Index IndexFromLiteral(int ref) {
76  return Index(ref >= 0 ? 2 * ref : -2 * ref - 1);
77  }
78 
79  std::vector<int> tmp_num_occurrences_;
80 
81  SparseBitset<Index> something_changed_;
82  absl::StrongVector<Index, std::vector<int>> enforcement_to_vars_;
83  absl::flat_hash_map<std::pair<Index, int>, Domain> deductions_;
84 };
85 
86 // Replaces the variable var in ct using the definition constraint.
87 // Currently the coefficient in the definition must be 1 or -1.
88 void SubstituteVariable(int var, int64 var_coeff_in_definition,
89  const ConstraintProto& definition, ConstraintProto* ct);
90 
91 } // namespace sat
92 } // namespace operations_research
93 
94 #endif // OR_TOOLS_SAT_PRESOLVE_UTIL_H_
var
IntVar * var
Definition: expr_array.cc:1858
integral_types.h
operations_research::sat::SubstituteVariable
void SubstituteVariable(int var, int64 var_coeff_in_definition, const ConstraintProto &definition, ConstraintProto *ct)
Definition: presolve_util.cc:182
operations_research::SparseBitset::size
IntegerType size() const
Definition: bitset.h:771
cp_model.pb.h
operations_research::SparseBitset::ClearAndResize
void ClearAndResize(IntegerType size)
Definition: bitset.h:780
operations_research::sat::DomainDeductions::MarkProcessingAsDoneForNow
void MarkProcessingAsDoneForNow()
Definition: presolve_util.h:66
operations_research::sat::DomainDeductions::NumDeductions
int NumDeductions() const
Definition: presolve_util.h:71
logging.h
operations_research::sat::DomainDeductions
Definition: presolve_util.h:46
operations_research
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Definition: dense_doubly_linked_list.h:21
operations_research::sat::DomainDeductions::AddDeduction
void AddDeduction(int literal_ref, int var, Domain domain)
Definition: presolve_util.cc:22
operations_research::Domain
We call domain any subset of Int64 = [kint64min, kint64max].
Definition: sorted_interval_list.h:81
int64
int64_t int64
Definition: integral_types.h:34
operations_research::SparseBitset< Index >
int_type.h
ct
const Constraint * ct
Definition: demon_profiler.cc:42
sorted_interval_list.h
absl::StrongVector
Definition: strong_vector.h:76
strong_vector.h
operations_research::glop::Index
int32 Index
Definition: lp_types.h:37
bitset.h
operations_research::sat::DomainDeductions::ProcessClause
std::vector< std::pair< int, Domain > > ProcessClause(absl::Span< const int > clause)
Definition: presolve_util.cc:47
cp_model_utils.h