1 /* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */ 2 /* */ 3 /* This file is part of the program and library */ 4 /* SCIP --- Solving Constraint Integer Programs */ 5 /* */ 6 /* Copyright (C) 2002-2022 Konrad-Zuse-Zentrum */ 7 /* fuer Informationstechnik Berlin */ 8 /* */ 9 /* SCIP is distributed under the terms of the ZIB Academic License. */ 10 /* */ 11 /* You should have received a copy of the ZIB Academic License */ 12 /* along with SCIP; see the file COPYING. If not visit scipopt.org. */ 13 /* */ 14 /* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */ 15 16 /**@file conflict_graphanalysis.h 17 * @ingroup OTHER_CFILES 18 * @brief methods and datastructures for conflict analysis 19 * @author Tobias Achterberg 20 * @author Timo Berthold 21 * @author Stefan Heinz 22 * @author Marc Pfetsch 23 * @author Michael Winkler 24 * @author Jakob Witzig 25 * 26 * This file implements a conflict analysis method like the one used in modern 27 * SAT solvers like zchaff. The algorithm works as follows: 28 * 29 * Given is a set of bound changes that are not allowed being applied simultaneously, because they 30 * render the current node infeasible (e.g. because a single constraint is infeasible in the these 31 * bounds, or because the LP relaxation is infeasible). The goal is to deduce a clause on variables 32 * -- a conflict clause -- representing the "reason" for this conflict, i.e., the branching decisions 33 * or the deductions (applied e.g. in domain propagation) that lead to the conflict. This clause can 34 * then be added to the constraint set to help cutting off similar parts of the branch and bound 35 * tree, that would lead to the same conflict. A conflict clause can also be generated, if the 36 * conflict was detected by a locally valid constraint. In this case, the resulting conflict clause 37 * is also locally valid in the same depth as the conflict detecting constraint. If all involved 38 * variables are binary, a linear (set covering) constraint can be generated, otherwise a bound 39 * disjunction constraint is generated. Details are given in 40 * 41 * Tobias Achterberg, Conflict Analysis in Mixed Integer Programming@n 42 * Discrete Optimization, 4, 4-20 (2007) 43 * 44 * See also @ref CONF. Here is an outline of the algorithm: 45 * 46 * -# Put all the given bound changes to a priority queue, which is ordered, 47 * such that the bound change that was applied last due to branching or deduction 48 * is at the top of the queue. The variables in the queue are always active 49 * problem variables. Because binary variables are preferred over general integer 50 * variables, integer variables are put on the priority queue prior to the binary 51 * variables. Create an empty conflict set. 52 * -# Remove the top bound change b from the priority queue. 53 * -# Perform the following case distinction: 54 * -# If the remaining queue is non-empty, and bound change b' (the one that is now 55 * on the top of the queue) was applied at the same depth level as b, and if 56 * b was a deduction with known inference reason, and if the inference constraint's 57 * valid depth is smaller or equal to the conflict detecting constraint's valid 58 * depth: 59 * - Resolve bound change b by asking the constraint that inferred the 60 * bound change to put all the bound changes on the priority queue, that 61 * lead to the deduction of b. 62 * Note that these bound changes have at most the same inference depth 63 * level as b, and were deduced earlier than b. 64 * -# Otherwise, the bound change b was a branching decision or a deduction with 65 * missing inference reason, or the inference constraint's validity is more local 66 * than the one of the conflict detecting constraint. 67 * - If a the bound changed corresponds to a binary variable, add it or its 68 * negation to the conflict set, depending on which of them is currently fixed to 69 * FALSE (i.e., the conflict set consists of literals that cannot be FALSE 70 * altogether at the same time). 71 * - Otherwise put the bound change into the conflict set. 72 * Note that if the bound change was a branching, all deduced bound changes 73 * remaining in the priority queue have smaller inference depth level than b, 74 * since deductions are always applied after the branching decisions. However, 75 * there is the possibility, that b was a deduction, where the inference 76 * reason was not given or the inference constraint was too local. 77 * With this lack of information, we must treat the deduced bound change like 78 * a branching, and there may exist other deduced bound changes of the same 79 * inference depth level in the priority queue. 80 * -# If priority queue is non-empty, goto step 2. 81 * -# The conflict set represents the conflict clause saying that at least one 82 * of the conflict variables must take a different value. The conflict set is then passed 83 * to the conflict handlers, that may create a corresponding constraint (e.g. a logicor 84 * constraint or bound disjunction constraint) out of these conflict variables and 85 * add it to the problem. 86 * 87 * If all deduced bound changes come with (global) inference information, depending on 88 * the conflict analyzing strategy, the resulting conflict set has the following property: 89 * - 1-FirstUIP: In the depth level where the conflict was found, at most one variable 90 * assigned at that level is member of the conflict set. This conflict variable is the 91 * first unique implication point of its depth level (FUIP). 92 * - All-FirstUIP: For each depth level, at most one variable assigned at that level is 93 * member of the conflict set. This conflict variable is the first unique implication 94 * point of its depth level (FUIP). 95 * 96 * The user has to do the following to get the conflict analysis running in its 97 * current implementation: 98 * - A constraint handler or propagator supporting the conflict analysis must implement 99 * the CONSRESPROP/PROPRESPROP call, that processes a bound change inference b and puts all 100 * the reason bounds leading to the application of b with calls to 101 * SCIPaddConflictBound() on the conflict queue (algorithm step 3.(a)). 102 * - If the current bounds lead to a deduction of a bound change (e.g. in domain 103 * propagation), a constraint handler should call SCIPinferVarLbCons() or 104 * SCIPinferVarUbCons(), thus providing the constraint that inferred the bound change. 105 * A propagator should call SCIPinferVarLbProp() or SCIPinferVarUbProp() instead, 106 * thus providing a pointer to itself. 107 * - If (in the current bounds) an infeasibility is detected, the constraint handler or 108 * propagator should 109 * 1. call SCIPinitConflictAnalysis() to initialize the conflict queue, 110 * 2. call SCIPaddConflictBound() for each bound that lead to the conflict, 111 * 3. call SCIPanalyzeConflictCons() or SCIPanalyzeConflict() to analyze the conflict 112 * and add an appropriate conflict constraint. 113 */ 114 115 /*---+----1----+----2----+----3----+----4----+----5----+----6----+----7----+----8----+----9----+----0----+----1----+----2*/ 116 117 #ifndef __SCIP_CONFLICT_GRAPHANALYSIS_H__ 118 #define __SCIP_CONFLICT_GRAPHANALYSIS_H__ 119 120 #include "scip/def.h" 121 #include "scip/type_cuts.h" 122 #include "scip/type_conflict.h" 123 #include "scip/type_reopt.h" 124 #include "scip/type_implics.h" 125 #include "scip/type_set.h" 126 #include "scip/type_stat.h" 127 #include "scip/type_lp.h" 128 #include "lpi/type_lpi.h" 129 #include "scip/type_branch.h" 130 #include "scip/type_mem.h" 131 #include "scip/type_var.h" 132 #include "scip/type_prob.h" 133 #include "scip/type_event.h" 134 #include <string.h> 135 #if defined(_WIN32) || defined(_WIN64) 136 #else 137 #include <strings.h> /*lint --e{766}*/ 138 #endif 139 140 #ifdef __cplusplus 141 extern "C" { 142 #endif 143 144 /** creates an empty conflict set */ 145 SCIP_RETCODE SCIPconflictsetCreate( 146 SCIP_CONFLICTSET** conflictset, /**< pointer to store the conflict set */ 147 BMS_BLKMEM* blkmem /**< block memory of transformed problem */ 148 ); 149 150 /** frees a conflict set */ 151 void SCIPconflictsetFree( 152 SCIP_CONFLICTSET** conflictset, /**< pointer to the conflict set */ 153 BMS_BLKMEM* blkmem /**< block memory of transformed problem */ 154 ); 155 156 /** copies the given conflict handler to a new scip */ 157 SCIP_RETCODE SCIPconflicthdlrCopyInclude( 158 SCIP_CONFLICTHDLR* conflicthdlr, /**< conflict handler */ 159 SCIP_SET* set /**< SCIP_SET of SCIP to copy to */ 160 ); 161 162 /** creates a conflict handler */ 163 SCIP_RETCODE SCIPconflicthdlrCreate( 164 SCIP_CONFLICTHDLR** conflicthdlr, /**< pointer to conflict handler data structure */ 165 SCIP_SET* set, /**< global SCIP settings */ 166 SCIP_MESSAGEHDLR* messagehdlr, /**< message handler */ 167 BMS_BLKMEM* blkmem, /**< block memory for parameter settings */ 168 const char* name, /**< name of conflict handler */ 169 const char* desc, /**< description of conflict handler */ 170 int priority, /**< priority of the conflict handler */ 171 SCIP_DECL_CONFLICTCOPY((*conflictcopy)), /**< copy method of conflict handler or NULL if you don't want to copy your plugin into sub-SCIPs */ 172 SCIP_DECL_CONFLICTFREE((*conflictfree)), /**< destructor of conflict handler */ 173 SCIP_DECL_CONFLICTINIT((*conflictinit)), /**< initialize conflict handler */ 174 SCIP_DECL_CONFLICTEXIT((*conflictexit)), /**< deinitialize conflict handler */ 175 SCIP_DECL_CONFLICTINITSOL((*conflictinitsol)),/**< solving process initialization method of conflict handler */ 176 SCIP_DECL_CONFLICTEXITSOL((*conflictexitsol)),/**< solving process deinitialization method of conflict handler */ 177 SCIP_DECL_CONFLICTEXEC((*conflictexec)), /**< conflict processing method of conflict handler */ 178 SCIP_CONFLICTHDLRDATA* conflicthdlrdata /**< conflict handler data */ 179 ); 180 181 /** calls destructor and frees memory of conflict handler */ 182 SCIP_RETCODE SCIPconflicthdlrFree( 183 SCIP_CONFLICTHDLR** conflicthdlr, /**< pointer to conflict handler data structure */ 184 SCIP_SET* set /**< global SCIP settings */ 185 ); 186 187 /** calls init method of conflict handler */ 188 SCIP_RETCODE SCIPconflicthdlrInit( 189 SCIP_CONFLICTHDLR* conflicthdlr, /**< conflict handler */ 190 SCIP_SET* set /**< global SCIP settings */ 191 ); 192 193 /** calls exit method of conflict handler */ 194 SCIP_RETCODE SCIPconflicthdlrExit( 195 SCIP_CONFLICTHDLR* conflicthdlr, /**< conflict handler */ 196 SCIP_SET* set /**< global SCIP settings */ 197 ); 198 199 /** informs conflict handler that the branch and bound process is being started */ 200 SCIP_RETCODE SCIPconflicthdlrInitsol( 201 SCIP_CONFLICTHDLR* conflicthdlr, /**< conflict handler */ 202 SCIP_SET* set /**< global SCIP settings */ 203 ); 204 205 /** informs conflict handler that the branch and bound process data is being freed */ 206 SCIP_RETCODE SCIPconflicthdlrExitsol( 207 SCIP_CONFLICTHDLR* conflicthdlr, /**< conflict handler */ 208 SCIP_SET* set /**< global SCIP settings */ 209 ); 210 211 /** calls execution method of conflict handler */ 212 SCIP_RETCODE SCIPconflicthdlrExec( 213 SCIP_CONFLICTHDLR* conflicthdlr, /**< conflict handler */ 214 SCIP_SET* set, /**< global SCIP settings */ 215 SCIP_NODE* node, /**< node to add conflict constraint to */ 216 SCIP_NODE* validnode, /**< node at which the constraint is valid */ 217 SCIP_BDCHGINFO** bdchginfos, /**< bound change resembling the conflict set */ 218 SCIP_Real* relaxedbds, /**< array with relaxed bounds which are efficient to create a valid conflict */ 219 int nbdchginfos, /**< number of bound changes in the conflict set */ 220 SCIP_CONFTYPE conftype, /**< type of the conflict */ 221 SCIP_Bool usescutoffbound, /**< depends the conflict on the cutoff bound? */ 222 SCIP_Bool resolved, /**< was the conflict set already used to create a constraint? */ 223 SCIP_RESULT* result /**< pointer to store the result of the callback method */ 224 ); 225 226 /** sets priority of conflict handler */ 227 void SCIPconflicthdlrSetPriority( 228 SCIP_CONFLICTHDLR* conflicthdlr, /**< conflict handler */ 229 SCIP_SET* set, /**< global SCIP settings */ 230 int priority /**< new priority of the conflict handler */ 231 ); 232 233 /** set copy method of conflict handler */ 234 void SCIPconflicthdlrSetCopy( 235 SCIP_CONFLICTHDLR* conflicthdlr, /**< conflict handler */ 236 SCIP_DECL_CONFLICTCOPY((*conflictcopy)) /**< copy method of the conflict handler */ 237 ); 238 239 /** set destructor of conflict handler */ 240 void SCIPconflicthdlrSetFree( 241 SCIP_CONFLICTHDLR* conflicthdlr, /**< conflict handler */ 242 SCIP_DECL_CONFLICTFREE((*conflictfree)) /**< destructor of conflict handler */ 243 ); 244 245 /** set initialization method of conflict handler */ 246 void SCIPconflicthdlrSetInit( 247 SCIP_CONFLICTHDLR* conflicthdlr, /**< conflict handler */ 248 SCIP_DECL_CONFLICTINIT((*conflictinit)) /**< initialization method conflict handler */ 249 ); 250 251 /** set deinitialization method of conflict handler */ 252 void SCIPconflicthdlrSetExit( 253 SCIP_CONFLICTHDLR* conflicthdlr, /**< conflict handler */ 254 SCIP_DECL_CONFLICTEXIT((*conflictexit)) /**< deinitialization method conflict handler */ 255 ); 256 257 /** set solving process initialization method of conflict handler */ 258 void SCIPconflicthdlrSetInitsol( 259 SCIP_CONFLICTHDLR* conflicthdlr, /**< conflict handler */ 260 SCIP_DECL_CONFLICTINITSOL((*conflictinitsol))/**< solving process initialization method of conflict handler */ 261 ); 262 263 /** set solving process deinitialization method of conflict handler */ 264 void SCIPconflicthdlrSetExitsol( 265 SCIP_CONFLICTHDLR* conflicthdlr, /**< conflict handler */ 266 SCIP_DECL_CONFLICTEXITSOL((*conflictexitsol))/**< solving process deinitialization method of conflict handler */ 267 ); 268 269 /** enables or disables all clocks of \p conflicthdlr, depending on the value of the flag */ 270 void SCIPconflicthdlrEnableOrDisableClocks( 271 SCIP_CONFLICTHDLR* conflicthdlr, /**< the conflict handler for which all clocks should be enabled or disabled */ 272 SCIP_Bool enable /**< should the clocks of the conflict handler be enabled? */ 273 ); 274 275 /** return TRUE if conflict analysis is applicable; In case the function return FALSE there is no need to initialize the 276 * conflict analysis since it will not be applied 277 */ 278 SCIP_Bool SCIPconflictApplicable( 279 SCIP_SET* set /**< global SCIP settings */ 280 ); 281 282 /** creates a temporary bound change information object that is destroyed after the conflict sets are flushed */ 283 SCIP_RETCODE conflictCreateTmpBdchginfo( 284 SCIP_CONFLICT* conflict, /**< conflict analysis data */ 285 BMS_BLKMEM* blkmem, /**< block memory */ 286 SCIP_SET* set, /**< global SCIP settings */ 287 SCIP_VAR* var, /**< active variable that changed the bounds */ 288 SCIP_BOUNDTYPE boundtype, /**< type of bound for var: lower or upper bound */ 289 SCIP_Real oldbound, /**< old value for bound */ 290 SCIP_Real newbound, /**< new value for bound */ 291 SCIP_BDCHGINFO** bdchginfo /**< pointer to store bound change information */ 292 ); 293 294 295 /* 296 * Conflict LP Bound Changes 297 */ 298 299 300 /** calculates the maximal size of conflict sets to be used */ 301 int conflictCalcMaxsize( 302 SCIP_SET* set, /**< global SCIP settings */ 303 SCIP_PROB* prob /**< problem data */ 304 ); 305 306 /** undoes bound changes on variables, still leaving the given infeasibility proof valid */ 307 SCIP_RETCODE SCIPundoBdchgsProof( 308 SCIP_SET* set, /**< global SCIP settings */ 309 SCIP_PROB* prob, /**< problem data */ 310 int currentdepth, /**< current depth in the tree */ 311 SCIP_Real* proofcoefs, /**< coefficients in infeasibility proof */ 312 SCIP_Real prooflhs, /**< left hand side of proof */ 313 SCIP_Real* proofact, /**< current activity of proof */ 314 SCIP_Real* curvarlbs, /**< current lower bounds of active problem variables */ 315 SCIP_Real* curvarubs, /**< current upper bounds of active problem variables */ 316 int* lbchginfoposs, /**< positions of currently active lower bound change information in variables' arrays */ 317 int* ubchginfoposs, /**< positions of currently active upper bound change information in variables' arrays */ 318 SCIP_LPBDCHGS* oldlpbdchgs, /**< old LP bound changes used for reset the LP bound change, or NULL */ 319 SCIP_LPBDCHGS* relaxedlpbdchgs, /**< relaxed LP bound changes used for reset the LP bound change, or NULL */ 320 SCIP_Bool* resolve, /**< pointer to store whether the changed LP should be resolved again, or NULL */ 321 SCIP_LPI* lpi /**< pointer to LPi to access infinity of LP solver; necessary to set correct values */ 322 ); 323 324 /** applies conflict analysis starting with given bound changes, that could not be undone during previous 325 * infeasibility analysis 326 */ 327 SCIP_RETCODE SCIPconflictAnalyzeRemainingBdchgs( 328 SCIP_CONFLICT* conflict, /**< conflict analysis data */ 329 BMS_BLKMEM* blkmem, /**< block memory of transformed problem */ 330 SCIP_SET* set, /**< global SCIP settings */ 331 SCIP_STAT* stat, /**< problem statistics */ 332 SCIP_PROB* prob, /**< problem data */ 333 SCIP_TREE* tree, /**< branch and bound tree */ 334 SCIP_Bool diving, /**< are we in strong branching or diving mode? */ 335 int* lbchginfoposs, /**< positions of currently active lower bound change information in variables' arrays */ 336 int* ubchginfoposs, /**< positions of currently active upper bound change information in variables' arrays */ 337 int* nconss, /**< pointer to store the number of generated conflict constraints */ 338 int* nliterals, /**< pointer to store the number of literals in generated conflict constraints */ 339 int* nreconvconss, /**< pointer to store the number of generated reconvergence constraints */ 340 int* nreconvliterals /**< pointer to store the number of literals generated reconvergence constraints */ 341 ); 342 343 /** initializes the propagation conflict analysis by clearing the conflict candidate queue */ 344 SCIP_RETCODE SCIPconflictInit( 345 SCIP_CONFLICT* conflict, /**< conflict analysis data */ 346 SCIP_SET* set, /**< global SCIP settings */ 347 SCIP_STAT* stat, /**< problem statistics */ 348 SCIP_PROB* prob, /**< problem data */ 349 SCIP_CONFTYPE conftype, /**< type of the conflict */ 350 SCIP_Bool usescutoffbound /**< depends the conflict on a cutoff bound? */ 351 ); 352 353 /** adds variable's bound to conflict candidate queue */ 354 SCIP_RETCODE SCIPconflictAddBound( 355 SCIP_CONFLICT* conflict, /**< conflict analysis data */ 356 BMS_BLKMEM* blkmem, /**< block memory */ 357 SCIP_SET* set, /**< global SCIP settings */ 358 SCIP_STAT* stat, /**< dynamic problem statistics */ 359 SCIP_VAR* var, /**< problem variable */ 360 SCIP_BOUNDTYPE boundtype, /**< type of bound that was changed: lower or upper bound */ 361 SCIP_BDCHGIDX* bdchgidx /**< bound change index (time stamp of bound change), or NULL for current time */ 362 ); 363 364 /** adds variable's bound to conflict candidate queue with the additional information of a relaxed bound */ 365 SCIP_RETCODE SCIPconflictAddRelaxedBound( 366 SCIP_CONFLICT* conflict, /**< conflict analysis data */ 367 BMS_BLKMEM* blkmem, /**< block memory */ 368 SCIP_SET* set, /**< global SCIP settings */ 369 SCIP_STAT* stat, /**< dynamic problem statistics */ 370 SCIP_VAR* var, /**< problem variable */ 371 SCIP_BOUNDTYPE boundtype, /**< type of bound that was changed: lower or upper bound */ 372 SCIP_BDCHGIDX* bdchgidx, /**< bound change index (time stamp of bound change), or NULL for current time */ 373 SCIP_Real relaxedbd /**< the relaxed bound */ 374 ); 375 376 /** checks if the given variable is already part of the current conflict set or queued for resolving with the same or 377 * even stronger bound 378 */ 379 SCIP_RETCODE SCIPconflictIsVarUsed( 380 SCIP_CONFLICT* conflict, /**< conflict analysis data */ 381 SCIP_VAR* var, /**< problem variable */ 382 SCIP_SET* set, /**< global SCIP settings */ 383 SCIP_BOUNDTYPE boundtype, /**< type of bound for which the score should be increased */ 384 SCIP_BDCHGIDX* bdchgidx, /**< bound change index (time stamp of bound change), or NULL for current time */ 385 SCIP_Bool* used /**< pointer to store if the variable is already used */ 386 ); 387 388 /** returns the conflict lower bound if the variable is present in the current conflict set; otherwise the global lower 389 * bound 390 */ 391 SCIP_Real SCIPconflictGetVarLb( 392 SCIP_CONFLICT* conflict, /**< conflict analysis data */ 393 SCIP_VAR* var /**< problem variable */ 394 ); 395 396 /** returns the conflict upper bound if the variable is present in the current conflict set; otherwise the global upper 397 * bound 398 */ 399 SCIP_Real SCIPconflictGetVarUb( 400 SCIP_CONFLICT* conflict, /**< conflict analysis data */ 401 SCIP_VAR* var /**< problem variable */ 402 ); 403 404 /** try to find a subset of changed bounds leading to an infeasible LP 405 * 406 * 1. call undoBdchgsDualfarkas() or undoBdchgsDualsol() 407 * -> update lb/ubchginfoposs arrays 408 * -> store additional changes in bdchg and curvarlbs/ubs arrays 409 * -> apply additional changes to the LPI 410 * 2. (optional) if additional bound changes were undone: 411 * -> resolve LP 412 * -> goto 1. 413 * 3. redo all bound changes in the LPI to restore the LPI to its original state 414 * 4. analyze conflict 415 * -> put remaining changed bounds (see lb/ubchginfoposs arrays) into starting conflict set 416 */ 417 SCIP_RETCODE SCIPrunBoundHeuristic( 418 SCIP_CONFLICT* conflict, /**< conflict data */ 419 SCIP_SET* set, /**< global SCIP settings */ 420 SCIP_STAT* stat, /**< problem statistics */ 421 SCIP_PROB* origprob, /**< original problem */ 422 SCIP_PROB* transprob, /**< transformed problem */ 423 SCIP_TREE* tree, /**< branch and bound tree */ 424 SCIP_REOPT* reopt, /**< reoptimization data */ 425 SCIP_LP* lp, /**< LP data */ 426 SCIP_LPI* lpi, /**< LPI data */ 427 BMS_BLKMEM* blkmem, /**< block memory */ 428 SCIP_Real* proofcoefs, /**< coefficients in the proof constraint */ 429 SCIP_Real* prooflhs, /**< lhs of the proof constraint */ 430 SCIP_Real* proofactivity, /**< maximal activity of the proof constraint */ 431 SCIP_Real* curvarlbs, /**< current lower bounds of active problem variables */ 432 SCIP_Real* curvarubs, /**< current upper bounds of active problem variables */ 433 int* lbchginfoposs, /**< positions of currently active lower bound change information in variables' arrays */ 434 int* ubchginfoposs, /**< positions of currently active upper bound change information in variables' arrays */ 435 int* iterations, /**< pointer to store the total number of LP iterations used */ 436 SCIP_Bool marklpunsolved, /**< whether LP should be marked unsolved after analysis (needed for strong branching) */ 437 SCIP_Bool* dualproofsuccess, /**< pointer to store success result of dual proof analysis */ 438 SCIP_Bool* valid /**< pointer to store whether the result is still a valid proof */ 439 ); 440 441 #ifdef __cplusplus 442 } 443 #endif 444 445 #endif 446