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_PRESOLVE_CONTEXT_H_ 15 #define OR_TOOLS_SAT_PRESOLVE_CONTEXT_H_ 16 17 #include <cstdint> 18 #include <deque> 19 #include <string> 20 #include <vector> 21 22 #include "absl/base/attributes.h" 23 #include "ortools/sat/cp_model.pb.h" 24 #include "ortools/sat/cp_model_utils.h" 25 #include "ortools/sat/model.h" 26 #include "ortools/sat/presolve_util.h" 27 #include "ortools/sat/sat_parameters.pb.h" 28 #include "ortools/sat/util.h" 29 #include "ortools/util/affine_relation.h" 30 #include "ortools/util/bitset.h" 31 #include "ortools/util/logging.h" 32 #include "ortools/util/sorted_interval_list.h" 33 #include "ortools/util/time_limit.h" 34 35 namespace operations_research { 36 namespace sat { 37 38 // We use some special constraint index in our variable <-> constraint graph. 39 constexpr int kObjectiveConstraint = -1; 40 constexpr int kAffineRelationConstraint = -2; 41 constexpr int kAssumptionsConstraint = -3; 42 43 class PresolveContext; 44 45 // When storing a reference to a literal, it is important not to forget when 46 // reading it back to take its representative. Otherwise, we might introduce 47 // literal that have already been removed, which will break invariants in a 48 // bunch of places. 49 class SavedLiteral { 50 public: SavedLiteral()51 SavedLiteral() {} SavedLiteral(int ref)52 explicit SavedLiteral(int ref) : ref_(ref) {} 53 int Get(PresolveContext* context) const; 54 55 private: 56 int ref_ = 0; 57 }; 58 59 // Same as SavedLiteral for variable. 60 class SavedVariable { 61 public: SavedVariable()62 SavedVariable() {} SavedVariable(int ref)63 explicit SavedVariable(int ref) : ref_(ref) {} 64 int Get(PresolveContext* context) const; 65 66 private: 67 int ref_ = 0; 68 }; 69 70 // Wrap the CpModelProto we are presolving with extra data structure like the 71 // in-memory domain of each variables and the constraint variable graph. 72 class PresolveContext { 73 public: PresolveContext(Model * model,CpModelProto * cp_model,CpModelProto * mapping)74 PresolveContext(Model* model, CpModelProto* cp_model, CpModelProto* mapping) 75 : working_model(cp_model), 76 mapping_model(mapping), 77 logger_(model->GetOrCreate<SolverLogger>()), 78 params_(*model->GetOrCreate<SatParameters>()), 79 time_limit_(model->GetOrCreate<TimeLimit>()), 80 random_(model->GetOrCreate<ModelRandomGenerator>()) {} 81 82 // Helpers to adds new variables to the presolved model. 83 // 84 // TODO(user): We should control more how this is called so we can update 85 // a solution hint accordingly. 86 int NewIntVar(const Domain& domain); 87 int NewBoolVar(); 88 int GetOrCreateConstantVar(int64_t cst); 89 90 // a => b. 91 void AddImplication(int a, int b); 92 93 // b => x in [lb, ub]. 94 void AddImplyInDomain(int b, int x, const Domain& domain); 95 96 // Helpers to query the current domain of a variable. 97 bool DomainIsEmpty(int ref) const; 98 bool IsFixed(int ref) const; 99 bool CanBeUsedAsLiteral(int ref) const; 100 bool LiteralIsTrue(int lit) const; 101 bool LiteralIsFalse(int lit) const; 102 int64_t MinOf(int ref) const; 103 int64_t MaxOf(int ref) const; 104 int64_t FixedValue(int ref) const; 105 bool DomainContains(int ref, int64_t value) const; 106 Domain DomainOf(int ref) const; 107 108 // Helper to query the state of an interval. 109 bool IntervalIsConstant(int ct_ref) const; 110 int64_t StartMin(int ct_ref) const; 111 int64_t StartMax(int ct_ref) const; 112 int64_t SizeMin(int ct_ref) const; 113 int64_t SizeMax(int ct_ref) const; 114 int64_t EndMin(int ct_ref) const; 115 int64_t EndMax(int ct_ref) const; 116 std::string IntervalDebugString(int ct_ref) const; 117 118 // Helpers to query the current domain of a linear expression. 119 // This doesn't check for integer overflow, but our linear expression 120 // should be such that this cannot happen (tested at validation). 121 int64_t MinOf(const LinearExpressionProto& expr) const; 122 int64_t MaxOf(const LinearExpressionProto& expr) const; 123 bool IsFixed(const LinearExpressionProto& expr) const; 124 int64_t FixedValue(const LinearExpressionProto& expr) const; 125 126 // This methods only works for affine expressions (checked). 127 bool DomainContains(const LinearExpressionProto& expr, int64_t value) const; 128 129 // Return a super-set of the domain of the linear expression. 130 Domain DomainSuperSetOf(const LinearExpressionProto& expr) const; 131 132 // Returns true iff the expr is of the form a * literal + b. 133 // The other function can be used to get the literal that achieve MaxOf(). 134 bool ExpressionIsAffineBoolean(const LinearExpressionProto& expr) const; 135 int LiteralForExpressionMax(const LinearExpressionProto& expr) const; 136 137 // Returns true iff the expr is of the form 1 * var + 0. 138 bool ExpressionIsSingleVariable(const LinearExpressionProto& expr) const; 139 140 // Returns true iff the expr is a literal (x or not(x)). 141 bool ExpressionIsALiteral(const LinearExpressionProto& expr, 142 int* literal = nullptr) const; 143 144 // This function takes a positive variable reference. DomainOfVarIsIncludedIn(int var,const Domain & domain)145 bool DomainOfVarIsIncludedIn(int var, const Domain& domain) { 146 return domains[var].IsIncludedIn(domain); 147 } 148 149 // Returns true if a presolve transformation is allowed to remove this 150 // variable. 151 bool VariableIsRemovable(int ref) const; 152 153 // Returns true if this ref only appear in one constraint. 154 bool VariableIsUniqueAndRemovable(int ref) const; 155 156 // Returns true if this ref no longer appears in the model. 157 bool VariableIsNotUsedAnymore(int ref) const; 158 159 // Functions to make sure that once we remove a variable, we no longer reuse 160 // it. 161 void MarkVariableAsRemoved(int ref); 162 bool VariableWasRemoved(int ref) const; 163 164 // Same as VariableIsUniqueAndRemovable() except that in this case the 165 // variable also appear in the objective in addition to a single constraint. 166 bool VariableWithCostIsUnique(int ref) const; 167 bool VariableWithCostIsUniqueAndRemovable(int ref) const; 168 169 // Returns true if an integer variable is only appearing in the rhs of 170 // constraints of the form lit => var in domain. When this is the case, then 171 // we can usually remove this variable and replace these constraints with 172 // the proper constraints on the enforcement literals. 173 bool VariableIsOnlyUsedInEncodingAndMaybeInObjective(int ref) const; 174 175 // Returns false if the new domain is empty. Sets 'domain_modified' (if 176 // provided) to true iff the domain is modified otherwise does not change it. 177 ABSL_MUST_USE_RESULT bool IntersectDomainWith( 178 int ref, const Domain& domain, bool* domain_modified = nullptr); 179 180 // Returns false if the 'lit' doesn't have the desired value in the domain. 181 ABSL_MUST_USE_RESULT bool SetLiteralToFalse(int lit); 182 ABSL_MUST_USE_RESULT bool SetLiteralToTrue(int lit); 183 184 // Same as IntersectDomainWith() but take a linear expression as input. 185 // If this expression if of size > 1, this does nothing for now, so it will 186 // only propagates for constant and affine expression. 187 ABSL_MUST_USE_RESULT bool IntersectDomainWith( 188 const LinearExpressionProto& expr, const Domain& domain, 189 bool* domain_modified = nullptr); 190 191 // This function always return false. It is just a way to make a little bit 192 // more sure that we abort right away when infeasibility is detected. 193 ABSL_MUST_USE_RESULT bool NotifyThatModelIsUnsat( 194 const std::string& message = "") { 195 // TODO(user): Report any explanation for the client in a nicer way? 196 SOLVER_LOG(logger_, "INFEASIBLE: '", message, "'"); 197 DCHECK(!is_unsat_); 198 is_unsat_ = true; 199 return false; 200 } ModelIsUnsat()201 bool ModelIsUnsat() const { return is_unsat_; } 202 203 // Stores a description of a rule that was just applied to have a summary of 204 // what the presolve did at the end. 205 void UpdateRuleStats(const std::string& name, int num_times = 1); 206 207 // Updates the constraints <-> variables graph. This needs to be called each 208 // time a constraint is modified. 209 void UpdateConstraintVariableUsage(int c); 210 211 // At the beginning of the presolve, we delay the costly creation of this 212 // "graph" until we at least ran some basic presolve. This is because during 213 // a LNS neighbhorhood, many constraints will be reduced significantly by 214 // this "simple" presolve. 215 bool ConstraintVariableGraphIsUpToDate() const; 216 217 // Calls UpdateConstraintVariableUsage() on all newly created constraints. 218 void UpdateNewConstraintsVariableUsage(); 219 220 // Returns true if our current constraints <-> variables graph is ok. 221 // This is meant to be used in DEBUG mode only. 222 bool ConstraintVariableUsageIsConsistent(); 223 224 // Regroups fixed variables with the same value. 225 // TODO(user): Also regroup cte and -cte? 226 void ExploitFixedDomain(int var); 227 228 // A "canonical domain" always have a MinOf() equal to zero. 229 // If needed we introduce a new variable with such canonical domain and 230 // add the relation X = Y + offset. 231 // 232 // This is useful in some corner case to avoid overflow. 233 // 234 // TODO(user): When we can always get rid of affine relation, it might be good 235 // to do a final pass to canonicalize all domains in a model after presolve. 236 void CanonicalizeVariable(int ref); 237 238 // Given the relation (X * coeff % mod = rhs % mod), this creates a new 239 // variable so that X = mod * Y + cte. 240 // 241 // This requires mod != 0 and coeff != 0. 242 // 243 // Note that the new variable will have a canonical domain (i.e. min == 0). 244 // We also do not create anything if this fixes the given variable or the 245 // relation simplifies. Returns false if the model is infeasible. 246 bool CanonicalizeAffineVariable(int ref, int64_t coeff, int64_t mod, 247 int64_t rhs); 248 249 // Adds the relation (ref_x = coeff * ref_y + offset) to the repository. 250 // Returns false if we detect infeasability because of this. 251 // 252 // Once the relation is added, it doesn't need to be enforced by a constraint 253 // in the model proto, since we will propagate such relation directly and add 254 // them to the proto at the end of the presolve. 255 // 256 // Note that this should always add a relation, even though it might need to 257 // create a new representative for both ref_x and ref_y in some cases. Like if 258 // x = 3z and y = 5t are already added, if we add x = 2y, we have 3z = 10t and 259 // can only resolve this by creating a new variable r such that z = 10r and t 260 // = 3r. 261 // 262 // All involved variables will be marked to appear in the special 263 // kAffineRelationConstraint. This will allow to identify when a variable is 264 // no longer needed (only appear there and is not a representative). 265 bool StoreAffineRelation(int ref_x, int ref_y, int64_t coeff, int64_t offset, 266 bool debug_no_recursion = false); 267 268 // Adds the fact that ref_a == ref_b using StoreAffineRelation() above. 269 // Returns false if this makes the problem infeasible. 270 bool StoreBooleanEqualityRelation(int ref_a, int ref_b); 271 272 // Stores/Get the relation target_ref = abs(ref); The first function returns 273 // false if it already exist and the second false if it is not present. 274 bool StoreAbsRelation(int target_ref, int ref); 275 bool GetAbsRelation(int target_ref, int* ref); 276 277 // Returns the representative of a literal. 278 int GetLiteralRepresentative(int ref) const; 279 280 // Returns another reference with exactly the same value. 281 int GetVariableRepresentative(int ref) const; 282 283 // Used for statistics. NumAffineRelations()284 int NumAffineRelations() const { return affine_relations_.NumRelations(); } NumEquivRelations()285 int NumEquivRelations() const { return var_equiv_relations_.NumRelations(); } 286 287 // This makes sure that the affine relation only uses one of the 288 // representative from the var_equiv_relations. 289 AffineRelation::Relation GetAffineRelation(int ref) const; 290 291 // To facilitate debugging. 292 std::string RefDebugString(int ref) const; 293 std::string AffineRelationDebugString(int ref) const; 294 295 // Makes sure the domain of ref and of its representative are in sync. 296 // Returns false on unsat. 297 bool PropagateAffineRelation(int ref); 298 299 // Creates the internal structure for any new variables in working_model. 300 void InitializeNewDomains(); 301 302 // Clears the "rules" statistics. 303 void ClearStats(); 304 305 // Inserts the given literal to encode ref == value. 306 // If an encoding already exists, it adds the two implications between 307 // the previous encoding and the new encoding. 308 // 309 // Important: This does not update the constraint<->variable graph, so 310 // ConstraintVariableGraphIsUpToDate() will be false until 311 // UpdateNewConstraintsVariableUsage() is called. 312 // 313 // Returns false if the model become UNSAT. 314 // 315 // TODO(user): This function is not always correct if 316 // !context->DomainOf(ref).contains(value), we could make it correct but it 317 // might be a bit expansive to do so. For now we just have a DCHECK(). 318 bool InsertVarValueEncoding(int literal, int ref, int64_t value); 319 320 // Gets the associated literal if it is already created. Otherwise 321 // create it, add the corresponding constraints and returns it. 322 // 323 // Important: This does not update the constraint<->variable graph, so 324 // ConstraintVariableGraphIsUpToDate() will be false until 325 // UpdateNewConstraintsVariableUsage() is called. 326 int GetOrCreateVarValueEncoding(int ref, int64_t value); 327 328 // Gets the associated literal if it is already created. Otherwise 329 // create it, add the corresponding constraints and returns it. 330 // 331 // Important: This does not update the constraint<->variable graph, so 332 // ConstraintVariableGraphIsUpToDate() will be false until 333 // UpdateNewConstraintsVariableUsage() is called. 334 int GetOrCreateAffineValueEncoding(const LinearExpressionProto& expr, 335 int64_t value); 336 337 // If not already done, adds a Boolean to represent any integer variables that 338 // take only two values. Make sure all the relevant affine and encoding 339 // relations are updated. 340 // 341 // Note that this might create a new Boolean variable. 342 void CanonicalizeDomainOfSizeTwo(int var); 343 344 // Returns true if a literal attached to ref == var exists. 345 // It assigns the corresponding to `literal` if non null. 346 bool HasVarValueEncoding(int ref, int64_t value, int* literal = nullptr); 347 348 // Returns true if we have literal <=> var = value for all values of var. 349 // 350 // TODO(user): If the domain was shrunk, we can have a false positive. 351 // Still it means that the number of values removed is greater than the number 352 // of values not encoded. 353 bool IsFullyEncoded(int ref) const; 354 355 // This methods only works for affine expressions (checked). 356 // It returns true iff the expression is constant or its one variable is full 357 // encoded. 358 bool IsFullyEncoded(const LinearExpressionProto& expr) const; 359 360 // Stores the fact that literal implies var == value. 361 // It returns true if that information is new. 362 bool StoreLiteralImpliesVarEqValue(int literal, int var, int64_t value); 363 364 // Stores the fact that literal implies var != value. 365 // It returns true if that information is new. 366 bool StoreLiteralImpliesVarNEqValue(int literal, int var, int64_t value); 367 368 // Objective handling functions. We load it at the beginning so that during 369 // presolve we can work on the more efficient hash_map representation. 370 // 371 // Note that ReadObjectiveFromProto() makes sure that var_to_constraints of 372 // all the variable that appear in the objective contains -1. This is later 373 // enforced by all the functions modifying the objective. 374 // 375 // Note(user): Because we process affine relation only on 376 // CanonicalizeObjective(), it is possible that when processing a 377 // canonicalized linear constraint, we don't detect that a variable in affine 378 // relation is in the objective. For now this is fine, because when this is 379 // the case, we also have an affine linear constraint, so we can't really do 380 // anything with that variable since it appear in at least two constraints. 381 void ReadObjectiveFromProto(); 382 ABSL_MUST_USE_RESULT bool CanonicalizeObjective(bool simplify_domain = true); 383 void WriteObjectiveToProto() const; 384 ABSL_MUST_USE_RESULT bool ScaleFloatingPointObjective(); 385 386 // Some function need the domain to be up to date in the proto. 387 // This make sures our in-memory domain are writted back to the proto. 388 void WriteVariableDomainsToProto() const; 389 390 // Checks if the given exactly_one is included in the objective, and simplify 391 // the objective by adding a constant value to all the exactly one terms. 392 bool ExploitExactlyOneInObjective(absl::Span<const int> exactly_one); 393 394 // Allows to manipulate the objective coefficients. 395 void RemoveVariableFromObjective(int var); 396 void AddToObjective(int var, int64_t value); 397 void AddToObjectiveOffset(int64_t value); 398 399 // Given a variable defined by the given inequality that also appear in the 400 // objective, remove it from the objective by transferring its cost to other 401 // variables in the equality. 402 // 403 // If new_vars_in_objective is not nullptr, it will be filled with "new" 404 // variables that where not in the objective before and are after 405 // substitution. 406 // 407 // Returns false, if the substitution cannot be done. This is the case if the 408 // model become UNSAT or if doing it will result in an objective that do not 409 // satisfy our overflow preconditions. Note that this can only happen if the 410 // substitued variable is not implied free (i.e. if its domain is smaller than 411 // the implied domain from the equality). 412 ABSL_MUST_USE_RESULT bool SubstituteVariableInObjective( 413 int var_in_equality, int64_t coeff_in_equality, 414 const ConstraintProto& equality, 415 std::vector<int>* new_vars_in_objective = nullptr); 416 417 // Objective getters. ObjectiveDomain()418 const Domain& ObjectiveDomain() const { return objective_domain_; } ObjectiveMap()419 const absl::flat_hash_map<int, int64_t>& ObjectiveMap() const { 420 return objective_map_; 421 } ObjectiveDomainIsConstraining()422 bool ObjectiveDomainIsConstraining() const { 423 return objective_domain_is_constraining_; 424 } 425 426 // Advanced usage. This should be called when a variable can be removed from 427 // the problem, so we don't count it as part of an affine relation anymore. 428 void RemoveVariableFromAffineRelation(int var); 429 void RemoveAllVariablesFromAffineRelationConstraint(); 430 431 // Variable <-> constraint graph. 432 // The vector list is sorted and contains unique elements. 433 // 434 // Important: To properly handle the objective, var_to_constraints[objective] 435 // contains -1 so that if the objective appear in only one constraint, the 436 // constraint cannot be simplified. ConstraintToVars(int c)437 const std::vector<int>& ConstraintToVars(int c) const { 438 DCHECK(ConstraintVariableGraphIsUpToDate()); 439 return constraint_to_vars_[c]; 440 } VarToConstraints(int var)441 const absl::flat_hash_set<int>& VarToConstraints(int var) const { 442 DCHECK(ConstraintVariableGraphIsUpToDate()); 443 return var_to_constraints_[var]; 444 } IntervalUsage(int c)445 int IntervalUsage(int c) const { 446 DCHECK(ConstraintVariableGraphIsUpToDate()); 447 return interval_usage_[c]; 448 } 449 450 // Checks if a constraint contains an enforcement literal set to false, 451 // or if it has been cleared. 452 bool ConstraintIsInactive(int ct_index) const; 453 454 // Checks if a constraint contains an enforcement literal not fixed, and 455 // no enforcement literals set to false. 456 bool ConstraintIsOptional(int ct_ref) const; 457 458 // Make sure we never delete an "assumption" literal by using a special 459 // constraint for that. RegisterVariablesUsedInAssumptions()460 void RegisterVariablesUsedInAssumptions() { 461 for (const int ref : working_model->assumptions()) { 462 var_to_constraints_[PositiveRef(ref)].insert(kAssumptionsConstraint); 463 } 464 } 465 466 // The "expansion" phase should be done once and allow to transform complex 467 // constraints into basic ones (see cp_model_expand.h). Some presolve rules 468 // need to know if the expansion was ran before beeing applied. ModelIsExpanded()469 bool ModelIsExpanded() const { return model_is_expanded_; } NotifyThatModelIsExpanded()470 void NotifyThatModelIsExpanded() { model_is_expanded_ = true; } 471 472 // The following helper adds the following constraint: 473 // result <=> (time_i <= time_j && active_i is true && active_j is true) 474 // and returns the (cached) literal result. 475 // 476 // Note that this cache should just be used temporarily and then cleared 477 // with ClearPrecedenceCache() because there is no mechanism to update the 478 // cached literals when literal equivalence are detected. 479 int GetOrCreateReifiedPrecedenceLiteral(const LinearExpressionProto& time_i, 480 const LinearExpressionProto& time_j, 481 int active_i, int active_j); 482 483 std::tuple<int, int64_t, int, int64_t, int64_t, int, int> 484 GetReifiedPrecedenceKey(const LinearExpressionProto& time_i, 485 const LinearExpressionProto& time_j, int active_i, 486 int active_j); 487 488 // Clear the precedence cache. 489 void ClearPrecedenceCache(); 490 491 // Logs stats to the logger. 492 void LogInfo(); 493 logger()494 SolverLogger* logger() const { return logger_; } params()495 const SatParameters& params() const { return params_; } time_limit()496 TimeLimit* time_limit() { return time_limit_; } random()497 ModelRandomGenerator* random() { return random_; } 498 499 // For each variables, list the constraints that just enforce a lower bound 500 // (resp. upper bound) on that variable. If all the constraints in which a 501 // variable appear are in the same direction, then we can usually fix a 502 // variable to one of its bound (modulo its cost). 503 // 504 // TODO(user): Keeping these extra vector of hash_set seems inefficient. Come 505 // up with a better way to detect if a variable is only constrainted in one 506 // direction. 507 std::vector<absl::flat_hash_set<int>> var_to_ub_only_constraints; 508 std::vector<absl::flat_hash_set<int>> var_to_lb_only_constraints; 509 510 CpModelProto* working_model = nullptr; 511 CpModelProto* mapping_model = nullptr; 512 513 // Indicate if we are allowed to remove irrelevant feasible solution from the 514 // set of feasible solution. For example, if a variable is unused, can we fix 515 // it to an arbitrary value (or its mimimum objective one)? This must be true 516 // if the client wants to enumerate all solutions or wants correct tightened 517 // bounds in the response. 518 bool keep_all_feasible_solutions = false; 519 520 // Number of "rules" applied. This should be equal to the sum of all numbers 521 // in stats_by_rule_name. This is used to decide if we should do one more pass 522 // of the presolve or not. Note that depending on the presolve transformation, 523 // a rule can correspond to a tiny change or a big change. Because of that, 524 // this isn't a perfect proxy for the efficacy of the presolve. 525 int64_t num_presolve_operations = 0; 526 527 // Temporary storage. 528 std::vector<int> tmp_literals; 529 std::vector<Domain> tmp_term_domains; 530 std::vector<Domain> tmp_left_domains; 531 absl::flat_hash_set<int> tmp_literal_set; 532 533 // Each time a domain is modified this is set to true. 534 SparseBitset<int64_t> modified_domains; 535 536 // Advanced presolve. See this class comment. 537 DomainDeductions deductions; 538 539 private: 540 // Helper to add an affine relation x = c.y + o to the given repository. 541 bool AddRelation(int x, int y, int64_t c, int64_t o, AffineRelation* repo); 542 543 void AddVariableUsage(int c); 544 void UpdateLinear1Usage(const ConstraintProto& ct, int c); 545 546 // Returns true iff the variable is not the representative of an equivalence 547 // class of size at least 2. 548 bool VariableIsNotRepresentativeOfEquivalenceClass(int var) const; 549 550 // Makes sure we only insert encoding about the current representative. 551 // 552 // Returns false if ref cannot take the given value (it might not have been 553 // propagated yet). 554 bool CanonicalizeEncoding(int* ref, int64_t* value); 555 556 // Inserts an half reified var value encoding (literal => var ==/!= value). 557 // It returns true if the new state is different from the old state. 558 // Not that if imply_eq is false, the literal will be stored in its negated 559 // form. 560 // 561 // Thus, if you detect literal <=> var == value, then two calls must be made: 562 // InsertHalfVarValueEncoding(literal, var, value, true); 563 // InsertHalfVarValueEncoding(NegatedRef(literal), var, value, false); 564 bool InsertHalfVarValueEncoding(int literal, int var, int64_t value, 565 bool imply_eq); 566 567 // Insert fully reified var-value encoding. 568 void InsertVarValueEncodingInternal(int literal, int var, int64_t value, 569 bool add_constraints); 570 571 SolverLogger* logger_; 572 const SatParameters& params_; 573 TimeLimit* time_limit_; 574 ModelRandomGenerator* random_; 575 576 // Initially false, and set to true on the first inconsistency. 577 bool is_unsat_ = false; 578 579 // The current domain of each variables. 580 std::vector<Domain> domains; 581 582 // Internal representation of the objective. During presolve, we first load 583 // the objective in this format in order to have more efficient substitution 584 // on large problems (also because the objective is often dense). At the end 585 // we re-convert it to its proto form. 586 absl::flat_hash_map<int, int64_t> objective_map_; 587 int64_t objective_overflow_detection_; 588 std::vector<std::pair<int, int64_t>> tmp_entries_; 589 bool objective_domain_is_constraining_ = false; 590 Domain objective_domain_; 591 double objective_offset_; 592 double objective_scaling_factor_; 593 int64_t objective_integer_offset_; 594 int64_t objective_integer_scaling_factor_; 595 596 // Constraints <-> Variables graph. 597 std::vector<std::vector<int>> constraint_to_vars_; 598 std::vector<absl::flat_hash_set<int>> var_to_constraints_; 599 600 // Number of constraints of the form [lit =>] var in domain. 601 std::vector<int> constraint_to_linear1_var_; 602 std::vector<int> var_to_num_linear1_; 603 604 // We maintain how many time each interval is used. 605 std::vector<std::vector<int>> constraint_to_intervals_; 606 std::vector<int> interval_usage_; 607 608 // Contains abs relation (key = abs(saved_variable)). 609 absl::flat_hash_map<int, SavedVariable> abs_relations_; 610 611 // For each constant variable appearing in the model, we maintain a reference 612 // variable with the same constant value. If two variables end up having the 613 // same fixed value, then we can detect it using this and add a new 614 // equivalence relation. See ExploitFixedDomain(). 615 absl::flat_hash_map<int64_t, SavedVariable> constant_to_ref_; 616 617 // Contains variables with some encoded value: encoding_[i][v] points 618 // to the literal attached to the value v of the variable i. 619 absl::flat_hash_map<int, absl::flat_hash_map<int64_t, SavedLiteral>> 620 encoding_; 621 622 // Contains the currently collected half value encodings: 623 // i.e.: literal => var ==/!= value 624 // The state is accumulated (adding x => var == value then !x => var != value) 625 // will deduce that x equivalent to var == value. 626 absl::flat_hash_map<int, 627 absl::flat_hash_map<int64_t, absl::flat_hash_set<int>>> 628 eq_half_encoding_; 629 absl::flat_hash_map<int, 630 absl::flat_hash_map<int64_t, absl::flat_hash_set<int>>> 631 neq_half_encoding_; 632 633 // This regroups all the affine relations between variables. Note that the 634 // constraints used to detect such relations will not be removed from the 635 // model at detection time (thus allowing proper domain propagation). However, 636 // if the arity of a variable becomes one, then such constraint will be 637 // removed. 638 AffineRelation affine_relations_; 639 AffineRelation var_equiv_relations_; 640 641 std::vector<int> tmp_new_usage_; 642 643 // Used by SetVariableAsRemoved() and VariableWasRemoved(). 644 absl::flat_hash_set<int> removed_variables_; 645 646 // Cache for the reified precedence literals created during the expansion of 647 // the reservoir constraint. This cache is only valid during the expansion 648 // phase, and is cleared afterwards. 649 absl::flat_hash_map<std::tuple<int, int64_t, int, int64_t, int64_t, int, int>, 650 int> 651 reified_precedences_cache_; 652 653 // Just used to display statistics on the presolve rules that were used. 654 absl::flat_hash_map<std::string, int> stats_by_rule_name_; 655 656 bool model_is_expanded_ = false; 657 }; 658 659 // Utility function to load the current problem into a in-memory representation 660 // that will be used for probing. Returns false if UNSAT. 661 bool LoadModelForProbing(PresolveContext* context, Model* local_model); 662 663 } // namespace sat 664 } // namespace operations_research 665 666 #endif // OR_TOOLS_SAT_PRESOLVE_CONTEXT_H_ 667