forked from google/or-tools
-
Notifications
You must be signed in to change notification settings - Fork 0
/
probing.h
181 lines (165 loc) · 8.64 KB
/
probing.h
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
// Copyright 2010-2018 Google LLC
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
#ifndef OR_TOOLS_SAT_PROBING_H_
#define OR_TOOLS_SAT_PROBING_H_
#include "absl/types/span.h"
#include "ortools/sat/model.h"
#include "ortools/sat/sat_base.h"
namespace operations_research {
namespace sat {
// Fixes Booleans variables to true/false and see what is propagated. This can:
//
// - Fix some Boolean variables (if we reach a conflict while probing).
//
// - Infer new direct implications. We add them directly to the
// BinaryImplicationGraph and they can later be used to detect equivalent
// literals, expand at most ones clique, etc...
//
// - Tighten the bounds of integer variables. If we probe the two possible
// values of a Boolean (b=0 and b=1), we get for each integer variables two
// propagated domain D_0 and D_1. The level zero domain can then be
// intersected with D_0 U D_1. This can restrict the lower/upper bounds of a
// variable, but it can also create holes in the domain! This will detect
// common cases like an integer variable in [0, 10] that actually only take
// two values [0] or [10] depending on one Boolean.
//
// Returns false if the problem was proved INFEASIBLE during probing.
//
// TODO(user): For now we process the Boolean in their natural order, this is
// not the most efficient.
//
// TODO(user): This might generate a lot of new direct implications. We might
// not want to add them directly to the BinaryImplicationGraph and could instead
// use them directly to detect equivalent literal like in
// ProbeAndFindEquivalentLiteral(). The situation is not clear.
//
// TODO(user): More generally, we might want to register any literal => bound in
// the IntegerEncoder. This would allow to remember them and use them in other
// part of the solver (cuts, lifting, ...).
//
// TODO(user): Rename to include Integer in the name and distinguish better
// from FailedLiteralProbing() below.
bool ProbeBooleanVariables(double deterministic_time_limit, Model* model,
bool log_info = false);
// Same as above method except it probes only on the variables given in
// 'bool_vars'.
bool ProbeBooleanVariables(double deterministic_time_limit,
absl::Span<const BooleanVariable> bool_vars,
Model* model, bool log_info = false);
// Try to randomly tweak the search and stop at the first conflict each time.
// This can sometimes find feasible solution, but more importantly, it is a form
// of probing that can sometimes find small and interesting conflicts or fix
// variables. This seems to work well on the SAT14/app/rook-* problems and
// do fix more variables if run before probing.
//
// If a feasible SAT solution is found (i.e. all Boolean assigned), then this
// abort and leave the solver with the full solution assigned.
//
// Returns false iff the problem is UNSAT.
bool LookForTrivialSatSolution(double deterministic_time_limit, Model* model,
bool log_info = false);
// Options for the FailedLiteralProbing() code below.
//
// A good reference for the algorithms involved here is the paper "Revisiting
// Hyper Binary Resolution" Marijn J. H. Heule, Matti Jarvisalo, Armin Biere,
// http://www.cs.utexas.edu/~marijn/cpaior2013.pdf
struct ProbingOptions {
// The probing will consume all this deterministic time or stop if nothing
// else can be deduced and everything has been probed until fix-point. The
// fix point depend on the extract_binay_clauses option:
// - If false, we will just stop when no more failed literal can be found.
// - If true, we will do more work and stop when all failed literal have been
// found and all hyper binary resolution have been performed.
//
// TODO(user): We can also provide a middle ground and probe all failed
// literal but do not extract all binary clauses.
//
// Note that the fix-point is unique, modulo the equivalent literal detection
// we do. And if we add binary clauses, modulo the transitive reduction of the
// binary implication graph.
//
// To be fast, we only use the binary clauses in the binary implication graph
// for the equivalence detection. So the power of the equivalence detection
// changes if the extract_binay_clauses option is true or not.
//
// TODO(user): The fix point is not yet reached since we don't currently
// simplify non-binary clauses with these equivalence, but we will.
double deterministic_limit = 1.0;
// This is also called hyper binary resolution. Basically, we make sure that
// the binary implication graph is augmented with all the implication of the
// form a => b that can be derived by fixing 'a' at level zero and doing a
// propagation using all constraints. Note that we only add clauses that
// cannot be derived by the current implication graph.
//
// With these extra clause the power of the equivalence literal detection
// using only the binary implication graph with increase. Note that it is
// possible to do exactly the same thing without adding these binary clause
// first. This is what is done by yet another probing algorithm (currently in
// simplification.cc).
//
// TODO(user): Note that adding binary clause before/during the SAT presolve
// is currently not always a good idea. This is because we don't simplify the
// other clause as much as we could. Also, there can be up to a quadratic
// number of clauses added this way, which might slow down things a lot. But
// then because of the deterministic limit, we usually cannot add too much
// clauses, even for huge problems, since we will reach the limit before that.
bool extract_binary_clauses = false;
// Use a version of the "Tree look" algorithm as explained in the paper above.
// This is usually faster and more efficient. Note that when extracting binary
// clauses it might currently produce more "redundant" one in the sense that a
// transitive reduction of the binary implication graph after all hyper binary
// resolution have been performed may need to do more work.
bool use_tree_look = true;
// There is two sligthly different implementation of the tree-look algo.
//
// TODO(user): Decide which one is better, currently the difference seems
// small but the queue seems slightly faster.
bool use_queue = true;
// If we detect as we probe that a new binary clause subsumes one of the
// non-binary clause, we will replace the long clause by the binary one. This
// is orthogonal to the extract_binary_clauses parameters which will add all
// binary clauses but not neceassirly check for subsumption.
bool subsume_with_binary_clause = true;
// We assume this is also true if --v 1 is activated.
bool log_info = false;
std::string ToString() const {
return absl::StrCat("deterministic_limit: ", deterministic_limit,
" extract_binary_clauses: ", extract_binary_clauses,
" use_tree_look: ", use_tree_look,
" use_queue: ", use_queue);
}
};
// Similar to ProbeBooleanVariables() but different :-)
//
// First, this do not consider integer variable. It doesn't do any disjunctive
// reasoning (i.e. changing the domain of an integer variable by intersecting it
// with the union of what happen when x is fixed and not(x) is fixed).
//
// However this should be more efficient and just work better for pure Boolean
// problems. On integer problems, we might also want to run this one first, and
// then do just one quick pass of ProbeBooleanVariables().
//
// Note that this by itself just do one "round", look at the code in the
// Inprocessing class that call this interleaved with other reductions until a
// fix point is reached.
//
// This can fix a lot of literals via failed literal detection, that is when we
// detect that x => not(x) via propagation after taking x as a decision. It also
// use the strongly connected component algorithm to detect equivalent literals.
//
// It will add any detected binary clause (via hyper binary resolution) to
// the implication graph. See the option comments for more details.
bool FailedLiteralProbingRound(ProbingOptions options, Model* model);
} // namespace sat
} // namespace operations_research
#endif // OR_TOOLS_SAT_PROBING_H_