OR-Tools  8.2
probing.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_PROBING_H_
15#define OR_TOOLS_SAT_PROBING_H_
16
17#include "absl/types/span.h"
18#include "ortools/sat/clause.h"
20#include "ortools/sat/integer.h"
21#include "ortools/sat/model.h"
23#include "ortools/sat/util.h"
24
25namespace operations_research {
26namespace sat {
27
28class Prober {
29 public:
30 explicit Prober(Model* model);
31
32 // Fixes Booleans variables to true/false and see what is propagated. This
33 // can:
34 //
35 // - Fix some Boolean variables (if we reach a conflict while probing).
36 //
37 // - Infer new direct implications. We add them directly to the
38 // BinaryImplicationGraph and they can later be used to detect equivalent
39 // literals, expand at most ones clique, etc...
40 //
41 // - Tighten the bounds of integer variables. If we probe the two possible
42 // values of a Boolean (b=0 and b=1), we get for each integer variables two
43 // propagated domain D_0 and D_1. The level zero domain can then be
44 // intersected with D_0 U D_1. This can restrict the lower/upper bounds of a
45 // variable, but it can also create holes in the domain! This will detect
46 // common cases like an integer variable in [0, 10] that actually only take
47 // two values [0] or [10] depending on one Boolean.
48 //
49 // Returns false if the problem was proved INFEASIBLE during probing.
50 //
51 // TODO(user): For now we process the Boolean in their natural order, this is
52 // not the most efficient.
53 //
54 // TODO(user): This might generate a lot of new direct implications. We might
55 // not want to add them directly to the BinaryImplicationGraph and could
56 // instead use them directly to detect equivalent literal like in
57 // ProbeAndFindEquivalentLiteral(). The situation is not clear.
58 //
59 // TODO(user): More generally, we might want to register any literal => bound
60 // in the IntegerEncoder. This would allow to remember them and use them in
61 // other part of the solver (cuts, lifting, ...).
62 //
63 // TODO(user): Rename to include Integer in the name and distinguish better
64 // from FailedLiteralProbing() below.
65 bool ProbeBooleanVariables(double deterministic_time_limit,
66 bool log_info = false);
67
68 // Same as above method except it probes only on the variables given in
69 // 'bool_vars'.
70 bool ProbeBooleanVariables(double deterministic_time_limit,
71 absl::Span<const BooleanVariable> bool_vars,
72 bool log_info = false);
73
74 bool ProbeOneVariable(BooleanVariable b);
75
76 private:
77 bool ProbeOneVariableInternal(BooleanVariable b);
78
79 // Model owned classes.
80 const Trail& trail_;
81 const VariablesAssignment& assignment_;
82 IntegerTrail* integer_trail_;
83 ImpliedBounds* implied_bounds_;
84 SatSolver* sat_solver_;
85 TimeLimit* time_limit_;
86 BinaryImplicationGraph* implication_graph_;
87
88 // To detect literal x that must be true because b => x and not(b) => x.
89 // When probing b, we add all propagated literal to propagated, and when
90 // probing not(b) we check if any are already there.
92
93 // Modifications found during probing.
94 std::vector<Literal> to_fix_at_true_;
95 std::vector<IntegerLiteral> new_integer_bounds_;
96 std::vector<std::pair<Literal, Literal>> new_binary_clauses_;
97
98 // Probing statistics.
99 int num_new_holes_ = 0;
100 int num_new_binary_ = 0;
101 int num_new_integer_bounds_ = 0;
102};
103
104// Try to randomly tweak the search and stop at the first conflict each time.
105// This can sometimes find feasible solution, but more importantly, it is a form
106// of probing that can sometimes find small and interesting conflicts or fix
107// variables. This seems to work well on the SAT14/app/rook-* problems and
108// do fix more variables if run before probing.
109//
110// If a feasible SAT solution is found (i.e. all Boolean assigned), then this
111// abort and leave the solver with the full solution assigned.
112//
113// Returns false iff the problem is UNSAT.
114bool LookForTrivialSatSolution(double deterministic_time_limit, Model* model,
115 bool log_info = false);
116
117// Options for the FailedLiteralProbing() code below.
118//
119// A good reference for the algorithms involved here is the paper "Revisiting
120// Hyper Binary Resolution" Marijn J. H. Heule, Matti Jarvisalo, Armin Biere,
121// http://www.cs.utexas.edu/~marijn/cpaior2013.pdf
123 // The probing will consume all this deterministic time or stop if nothing
124 // else can be deduced and everything has been probed until fix-point. The
125 // fix point depend on the extract_binay_clauses option:
126 // - If false, we will just stop when no more failed literal can be found.
127 // - If true, we will do more work and stop when all failed literal have been
128 // found and all hyper binary resolution have been performed.
129 //
130 // TODO(user): We can also provide a middle ground and probe all failed
131 // literal but do not extract all binary clauses.
132 //
133 // Note that the fix-point is unique, modulo the equivalent literal detection
134 // we do. And if we add binary clauses, modulo the transitive reduction of the
135 // binary implication graph.
136 //
137 // To be fast, we only use the binary clauses in the binary implication graph
138 // for the equivalence detection. So the power of the equivalence detection
139 // changes if the extract_binay_clauses option is true or not.
140 //
141 // TODO(user): The fix point is not yet reached since we don't currently
142 // simplify non-binary clauses with these equivalence, but we will.
144
145 // This is also called hyper binary resolution. Basically, we make sure that
146 // the binary implication graph is augmented with all the implication of the
147 // form a => b that can be derived by fixing 'a' at level zero and doing a
148 // propagation using all constraints. Note that we only add clauses that
149 // cannot be derived by the current implication graph.
150 //
151 // With these extra clause the power of the equivalence literal detection
152 // using only the binary implication graph with increase. Note that it is
153 // possible to do exactly the same thing without adding these binary clause
154 // first. This is what is done by yet another probing algorithm (currently in
155 // simplification.cc).
156 //
157 // TODO(user): Note that adding binary clause before/during the SAT presolve
158 // is currently not always a good idea. This is because we don't simplify the
159 // other clause as much as we could. Also, there can be up to a quadratic
160 // number of clauses added this way, which might slow down things a lot. But
161 // then because of the deterministic limit, we usually cannot add too much
162 // clauses, even for huge problems, since we will reach the limit before that.
164
165 // Use a version of the "Tree look" algorithm as explained in the paper above.
166 // This is usually faster and more efficient. Note that when extracting binary
167 // clauses it might currently produce more "redundant" one in the sense that a
168 // transitive reduction of the binary implication graph after all hyper binary
169 // resolution have been performed may need to do more work.
170 bool use_tree_look = true;
171
172 // There is two sligthly different implementation of the tree-look algo.
173 //
174 // TODO(user): Decide which one is better, currently the difference seems
175 // small but the queue seems slightly faster.
176 bool use_queue = true;
177
178 // If we detect as we probe that a new binary clause subsumes one of the
179 // non-binary clause, we will replace the long clause by the binary one. This
180 // is orthogonal to the extract_binary_clauses parameters which will add all
181 // binary clauses but not neceassirly check for subsumption.
183
184 // We assume this is also true if --v 1 is activated.
185 bool log_info = false;
186
187 std::string ToString() const {
188 return absl::StrCat("deterministic_limit: ", deterministic_limit,
189 " extract_binary_clauses: ", extract_binary_clauses,
190 " use_tree_look: ", use_tree_look,
191 " use_queue: ", use_queue);
192 }
193};
194
195// Similar to ProbeBooleanVariables() but different :-)
196//
197// First, this do not consider integer variable. It doesn't do any disjunctive
198// reasoning (i.e. changing the domain of an integer variable by intersecting
199// it with the union of what happen when x is fixed and not(x) is fixed).
200//
201// However this should be more efficient and just work better for pure Boolean
202// problems. On integer problems, we might also want to run this one first,
203// and then do just one quick pass of ProbeBooleanVariables().
204//
205// Note that this by itself just do one "round", look at the code in the
206// Inprocessing class that call this interleaved with other reductions until a
207// fix point is reached.
208//
209// This can fix a lot of literals via failed literal detection, that is when
210// we detect that x => not(x) via propagation after taking x as a decision. It
211// also use the strongly connected component algorithm to detect equivalent
212// literals.
213//
214// It will add any detected binary clause (via hyper binary resolution) to
215// the implication graph. See the option comments for more details.
216bool FailedLiteralProbingRound(ProbingOptions options, Model* model);
217
218} // namespace sat
219} // namespace operations_research
220
221#endif // OR_TOOLS_SAT_PROBING_H_
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
Definition: time_limit.h:105
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
bool ProbeOneVariable(BooleanVariable b)
Definition: probing.cc:179
bool ProbeBooleanVariables(double deterministic_time_limit, bool log_info=false)
Definition: probing.cc:41
GRBmodel * model
bool LookForTrivialSatSolution(double deterministic_time_limit, Model *model, bool log_info)
Definition: probing.cc:270
bool FailedLiteralProbingRound(ProbingOptions options, Model *model)
Definition: probing.cc:350
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...