OR-Tools  8.2
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"
25#include "ortools/sat/cp_model.pb.h"
27#include "ortools/util/bitset.h"
29
30namespace operations_research {
31namespace 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_;
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.
88void 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_
We call domain any subset of Int64 = [kint64min, kint64max].
IntegerType size() const
Definition: bitset.h:769
void ClearAndResize(IntegerType size)
Definition: bitset.h:778
std::vector< std::pair< int, Domain > > ProcessClause(absl::Span< const int > clause)
void AddDeduction(int literal_ref, int var, Domain domain)
const Constraint * ct
IntVar * var
Definition: expr_array.cc:1858
int64_t int64
void SubstituteVariable(int var, int64 var_coeff_in_definition, const ConstraintProto &definition, ConstraintProto *ct)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...