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