Scippy

SCIP

Solving Constraint Integer Programs

conflict.c
Go to the documentation of this file.
1 /* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
2 /* */
3 /* This file is part of the program and library */
4 /* SCIP --- Solving Constraint Integer Programs */
5 /* */
6 /* Copyright (C) 2002-2020 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 /**@file conflict.c
16  * @ingroup OTHER_CFILES
17  * @brief methods and datastructures for conflict analysis
18  * @author Tobias Achterberg
19  * @author Timo Berthold
20  * @author Stefan Heinz
21  * @author Marc Pfetsch
22  * @author Michael Winkler
23  * @author Jakob Witzig
24  *
25  * This file implements a conflict analysis method like the one used in modern
26  * SAT solvers like zchaff. The algorithm works as follows:
27  *
28  * Given is a set of bound changes that are not allowed being applied simultaneously, because they
29  * render the current node infeasible (e.g. because a single constraint is infeasible in the these
30  * bounds, or because the LP relaxation is infeasible). The goal is to deduce a clause on variables
31  * -- a conflict clause -- representing the "reason" for this conflict, i.e., the branching decisions
32  * or the deductions (applied e.g. in domain propagation) that lead to the conflict. This clause can
33  * then be added to the constraint set to help cutting off similar parts of the branch and bound
34  * tree, that would lead to the same conflict. A conflict clause can also be generated, if the
35  * conflict was detected by a locally valid constraint. In this case, the resulting conflict clause
36  * is also locally valid in the same depth as the conflict detecting constraint. If all involved
37  * variables are binary, a linear (set covering) constraint can be generated, otherwise a bound
38  * disjunction constraint is generated. Details are given in
39  *
40  * Tobias Achterberg, Conflict Analysis in Mixed Integer Programming@n
41  * Discrete Optimization, 4, 4-20 (2007)
42  *
43  * See also @ref CONF. Here is an outline of the algorithm:
44  *
45  * -# Put all the given bound changes to a priority queue, which is ordered,
46  * such that the bound change that was applied last due to branching or deduction
47  * is at the top of the queue. The variables in the queue are always active
48  * problem variables. Because binary variables are preferred over general integer
49  * variables, integer variables are put on the priority queue prior to the binary
50  * variables. Create an empty conflict set.
51  * -# Remove the top bound change b from the priority queue.
52  * -# Perform the following case distinction:
53  * -# If the remaining queue is non-empty, and bound change b' (the one that is now
54  * on the top of the queue) was applied at the same depth level as b, and if
55  * b was a deduction with known inference reason, and if the inference constraint's
56  * valid depth is smaller or equal to the conflict detecting constraint's valid
57  * depth:
58  * - Resolve bound change b by asking the constraint that inferred the
59  * bound change to put all the bound changes on the priority queue, that
60  * lead to the deduction of b.
61  * Note that these bound changes have at most the same inference depth
62  * level as b, and were deduced earlier than b.
63  * -# Otherwise, the bound change b was a branching decision or a deduction with
64  * missing inference reason, or the inference constraint's validity is more local
65  * than the one of the conflict detecting constraint.
66  * - If a the bound changed corresponds to a binary variable, add it or its
67  * negation to the conflict set, depending on which of them is currently fixed to
68  * FALSE (i.e., the conflict set consists of literals that cannot be FALSE
69  * altogether at the same time).
70  * - Otherwise put the bound change into the conflict set.
71  * Note that if the bound change was a branching, all deduced bound changes
72  * remaining in the priority queue have smaller inference depth level than b,
73  * since deductions are always applied after the branching decisions. However,
74  * there is the possibility, that b was a deduction, where the inference
75  * reason was not given or the inference constraint was too local.
76  * With this lack of information, we must treat the deduced bound change like
77  * a branching, and there may exist other deduced bound changes of the same
78  * inference depth level in the priority queue.
79  * -# If priority queue is non-empty, goto step 2.
80  * -# The conflict set represents the conflict clause saying that at least one
81  * of the conflict variables must take a different value. The conflict set is then passed
82  * to the conflict handlers, that may create a corresponding constraint (e.g. a logicor
83  * constraint or bound disjunction constraint) out of these conflict variables and
84  * add it to the problem.
85  *
86  * If all deduced bound changes come with (global) inference information, depending on
87  * the conflict analyzing strategy, the resulting conflict set has the following property:
88  * - 1-FirstUIP: In the depth level where the conflict was found, at most one variable
89  * assigned at that level is member of the conflict set. This conflict variable is the
90  * first unique implication point of its depth level (FUIP).
91  * - All-FirstUIP: For each depth level, at most one variable assigned at that level is
92  * member of the conflict set. This conflict variable is the first unique implication
93  * point of its depth level (FUIP).
94  *
95  * The user has to do the following to get the conflict analysis running in its
96  * current implementation:
97  * - A constraint handler or propagator supporting the conflict analysis must implement
98  * the CONSRESPROP/PROPRESPROP call, that processes a bound change inference b and puts all
99  * the reason bounds leading to the application of b with calls to
100  * SCIPaddConflictBound() on the conflict queue (algorithm step 3.(a)).
101  * - If the current bounds lead to a deduction of a bound change (e.g. in domain
102  * propagation), a constraint handler should call SCIPinferVarLbCons() or
103  * SCIPinferVarUbCons(), thus providing the constraint that infered the bound change.
104  * A propagator should call SCIPinferVarLbProp() or SCIPinferVarUbProp() instead,
105  * thus providing a pointer to itself.
106  * - If (in the current bounds) an infeasibility is detected, the constraint handler or
107  * propagator should
108  * 1. call SCIPinitConflictAnalysis() to initialize the conflict queue,
109  * 2. call SCIPaddConflictBound() for each bound that lead to the conflict,
110  * 3. call SCIPanalyzeConflictCons() or SCIPanalyzeConflict() to analyze the conflict
111  * and add an appropriate conflict constraint.
112  */
113 
114 /*---+----1----+----2----+----3----+----4----+----5----+----6----+----7----+----8----+----9----+----0----+----1----+----2*/
115 
116 #include "lpi/lpi.h"
117 #include "scip/clock.h"
118 #include "scip/conflict.h"
119 #include "scip/conflictstore.h"
120 #include "scip/cons.h"
121 #include "scip/cons_linear.h"
122 #include "scip/cuts.h"
123 #include "scip/history.h"
124 #include "scip/lp.h"
125 #include "scip/presolve.h"
126 #include "scip/prob.h"
127 #include "scip/prop.h"
128 #include "scip/pub_conflict.h"
129 #include "scip/pub_cons.h"
130 #include "scip/pub_lp.h"
131 #include "scip/pub_message.h"
132 #include "scip/pub_misc.h"
133 #include "scip/pub_misc_sort.h"
134 #include "scip/pub_paramset.h"
135 #include "scip/pub_prop.h"
136 #include "scip/pub_tree.h"
137 #include "scip/pub_var.h"
138 #include "scip/scip_conflict.h"
139 #include "scip/scip_cons.h"
140 #include "scip/scip_mem.h"
141 #include "scip/scip_sol.h"
142 #include "scip/scip_var.h"
143 #include "scip/set.h"
144 #include "scip/sol.h"
145 #include "scip/struct_conflict.h"
146 #include "scip/struct_lp.h"
147 #include "scip/struct_prob.h"
148 #include "scip/struct_set.h"
149 #include "scip/struct_stat.h"
150 #include "scip/struct_tree.h"
151 #include "scip/struct_var.h"
152 #include "scip/tree.h"
153 #include "scip/var.h"
154 #include "scip/visual.h"
155 #include <string.h>
156 #if defined(_WIN32) || defined(_WIN64)
157 #else
158 #include <strings.h> /*lint --e{766}*/
159 #endif
160 
161 
162 
163 #define BOUNDSWITCH 0.51 /**< threshold for bound switching - see cuts.c */
164 #define POSTPROCESS FALSE /**< apply postprocessing to the cut - see cuts.c */
165 #define USEVBDS FALSE /**< use variable bounds - see cuts.c */
166 #define ALLOWLOCAL FALSE /**< allow to generate local cuts - see cuts. */
167 #define MINFRAC 0.05 /**< minimal fractionality of floor(rhs) - see cuts.c */
168 #define MAXFRAC 0.999 /**< maximal fractionality of floor(rhs) - see cuts.c */
169 
170 /*#define SCIP_CONFGRAPH*/
171 
172 
173 #ifdef SCIP_CONFGRAPH
174 /*
175  * Output of Conflict Graph
176  */
177 
178 #include <stdio.h>
179 
180 static FILE* confgraphfile = NULL; /**< output file for current conflict graph */
181 static SCIP_BDCHGINFO* confgraphcurrentbdchginfo = NULL; /**< currently resolved bound change */
182 static int confgraphnconflictsets = 0; /**< number of conflict sets marked in the graph */
183 
184 /** writes a node section to the conflict graph file */
185 static
186 void confgraphWriteNode(
187  void* idptr, /**< id of the node */
188  const char* label, /**< label of the node */
189  const char* nodetype, /**< type of the node */
190  const char* fillcolor, /**< color of the node's interior */
191  const char* bordercolor /**< color of the node's border */
192  )
193 {
194  assert(confgraphfile != NULL);
195 
196  SCIPgmlWriteNode(confgraphfile, (unsigned int)(size_t)idptr, label, nodetype, fillcolor, bordercolor);
197 }
198 
199 /** writes an edge section to the conflict graph file */
200 static
201 void confgraphWriteEdge(
202  void* source, /**< source node of the edge */
203  void* target, /**< target node of the edge */
204  const char* color /**< color of the edge */
205  )
206 {
207  assert(confgraphfile != NULL);
208 
209 #ifndef SCIP_CONFGRAPH_EDGE
210  SCIPgmlWriteArc(confgraphfile, (unsigned int)(size_t)source, (unsigned int)(size_t)target, NULL, color);
211 #else
212  SCIPgmlWriteEdge(confgraphfile, (unsigned int)(size_t)source, (unsigned int)(size_t)target, NULL, color);
213 #endif
214 }
215 
216 /** creates a file to output the current conflict graph into; adds the conflict vertex to the graph */
217 static
218 SCIP_RETCODE confgraphCreate(
219  SCIP_SET* set, /**< global SCIP settings */
220  SCIP_CONFLICT* conflict /**< conflict analysis data */
221  )
222 {
223  char fname[SCIP_MAXSTRLEN];
224 
225  assert(conflict != NULL);
226  assert(confgraphfile == NULL);
227 
228  (void) SCIPsnprintf(fname, SCIP_MAXSTRLEN, "conf%p%d.gml", conflict, conflict->count);
229  SCIPinfoMessage(set->scip, NULL, "storing conflict graph in file <%s>\n", fname);
230 
231  confgraphfile = fopen(fname, "w");
232 
233  if( confgraphfile == NULL )
234  {
235  SCIPerrorMessage("cannot open graph file <%s>\n", fname);
236  SCIPABORT(); /*lint !e527*/
237  return SCIP_WRITEERROR;
238  }
239 
240  SCIPgmlWriteOpening(confgraphfile, TRUE);
241 
242  confgraphWriteNode(NULL, "conflict", "ellipse", "#ff0000", "#000000");
243 
244  confgraphcurrentbdchginfo = NULL;
245 
246  return SCIP_OKAY;
247 }
248 
249 /** closes conflict graph file */
250 static
251 void confgraphFree(
252  void
253  )
254 {
255  if( confgraphfile != NULL )
256  {
257  SCIPgmlWriteClosing(confgraphfile);
258 
259  fclose(confgraphfile);
260 
261  confgraphfile = NULL;
262  confgraphnconflictsets = 0;
263  }
264 }
265 
266 /** adds a bound change node to the conflict graph and links it to the currently resolved bound change */
267 static
268 void confgraphAddBdchg(
269  SCIP_BDCHGINFO* bdchginfo /**< bound change to add to the conflict graph */
270  )
271 {
272  const char* colors[] = {
273  "#8888ff", /* blue for constraint resolving */
274  "#ffff00", /* yellow for propagator resolving */
275  "#55ff55" /* green branching decision */
276  };
277  char label[SCIP_MAXSTRLEN];
278  char depth[SCIP_MAXSTRLEN];
279  int col;
280 
281  switch( SCIPbdchginfoGetChgtype(bdchginfo) )
282  {
284  col = 2;
285  break;
287  col = 0;
288  break;
290  col = (SCIPbdchginfoGetInferProp(bdchginfo) == NULL ? 1 : 0);
291  break;
292  default:
293  SCIPerrorMessage("invalid bound change type\n");
294  col = 0;
295  SCIPABORT();
296  break;
297  }
298 
299  if( SCIPbdchginfoGetDepth(bdchginfo) == INT_MAX )
300  (void) SCIPsnprintf(depth, SCIP_MAXSTRLEN, "dive");
301  else
302  (void) SCIPsnprintf(depth, SCIP_MAXSTRLEN, "%d", SCIPbdchginfoGetDepth(bdchginfo));
303  (void) SCIPsnprintf(label, SCIP_MAXSTRLEN, "%s %s %g\n[%s:%d]", SCIPvarGetName(SCIPbdchginfoGetVar(bdchginfo)),
304  SCIPbdchginfoGetBoundtype(bdchginfo) == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=",
305  SCIPbdchginfoGetNewbound(bdchginfo), depth, SCIPbdchginfoGetPos(bdchginfo));
306  confgraphWriteNode(bdchginfo, label, "ellipse", colors[col], "#000000");
307  confgraphWriteEdge(bdchginfo, confgraphcurrentbdchginfo, "#000000");
308 }
309 
310 /** links the already existing bound change node to the currently resolved bound change */
311 static
312 void confgraphLinkBdchg(
313  SCIP_BDCHGINFO* bdchginfo /**< bound change to add to the conflict graph */
314  )
315 {
316  confgraphWriteEdge(bdchginfo, confgraphcurrentbdchginfo, "#000000");
317 }
318 
319 /** marks the given bound change to be the currently resolved bound change */
320 static
321 void confgraphSetCurrentBdchg(
322  SCIP_BDCHGINFO* bdchginfo /**< bound change to add to the conflict graph */
323  )
324 {
325  confgraphcurrentbdchginfo = bdchginfo;
326 }
327 
328 /** marks given conflict set in the conflict graph */
329 static
330 void confgraphMarkConflictset(
331  SCIP_CONFLICTSET* conflictset /**< conflict set */
332  )
333 {
334  char label[SCIP_MAXSTRLEN];
335  int i;
336 
337  assert(conflictset != NULL);
338 
339  confgraphnconflictsets++;
340  (void) SCIPsnprintf(label, SCIP_MAXSTRLEN, "conf %d (%d)", confgraphnconflictsets, conflictset->validdepth);
341  confgraphWriteNode((void*)(size_t)confgraphnconflictsets, label, "rectangle", "#ff00ff", "#000000");
342  for( i = 0; i < conflictset->nbdchginfos; ++i )
343  confgraphWriteEdge((void*)(size_t)confgraphnconflictsets, conflictset->bdchginfos[i], "#ff00ff");
344 }
345 
346 #endif
347 
348 /*
349  * Conflict Handler
350  */
351 
352 /** compares two conflict handlers w. r. to their priority */
353 SCIP_DECL_SORTPTRCOMP(SCIPconflicthdlrComp)
354 { /*lint --e{715}*/
355  return ((SCIP_CONFLICTHDLR*)elem2)->priority - ((SCIP_CONFLICTHDLR*)elem1)->priority;
356 }
357 
358 /** comparison method for sorting conflict handler w.r.t. to their name */
359 SCIP_DECL_SORTPTRCOMP(SCIPconflicthdlrCompName)
360 {
362 }
363 
364 /** method to call, when the priority of a conflict handler was changed */
365 static
366 SCIP_DECL_PARAMCHGD(paramChgdConflicthdlrPriority)
367 { /*lint --e{715}*/
368  SCIP_PARAMDATA* paramdata;
369 
370  paramdata = SCIPparamGetData(param);
371  assert(paramdata != NULL);
372 
373  /* use SCIPsetConflicthdlrPriority() to mark the conflicthdlrs unsorted */
374  SCIP_CALL( SCIPsetConflicthdlrPriority(scip, (SCIP_CONFLICTHDLR*)paramdata, SCIPparamGetInt(param)) ); /*lint !e740*/
375 
376  return SCIP_OKAY;
377 }
378 
379 /** copies the given conflict handler to a new scip */
381  SCIP_CONFLICTHDLR* conflicthdlr, /**< conflict handler */
382  SCIP_SET* set /**< SCIP_SET of SCIP to copy to */
383  )
384 {
385  assert(conflicthdlr != NULL);
386  assert(set != NULL);
387  assert(set->scip != NULL);
388 
389  if( conflicthdlr->conflictcopy != NULL )
390  {
391  SCIPsetDebugMsg(set, "including conflict handler %s in subscip %p\n", SCIPconflicthdlrGetName(conflicthdlr), (void*)set->scip);
392  SCIP_CALL( conflicthdlr->conflictcopy(set->scip, conflicthdlr) );
393  }
394 
395  return SCIP_OKAY;
396 }
397 
398 /** internal method for creating a conflict handler */
399 static
401  SCIP_CONFLICTHDLR** conflicthdlr, /**< pointer to conflict handler data structure */
402  SCIP_SET* set, /**< global SCIP settings */
403  SCIP_MESSAGEHDLR* messagehdlr, /**< message handler */
404  BMS_BLKMEM* blkmem, /**< block memory for parameter settings */
405  const char* name, /**< name of conflict handler */
406  const char* desc, /**< description of conflict handler */
407  int priority, /**< priority of the conflict handler */
408  SCIP_DECL_CONFLICTCOPY((*conflictcopy)), /**< copy method of conflict handler or NULL if you don't want to copy your plugin into sub-SCIPs */
409  SCIP_DECL_CONFLICTFREE((*conflictfree)), /**< destructor of conflict handler */
410  SCIP_DECL_CONFLICTINIT((*conflictinit)), /**< initialize conflict handler */
411  SCIP_DECL_CONFLICTEXIT((*conflictexit)), /**< deinitialize conflict handler */
412  SCIP_DECL_CONFLICTINITSOL((*conflictinitsol)),/**< solving process initialization method of conflict handler */
413  SCIP_DECL_CONFLICTEXITSOL((*conflictexitsol)),/**< solving process deinitialization method of conflict handler */
414  SCIP_DECL_CONFLICTEXEC((*conflictexec)), /**< conflict processing method of conflict handler */
415  SCIP_CONFLICTHDLRDATA* conflicthdlrdata /**< conflict handler data */
416  )
417 {
419  char paramdesc[SCIP_MAXSTRLEN];
420 
421  assert(conflicthdlr != NULL);
422  assert(name != NULL);
423  assert(desc != NULL);
424 
425  SCIP_ALLOC( BMSallocMemory(conflicthdlr) );
426  BMSclearMemory(*conflicthdlr);
427 
428  SCIP_ALLOC( BMSduplicateMemoryArray(&(*conflicthdlr)->name, name, strlen(name)+1) );
429  SCIP_ALLOC( BMSduplicateMemoryArray(&(*conflicthdlr)->desc, desc, strlen(desc)+1) );
430  (*conflicthdlr)->priority = priority;
431  (*conflicthdlr)->conflictcopy = conflictcopy;
432  (*conflicthdlr)->conflictfree = conflictfree;
433  (*conflicthdlr)->conflictinit = conflictinit;
434  (*conflicthdlr)->conflictexit = conflictexit;
435  (*conflicthdlr)->conflictinitsol = conflictinitsol;
436  (*conflicthdlr)->conflictexitsol = conflictexitsol;
437  (*conflicthdlr)->conflictexec = conflictexec;
438  (*conflicthdlr)->conflicthdlrdata = conflicthdlrdata;
439  (*conflicthdlr)->initialized = FALSE;
440 
441  SCIP_CALL( SCIPclockCreate(&(*conflicthdlr)->setuptime, SCIP_CLOCKTYPE_DEFAULT) );
442  SCIP_CALL( SCIPclockCreate(&(*conflicthdlr)->conflicttime, SCIP_CLOCKTYPE_DEFAULT) );
443 
444  /* add parameters */
445  (void) SCIPsnprintf(paramname, SCIP_MAXSTRLEN, "conflict/%s/priority", name);
446  (void) SCIPsnprintf(paramdesc, SCIP_MAXSTRLEN, "priority of conflict handler <%s>", name);
447  SCIP_CALL( SCIPsetAddIntParam(set, messagehdlr, blkmem, paramname, paramdesc, &(*conflicthdlr)->priority, TRUE, \
448  priority, INT_MIN, INT_MAX, paramChgdConflicthdlrPriority, (SCIP_PARAMDATA*)(*conflicthdlr)) ); /*lint !e740*/
449 
450  return SCIP_OKAY;
451 }
452 
453 /** creates a conflict handler */
455  SCIP_CONFLICTHDLR** conflicthdlr, /**< pointer to conflict handler data structure */
456  SCIP_SET* set, /**< global SCIP settings */
457  SCIP_MESSAGEHDLR* messagehdlr, /**< message handler */
458  BMS_BLKMEM* blkmem, /**< block memory for parameter settings */
459  const char* name, /**< name of conflict handler */
460  const char* desc, /**< description of conflict handler */
461  int priority, /**< priority of the conflict handler */
462  SCIP_DECL_CONFLICTCOPY((*conflictcopy)), /**< copy method of conflict handler or NULL if you don't want to
463  * copy your plugin into sub-SCIPs */
464  SCIP_DECL_CONFLICTFREE((*conflictfree)), /**< destructor of conflict handler */
465  SCIP_DECL_CONFLICTINIT((*conflictinit)), /**< initialize conflict handler */
466  SCIP_DECL_CONFLICTEXIT((*conflictexit)), /**< deinitialize conflict handler */
467  SCIP_DECL_CONFLICTINITSOL((*conflictinitsol)),/**< solving process initialization method of conflict handler */
468  SCIP_DECL_CONFLICTEXITSOL((*conflictexitsol)),/**< solving process deinitialization method of conflict handler */
469  SCIP_DECL_CONFLICTEXEC((*conflictexec)), /**< conflict processing method of conflict handler */
470  SCIP_CONFLICTHDLRDATA* conflicthdlrdata /**< conflict handler data */
471  )
472 {
473  assert(conflicthdlr != NULL);
474  assert(name != NULL);
475  assert(desc != NULL);
476 
477  SCIP_CALL_FINALLY( doConflicthdlrCreate(conflicthdlr, set, messagehdlr, blkmem, name, desc, priority,
478  conflictcopy, conflictfree, conflictinit, conflictexit, conflictinitsol, conflictexitsol, conflictexec,
479  conflicthdlrdata), (void) SCIPconflicthdlrFree(conflicthdlr, set) );
480 
481  return SCIP_OKAY;
482 }
483 
484 /** calls destructor and frees memory of conflict handler */
486  SCIP_CONFLICTHDLR** conflicthdlr, /**< pointer to conflict handler data structure */
487  SCIP_SET* set /**< global SCIP settings */
488  )
489 {
490  assert(conflicthdlr != NULL);
491  if( *conflicthdlr == NULL )
492  return SCIP_OKAY;
493  assert(!(*conflicthdlr)->initialized);
494  assert(set != NULL);
495 
496  /* call destructor of conflict handler */
497  if( (*conflicthdlr)->conflictfree != NULL )
498  {
499  SCIP_CALL( (*conflicthdlr)->conflictfree(set->scip, *conflicthdlr) );
500  }
501 
502  SCIPclockFree(&(*conflicthdlr)->conflicttime);
503  SCIPclockFree(&(*conflicthdlr)->setuptime);
504 
505  BMSfreeMemoryArrayNull(&(*conflicthdlr)->name);
506  BMSfreeMemoryArrayNull(&(*conflicthdlr)->desc);
507  BMSfreeMemory(conflicthdlr);
508 
509  return SCIP_OKAY;
510 }
511 
512 /** calls initialization method of conflict handler */
514  SCIP_CONFLICTHDLR* conflicthdlr, /**< conflict handler */
515  SCIP_SET* set /**< global SCIP settings */
516  )
517 {
518  assert(conflicthdlr != NULL);
519  assert(set != NULL);
520 
521  if( conflicthdlr->initialized )
522  {
523  SCIPerrorMessage("conflict handler <%s> already initialized\n", conflicthdlr->name);
524  return SCIP_INVALIDCALL;
525  }
526 
527  if( set->misc_resetstat )
528  {
529  SCIPclockReset(conflicthdlr->setuptime);
530  SCIPclockReset(conflicthdlr->conflicttime);
531  }
532 
533  /* call initialization method of conflict handler */
534  if( conflicthdlr->conflictinit != NULL )
535  {
536  /* start timing */
537  SCIPclockStart(conflicthdlr->setuptime, set);
538 
539  SCIP_CALL( conflicthdlr->conflictinit(set->scip, conflicthdlr) );
540 
541  /* stop timing */
542  SCIPclockStop(conflicthdlr->setuptime, set);
543  }
544  conflicthdlr->initialized = TRUE;
545 
546  return SCIP_OKAY;
547 }
548 
549 /** calls exit method of conflict handler */
551  SCIP_CONFLICTHDLR* conflicthdlr, /**< conflict handler */
552  SCIP_SET* set /**< global SCIP settings */
553  )
554 {
555  assert(conflicthdlr != NULL);
556  assert(set != NULL);
557 
558  if( !conflicthdlr->initialized )
559  {
560  SCIPerrorMessage("conflict handler <%s> not initialized\n", conflicthdlr->name);
561  return SCIP_INVALIDCALL;
562  }
563 
564  /* call deinitialization method of conflict handler */
565  if( conflicthdlr->conflictexit != NULL )
566  {
567  /* start timing */
568  SCIPclockStart(conflicthdlr->setuptime, set);
569 
570  SCIP_CALL( conflicthdlr->conflictexit(set->scip, conflicthdlr) );
571 
572  /* stop timing */
573  SCIPclockStop(conflicthdlr->setuptime, set);
574  }
575  conflicthdlr->initialized = FALSE;
576 
577  return SCIP_OKAY;
578 }
579 
580 /** informs conflict handler that the branch and bound process is being started */
582  SCIP_CONFLICTHDLR* conflicthdlr, /**< conflict handler */
583  SCIP_SET* set /**< global SCIP settings */
584  )
585 {
586  assert(conflicthdlr != NULL);
587  assert(set != NULL);
588 
589  /* call solving process initialization method of conflict handler */
590  if( conflicthdlr->conflictinitsol != NULL )
591  {
592  /* start timing */
593  SCIPclockStart(conflicthdlr->setuptime, set);
594 
595  SCIP_CALL( conflicthdlr->conflictinitsol(set->scip, conflicthdlr) );
596 
597  /* stop timing */
598  SCIPclockStop(conflicthdlr->setuptime, set);
599  }
600 
601  return SCIP_OKAY;
602 }
603 
604 /** informs conflict handler that the branch and bound process data is being freed */
606  SCIP_CONFLICTHDLR* conflicthdlr, /**< conflict handler */
607  SCIP_SET* set /**< global SCIP settings */
608  )
609 {
610  assert(conflicthdlr != NULL);
611  assert(set != NULL);
612 
613  /* call solving process deinitialization method of conflict handler */
614  if( conflicthdlr->conflictexitsol != NULL )
615  {
616  /* start timing */
617  SCIPclockStart(conflicthdlr->setuptime, set);
618 
619  SCIP_CALL( conflicthdlr->conflictexitsol(set->scip, conflicthdlr) );
620 
621  /* stop timing */
622  SCIPclockStop(conflicthdlr->setuptime, set);
623  }
624 
625  return SCIP_OKAY;
626 }
627 
628 /** calls execution method of conflict handler */
630  SCIP_CONFLICTHDLR* conflicthdlr, /**< conflict handler */
631  SCIP_SET* set, /**< global SCIP settings */
632  SCIP_NODE* node, /**< node to add conflict constraint to */
633  SCIP_NODE* validnode, /**< node at which the constraint is valid */
634  SCIP_BDCHGINFO** bdchginfos, /**< bound change resembling the conflict set */
635  SCIP_Real* relaxedbds, /**< array with relaxed bounds which are efficient to create a valid conflict */
636  int nbdchginfos, /**< number of bound changes in the conflict set */
637  SCIP_CONFTYPE conftype, /**< type of the conflict */
638  SCIP_Bool usescutoffbound, /**< depends the conflict on the cutoff bound? */
639  SCIP_Bool resolved, /**< was the conflict set already used to create a constraint? */
640  SCIP_RESULT* result /**< pointer to store the result of the callback method */
641  )
642 {
643  assert(conflicthdlr != NULL);
644  assert(set != NULL);
645  assert(bdchginfos != NULL || nbdchginfos == 0);
646  assert(result != NULL);
647 
648  /* call solution start method of conflict handler */
649  *result = SCIP_DIDNOTRUN;
650  if( conflicthdlr->conflictexec != NULL )
651  {
652  /* start timing */
653  SCIPclockStart(conflicthdlr->conflicttime, set);
654 
655  SCIP_CALL( conflicthdlr->conflictexec(set->scip, conflicthdlr, node, validnode, bdchginfos, relaxedbds, nbdchginfos,
656  conftype, usescutoffbound, set->conf_separate, (SCIPnodeGetDepth(validnode) > 0), set->conf_dynamic,
657  set->conf_removable, resolved, result) );
658 
659  /* stop timing */
660  SCIPclockStop(conflicthdlr->conflicttime, set);
661 
662  if( *result != SCIP_CONSADDED
663  && *result != SCIP_DIDNOTFIND
664  && *result != SCIP_DIDNOTRUN )
665  {
666  SCIPerrorMessage("execution method of conflict handler <%s> returned invalid result <%d>\n",
667  conflicthdlr->name, *result);
668  return SCIP_INVALIDRESULT;
669  }
670  }
671 
672  return SCIP_OKAY;
673 }
674 
675 /** gets user data of conflict handler */
677  SCIP_CONFLICTHDLR* conflicthdlr /**< conflict handler */
678  )
679 {
680  assert(conflicthdlr != NULL);
681 
682  return conflicthdlr->conflicthdlrdata;
683 }
684 
685 /** sets user data of conflict handler; user has to free old data in advance! */
687  SCIP_CONFLICTHDLR* conflicthdlr, /**< conflict handler */
688  SCIP_CONFLICTHDLRDATA* conflicthdlrdata /**< new conflict handler user data */
689  )
690 {
691  assert(conflicthdlr != NULL);
692 
693  conflicthdlr->conflicthdlrdata = conflicthdlrdata;
694 }
695 
696 /** set copy method of conflict handler */
698  SCIP_CONFLICTHDLR* conflicthdlr, /**< conflict handler */
699  SCIP_DECL_CONFLICTCOPY((*conflictcopy)) /**< copy method of the conflict handler */
700  )
701 {
702  assert(conflicthdlr != NULL);
703 
704  conflicthdlr->conflictcopy = conflictcopy;
705 }
706 
707 /** set destructor of conflict handler */
709  SCIP_CONFLICTHDLR* conflicthdlr, /**< conflict handler */
710  SCIP_DECL_CONFLICTFREE((*conflictfree)) /**< destructor of conflict handler */
711  )
712 {
713  assert(conflicthdlr != NULL);
714 
715  conflicthdlr->conflictfree = conflictfree;
716 }
717 
718 /** set initialization method of conflict handler */
720  SCIP_CONFLICTHDLR* conflicthdlr, /**< conflict handler */
721  SCIP_DECL_CONFLICTINIT((*conflictinit)) /**< initialization method conflict handler */
722  )
723 {
724  assert(conflicthdlr != NULL);
725 
726  conflicthdlr->conflictinit = conflictinit;
727 }
728 
729 /** set deinitialization method of conflict handler */
731  SCIP_CONFLICTHDLR* conflicthdlr, /**< conflict handler */
732  SCIP_DECL_CONFLICTEXIT((*conflictexit)) /**< deinitialization method conflict handler */
733  )
734 {
735  assert(conflicthdlr != NULL);
736 
737  conflicthdlr->conflictexit = conflictexit;
738 }
739 
740 /** set solving process initialization method of conflict handler */
742  SCIP_CONFLICTHDLR* conflicthdlr, /**< conflict handler */
743  SCIP_DECL_CONFLICTINITSOL((*conflictinitsol))/**< solving process initialization method of conflict handler */
744  )
745 {
746  assert(conflicthdlr != NULL);
747 
748  conflicthdlr->conflictinitsol = conflictinitsol;
749 }
750 
751 /** set solving process deinitialization method of conflict handler */
753  SCIP_CONFLICTHDLR* conflicthdlr, /**< conflict handler */
754  SCIP_DECL_CONFLICTEXITSOL((*conflictexitsol))/**< solving process deinitialization method of conflict handler */
755  )
756 {
757  assert(conflicthdlr != NULL);
758 
759  conflicthdlr->conflictexitsol = conflictexitsol;
760 }
761 
762 /** gets name of conflict handler */
764  SCIP_CONFLICTHDLR* conflicthdlr /**< conflict handler */
765  )
766 {
767  assert(conflicthdlr != NULL);
768 
769  return conflicthdlr->name;
770 }
771 
772 /** gets description of conflict handler */
774  SCIP_CONFLICTHDLR* conflicthdlr /**< conflict handler */
775  )
776 {
777  assert(conflicthdlr != NULL);
778 
779  return conflicthdlr->desc;
780 }
781 
782 /** gets priority of conflict handler */
784  SCIP_CONFLICTHDLR* conflicthdlr /**< conflict handler */
785  )
786 {
787  assert(conflicthdlr != NULL);
788 
789  return conflicthdlr->priority;
790 }
791 
792 /** sets priority of conflict handler */
794  SCIP_CONFLICTHDLR* conflicthdlr, /**< conflict handler */
795  SCIP_SET* set, /**< global SCIP settings */
796  int priority /**< new priority of the conflict handler */
797  )
798 {
799  assert(conflicthdlr != NULL);
800  assert(set != NULL);
801 
802  conflicthdlr->priority = priority;
803  set->conflicthdlrssorted = FALSE;
804 }
805 
806 /** is conflict handler initialized? */
808  SCIP_CONFLICTHDLR* conflicthdlr /**< conflict handler */
809  )
810 {
811  assert(conflicthdlr != NULL);
812 
813  return conflicthdlr->initialized;
814 }
815 
816 /** enables or disables all clocks of \p conflicthdlr, depending on the value of the flag */
818  SCIP_CONFLICTHDLR* conflicthdlr, /**< the conflict handler for which all clocks should be enabled or disabled */
819  SCIP_Bool enable /**< should the clocks of the conflict handler be enabled? */
820  )
821 {
822  assert(conflicthdlr != NULL);
823 
824  SCIPclockEnableOrDisable(conflicthdlr->setuptime, enable);
825  SCIPclockEnableOrDisable(conflicthdlr->conflicttime, enable);
826 }
827 
828 /** gets time in seconds used in this conflict handler for setting up for next stages */
830  SCIP_CONFLICTHDLR* conflicthdlr /**< conflict handler */
831  )
832 {
833  assert(conflicthdlr != NULL);
834 
835  return SCIPclockGetTime(conflicthdlr->setuptime);
836 }
837 
838 /** gets time in seconds used in this conflict handler */
840  SCIP_CONFLICTHDLR* conflicthdlr /**< conflict handler */
841  )
842 {
843  assert(conflicthdlr != NULL);
844 
845  return SCIPclockGetTime(conflicthdlr->conflicttime);
846 }
847 
848 /*
849  * Conflict LP Bound Changes
850  */
851 
852 
853 /** create conflict LP bound change data structure */
854 static
856  SCIP_LPBDCHGS** lpbdchgs, /**< pointer to store the conflict LP bound change data structure */
857  SCIP_SET* set, /**< global SCIP settings */
858  int ncols /**< number of columns */
859  )
860 {
861  SCIP_CALL( SCIPsetAllocBuffer(set, lpbdchgs) );
862 
863  SCIP_CALL( SCIPsetAllocBufferArray(set, &(*lpbdchgs)->bdchginds, ncols) );
864  SCIP_CALL( SCIPsetAllocBufferArray(set, &(*lpbdchgs)->bdchglbs, ncols) );
865  SCIP_CALL( SCIPsetAllocBufferArray(set, &(*lpbdchgs)->bdchgubs, ncols) );
866  SCIP_CALL( SCIPsetAllocBufferArray(set, &(*lpbdchgs)->bdchgcolinds, ncols) );
867  SCIP_CALL( SCIPsetAllocBufferArray(set, &(*lpbdchgs)->usedcols, ncols) );
868  BMSclearMemoryArray((*lpbdchgs)->usedcols, ncols);
869 
870  (*lpbdchgs)->nbdchgs = 0;
871 
872  return SCIP_OKAY;
873 }
874 
875 /** reset conflict LP bound change data structure */
876 static
878  SCIP_LPBDCHGS* lpbdchgs, /**< conflict LP bound change data structure */
879  int ncols /**< number of columns */
880  )
881 {
882  assert(lpbdchgs != NULL);
883 
884  BMSclearMemoryArray(lpbdchgs->usedcols, ncols);
885  lpbdchgs->nbdchgs = 0;
886 }
887 
888 /** free conflict LP bound change data structure */
889 static
891  SCIP_LPBDCHGS** lpbdchgs, /**< pointer to store the conflict LP bound change data structure */
892  SCIP_SET* set /**< global SCIP settings */
893  )
894 {
895  SCIPsetFreeBufferArray(set, &(*lpbdchgs)->usedcols);
896  SCIPsetFreeBufferArray(set, &(*lpbdchgs)->bdchgcolinds);
897  SCIPsetFreeBufferArray(set, &(*lpbdchgs)->bdchgubs);
898  SCIPsetFreeBufferArray(set, &(*lpbdchgs)->bdchglbs);
899  SCIPsetFreeBufferArray(set, &(*lpbdchgs)->bdchginds);
900 
901  SCIPsetFreeBuffer(set, lpbdchgs);
902 }
903 
904 /*
905  * Proof Sets
906  */
907 
908 /** return the char associated with the type of the variable */
909 static
911  SCIP_VAR* var /**< variable */
912  )
913 {
914  SCIP_VARTYPE vartype = SCIPvarGetType(var);
915 
916  return (!SCIPvarIsIntegral(var) ? 'C' :
917  (vartype == SCIP_VARTYPE_BINARY ? 'B' :
918  (vartype == SCIP_VARTYPE_INTEGER ? 'I' : 'M')));
919 }
920 
921 /** resets the data structure of a proofset */
922 static
924  SCIP_PROOFSET* proofset /**< proof set */
925  )
926 {
927  assert(proofset != NULL);
928 
929  proofset->nnz = 0;
930  proofset->rhs = 0.0;
931  proofset->validdepth = 0;
933 }
934 
935 /** creates a proofset */
936 static
938  SCIP_PROOFSET** proofset, /**< proof set */
939  BMS_BLKMEM* blkmem /**< block memory of transformed problem */
940  )
941 {
942  assert(proofset != NULL);
943 
944  SCIP_ALLOC( BMSallocBlockMemory(blkmem, proofset) );
945  (*proofset)->vals = NULL;
946  (*proofset)->inds = NULL;
947  (*proofset)->rhs = 0.0;
948  (*proofset)->nnz = 0;
949  (*proofset)->size = 0;
950  (*proofset)->validdepth = 0;
951  (*proofset)->conflicttype = SCIP_CONFTYPE_UNKNOWN;
952 
953  return SCIP_OKAY;
954 }
955 
956 /** creates and clears the proofset */
957 static
959  SCIP_CONFLICT* conflict, /**< conflict analysis data */
960  BMS_BLKMEM* blkmem /**< block memory of transformed problem */
961  )
962 {
963  assert(conflict != NULL);
964  assert(blkmem != NULL);
965 
966  SCIP_CALL( proofsetCreate(&conflict->proofset, blkmem) );
967 
968  return SCIP_OKAY;
969 }
970 
971 /** frees a proofset */
972 static
974  SCIP_PROOFSET** proofset, /**< proof set */
975  BMS_BLKMEM* blkmem /**< block memory */
976  )
977 {
978  assert(proofset != NULL);
979  assert(*proofset != NULL);
980  assert(blkmem != NULL);
981 
982  BMSfreeBlockMemoryArrayNull(blkmem, &(*proofset)->vals, (*proofset)->size);
983  BMSfreeBlockMemoryArrayNull(blkmem, &(*proofset)->inds, (*proofset)->size);
984  BMSfreeBlockMemory(blkmem, proofset);
985  (*proofset) = NULL;
986 }
987 
988 #ifdef SCIP_DEBUG
989 static
990 void proofsetPrint(
991  SCIP_PROOFSET* proofset,
992  SCIP_SET* set,
993  SCIP_PROB* transprob
994  )
995 {
996  SCIP_VAR** vars;
997  int i;
998 
999  assert(proofset != NULL);
1000 
1001  vars = SCIPprobGetVars(transprob);
1002  assert(vars != NULL);
1003 
1004  printf("proofset: ");
1005  for( i = 0; i < proofset->nnz; i++ )
1006  printf("%+.15g <%s> ", proofset->vals[i], SCIPvarGetName(vars[proofset->inds[i]]));
1007  printf(" <= %.15g\n", proofset->rhs);
1008 }
1009 #endif
1010 
1011 /** return the indices of variables in the proofset */
1012 static
1014  SCIP_PROOFSET* proofset /**< proof set */
1015  )
1016 {
1017  assert(proofset != NULL);
1018 
1019  return proofset->inds;
1020 }
1021 
1022 /** return coefficient of variable in the proofset with given probindex */
1023 static
1025  SCIP_PROOFSET* proofset /**< proof set */
1026  )
1027 {
1028  assert(proofset != NULL);
1029 
1030  return proofset->vals;
1031 }
1032 
1033 /** return the right-hand side if a proofset */
1034 static
1036  SCIP_PROOFSET* proofset /**< proof set */
1037  )
1038 {
1039  assert(proofset != NULL);
1040 
1041  return proofset->rhs;
1042 }
1043 
1044 /** returns the number of variables in the proofset */
1045 static
1047  SCIP_PROOFSET* proofset /**< proof set */
1048  )
1049 {
1050  assert(proofset != NULL);
1051 
1052  return proofset->nnz;
1053 }
1054 
1055 /** returns the number of variables in the proofset */
1056 static
1058  SCIP_PROOFSET* proofset /**< proof set */
1059  )
1060 {
1061  assert(proofset != NULL);
1062 
1063  return proofset->conflicttype;
1064 }
1065 
1066 /** adds given data as aggregation row to the proofset */
1067 static
1069  SCIP_PROOFSET* proofset, /**< proof set */
1070  BMS_BLKMEM* blkmem, /**< block memory */
1071  SCIP_Real* vals, /**< variable coefficients */
1072  int* inds, /**< variable array */
1073  int nnz, /**< size of variable and coefficient array */
1074  SCIP_Real rhs /**< right-hand side of the aggregation row */
1075  )
1076 {
1077  assert(proofset != NULL);
1078  assert(blkmem != NULL);
1079 
1080  if( proofset->size == 0 )
1081  {
1082  assert(proofset->vals == NULL);
1083  assert(proofset->inds == NULL);
1084 
1085  SCIP_ALLOC( BMSduplicateBlockMemoryArray(blkmem, &proofset->vals, vals, nnz) );
1086  SCIP_ALLOC( BMSduplicateBlockMemoryArray(blkmem, &proofset->inds, inds, nnz) );
1087 
1088  proofset->size = nnz;
1089  }
1090  else
1091  {
1092  int i;
1093 
1094  assert(proofset->vals != NULL);
1095  assert(proofset->inds != NULL);
1096 
1097  if( proofset->size < nnz )
1098  {
1099  SCIP_ALLOC( BMSreallocBlockMemoryArray(blkmem, &proofset->vals, proofset->size, nnz) );
1100  SCIP_ALLOC( BMSreallocBlockMemoryArray(blkmem, &proofset->inds, proofset->size, nnz) );
1101  proofset->size = nnz;
1102  }
1103 
1104  for( i = 0; i < nnz; i++ )
1105  {
1106  proofset->vals[i] = vals[i];
1107  proofset->inds[i] = inds[i];
1108  }
1109  }
1110 
1111  proofset->rhs = rhs;
1112  proofset->nnz = nnz;
1113 
1114  return SCIP_OKAY;
1115 }
1116 
1117 /** adds an aggregation row to the proofset */
1118 static
1120  SCIP_PROOFSET* proofset, /**< proof set */
1121  SCIP_SET* set, /**< global SCIP settings */
1122  BMS_BLKMEM* blkmem, /**< block memory */
1123  SCIP_AGGRROW* aggrrow /**< aggregation row to add */
1124  )
1125 {
1126  SCIP_Real* vals;
1127  int* inds;
1128  int nnz;
1129  int i;
1130 
1131  assert(proofset != NULL);
1132  assert(set != NULL);
1133 
1134  inds = SCIPaggrRowGetInds(aggrrow);
1135  assert(inds != NULL);
1136 
1137  nnz = SCIPaggrRowGetNNz(aggrrow);
1138  assert(nnz > 0);
1139 
1140  SCIP_CALL( SCIPsetAllocBufferArray(set, &vals, nnz) );
1141 
1142  for( i = 0; i < nnz; i++ )
1143  {
1144  vals[i] = SCIPaggrRowGetProbvarValue(aggrrow, inds[i]);
1145  }
1146 
1147  SCIP_CALL( proofsetAddSparseData(proofset, blkmem, vals, inds, nnz, SCIPaggrRowGetRhs(aggrrow)) );
1148 
1149  SCIPsetFreeBufferArray(set, &vals);
1150 
1151  return SCIP_OKAY;
1152 }
1153 
1154 /** Removes a given variable @p var from position @p pos from the proofset and updates the right-hand side according
1155  * to sign of the coefficient, i.e., rhs -= coef * bound, where bound = lb if coef >= 0 and bound = ub, otherwise.
1156  *
1157  * @note: The list of non-zero indices and coefficients will be updated by swapping the last non-zero index to @p pos.
1158  */
1159 static
1161  SCIP_PROOFSET* proofset,
1162  SCIP_SET* set,
1163  SCIP_VAR* var,
1164  int pos,
1165  SCIP_Bool* valid
1166  )
1167 {
1168  assert(proofset != NULL);
1169  assert(var != NULL);
1170  assert(pos >= 0 && pos < proofset->nnz);
1171  assert(valid != NULL);
1172 
1173  *valid = TRUE;
1174 
1175  /* cancel with lower bound */
1176  if( proofset->vals[pos] > 0.0 )
1177  {
1178  proofset->rhs -= proofset->vals[pos] * SCIPvarGetLbGlobal(var);
1179  }
1180  /* cancel with upper bound */
1181  else
1182  {
1183  assert(proofset->vals[pos] < 0.0);
1184  proofset->rhs -= proofset->vals[pos] * SCIPvarGetUbGlobal(var);
1185  }
1186 
1187  --proofset->nnz;
1188 
1189  proofset->vals[pos] = proofset->vals[proofset->nnz];
1190  proofset->inds[pos] = proofset->inds[proofset->nnz];
1191  proofset->vals[proofset->nnz] = 0.0;
1192  proofset->inds[proofset->nnz] = 0;
1193 
1194  if( SCIPsetIsInfinity(set, proofset->rhs) )
1195  *valid = FALSE;
1196 }
1197 
1198 /*
1199  * Conflict Sets
1200  */
1201 
1202 /** resizes the array of the temporary bound change informations to be able to store at least num bound change entries */
1203 static
1205  SCIP_CONFLICT* conflict, /**< conflict analysis data */
1206  SCIP_SET* set, /**< global SCIP settings */
1207  int num /**< minimal number of slots in arrays */
1208  )
1209 {
1210  assert(conflict != NULL);
1211  assert(set != NULL);
1212 
1213  if( num > conflict->tmpbdchginfossize )
1214  {
1215  int newsize;
1216 
1217  newsize = SCIPsetCalcMemGrowSize(set, num);
1218  SCIP_ALLOC( BMSreallocMemoryArray(&conflict->tmpbdchginfos, newsize) );
1219  conflict->tmpbdchginfossize = newsize;
1220  }
1221  assert(num <= conflict->tmpbdchginfossize);
1222 
1223  return SCIP_OKAY;
1224 }
1225 
1226 /** creates a temporary bound change information object that is destroyed after the conflict sets are flushed */
1227 static
1229  SCIP_CONFLICT* conflict, /**< conflict analysis data */
1230  BMS_BLKMEM* blkmem, /**< block memory */
1231  SCIP_SET* set, /**< global SCIP settings */
1232  SCIP_VAR* var, /**< active variable that changed the bounds */
1233  SCIP_BOUNDTYPE boundtype, /**< type of bound for var: lower or upper bound */
1234  SCIP_Real oldbound, /**< old value for bound */
1235  SCIP_Real newbound, /**< new value for bound */
1236  SCIP_BDCHGINFO** bdchginfo /**< pointer to store bound change information */
1237  )
1238 {
1239  assert(conflict != NULL);
1240 
1241  SCIP_CALL( conflictEnsureTmpbdchginfosMem(conflict, set, conflict->ntmpbdchginfos+1) );
1242  SCIP_CALL( SCIPbdchginfoCreate(&conflict->tmpbdchginfos[conflict->ntmpbdchginfos], blkmem,
1243  var, boundtype, oldbound, newbound) );
1244  *bdchginfo = conflict->tmpbdchginfos[conflict->ntmpbdchginfos];
1245  conflict->ntmpbdchginfos++;
1246 
1247  return SCIP_OKAY;
1248 }
1249 
1250 /** frees all temporarily created bound change information data */
1251 static
1253  SCIP_CONFLICT* conflict, /**< conflict analysis data */
1254  BMS_BLKMEM* blkmem /**< block memory */
1255  )
1256 {
1257  int i;
1258 
1259  assert(conflict != NULL);
1260 
1261  for( i = 0; i < conflict->ntmpbdchginfos; ++i )
1262  SCIPbdchginfoFree(&conflict->tmpbdchginfos[i], blkmem);
1263  conflict->ntmpbdchginfos = 0;
1264 }
1265 
1266 /** clears the given conflict set */
1267 static
1269  SCIP_CONFLICTSET* conflictset /**< conflict set */
1270  )
1271 {
1272  assert(conflictset != NULL);
1273 
1274  conflictset->nbdchginfos = 0;
1275  conflictset->validdepth = 0;
1276  conflictset->insertdepth = 0;
1277  conflictset->conflictdepth = 0;
1278  conflictset->repropdepth = 0;
1279  conflictset->repropagate = TRUE;
1280  conflictset->usescutoffbound = FALSE;
1281  conflictset->conflicttype = SCIP_CONFTYPE_UNKNOWN;
1282 }
1283 
1284 /** creates an empty conflict set */
1285 static
1287  SCIP_CONFLICTSET** conflictset, /**< pointer to store the conflict set */
1288  BMS_BLKMEM* blkmem /**< block memory of transformed problem */
1289  )
1290 {
1291  assert(conflictset != NULL);
1292 
1293  SCIP_ALLOC( BMSallocBlockMemory(blkmem, conflictset) );
1294  (*conflictset)->bdchginfos = NULL;
1295  (*conflictset)->relaxedbds = NULL;
1296  (*conflictset)->sortvals = NULL;
1297  (*conflictset)->bdchginfossize = 0;
1298 
1299  conflictsetClear(*conflictset);
1300 
1301  return SCIP_OKAY;
1302 }
1303 
1304 /** creates a copy of the given conflict set, allocating an additional amount of memory */
1305 static
1307  SCIP_CONFLICTSET** targetconflictset, /**< pointer to store the conflict set */
1308  BMS_BLKMEM* blkmem, /**< block memory of transformed problem */
1309  SCIP_CONFLICTSET* sourceconflictset, /**< source conflict set */
1310  int nadditionalelems /**< number of additional elements to allocate memory for */
1311  )
1312 {
1313  int targetsize;
1314 
1315  assert(targetconflictset != NULL);
1316  assert(sourceconflictset != NULL);
1317 
1318  targetsize = sourceconflictset->nbdchginfos + nadditionalelems;
1319  SCIP_ALLOC( BMSallocBlockMemory(blkmem, targetconflictset) );
1320  SCIP_ALLOC( BMSallocBlockMemoryArray(blkmem, &(*targetconflictset)->bdchginfos, targetsize) );
1321  SCIP_ALLOC( BMSallocBlockMemoryArray(blkmem, &(*targetconflictset)->relaxedbds, targetsize) );
1322  SCIP_ALLOC( BMSallocBlockMemoryArray(blkmem, &(*targetconflictset)->sortvals, targetsize) );
1323  (*targetconflictset)->bdchginfossize = targetsize;
1324 
1325  BMScopyMemoryArray((*targetconflictset)->bdchginfos, sourceconflictset->bdchginfos, sourceconflictset->nbdchginfos);
1326  BMScopyMemoryArray((*targetconflictset)->relaxedbds, sourceconflictset->relaxedbds, sourceconflictset->nbdchginfos);
1327  BMScopyMemoryArray((*targetconflictset)->sortvals, sourceconflictset->sortvals, sourceconflictset->nbdchginfos);
1328 
1329  (*targetconflictset)->nbdchginfos = sourceconflictset->nbdchginfos;
1330  (*targetconflictset)->validdepth = sourceconflictset->validdepth;
1331  (*targetconflictset)->insertdepth = sourceconflictset->insertdepth;
1332  (*targetconflictset)->conflictdepth = sourceconflictset->conflictdepth;
1333  (*targetconflictset)->repropdepth = sourceconflictset->repropdepth;
1334  (*targetconflictset)->usescutoffbound = sourceconflictset->usescutoffbound;
1335  (*targetconflictset)->conflicttype = sourceconflictset->conflicttype;
1336 
1337  return SCIP_OKAY;
1338 }
1339 
1340 /** frees a conflict set */
1341 static
1343  SCIP_CONFLICTSET** conflictset, /**< pointer to the conflict set */
1344  BMS_BLKMEM* blkmem /**< block memory of transformed problem */
1345  )
1346 {
1347  assert(conflictset != NULL);
1348  assert(*conflictset != NULL);
1349 
1350  BMSfreeBlockMemoryArrayNull(blkmem, &(*conflictset)->bdchginfos, (*conflictset)->bdchginfossize);
1351  BMSfreeBlockMemoryArrayNull(blkmem, &(*conflictset)->relaxedbds, (*conflictset)->bdchginfossize);
1352  BMSfreeBlockMemoryArrayNull(blkmem, &(*conflictset)->sortvals, (*conflictset)->bdchginfossize);
1353  BMSfreeBlockMemory(blkmem, conflictset);
1354 }
1355 
1356 /** resizes the arrays of the conflict set to be able to store at least num bound change entries */
1357 static
1359  SCIP_CONFLICTSET* conflictset, /**< conflict set */
1360  BMS_BLKMEM* blkmem, /**< block memory of transformed problem */
1361  SCIP_SET* set, /**< global SCIP settings */
1362  int num /**< minimal number of slots in arrays */
1363  )
1364 {
1365  assert(conflictset != NULL);
1366  assert(set != NULL);
1367 
1368  if( num > conflictset->bdchginfossize )
1369  {
1370  int newsize;
1371 
1372  newsize = SCIPsetCalcMemGrowSize(set, num);
1373  SCIP_ALLOC( BMSreallocBlockMemoryArray(blkmem, &conflictset->bdchginfos, conflictset->bdchginfossize, newsize) );
1374  SCIP_ALLOC( BMSreallocBlockMemoryArray(blkmem, &conflictset->relaxedbds, conflictset->bdchginfossize, newsize) );
1375  SCIP_ALLOC( BMSreallocBlockMemoryArray(blkmem, &conflictset->sortvals, conflictset->bdchginfossize, newsize) );
1376  conflictset->bdchginfossize = newsize;
1377  }
1378  assert(num <= conflictset->bdchginfossize);
1379 
1380  return SCIP_OKAY;
1381 }
1382 
1383 /** calculates the score of the conflict set
1384  *
1385  * the score is weighted sum of number of bound changes, repropagation depth, and valid depth
1386  */
1387 static
1389  SCIP_CONFLICTSET* conflictset, /**< conflict set */
1390  SCIP_SET* set /**< global SCIP settings */
1391  )
1392 {
1393  assert(conflictset != NULL);
1394 
1395  return -(set->conf_weightsize * conflictset->nbdchginfos
1396  + set->conf_weightrepropdepth * conflictset->repropdepth
1397  + set->conf_weightvaliddepth * conflictset->validdepth);
1398 }
1399 
1400 /** calculates the score of a bound change within a conflict */
1401 static
1403  SCIP_Real prooflhs, /**< lhs of proof constraint */
1404  SCIP_Real proofact, /**< activity of the proof constraint */
1405  SCIP_Real proofactdelta, /**< activity change */
1406  SCIP_Real proofcoef, /**< coefficient in proof constraint */
1407  int depth, /**< bound change depth */
1408  int currentdepth, /**< current depth */
1409  SCIP_VAR* var, /**< variable corresponding to bound change */
1410  SCIP_SET* set /**< global SCIP settings */
1411  )
1412 {
1413  SCIP_COL* col;
1414  SCIP_Real score;
1415 
1416  score = set->conf_proofscorefac * (1.0 - proofactdelta/(prooflhs - proofact));
1417  score = MAX(score, 0.0);
1418  score += set->conf_depthscorefac * (SCIP_Real)(depth+1)/(SCIP_Real)(currentdepth+1);
1419 
1421  col = SCIPvarGetCol(var);
1422  else
1423  col = NULL;
1424 
1425  if( proofcoef > 0.0 )
1426  {
1427  if( col != NULL && SCIPcolGetNNonz(col) > 0 )
1428  score += set->conf_uplockscorefac
1430  else
1431  score += set->conf_uplockscorefac * SCIPvarGetNLocksUpType(var, SCIP_LOCKTYPE_MODEL);
1432  }
1433  else
1434  {
1435  if( col != NULL && SCIPcolGetNNonz(col) > 0 )
1436  score += set->conf_downlockscorefac
1438  else
1439  score += set->conf_downlockscorefac * SCIPvarGetNLocksDownType(var, SCIP_LOCKTYPE_MODEL);
1440  }
1441 
1442  return score;
1443 }
1444 
1445 /** check if the bound change info (which is the potential next candidate which is queued) is valid for the current
1446  * conflict analysis; a bound change info can get invalid if after this one was added to the queue, a weaker bound
1447  * change was added to the queue (due the bound widening idea) which immediately makes this bound change redundant; due
1448  * to the priority we did not removed that bound change info since that cost O(log(n)); hence we have to skip/ignore it
1449  * now
1450  *
1451  * The following situations can occur before for example the bound change info (x >= 3) is potentially popped from the
1452  * queue.
1453  *
1454  * Postcondition: the reason why (x >= 3) was queued is that at this time point no lower bound of x was involved yet in
1455  * the current conflict or the lower bound which was involved until then was stronger, e.g., (x >= 2).
1456  *
1457  * 1) during the time until (x >= 3) gets potentially popped no weaker lower bound was added to the queue, in that case
1458  * the conflictlbcount is valid and conflictlb is 3; that is (var->conflictlbcount == conflict->count &&
1459  * var->conflictlb == 3)
1460  *
1461  * 2) a weaker bound change info gets queued (e.g., x >= 4); this bound change is popped before (x >= 3) since it has
1462  * higher priority (which is the time stamp of the bound change info and (x >= 4) has to be done after (x >= 3)
1463  * during propagation or branching)
1464  *
1465  * a) if (x >= 4) is popped and added to the conflict set the conflictlbcount is still valid and conflictlb is at
1466  * most 4; that is (var->conflictlbcount == conflict->count && var->conflictlb >= 4); it follows that any bound
1467  * change info which is stronger than (x >= 4) gets ignored (for example x >= 2)
1468  *
1469  * b) if (x >= 4) is popped and resolved without introducing a new lower bound on x until (x >= 3) is a potentially
1470  * candidate the conflictlbcount indicates that bound change is currently not present; that is
1471  * (var->conflictlbcount != conflict->count)
1472  *
1473  * c) if (x >= 4) is popped and resolved and a new lower bound on x (e.g., x >= 2) is introduced until (x >= 3) is
1474  * pooped, the conflictlbcount indicates that bound change is currently present; that is (var->conflictlbcount ==
1475  * conflict->count); however the (x >= 3) only has be explained if conflictlb matches that one; that is
1476  * (var->conflictlb == bdchginfo->newbound); otherwise it redundant/invalid.
1477  */
1478 static
1480  SCIP_CONFLICT* conflict, /**< conflict analysis data */
1481  SCIP_BDCHGINFO* bdchginfo /**< bound change information */
1482  )
1483 {
1484  SCIP_VAR* var;
1485 
1486  assert(bdchginfo != NULL);
1487 
1488  var = SCIPbdchginfoGetVar(bdchginfo);
1489  assert(var != NULL);
1490 
1491  /* the bound change info of a binary (domained) variable can never be invalid since the concepts of relaxed bounds
1492  * and bound widening do not make sense for these type of variables
1493  */
1494  if( SCIPvarIsBinary(var) )
1495  return FALSE;
1496 
1497  /* check if the bdchginfo is invaild since a tight/weaker bound change was already explained */
1499  {
1500  if( var->conflictlbcount != conflict->count || var->conflictlb != SCIPbdchginfoGetNewbound(bdchginfo) ) /*lint !e777*/
1501  {
1502  assert(!SCIPvarIsBinary(var));
1503  return TRUE;
1504  }
1505  }
1506  else
1507  {
1508  assert(SCIPbdchginfoGetBoundtype(bdchginfo) == SCIP_BOUNDTYPE_UPPER);
1509 
1510  if( var->conflictubcount != conflict->count || var->conflictub != SCIPbdchginfoGetNewbound(bdchginfo) ) /*lint !e777*/
1511  {
1512  assert(!SCIPvarIsBinary(var));
1513  return TRUE;
1514  }
1515  }
1516 
1517  return FALSE;
1518 }
1519 
1520 /** adds a bound change to a conflict set */
1521 static
1523  SCIP_CONFLICTSET* conflictset, /**< conflict set */
1524  BMS_BLKMEM* blkmem, /**< block memory of transformed problem */
1525  SCIP_SET* set, /**< global SCIP settings */
1526  SCIP_BDCHGINFO* bdchginfo, /**< bound change to add to the conflict set */
1527  SCIP_Real relaxedbd /**< relaxed bound */
1528  )
1529 {
1530  SCIP_BDCHGINFO** bdchginfos;
1531  SCIP_Real* relaxedbds;
1532  int* sortvals;
1533  SCIP_VAR* var;
1534  SCIP_BOUNDTYPE boundtype;
1535  int idx;
1536  int sortval;
1537  int pos;
1538 
1539  assert(conflictset != NULL);
1540  assert(bdchginfo != NULL);
1541 
1542  /* allocate memory for additional element */
1543  SCIP_CALL( conflictsetEnsureBdchginfosMem(conflictset, blkmem, set, conflictset->nbdchginfos+1) );
1544 
1545  /* insert the new bound change in the arrays sorted by increasing variable index and by bound type */
1546  bdchginfos = conflictset->bdchginfos;
1547  relaxedbds = conflictset->relaxedbds;
1548  sortvals = conflictset->sortvals;
1549  var = SCIPbdchginfoGetVar(bdchginfo);
1550  boundtype = SCIPbdchginfoGetBoundtype(bdchginfo);
1551  idx = SCIPvarGetIndex(var);
1552  assert(idx < INT_MAX/2);
1553  assert((int)boundtype == 0 || (int)boundtype == 1);
1554  sortval = 2*idx + (int)boundtype; /* first sorting criteria: variable index, second criteria: boundtype */
1555 
1556  /* insert new element into the sorted arrays; if an element exits with the same value insert the new element afterwards
1557  *
1558  * @todo check if it better (faster) to first search for the position O(log n) and compare the sort values and if
1559  * they are equal just replace the element and if not run the insert method O(n)
1560  */
1561 
1562  SCIPsortedvecInsertIntPtrReal(sortvals, (void**)bdchginfos, relaxedbds, sortval, (void*)bdchginfo, relaxedbd, &conflictset->nbdchginfos, &pos);
1563  assert(pos == conflictset->nbdchginfos - 1 || sortval < sortvals[pos+1]);
1564 
1565  /* merge multiple bound changes */
1566  if( pos > 0 && sortval == sortvals[pos-1] )
1567  {
1568  /* this is a multiple bound change */
1569  if( SCIPbdchginfoIsTighter(bdchginfo, bdchginfos[pos-1]) )
1570  {
1571  /* remove the "old" bound change since the "new" one in tighter */
1572  SCIPsortedvecDelPosIntPtrReal(sortvals, (void**)bdchginfos, relaxedbds, pos-1, &conflictset->nbdchginfos);
1573  }
1574  else if( SCIPbdchginfoIsTighter(bdchginfos[pos-1], bdchginfo) )
1575  {
1576  /* remove the "new" bound change since the "old" one is tighter */
1577  SCIPsortedvecDelPosIntPtrReal(sortvals, (void**)bdchginfos, relaxedbds, pos, &conflictset->nbdchginfos);
1578  }
1579  else
1580  {
1581  /* both bound change are equivalent; hence, keep the worse relaxed bound and remove one of them */
1582  relaxedbds[pos-1] = boundtype == SCIP_BOUNDTYPE_LOWER ? MAX(relaxedbds[pos-1], relaxedbd) : MIN(relaxedbds[pos-1], relaxedbd);
1583  SCIPsortedvecDelPosIntPtrReal(sortvals, (void**)bdchginfos, relaxedbds, pos, &conflictset->nbdchginfos);
1584  }
1585  }
1586 
1587  return SCIP_OKAY;
1588 }
1589 
1590 /** adds given bound changes to a conflict set */
1591 static
1593  SCIP_CONFLICT* conflict, /**< conflict analysis data */
1594  SCIP_CONFLICTSET* conflictset, /**< conflict set */
1595  BMS_BLKMEM* blkmem, /**< block memory of transformed problem */
1596  SCIP_SET* set, /**< global SCIP settings */
1597  SCIP_BDCHGINFO** bdchginfos, /**< bound changes to add to the conflict set */
1598  int nbdchginfos /**< number of bound changes to add */
1599  )
1600 {
1601  SCIP_BDCHGINFO** confbdchginfos;
1602  SCIP_BDCHGINFO* bdchginfo;
1603  SCIP_Real* confrelaxedbds;
1604  int* confsortvals;
1605  int confnbdchginfos;
1606  int idx;
1607  int sortval;
1608  int i;
1609  SCIP_BOUNDTYPE boundtype;
1610 
1611  assert(conflict != NULL);
1612  assert(conflictset != NULL);
1613  assert(blkmem != NULL);
1614  assert(set != NULL);
1615  assert(bdchginfos != NULL || nbdchginfos == 0);
1616 
1617  /* nothing to add */
1618  if( nbdchginfos == 0 )
1619  return SCIP_OKAY;
1620 
1621  assert(bdchginfos != NULL);
1622 
1623  /* only one element to add, use the single insertion method */
1624  if( nbdchginfos == 1 )
1625  {
1626  bdchginfo = bdchginfos[0];
1627  assert(bdchginfo != NULL);
1628 
1629  if( !bdchginfoIsInvalid(conflict, bdchginfo) )
1630  {
1631  SCIP_CALL( conflictsetAddBound(conflictset, blkmem, set, bdchginfo, SCIPbdchginfoGetRelaxedBound(bdchginfo)) );
1632  }
1633  else
1634  {
1635  SCIPsetDebugMsg(set, "-> bound change info [%d:<%s> %s %g] is invaild -> ignore it\n", SCIPbdchginfoGetDepth(bdchginfo),
1636  SCIPvarGetName(SCIPbdchginfoGetVar(bdchginfo)),
1637  SCIPbdchginfoGetBoundtype(bdchginfo) == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=",
1638  SCIPbdchginfoGetNewbound(bdchginfo));
1639  }
1640 
1641  return SCIP_OKAY;
1642  }
1643 
1644  confnbdchginfos = conflictset->nbdchginfos;
1645 
1646  /* allocate memory for additional element */
1647  SCIP_CALL( conflictsetEnsureBdchginfosMem(conflictset, blkmem, set, confnbdchginfos + nbdchginfos) );
1648 
1649  confbdchginfos = conflictset->bdchginfos;
1650  confrelaxedbds = conflictset->relaxedbds;
1651  confsortvals = conflictset->sortvals;
1652 
1653  assert(SCIP_BOUNDTYPE_LOWER == FALSE);/*lint !e641*/
1654  assert(SCIP_BOUNDTYPE_UPPER == TRUE);/*lint !e641*/
1655 
1656  for( i = 0; i < nbdchginfos; ++i )
1657  {
1658  bdchginfo = bdchginfos[i];
1659  assert(bdchginfo != NULL);
1660 
1661  /* add only valid bound change infos */
1662  if( !bdchginfoIsInvalid(conflict, bdchginfo) )
1663  {
1664  /* calculate sorting value */
1665  boundtype = SCIPbdchginfoGetBoundtype(bdchginfo);
1666  assert(SCIPbdchginfoGetVar(bdchginfo) != NULL);
1667 
1668  idx = SCIPvarGetIndex(SCIPbdchginfoGetVar(bdchginfo));
1669  assert(idx < INT_MAX/2);
1670 
1671  assert((int)boundtype == 0 || (int)boundtype == 1);
1672  sortval = 2*idx + (int)boundtype; /* first sorting criteria: variable index, second criteria: boundtype */
1673 
1674  /* add new element */
1675  confbdchginfos[confnbdchginfos] = bdchginfo;
1676  confrelaxedbds[confnbdchginfos] = SCIPbdchginfoGetRelaxedBound(bdchginfo);
1677  confsortvals[confnbdchginfos] = sortval;
1678  ++confnbdchginfos;
1679  }
1680  else
1681  {
1682  SCIPsetDebugMsg(set, "-> bound change info [%d:<%s> %s %g] is invaild -> ignore it\n", SCIPbdchginfoGetDepth(bdchginfo),
1683  SCIPvarGetName(SCIPbdchginfoGetVar(bdchginfo)),
1684  SCIPbdchginfoGetBoundtype(bdchginfo) == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=",
1685  SCIPbdchginfoGetNewbound(bdchginfo));
1686  }
1687  }
1688  assert(confnbdchginfos <= conflictset->nbdchginfos + nbdchginfos);
1689 
1690  /* sort and merge the new conflict set */
1691  if( confnbdchginfos > conflictset->nbdchginfos )
1692  {
1693  int k = 0;
1694 
1695  /* sort array */
1696  SCIPsortIntPtrReal(confsortvals, (void**)confbdchginfos, confrelaxedbds, confnbdchginfos);
1697 
1698  i = 1;
1699  /* merge multiple bound changes */
1700  while( i < confnbdchginfos )
1701  {
1702  assert(i > k);
1703 
1704  /* is this a multiple bound change */
1705  if( confsortvals[k] == confsortvals[i] )
1706  {
1707  if( SCIPbdchginfoIsTighter(confbdchginfos[k], confbdchginfos[i]) )
1708  ++i;
1709  else if( SCIPbdchginfoIsTighter(confbdchginfos[i], confbdchginfos[k]) )
1710  {
1711  /* replace worse bound change info by tighter bound change info */
1712  confbdchginfos[k] = confbdchginfos[i];
1713  confrelaxedbds[k] = confrelaxedbds[i];
1714  confsortvals[k] = confsortvals[i];
1715  ++i;
1716  }
1717  else
1718  {
1719  assert(confsortvals[k] == confsortvals[i]);
1720 
1721  /* both bound change are equivalent; hence, keep the worse relaxed bound and remove one of them */
1722  confrelaxedbds[k] = (confsortvals[k] % 2 == 0) ? MAX(confrelaxedbds[k], confrelaxedbds[i]) : MIN(confrelaxedbds[k], confrelaxedbds[i]);
1723  ++i;
1724  }
1725  }
1726  else
1727  {
1728  /* all bound change infos must be valid */
1729  assert(!bdchginfoIsInvalid(conflict, confbdchginfos[k]));
1730 
1731  ++k;
1732  /* move next comparison element to the correct position */
1733  if( k != i )
1734  {
1735  confbdchginfos[k] = confbdchginfos[i];
1736  confrelaxedbds[k] = confrelaxedbds[i];
1737  confsortvals[k] = confsortvals[i];
1738  }
1739  ++i;
1740  }
1741  }
1742  /* last bound change infos must also be valid */
1743  assert(!bdchginfoIsInvalid(conflict, confbdchginfos[k]));
1744  /* the number of bound change infos cannot be decreased, it would mean that the conflict set was not merged
1745  * before
1746  */
1747  assert(conflictset->nbdchginfos <= k + 1 );
1748  assert(k + 1 <= confnbdchginfos);
1749 
1750  conflictset->nbdchginfos = k + 1;
1751  }
1752 
1753  return SCIP_OKAY;
1754 }
1755 
1756 /** calculates the conflict and the repropagation depths of the conflict set */
1757 static
1759  SCIP_CONFLICTSET* conflictset /**< conflict set */
1760  )
1761 {
1762  int maxdepth[2];
1763  int i;
1764 
1765  assert(conflictset != NULL);
1766  assert(conflictset->validdepth <= conflictset->insertdepth);
1767 
1768  /* get the depth of the last and last but one bound change */
1769  maxdepth[0] = conflictset->validdepth;
1770  maxdepth[1] = conflictset->validdepth;
1771  for( i = 0; i < conflictset->nbdchginfos; ++i )
1772  {
1773  int depth;
1774 
1775  depth = SCIPbdchginfoGetDepth(conflictset->bdchginfos[i]);
1776  assert(depth >= 0);
1777  if( depth > maxdepth[0] )
1778  {
1779  maxdepth[1] = maxdepth[0];
1780  maxdepth[0] = depth;
1781  }
1782  else if( depth > maxdepth[1] )
1783  maxdepth[1] = depth;
1784  }
1785  assert(maxdepth[0] >= maxdepth[1]);
1786 
1787  conflictset->conflictdepth = maxdepth[0];
1788  conflictset->repropdepth = maxdepth[1];
1789 }
1790 
1791 /** identifies the depth, at which the conflict set should be added:
1792  * - if the branching rule operates on variables only, and if all branching variables up to a certain
1793  * depth level are member of the conflict, the conflict constraint can only be violated in the subtree
1794  * of the node at that depth, because in all other nodes, at least one of these branching variables
1795  * violates its conflicting bound, such that the conflict constraint is feasible
1796  * - if there is at least one branching variable in a node, we assume, that this branching was performed
1797  * on variables, and that the siblings of this node are disjunct w.r.t. the branching variables' fixings
1798  * - we have to add the conflict set at least in the valid depth of the initial conflict set,
1799  * so we start searching at the first branching after this depth level, i.e. validdepth+1
1800  */
1801 static
1803  SCIP_CONFLICTSET* conflictset, /**< conflict set */
1804  SCIP_SET* set, /**< global SCIP settings */
1805  SCIP_TREE* tree /**< branch and bound tree */
1806  )
1807 {
1808  SCIP_Bool* branchingincluded;
1809  int currentdepth;
1810  int i;
1811 
1812  assert(conflictset != NULL);
1813  assert(set != NULL);
1814  assert(tree != NULL);
1815 
1816  /* the conflict set must not be inserted prior to its valid depth */
1817  conflictset->insertdepth = conflictset->validdepth;
1818  assert(conflictset->insertdepth >= 0);
1819 
1820  currentdepth = SCIPtreeGetCurrentDepth(tree);
1821  assert(currentdepth == tree->pathlen-1);
1822 
1823  /* mark the levels for which a branching variable is included in the conflict set */
1824  SCIP_CALL( SCIPsetAllocBufferArray(set, &branchingincluded, currentdepth+2) );
1825  BMSclearMemoryArray(branchingincluded, currentdepth+2);
1826  for( i = 0; i < conflictset->nbdchginfos; ++i )
1827  {
1828  int depth;
1829 
1830  depth = SCIPbdchginfoGetDepth(conflictset->bdchginfos[i]);
1831  depth = MIN(depth, currentdepth+1); /* put diving/probing/strong branching changes in this depth level */
1832  branchingincluded[depth] = TRUE;
1833  }
1834 
1835  /* skip additional depth levels where branching on the conflict variables was applied */
1836  while( conflictset->insertdepth < currentdepth && branchingincluded[conflictset->insertdepth+1] )
1837  conflictset->insertdepth++;
1838 
1839  /* free temporary memory */
1840  SCIPsetFreeBufferArray(set, &branchingincluded);
1841 
1842  assert(conflictset->validdepth <= conflictset->insertdepth && conflictset->insertdepth <= currentdepth);
1843 
1844  return SCIP_OKAY;
1845 }
1846 
1847 /** checks whether the first conflict set is redundant to the second one */
1848 static
1850  SCIP_CONFLICTSET* conflictset1, /**< first conflict conflict set */
1851  SCIP_CONFLICTSET* conflictset2 /**< second conflict conflict set */
1852  )
1853 {
1854  int i1;
1855  int i2;
1856 
1857  assert(conflictset1 != NULL);
1858  assert(conflictset2 != NULL);
1859 
1860  /* if conflictset1 has smaller validdepth, it is definitely not redundant to conflictset2 */
1861  if( conflictset1->validdepth < conflictset2->validdepth )
1862  return FALSE;
1863 
1864  /* check, if all bound changes in conflictset2 are also present at least as tight in conflictset1;
1865  * we can stop immediately, if more bound changes are remaining in conflictset2 than in conflictset1
1866  */
1867  for( i1 = 0, i2 = 0; i2 < conflictset2->nbdchginfos && conflictset1->nbdchginfos - i1 >= conflictset2->nbdchginfos - i2;
1868  ++i1, ++i2 )
1869  {
1870  int sortval;
1871 
1872  assert(i2 == 0 || conflictset2->sortvals[i2-1] < conflictset2->sortvals[i2]);
1873 
1874  sortval = conflictset2->sortvals[i2];
1875  for( ; i1 < conflictset1->nbdchginfos && conflictset1->sortvals[i1] < sortval; ++i1 )
1876  {
1877  /* while scanning conflictset1, check consistency */
1878  assert(i1 == 0 || conflictset1->sortvals[i1-1] < conflictset1->sortvals[i1]);
1879  }
1880  if( i1 >= conflictset1->nbdchginfos || conflictset1->sortvals[i1] > sortval
1881  || SCIPbdchginfoIsTighter(conflictset2->bdchginfos[i2], conflictset1->bdchginfos[i1]) )
1882  return FALSE;
1883  }
1884 
1885  return (i2 == conflictset2->nbdchginfos);
1886 }
1887 
1888 #ifdef SCIP_DEBUG
1889 /** prints a conflict set to the screen */
1890 static
1891 void conflictsetPrint(
1892  SCIP_CONFLICTSET* conflictset /**< conflict set */
1893  )
1894 {
1895  int i;
1896 
1897  assert(conflictset != NULL);
1898  for( i = 0; i < conflictset->nbdchginfos; ++i )
1899  {
1900  SCIPdebugPrintf(" [%d:<%s> %s %g(%g)]", SCIPbdchginfoGetDepth(conflictset->bdchginfos[i]),
1901  SCIPvarGetName(SCIPbdchginfoGetVar(conflictset->bdchginfos[i])),
1902  SCIPbdchginfoGetBoundtype(conflictset->bdchginfos[i]) == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=",
1903  SCIPbdchginfoGetNewbound(conflictset->bdchginfos[i]), conflictset->relaxedbds[i]);
1904  }
1905  SCIPdebugPrintf("\n");
1906 }
1907 #endif
1908 
1909 /** resizes proofsets array to be able to store at least num entries */
1910 static
1912  SCIP_CONFLICT* conflict, /**< conflict analysis data */
1913  SCIP_SET* set, /**< global SCIP settings */
1914  int num /**< minimal number of slots in array */
1915  )
1916 {
1917  assert(conflict != NULL);
1918  assert(set != NULL);
1919 
1920  if( num > conflict->proofsetssize )
1921  {
1922  int newsize;
1923 
1924  newsize = SCIPsetCalcMemGrowSize(set, num);
1925  SCIP_ALLOC( BMSreallocMemoryArray(&conflict->proofsets, newsize) );
1926  conflict->proofsetssize = newsize;
1927  }
1928  assert(num <= conflict->proofsetssize);
1929 
1930  return SCIP_OKAY;
1931 }
1932 
1933 /** resizes conflictsets array to be able to store at least num entries */
1934 static
1936  SCIP_CONFLICT* conflict, /**< conflict analysis data */
1937  SCIP_SET* set, /**< global SCIP settings */
1938  int num /**< minimal number of slots in array */
1939  )
1940 {
1941  assert(conflict != NULL);
1942  assert(set != NULL);
1943 
1944  if( num > conflict->conflictsetssize )
1945  {
1946  int newsize;
1947 
1948  newsize = SCIPsetCalcMemGrowSize(set, num);
1949  SCIP_ALLOC( BMSreallocMemoryArray(&conflict->conflictsets, newsize) );
1950  SCIP_ALLOC( BMSreallocMemoryArray(&conflict->conflictsetscores, newsize) );
1951  conflict->conflictsetssize = newsize;
1952  }
1953  assert(num <= conflict->conflictsetssize);
1954 
1955  return SCIP_OKAY;
1956 }
1957 
1958 /** add a proofset to the list of all proofsets */
1959 static
1961  SCIP_CONFLICT* conflict, /**< conflict analysis data */
1962  SCIP_SET* set, /**< global SCIP settings */
1963  SCIP_PROOFSET* proofset /**< proof set to add */
1964  )
1965 {
1966  assert(conflict != NULL);
1967  assert(proofset != NULL);
1968 
1969  /* insert proofset into the sorted proofsets array */
1970  SCIP_CALL( conflictEnsureProofsetsMem(conflict, set, conflict->nproofsets + 1) );
1971 
1972  conflict->proofsets[conflict->nproofsets] = proofset;
1973  ++conflict->nproofsets;
1974 
1975  return SCIP_OKAY;
1976 }
1977 
1978 /** inserts conflict set into sorted conflictsets array and deletes the conflict set pointer */
1979 static
1981  SCIP_CONFLICT* conflict, /**< conflict analysis data */
1982  BMS_BLKMEM* blkmem, /**< block memory of transformed problem */
1983  SCIP_SET* set, /**< global SCIP settings */
1984  SCIP_CONFLICTSET** conflictset /**< pointer to conflict set to insert */
1985  )
1986 {
1987  SCIP_Real score;
1988  int pos;
1989  int i;
1990  int j;
1991 
1992  assert(conflict != NULL);
1993  assert(set != NULL);
1994  assert(conflictset != NULL);
1995  assert(*conflictset != NULL);
1996  assert((*conflictset)->validdepth <= (*conflictset)->insertdepth);
1997  assert(set->conf_allowlocal || (*conflictset)->validdepth == 0);
1998 
1999  /* calculate conflict and repropagation depth */
2000  conflictsetCalcConflictDepth(*conflictset);
2001 
2002  /* if we apply repropagations, the conflict set should be inserted at most at its repropdepth */
2003  if( set->conf_repropagate )
2004  (*conflictset)->insertdepth = MIN((*conflictset)->insertdepth, (*conflictset)->repropdepth);
2005  else
2006  (*conflictset)->repropdepth = INT_MAX;
2007  assert((*conflictset)->insertdepth <= (*conflictset)->repropdepth);
2008 
2009  SCIPsetDebugMsg(set, "inserting conflict set (valid: %d, insert: %d, conf: %d, reprop: %d):\n",
2010  (*conflictset)->validdepth, (*conflictset)->insertdepth, (*conflictset)->conflictdepth, (*conflictset)->repropdepth);
2011  SCIPdebug(conflictsetPrint(*conflictset));
2012 
2013  /* get the score of the conflict set */
2014  score = conflictsetCalcScore(*conflictset, set);
2015 
2016  /* check, if conflict set is redundant to a better conflict set */
2017  for( pos = 0; pos < conflict->nconflictsets && score < conflict->conflictsetscores[pos]; ++pos )
2018  {
2019  /* check if conflict set is redundant with respect to conflictsets[pos] */
2020  if( conflictsetIsRedundant(*conflictset, conflict->conflictsets[pos]) )
2021  {
2022  SCIPsetDebugMsg(set, " -> conflict set is redundant to: ");
2023  SCIPdebug(conflictsetPrint(conflict->conflictsets[pos]));
2024  conflictsetFree(conflictset, blkmem);
2025  return SCIP_OKAY;
2026  }
2027 
2028  /**@todo like in sepastore.c: calculate overlap between conflictsets -> large overlap reduces score */
2029  }
2030 
2031  /* insert conflictset into the sorted conflictsets array */
2032  SCIP_CALL( conflictEnsureConflictsetsMem(conflict, set, conflict->nconflictsets + 1) );
2033  for( i = conflict->nconflictsets; i > pos; --i )
2034  {
2035  assert(score >= conflict->conflictsetscores[i-1]);
2036  conflict->conflictsets[i] = conflict->conflictsets[i-1];
2037  conflict->conflictsetscores[i] = conflict->conflictsetscores[i-1];
2038  }
2039  conflict->conflictsets[pos] = *conflictset;
2040  conflict->conflictsetscores[pos] = score;
2041  conflict->nconflictsets++;
2042 
2043  /* remove worse conflictsets that are redundant to the new conflictset */
2044  for( i = pos+1, j = pos+1; i < conflict->nconflictsets; ++i )
2045  {
2046  if( conflictsetIsRedundant(conflict->conflictsets[i], *conflictset) )
2047  {
2048  SCIPsetDebugMsg(set, " -> conflict set dominates: ");
2049  SCIPdebug(conflictsetPrint(conflict->conflictsets[i]));
2050  conflictsetFree(&conflict->conflictsets[i], blkmem);
2051  }
2052  else
2053  {
2054  assert(j <= i);
2055  conflict->conflictsets[j] = conflict->conflictsets[i];
2056  conflict->conflictsetscores[j] = conflict->conflictsetscores[i];
2057  j++;
2058  }
2059  }
2060  assert(j <= conflict->nconflictsets);
2061  conflict->nconflictsets = j;
2062 
2063 #ifdef SCIP_CONFGRAPH
2064  confgraphMarkConflictset(*conflictset);
2065 #endif
2066 
2067  *conflictset = NULL; /* ownership of pointer is now in the conflictsets array */
2068 
2069  return SCIP_OKAY;
2070 }
2071 
2072 /** calculates the maximal size of conflict sets to be used */
2073 static
2075  SCIP_SET* set, /**< global SCIP settings */
2076  SCIP_PROB* prob /**< problem data */
2077  )
2078 {
2079  int maxsize;
2080 
2081  assert(set != NULL);
2082  assert(prob != NULL);
2083 
2084  maxsize = (int)(set->conf_maxvarsfac * (prob->nvars - prob->ncontvars));
2085  maxsize = MAX(maxsize, set->conf_minmaxvars);
2086 
2087  return maxsize;
2088 }
2089 
2090 /** increases the conflict score of the variable in the given direction */
2091 static
2093  SCIP_VAR* var, /**< problem variable */
2094  BMS_BLKMEM* blkmem, /**< block memory */
2095  SCIP_SET* set, /**< global SCIP settings */
2096  SCIP_STAT* stat, /**< dynamic problem statistics */
2097  SCIP_BOUNDTYPE boundtype, /**< type of bound for which the score should be increased */
2098  SCIP_Real value, /**< value of the bound */
2099  SCIP_Real weight /**< weight of this VSIDS updates */
2100  )
2101 {
2102  SCIP_BRANCHDIR branchdir;
2103 
2104  assert(var != NULL);
2105  assert(stat != NULL);
2106 
2107  /* weight the VSIDS by the given weight */
2108  weight *= stat->vsidsweight;
2109 
2110  if( SCIPsetIsZero(set, weight) )
2111  return SCIP_OKAY;
2112 
2113  branchdir = (boundtype == SCIP_BOUNDTYPE_LOWER ? SCIP_BRANCHDIR_UPWARDS : SCIP_BRANCHDIR_DOWNWARDS); /*lint !e641*/
2114  SCIP_CALL( SCIPvarIncVSIDS(var, blkmem, set, stat, branchdir, value, weight) );
2115  SCIPhistoryIncVSIDS(stat->glbhistory, branchdir, weight);
2116  SCIPhistoryIncVSIDS(stat->glbhistorycrun, branchdir, weight);
2117 
2118  return SCIP_OKAY;
2119 }
2120 
2121 /** update conflict statistics */
2122 static
2124  SCIP_CONFLICT* conflict, /**< conflict analysis data */
2125  BMS_BLKMEM* blkmem, /**< block memory */
2126  SCIP_SET* set, /**< global SCIP settings */
2127  SCIP_STAT* stat, /**< dynamic problem statistics */
2128  SCIP_CONFLICTSET* conflictset, /**< conflict set to add to the tree */
2129  int insertdepth /**< depth level at which the conflict set should be added */
2130  )
2131 {
2132  if( insertdepth > 0 )
2133  {
2134  conflict->nappliedlocconss++;
2135  conflict->nappliedlocliterals += conflictset->nbdchginfos;
2136  }
2137  else
2138  {
2139  int i;
2140  int conflictlength;
2141  conflictlength = conflictset->nbdchginfos;
2142 
2143  for( i = 0; i < conflictlength; i++ )
2144  {
2145  SCIP_VAR* var;
2146  SCIP_BRANCHDIR branchdir;
2147  SCIP_BOUNDTYPE boundtype;
2148  SCIP_Real bound;
2149 
2150  assert(stat != NULL);
2151 
2152  var = conflictset->bdchginfos[i]->var;
2153  boundtype = SCIPbdchginfoGetBoundtype(conflictset->bdchginfos[i]);
2154  bound = conflictset->relaxedbds[i];
2155 
2156  branchdir = (boundtype == SCIP_BOUNDTYPE_LOWER ? SCIP_BRANCHDIR_UPWARDS : SCIP_BRANCHDIR_DOWNWARDS); /*lint !e641*/
2157 
2158  SCIP_CALL( SCIPvarIncNActiveConflicts(var, blkmem, set, stat, branchdir, bound, (SCIP_Real)conflictlength) );
2159  SCIPhistoryIncNActiveConflicts(stat->glbhistory, branchdir, (SCIP_Real)conflictlength);
2160  SCIPhistoryIncNActiveConflicts(stat->glbhistorycrun, branchdir, (SCIP_Real)conflictlength);
2161 
2162  /* each variable which is part of the conflict gets an increase in the VSIDS */
2163  SCIP_CALL( incVSIDS(var, blkmem, set, stat, boundtype, bound, set->conf_conflictweight) );
2164  }
2165  conflict->nappliedglbconss++;
2166  conflict->nappliedglbliterals += conflictset->nbdchginfos;
2167  }
2168 
2169  return SCIP_OKAY;
2170 }
2171 
2172 
2173 /** check conflict set for redundancy, other conflicts in the same conflict analysis could have led to global reductions
2174  * an made this conflict set redundant
2175  */
2176 static
2178  SCIP_SET* set, /**< global SCIP settings */
2179  SCIP_CONFLICTSET* conflictset /**< conflict set */
2180  )
2181 {
2182  SCIP_BDCHGINFO** bdchginfos;
2183  SCIP_VAR* var;
2184  SCIP_Real* relaxedbds;
2185  SCIP_Real bound;
2186  int v;
2187 
2188  assert(set != NULL);
2189  assert(conflictset != NULL);
2190 
2191  bdchginfos = conflictset->bdchginfos;
2192  relaxedbds = conflictset->relaxedbds;
2193  assert(bdchginfos != NULL);
2194  assert(relaxedbds != NULL);
2195 
2196  /* check all boundtypes and bounds for redundancy */
2197  for( v = conflictset->nbdchginfos - 1; v >= 0; --v )
2198  {
2199  var = SCIPbdchginfoGetVar(bdchginfos[v]);
2200  assert(var != NULL);
2201  assert(SCIPvarGetProbindex(var) >= 0);
2202 
2203  /* check if the relaxed bound is really a relaxed bound */
2204  assert(SCIPbdchginfoGetBoundtype(bdchginfos[v]) == SCIP_BOUNDTYPE_LOWER || SCIPsetIsGE(set, relaxedbds[v], SCIPbdchginfoGetNewbound(bdchginfos[v])));
2205  assert(SCIPbdchginfoGetBoundtype(bdchginfos[v]) == SCIP_BOUNDTYPE_UPPER || SCIPsetIsLE(set, relaxedbds[v], SCIPbdchginfoGetNewbound(bdchginfos[v])));
2206 
2207  bound = relaxedbds[v];
2208 
2209  if( SCIPbdchginfoGetBoundtype(bdchginfos[v]) == SCIP_BOUNDTYPE_UPPER )
2210  {
2212  {
2213  assert(SCIPsetIsIntegral(set, bound));
2214  bound += 1.0;
2215  }
2216 
2217  /* check if the bound is already fulfilled globally */
2218  if( SCIPsetIsFeasGE(set, SCIPvarGetLbGlobal(var), bound) )
2219  return TRUE;
2220  }
2221  else
2222  {
2223  assert(SCIPbdchginfoGetBoundtype(bdchginfos[v]) == SCIP_BOUNDTYPE_LOWER);
2224 
2226  {
2227  assert(SCIPsetIsIntegral(set, bound));
2228  bound -= 1.0;
2229  }
2230 
2231  /* check if the bound is already fulfilled globally */
2232  if( SCIPsetIsFeasLE(set, SCIPvarGetUbGlobal(var), bound) )
2233  return TRUE;
2234  }
2235  }
2236 
2237  return FALSE;
2238 }
2239 
2240 /** find global fixings which can be derived from the new conflict set */
2241 static
2243  SCIP_SET* set, /**< global SCIP settings */
2244  SCIP_PROB* prob, /**< transformed problem after presolve */
2245  SCIP_CONFLICTSET* conflictset, /**< conflict set to add to the tree */
2246  int* nbdchgs, /**< number of global deducted bound changes due to the conflict set */
2247  int* nredvars, /**< number of redundant and removed variables from conflict set */
2248  SCIP_Bool* redundant /**< did we found a global reduction on a conflict set variable, which makes this conflict redundant */
2249  )
2250 {
2251  SCIP_BDCHGINFO** bdchginfos;
2252  SCIP_Real* relaxedbds;
2253  SCIP_VAR* var;
2254  SCIP_Bool* boundtypes;
2255  SCIP_Real* bounds;
2256  SCIP_Longint* nbinimpls;
2257  int* sortvals;
2258  SCIP_Real bound;
2259  SCIP_Bool isupper;
2260  int ntrivialredvars;
2261  int nbdchginfos;
2262  int nzeroimpls;
2263  int v;
2264 
2265  assert(set != NULL);
2266  assert(prob != NULL);
2267  assert(SCIPprobIsTransformed(prob));
2268  assert(conflictset != NULL);
2269  assert(nbdchgs != NULL);
2270  assert(nredvars != NULL);
2271  /* only check conflict sets with more than one variable */
2272  assert(conflictset->nbdchginfos > 1);
2273 
2274  *nbdchgs = 0;
2275  *nredvars = 0;
2276 
2277  /* due to other conflict in the same conflict analysis, this conflict set might have become redundant */
2278  *redundant = checkRedundancy(set, conflictset);
2279 
2280  if( *redundant )
2281  return SCIP_OKAY;
2282 
2283  bdchginfos = conflictset->bdchginfos;
2284  relaxedbds = conflictset->relaxedbds;
2285  nbdchginfos = conflictset->nbdchginfos;
2286  sortvals = conflictset->sortvals;
2287 
2288  assert(bdchginfos != NULL);
2289  assert(relaxedbds != NULL);
2290  assert(sortvals != NULL);
2291 
2292  /* check if the boolean representation of boundtypes matches the 'standard' definition */
2293  assert(SCIP_BOUNDTYPE_LOWER == FALSE); /*lint !e641*/
2294  assert(SCIP_BOUNDTYPE_UPPER == TRUE); /*lint !e641*/
2295 
2296  ntrivialredvars = 0;
2297 
2298  /* due to multiple conflict sets for one conflict, it can happen, that we already have redundant information in the
2299  * conflict set
2300  */
2301  for( v = nbdchginfos - 1; v >= 0; --v )
2302  {
2303  var = SCIPbdchginfoGetVar(bdchginfos[v]);
2304  bound = relaxedbds[v];
2305  isupper = (SCIP_Bool) SCIPboundtypeOpposite(SCIPbdchginfoGetBoundtype(bdchginfos[v]));
2306 
2307  /* for integral variable we can increase/decrease the conflicting bound */
2308  if( SCIPvarIsIntegral(var) )
2309  bound += (isupper ? -1.0 : +1.0);
2310 
2311  /* if conflict variable cannot fulfill the conflict we can remove it */
2312  if( (isupper && SCIPsetIsFeasLT(set, bound, SCIPvarGetLbGlobal(var))) ||
2313  (!isupper && SCIPsetIsFeasGT(set, bound, SCIPvarGetUbGlobal(var))) )
2314  {
2315  SCIPsetDebugMsg(set, "remove redundant variable <%s> from conflict set\n", SCIPvarGetName(var));
2316 
2317  bdchginfos[v] = bdchginfos[nbdchginfos - 1];
2318  relaxedbds[v] = relaxedbds[nbdchginfos - 1];
2319  sortvals[v] = sortvals[nbdchginfos - 1];
2320 
2321  --nbdchginfos;
2322  ++ntrivialredvars;
2323  }
2324  }
2325  assert(ntrivialredvars + nbdchginfos == conflictset->nbdchginfos);
2326 
2327  SCIPsetDebugMsg(set, "trivially removed %d redundant of %d variables from conflictset (%p)\n", ntrivialredvars, conflictset->nbdchginfos, (void*)conflictset);
2328  conflictset->nbdchginfos = nbdchginfos;
2329 
2330  /* all variables where removed, the conflict cannot be fulfilled, i.e., we have an infeasibility proof */
2331  if( conflictset->nbdchginfos == 0 )
2332  return SCIP_OKAY;
2333 
2334  /* do not check to big or trivial conflicts */
2335  if( conflictset->nbdchginfos > set->conf_maxvarsdetectimpliedbounds || conflictset->nbdchginfos == 1 )
2336  {
2337  *nredvars = ntrivialredvars;
2338  return SCIP_OKAY;
2339  }
2340 
2341  /* create array of boundtypes, and bound values in conflict set */
2342  SCIP_CALL( SCIPsetAllocBufferArray(set, &boundtypes, nbdchginfos) );
2343  SCIP_CALL( SCIPsetAllocBufferArray(set, &bounds, nbdchginfos) );
2344  /* memory for the estimates for binary implications used for sorting */
2345  SCIP_CALL( SCIPsetAllocBufferArray(set, &nbinimpls, nbdchginfos) );
2346 
2347  nzeroimpls = 0;
2348 
2349  /* collect estimates and initialize variables, boundtypes, and bounds array */
2350  for( v = 0; v < nbdchginfos; ++v )
2351  {
2352  var = SCIPbdchginfoGetVar(bdchginfos[v]);
2353  boundtypes[v] = (SCIP_Bool) SCIPboundtypeOpposite(SCIPbdchginfoGetBoundtype(bdchginfos[v]));
2354  bounds[v] = relaxedbds[v];
2355 
2356  assert(SCIPvarGetProbindex(var) >= 0);
2357 
2358  /* check if the relaxed bound is really a relaxed bound */
2359  assert(SCIPbdchginfoGetBoundtype(bdchginfos[v]) == SCIP_BOUNDTYPE_LOWER || SCIPsetIsGE(set, relaxedbds[v], SCIPbdchginfoGetNewbound(bdchginfos[v])));
2360  assert(SCIPbdchginfoGetBoundtype(bdchginfos[v]) == SCIP_BOUNDTYPE_UPPER || SCIPsetIsLE(set, relaxedbds[v], SCIPbdchginfoGetNewbound(bdchginfos[v])));
2361 
2362  /* for continuous variables, we can only use the relaxed version of the bounds negation: !(x <= u) -> x >= u */
2363  if( SCIPvarIsBinary(var) )
2364  {
2365  if( !boundtypes[v] )
2366  {
2367  assert(SCIPsetIsZero(set, bounds[v]));
2368  bounds[v] = 1.0;
2369  nbinimpls[v] = (SCIP_Longint)SCIPvarGetNCliques(var, TRUE) * 2;
2370  }
2371  else
2372  {
2373  assert(SCIPsetIsEQ(set, bounds[v], 1.0));
2374  bounds[v] = 0.0;
2375  nbinimpls[v] = (SCIP_Longint)SCIPvarGetNCliques(var, FALSE) * 2;
2376  }
2377  }
2378  else if( SCIPvarIsIntegral(var) )
2379  {
2380  assert(SCIPsetIsIntegral(set, bounds[v]));
2381 
2382  bounds[v] += ((!boundtypes[v]) ? +1.0 : -1.0);
2383  nbinimpls[v] = (boundtypes[v] ? SCIPvarGetNVlbs(var) : SCIPvarGetNVubs(var));
2384  }
2385  else if( ((!boundtypes[v]) && SCIPsetIsFeasEQ(set, SCIPvarGetLbGlobal(var), bounds[v]))
2386  || ((boundtypes[v]) && SCIPsetIsFeasEQ(set, SCIPvarGetUbGlobal(var), bounds[v])) )
2387  {
2388  /* the literal is satisfied in global bounds (may happen due to weak "negation" of continuous variables)
2389  * -> discard the conflict constraint
2390  */
2391  break;
2392  }
2393  else
2394  {
2395  nbinimpls[v] = (boundtypes[v] ? SCIPvarGetNVlbs(var) : SCIPvarGetNVubs(var));
2396  }
2397 
2398  if( nbinimpls[v] == 0 )
2399  ++nzeroimpls;
2400  }
2401 
2402  /* starting to derive global bound changes */
2403  if( v == nbdchginfos && ((!set->conf_fullshortenconflict && nzeroimpls < 2) || (set->conf_fullshortenconflict && nzeroimpls < nbdchginfos)) )
2404  {
2405  SCIP_VAR** vars;
2406  SCIP_Bool* redundants;
2407  SCIP_Bool glbinfeas;
2408 
2409  /* sort variables in increasing order of binary implications to gain speed later on */
2410  SCIPsortLongPtrRealRealBool(nbinimpls, (void**)bdchginfos, relaxedbds, bounds, boundtypes, v);
2411 
2412  SCIPsetDebugMsg(set, "checking for global reductions and redundant conflict variables(in %s) on conflict:\n", SCIPprobGetName(prob));
2413  SCIPsetDebugMsg(set, "[");
2414  for( v = 0; v < nbdchginfos; ++v )
2415  {
2416  SCIPsetDebugMsgPrint(set, "%s %s %g", SCIPvarGetName(SCIPbdchginfoGetVar(bdchginfos[v])), (!boundtypes[v]) ? ">=" : "<=", bounds[v]);
2417  if( v < nbdchginfos - 1 )
2418  SCIPsetDebugMsgPrint(set, ", ");
2419  }
2420  SCIPsetDebugMsgPrint(set, "]\n");
2421 
2422  SCIP_CALL( SCIPsetAllocBufferArray(set, &vars, v) );
2423  SCIP_CALL( SCIPsetAllocCleanBufferArray(set, &redundants, v) );
2424 
2425  /* initialize conflict variable data */
2426  for( v = 0; v < nbdchginfos; ++v )
2427  vars[v] = SCIPbdchginfoGetVar(bdchginfos[v]);
2428 
2429  SCIP_CALL( SCIPshrinkDisjunctiveVarSet(set->scip, vars, bounds, boundtypes, redundants, nbdchginfos, nredvars, \
2430  nbdchgs, redundant, &glbinfeas, set->conf_fullshortenconflict) );
2431 
2432  if( glbinfeas )
2433  {
2434  SCIPsetDebugMsg(set, "conflict set (%p) led to global infeasibility\n", (void*) conflictset);
2435  goto TERMINATE;
2436  }
2437 
2438 #ifdef SCIP_DEBUG
2439  if( *nbdchgs > 0 )
2440  {
2441  SCIPsetDebugMsg(set, "conflict set (%p) led to %d global bound reductions\n", (void*) conflictset, *nbdchgs);
2442  }
2443 #endif
2444 
2445  /* remove as redundant marked variables */
2446  if( *redundant )
2447  {
2448  SCIPsetDebugMsg(set, "conflict set (%p) is redundant because at least one global reduction, fulfills the conflict constraint\n", (void*)conflictset);
2449 
2450  /* clear the memory array before freeing it */
2451  BMSclearMemoryArray(redundants, nbdchginfos);
2452  }
2453  else if( *nredvars > 0 )
2454  {
2455  assert(bdchginfos == conflictset->bdchginfos);
2456  assert(relaxedbds == conflictset->relaxedbds);
2457  assert(sortvals == conflictset->sortvals);
2458 
2459  for( v = nbdchginfos - 1; v >= 0; --v )
2460  {
2461  /* if conflict variable was marked to be redundant remove it */
2462  if( redundants[v] )
2463  {
2464  SCIPsetDebugMsg(set, "remove redundant variable <%s> from conflict set\n", SCIPvarGetName(SCIPbdchginfoGetVar(bdchginfos[v])));
2465 
2466  bdchginfos[v] = bdchginfos[nbdchginfos - 1];
2467  relaxedbds[v] = relaxedbds[nbdchginfos - 1];
2468  sortvals[v] = sortvals[nbdchginfos - 1];
2469 
2470  /* reset redundants[v] to 0 */
2471  redundants[v] = 0;
2472 
2473  --nbdchginfos;
2474  }
2475  }
2476  assert((*nredvars) + nbdchginfos == conflictset->nbdchginfos);
2477 
2478  SCIPsetDebugMsg(set, "removed %d redundant of %d variables from conflictset (%p)\n", (*nredvars), conflictset->nbdchginfos, (void*)conflictset);
2479  conflictset->nbdchginfos = nbdchginfos;
2480  }
2481  else
2482  {
2483  /* clear the memory array before freeing it */
2484  BMSclearMemoryArray(redundants, nbdchginfos);
2485  }
2486 
2487  TERMINATE:
2488  SCIPsetFreeCleanBufferArray(set, &redundants);
2489  SCIPsetFreeBufferArray(set, &vars);
2490  }
2491 
2492  /* free temporary memory */
2493  SCIPsetFreeBufferArray(set, &nbinimpls);
2494  SCIPsetFreeBufferArray(set, &bounds);
2495  SCIPsetFreeBufferArray(set, &boundtypes);
2496 
2497  *nredvars += ntrivialredvars;
2498 
2499  return SCIP_OKAY;
2500 }
2501 
2502 /** tighten the bound of a singleton variable in a constraint
2503  *
2504  * if the bound is contradicting with a global bound we cannot tighten the bound directly.
2505  * in this case we need to create and add a constraint of size one such that propagating this constraint will
2506  * enforce the infeasibility.
2507  */
2508 static
2510  SCIP_CONFLICT* conflict, /**< conflict analysis data */
2511  SCIP_SET* set, /**< global SCIP settings */
2512  SCIP_STAT* stat, /**< dynamic SCIP statistics */
2513  SCIP_TREE* tree, /**< tree data */
2514  BMS_BLKMEM* blkmem, /**< block memory */
2515  SCIP_PROB* origprob, /**< original problem */
2516  SCIP_PROB* transprob, /**< transformed problem */
2517  SCIP_REOPT* reopt, /**< reoptimization data */
2518  SCIP_LP* lp, /**< LP data */
2519  SCIP_BRANCHCAND* branchcand, /**< branching candidates */
2520  SCIP_EVENTQUEUE* eventqueue, /**< event queue */
2521  SCIP_CLIQUETABLE* cliquetable, /**< clique table */
2522  SCIP_VAR* var, /**< problem variable */
2523  SCIP_Real val, /**< coefficient of the variable */
2524  SCIP_Real rhs, /**< rhs of the constraint */
2525  SCIP_CONFTYPE prooftype, /**< type of the proof */
2526  int validdepth /**< depth where the bound change is valid */
2527  )
2528 {
2529  SCIP_Real newbound;
2530  SCIP_Bool applyglobal;
2531  SCIP_BOUNDTYPE boundtype;
2532 
2533  assert(tree != NULL);
2534  assert(validdepth >= 0);
2535 
2536  applyglobal = (validdepth <= SCIPtreeGetEffectiveRootDepth(tree));
2537 
2538  /* if variable and coefficient are integral the rhs can be rounded down */
2539  if( SCIPvarIsIntegral(var) && SCIPsetIsIntegral(set, val) )
2540  newbound = SCIPsetFeasFloor(set, rhs)/val;
2541  else
2542  newbound = rhs/val;
2543 
2544  boundtype = (val > 0.0 ? SCIP_BOUNDTYPE_UPPER : SCIP_BOUNDTYPE_LOWER);
2545  SCIPvarAdjustBd(var, set, boundtype, &newbound);
2546 
2547  /* skip numerical unstable bound changes */
2548  if( applyglobal
2549  && ((boundtype == SCIP_BOUNDTYPE_LOWER && SCIPsetIsLE(set, newbound, SCIPvarGetLbGlobal(var)))
2550  || (boundtype == SCIP_BOUNDTYPE_UPPER && SCIPsetIsGE(set, newbound, SCIPvarGetUbGlobal(var)))) )
2551  {
2552  return SCIP_OKAY;
2553  }
2554 
2555  /* the new bound contradicts a global bound, we can cutoff the root node immediately */
2556  if( applyglobal
2557  && ((boundtype == SCIP_BOUNDTYPE_LOWER && SCIPsetIsGT(set, newbound, SCIPvarGetUbGlobal(var)))
2558  || (boundtype == SCIP_BOUNDTYPE_UPPER && SCIPsetIsLT(set, newbound, SCIPvarGetLbGlobal(var)))) )
2559  {
2560  SCIPsetDebugMsg(set, "detected global infeasibility at var <%s>: locdom=[%g,%g] glbdom=[%g,%g] new %s bound=%g\n",
2561  SCIPvarGetName(var), SCIPvarGetLbLocal(var),
2563  (boundtype == SCIP_BOUNDTYPE_LOWER ? "lower" : "upper"), newbound);
2564  SCIP_CALL( SCIPnodeCutoff(tree->path[0], set, stat, tree, transprob, origprob, reopt, lp, blkmem) );
2565  }
2566  else
2567  {
2568  if( lp->strongbranching || !applyglobal )
2569  {
2570  SCIP_CONS* cons;
2571  SCIP_Real conslhs;
2572  SCIP_Real consrhs;
2573  char name[SCIP_MAXSTRLEN];
2574 
2575  SCIPsetDebugMsg(set, "add constraint <%s>[%c] %s %g to node #%lld in depth %d\n",
2576  SCIPvarGetName(var), varGetChar(var), boundtype == SCIP_BOUNDTYPE_UPPER ? "<=" : ">=", newbound,
2577  SCIPnodeGetNumber(tree->path[validdepth]), validdepth);
2578 
2579  (void)SCIPsnprintf(name, SCIP_MAXSTRLEN, "pc_fix_%s", SCIPvarGetName(var));
2580 
2581  if( boundtype == SCIP_BOUNDTYPE_UPPER )
2582  {
2583  conslhs = -SCIPsetInfinity(set);
2584  consrhs = newbound;
2585  }
2586  else
2587  {
2588  conslhs = newbound;
2589  consrhs = SCIPsetInfinity(set);
2590  }
2591 
2592  SCIP_CALL( SCIPcreateConsLinear(set->scip, &cons, name, 0, NULL, NULL, conslhs, consrhs,
2594 
2595  SCIP_CALL( SCIPaddCoefLinear(set->scip, cons, var, 1.0) );
2596 
2597  if( applyglobal )
2598  {
2599  SCIP_CALL( SCIPprobAddCons(transprob, set, stat, cons) );
2600  }
2601  else
2602  {
2603  SCIP_CALL( SCIPnodeAddCons(tree->path[validdepth], blkmem, set, stat, tree, cons) );
2604  }
2605 
2606  SCIP_CALL( SCIPconsRelease(&cons, blkmem, set) );
2607  }
2608  else
2609  {
2610  assert(applyglobal);
2611 
2612  SCIPsetDebugMsg(set, "change global %s bound of <%s>[%c]: %g -> %g\n",
2613  (boundtype == SCIP_BOUNDTYPE_LOWER ? "lower" : "upper"),
2614  SCIPvarGetName(var), varGetChar(var),
2615  (boundtype == SCIP_BOUNDTYPE_LOWER ? SCIPvarGetLbGlobal(var) : SCIPvarGetUbGlobal(var)),
2616  newbound);
2617 
2618  SCIP_CALL( SCIPnodeAddBoundchg(tree->path[0], blkmem, set, stat, transprob, origprob, tree, reopt, lp, branchcand, \
2619  eventqueue, cliquetable, var, newbound, boundtype, FALSE) );
2620 
2621  /* mark the node in the validdepth to be propagated again */
2622  SCIPnodePropagateAgain(tree->path[0], set, stat, tree);
2623  }
2624  }
2625 
2626  if( applyglobal )
2627  ++conflict->nglbchgbds;
2628  else
2629  ++conflict->nlocchgbds;
2630 
2631  if( prooftype == SCIP_CONFTYPE_INFEASLP || prooftype == SCIP_CONFTYPE_ALTINFPROOF )
2632  {
2633  ++conflict->dualproofsinfnnonzeros; /* we count a global bound reduction as size 1 */
2634  ++conflict->ndualproofsinfsuccess;
2635  ++conflict->ninflpsuccess;
2636 
2637  if( applyglobal )
2638  ++conflict->ndualproofsinfglobal;
2639  else
2640  ++conflict->ndualproofsinflocal;
2641  }
2642  else
2643  {
2644  ++conflict->dualproofsbndnnonzeros; /* we count a global bound reduction as size 1 */
2645  ++conflict->ndualproofsbndsuccess;
2646  ++conflict->nboundlpsuccess;
2647 
2648  if( applyglobal )
2649  ++conflict->ndualproofsbndglobal;
2650  else
2651  ++conflict->ndualproofsbndlocal;
2652  }
2653 
2654  return SCIP_OKAY;
2655 }
2656 
2657 /** calculates the minimal activity of a given aggregation row */
2658 static
2660  SCIP_SET* set, /**< global SCIP settings */
2661  SCIP_PROB* transprob, /**< transformed problem data */
2662  SCIP_AGGRROW* aggrrow, /**< aggregation row */
2663  SCIP_Real* curvarlbs, /**< current lower bounds of active problem variables (or NULL for global bounds) */
2664  SCIP_Real* curvarubs, /**< current upper bounds of active problem variables (or NULL for global bounds) */
2665  SCIP_Bool* infdelta /**< pointer to store whether at least one variable contributes with an infinite value */
2666  )
2667 {
2668  SCIP_VAR** vars;
2669  SCIP_Real QUAD(minact);
2670  int* inds;
2671  int nnz;
2672  int i;
2673 
2674  vars = SCIPprobGetVars(transprob);
2675  assert(vars != NULL);
2676 
2677  nnz = SCIPaggrRowGetNNz(aggrrow);
2678  inds = SCIPaggrRowGetInds(aggrrow);
2679 
2680  QUAD_ASSIGN(minact, 0.0);
2681 
2682  if( infdelta != NULL )
2683  *infdelta = FALSE;
2684 
2685  for( i = 0; i < nnz; i++ )
2686  {
2687  SCIP_Real val;
2688  SCIP_Real QUAD(delta);
2689  int v = inds[i];
2690 
2691  assert(SCIPvarGetProbindex(vars[v]) == v);
2692 
2693  val = SCIPaggrRowGetProbvarValue(aggrrow, v);
2694 
2695  if( val > 0.0 )
2696  {
2697  SCIP_Real bnd = (curvarlbs == NULL ? SCIPvarGetLbGlobal(vars[v]) : curvarlbs[v]);
2698  SCIPquadprecProdDD(delta, val, bnd);
2699  }
2700  else
2701  {
2702  SCIP_Real bnd = (curvarubs == NULL ? SCIPvarGetUbGlobal(vars[v]) : curvarubs[v]);
2703  SCIPquadprecProdDD(delta, val, bnd);
2704  }
2705 
2706  /* update minimal activity */
2707  SCIPquadprecSumQQ(minact, minact, delta);
2708 
2709  if( infdelta != NULL && SCIPsetIsInfinity(set, REALABS(QUAD_TO_DBL(delta))) )
2710  {
2711  *infdelta = TRUE;
2712  goto TERMINATE;
2713  }
2714  }
2715 
2716  TERMINATE:
2717  /* check whether the minimal activity is infinite */
2718  if( SCIPsetIsInfinity(set, QUAD_TO_DBL(minact)) )
2719  return SCIPsetInfinity(set);
2720  if( SCIPsetIsInfinity(set, -QUAD_TO_DBL(minact)) )
2721  return -SCIPsetInfinity(set);
2722 
2723  return QUAD_TO_DBL(minact);
2724 }
2725 
2726 /** calculates the minimal activity of a given set of bounds and coefficients */
2727 static
2729  SCIP_SET* set, /**< global SCIP settings */
2730  SCIP_PROB* transprob, /**< transformed problem data */
2731  SCIP_Real* coefs, /**< coefficients in sparse representation */
2732  int* inds, /**< non-zero indices */
2733  int nnz, /**< number of non-zero indices */
2734  SCIP_Real* curvarlbs, /**< current lower bounds of active problem variables (or NULL for global bounds) */
2735  SCIP_Real* curvarubs /**< current upper bounds of active problem variables (or NULL for global bounds) */
2736  )
2737 {
2738  SCIP_VAR** vars;
2739  SCIP_Real QUAD(minact);
2740  int i;
2741 
2742  assert(coefs != NULL);
2743  assert(inds != NULL);
2744 
2745  vars = SCIPprobGetVars(transprob);
2746  assert(vars != NULL);
2747 
2748  QUAD_ASSIGN(minact, 0.0);
2749 
2750  for( i = 0; i < nnz; i++ )
2751  {
2752  SCIP_Real val;
2753  SCIP_Real QUAD(delta);
2754  int v = inds[i];
2755 
2756  assert(SCIPvarGetProbindex(vars[v]) == v);
2757 
2758  val = coefs[i];
2759 
2760  if( val > 0.0 )
2761  {
2762  SCIP_Real bnd;
2763 
2764  assert(curvarlbs == NULL || !SCIPsetIsInfinity(set, -curvarlbs[v]));
2765 
2766  bnd = (curvarlbs == NULL ? SCIPvarGetLbGlobal(vars[v]) : curvarlbs[v]);
2767  SCIPquadprecProdDD(delta, val, bnd);
2768  }
2769  else
2770  {
2771  SCIP_Real bnd;
2772 
2773  assert(curvarubs == NULL || !SCIPsetIsInfinity(set, curvarubs[v]));
2774 
2775  bnd = (curvarubs == NULL ? SCIPvarGetUbGlobal(vars[v]) : curvarubs[v]);
2776  SCIPquadprecProdDD(delta, val, bnd);
2777  }
2778 
2779  /* update minimal activity */
2780  SCIPquadprecSumQQ(minact, minact, delta);
2781  }
2782 
2783  /* check whether the minmal activity is infinite */
2784  if( SCIPsetIsInfinity(set, QUAD_TO_DBL(minact)) )
2785  return SCIPsetInfinity(set);
2786  if( SCIPsetIsInfinity(set, -QUAD_TO_DBL(minact)) )
2787  return -SCIPsetInfinity(set);
2788 
2789  return QUAD_TO_DBL(minact);
2790 }
2791 
2792 /** calculates the minimal activity of a given set of bounds and coefficients */
2793 static
2795  SCIP_SET* set, /**< global SCIP settings */
2796  SCIP_PROB* transprob, /**< transformed problem data */
2797  SCIP_Real* coefs, /**< coefficients in sparse representation */
2798  int* inds, /**< non-zero indices */
2799  int nnz, /**< number of non-zero indices */
2800  SCIP_Real* curvarlbs, /**< current lower bounds of active problem variables (or NULL for global bounds) */
2801  SCIP_Real* curvarubs /**< current upper bounds of active problem variables (or NULL for global bounds) */
2802  )
2803 {
2804  SCIP_VAR** vars;
2805  SCIP_Real QUAD(maxact);
2806  int i;
2807 
2808  assert(coefs != NULL);
2809  assert(inds != NULL);
2810 
2811  vars = SCIPprobGetVars(transprob);
2812  assert(vars != NULL);
2813 
2814  QUAD_ASSIGN(maxact, 0.0);
2815 
2816  for( i = 0; i < nnz; i++ )
2817  {
2818  SCIP_Real val;
2819  SCIP_Real QUAD(delta);
2820  int v = inds[i];
2821 
2822  assert(SCIPvarGetProbindex(vars[v]) == v);
2823 
2824  val = coefs[i];
2825 
2826  if( val < 0.0 )
2827  {
2828  SCIP_Real bnd;
2829 
2830  assert(curvarlbs == NULL || !SCIPsetIsInfinity(set, -curvarlbs[v]));
2831 
2832  bnd = (curvarlbs == NULL ? SCIPvarGetLbGlobal(vars[v]) : curvarlbs[v]);
2833  SCIPquadprecProdDD(delta, val, bnd);
2834  }
2835  else
2836  {
2837  SCIP_Real bnd;
2838 
2839  assert(curvarubs == NULL || !SCIPsetIsInfinity(set, curvarubs[v]));
2840 
2841  bnd = (curvarubs == NULL ? SCIPvarGetUbGlobal(vars[v]) : curvarubs[v]);
2842  SCIPquadprecProdDD(delta, val, bnd);
2843  }
2844 
2845  /* update maximal activity */
2846  SCIPquadprecSumQQ(maxact, maxact, delta);
2847  }
2848 
2849  /* check whether the maximal activity got infinite */
2850  if( SCIPsetIsInfinity(set, QUAD_TO_DBL(maxact)) )
2851  return SCIPsetInfinity(set);
2852  if( SCIPsetIsInfinity(set, -QUAD_TO_DBL(maxact)) )
2853  return -SCIPsetInfinity(set);
2854 
2855  return QUAD_TO_DBL(maxact);
2856 }
2857 
2858 static
2860  SCIP_CONFLICT* conflict, /**< conflict analysis data */
2861  SCIP_SET* set, /**< global SCIP settings */
2862  SCIP_STAT* stat, /**< dynamic SCIP statistics */
2863  SCIP_REOPT* reopt, /**< reoptimization data */
2864  SCIP_TREE* tree, /**< tree data */
2865  BMS_BLKMEM* blkmem, /**< block memory */
2866  SCIP_PROB* origprob, /**< original problem */
2867  SCIP_PROB* transprob, /**< transformed problem */
2868  SCIP_LP* lp, /**< LP data */
2869  SCIP_BRANCHCAND* branchcand, /**< branching candidate storage */
2870  SCIP_EVENTQUEUE* eventqueue, /**< event queue */
2871  SCIP_CLIQUETABLE* cliquetable, /**< clique table data structure */
2872  SCIP_Real* coefs, /**< coefficients in sparse representation */
2873  int* inds, /**< non-zero indices */
2874  int nnz, /**< number of non-zero indices */
2875  SCIP_Real rhs, /**< right-hand side */
2876  SCIP_CONFTYPE conflicttype, /**< type of the conflict */
2877  int validdepth /**< depth where the proof is valid */
2878  )
2879 {
2880  SCIP_VAR** vars;
2881  SCIP_Real minact;
2882  int i;
2883 
2884  assert(coefs != NULL);
2885  assert(inds != NULL);
2886  assert(nnz >= 0);
2887 
2888  vars = SCIPprobGetVars(transprob);
2889  minact = getMinActivity(set, transprob, coefs, inds, nnz, NULL, NULL);
2890 
2891  /* we cannot find global tightenings */
2892  if( SCIPsetIsInfinity(set, -minact) )
2893  return SCIP_OKAY;
2894 
2895  for( i = 0; i < nnz; i++ )
2896  {
2897  SCIP_VAR* var;
2898  SCIP_Real val;
2899  SCIP_Real resminact;
2900  SCIP_Real lb;
2901  SCIP_Real ub;
2902  int pos;
2903 
2904  pos = inds[i];
2905  val = coefs[i];
2906  var = vars[pos];
2907  lb = SCIPvarGetLbGlobal(var);
2908  ub = SCIPvarGetUbGlobal(var);
2909 
2910  assert(!SCIPsetIsZero(set, val));
2911 
2912  resminact = minact;
2913 
2914  /* we got a potential new upper bound */
2915  if( val > 0.0 )
2916  {
2917  SCIP_Real newub;
2918 
2919  resminact -= (val * lb);
2920  newub = (rhs - resminact)/val;
2921 
2922  if( SCIPsetIsInfinity(set, newub) )
2923  continue;
2924 
2925  /* we cannot tighten the upper bound */
2926  if( SCIPsetIsGE(set, newub, ub) )
2927  continue;
2928 
2929  SCIP_CALL( tightenSingleVar(conflict, set, stat, tree, blkmem, origprob, transprob, reopt, lp, branchcand, \
2930  eventqueue, cliquetable, var, val, rhs-resminact, conflicttype, validdepth) );
2931  }
2932  /* we got a potential new lower bound */
2933  else
2934  {
2935  SCIP_Real newlb;
2936 
2937  resminact -= (val * ub);
2938  newlb = (rhs - resminact)/val;
2939 
2940  if( SCIPsetIsInfinity(set, -newlb) )
2941  continue;
2942 
2943  /* we cannot tighten the lower bound */
2944  if( SCIPsetIsLE(set, newlb, lb) )
2945  continue;
2946 
2947  SCIP_CALL( tightenSingleVar(conflict, set, stat, tree, blkmem, origprob, transprob, reopt, lp, branchcand, \
2948  eventqueue, cliquetable, var, val, rhs-resminact, conflicttype, validdepth) );
2949  }
2950 
2951  /* the minimal activity should stay unchanged because we tightened the bound that doesn't contribute to the
2952  * minimal activity
2953  */
2954  assert(SCIPsetIsEQ(set, minact, getMinActivity(set, transprob, coefs, inds, nnz, NULL, NULL)));
2955  }
2956 
2957  return SCIP_OKAY;
2958 }
2959 
2960 
2961 /** creates a proof constraint and tries to add it to the storage */
2962 static
2964  SCIP_CONFLICT* conflict, /**< conflict analysis data */
2965  SCIP_CONFLICTSTORE* conflictstore, /**< conflict pool data */
2966  SCIP_PROOFSET* proofset, /**< proof set */
2967  SCIP_SET* set, /**< global SCIP settings */
2968  SCIP_STAT* stat, /**< dynamic SCIP statistics */
2969  SCIP_PROB* origprob, /**< original problem */
2970  SCIP_PROB* transprob, /**< transformed problem */
2971  SCIP_TREE* tree, /**< tree data */
2972  SCIP_REOPT* reopt, /**< reoptimization data */
2973  SCIP_LP* lp, /**< LP data */
2974  SCIP_BRANCHCAND* branchcand, /**< branching candidate storage */
2975  SCIP_EVENTQUEUE* eventqueue, /**< event queue */
2976  SCIP_CLIQUETABLE* cliquetable, /**< clique table data structure */
2977  BMS_BLKMEM* blkmem /**< block memory */
2978  )
2979 {
2980  SCIP_CONS* cons;
2981  SCIP_CONS* upgdcons;
2982  SCIP_VAR** vars;
2983  SCIP_Real* coefs;
2984  int* inds;
2985  SCIP_Real rhs;
2986  SCIP_Real fillin;
2987  SCIP_Real globalminactivity;
2988  SCIP_Bool applyglobal;
2989  SCIP_Bool toolong;
2990  SCIP_Bool contonly;
2991  SCIP_Bool hasrelaxvar;
2992  SCIP_CONFTYPE conflicttype;
2993  char name[SCIP_MAXSTRLEN];
2994  int nnz;
2995  int i;
2996 
2997  assert(conflict != NULL);
2998  assert(conflictstore != NULL);
2999  assert(proofset != NULL);
3000  assert(proofset->validdepth == 0 || proofset->validdepth < SCIPtreeGetFocusDepth(tree));
3001 
3002  nnz = proofsetGetNVars(proofset);
3003 
3004  if( nnz == 0 )
3005  return SCIP_OKAY;
3006 
3007  vars = SCIPprobGetVars(transprob);
3008 
3009  rhs = proofsetGetRhs(proofset);
3010  assert(!SCIPsetIsInfinity(set, rhs));
3011 
3012  coefs = proofsetGetVals(proofset);
3013  assert(coefs != NULL);
3014 
3015  inds = proofsetGetInds(proofset);
3016  assert(inds != NULL);
3017 
3018  conflicttype = proofsetGetConftype(proofset);
3019 
3020  applyglobal = (proofset->validdepth <= SCIPtreeGetEffectiveRootDepth(tree));
3021 
3022  if( applyglobal )
3023  {
3024  SCIP_Real globalmaxactivity = getMaxActivity(set, transprob, coefs, inds, nnz, NULL, NULL);
3025 
3026  /* check whether the alternative proof is redundant */
3027  if( SCIPsetIsLE(set, globalmaxactivity, rhs) )
3028  return SCIP_OKAY;
3029 
3030  /* check whether the constraint proves global infeasibility */
3031  globalminactivity = getMinActivity(set, transprob, coefs, inds, nnz, NULL, NULL);
3032  if( SCIPsetIsGT(set, globalminactivity, rhs) )
3033  {
3034  SCIPsetDebugMsg(set, "detect global infeasibility: minactivity=%g, rhs=%g\n", globalminactivity, rhs);
3035 
3036  SCIP_CALL( SCIPnodeCutoff(tree->path[proofset->validdepth], set, stat, tree, transprob, origprob, reopt, lp, blkmem) );
3037 
3038  goto UPDATESTATISTICS;
3039  }
3040  }
3041 
3042  if( set->conf_minmaxvars >= nnz )
3043  toolong = FALSE;
3044  else
3045  {
3046  SCIP_Real maxnnz;
3047 
3048  if( transprob->startnconss < 100 )
3049  maxnnz = 0.85 * transprob->nvars;
3050  else
3051  maxnnz = (SCIP_Real)transprob->nvars;
3052 
3053  fillin = nnz;
3054  if( conflicttype == SCIP_CONFTYPE_INFEASLP || conflicttype == SCIP_CONFTYPE_ALTINFPROOF )
3055  {
3056  fillin += SCIPconflictstoreGetNDualInfProofs(conflictstore) * SCIPconflictstoreGetAvgNnzDualInfProofs(conflictstore);
3057  fillin /= (SCIPconflictstoreGetNDualInfProofs(conflictstore) + 1.0);
3058  toolong = (fillin > MIN(2.0 * stat->avgnnz, maxnnz));
3059  }
3060  else
3061  {
3062  assert(conflicttype == SCIP_CONFTYPE_BNDEXCEEDING || conflicttype == SCIP_CONFTYPE_ALTBNDPROOF);
3063 
3064  fillin += SCIPconflictstoreGetNDualBndProofs(conflictstore) * SCIPconflictstoreGetAvgNnzDualBndProofs(conflictstore);
3065  fillin /= (SCIPconflictstoreGetNDualBndProofs(conflictstore) + 1.0);
3066  toolong = (fillin > MIN(1.5 * stat->avgnnz, maxnnz));
3067  }
3068 
3069  toolong = (toolong && (nnz > set->conf_maxvarsfac * transprob->nvars));
3070  }
3071 
3072  /* don't store global dual proofs that are too long / have too many non-zeros */
3073  if( toolong )
3074  {
3075  if( applyglobal )
3076  {
3077  SCIP_CALL( propagateLongProof(conflict, set, stat, reopt, tree, blkmem, origprob, transprob, lp, branchcand,
3078  eventqueue, cliquetable, coefs, inds, nnz, rhs, conflicttype, proofset->validdepth) );
3079  }
3080  return SCIP_OKAY;
3081  }
3082 
3083  /* check if conflict contains variables that are invalid after a restart to label it appropriately */
3084  hasrelaxvar = FALSE;
3085  contonly = TRUE;
3086  for( i = 0; i < nnz && (!hasrelaxvar || contonly); ++i )
3087  {
3088  hasrelaxvar |= SCIPvarIsRelaxationOnly(vars[inds[i]]);
3089 
3090  if( SCIPvarIsIntegral(vars[inds[i]]) )
3091  contonly = FALSE;
3092  }
3093 
3094  if( !applyglobal && contonly )
3095  return SCIP_OKAY;
3096 
3097  if( conflicttype == SCIP_CONFTYPE_INFEASLP || conflicttype == SCIP_CONFTYPE_ALTINFPROOF )
3098  (void)SCIPsnprintf(name, SCIP_MAXSTRLEN, "dualproof_inf_%d", conflict->ndualproofsinfsuccess);
3099  else if( conflicttype == SCIP_CONFTYPE_BNDEXCEEDING || conflicttype == SCIP_CONFTYPE_ALTBNDPROOF )
3100  (void)SCIPsnprintf(name, SCIP_MAXSTRLEN, "dualproof_bnd_%d", conflict->ndualproofsbndsuccess);
3101  else
3102  return SCIP_INVALIDCALL;
3103 
3104  SCIP_CALL( SCIPcreateConsLinear(set->scip, &cons, name, 0, NULL, NULL, -SCIPsetInfinity(set), rhs,
3105  FALSE, FALSE, FALSE, FALSE, TRUE, !applyglobal,
3106  FALSE, TRUE, TRUE, FALSE) );
3107 
3108  for( i = 0; i < nnz; i++ )
3109  {
3110  int v = inds[i];
3111  SCIP_CALL( SCIPaddCoefLinear(set->scip, cons, vars[v], coefs[i]) );
3112  }
3113 
3114  /* do not upgrade linear constraints of size 1 */
3115  if( nnz > 1 )
3116  {
3117  upgdcons = NULL;
3118  /* try to automatically convert a linear constraint into a more specific and more specialized constraint */
3119  SCIP_CALL( SCIPupgradeConsLinear(set->scip, cons, &upgdcons) );
3120  if( upgdcons != NULL )
3121  {
3122  SCIP_CALL( SCIPreleaseCons(set->scip, &cons) );
3123  cons = upgdcons;
3124 
3125  if( conflicttype == SCIP_CONFTYPE_INFEASLP )
3126  conflicttype = SCIP_CONFTYPE_ALTINFPROOF;
3127  else if( conflicttype == SCIP_CONFTYPE_BNDEXCEEDING )
3128  conflicttype = SCIP_CONFTYPE_ALTBNDPROOF;
3129  }
3130  }
3131 
3132  /* mark constraint to be a conflict */
3133  SCIPconsMarkConflict(cons);
3134 
3135  /* add constraint to storage */
3136  if( conflicttype == SCIP_CONFTYPE_INFEASLP || conflicttype == SCIP_CONFTYPE_ALTINFPROOF )
3137  {
3138  /* add dual proof to storage */
3139  SCIP_CALL( SCIPconflictstoreAddDualraycons(conflictstore, cons, blkmem, set, stat, transprob, reopt, hasrelaxvar) );
3140  }
3141  else
3142  {
3143  SCIP_Real scale = 1.0;
3144  SCIP_Bool updateside = FALSE;
3145 
3146  /* In some cases the constraint could not be updated to a more special type. However, it is possible that
3147  * constraint got scaled. Therefore, we need to be very careful when updating the lhs/rhs after the incumbent
3148  * solution has improved.
3149  */
3150  if( conflicttype == SCIP_CONFTYPE_BNDEXCEEDING )
3151  {
3152  SCIP_Real side;
3153 
3154 #ifndef NDEBUG
3155  SCIP_CONSHDLR* conshdlr = SCIPconsGetHdlr(cons);
3156 
3157  assert(conshdlr != NULL);
3158  assert(strcmp(SCIPconshdlrGetName(conshdlr), "linear") == 0);
3159 #endif
3160  side = SCIPgetLhsLinear(set->scip, cons);
3161 
3162  if( !SCIPsetIsInfinity(set, -side) )
3163  {
3164  if( SCIPsetIsZero(set, side) )
3165  {
3166  scale = 1.0;
3167  }
3168  else
3169  {
3170  scale = proofsetGetRhs(proofset) / side;
3171  assert(SCIPsetIsNegative(set, scale));
3172  }
3173  }
3174  else
3175  {
3176  side = SCIPgetRhsLinear(set->scip, cons);
3177  assert(!SCIPsetIsInfinity(set, side));
3178 
3179  if( SCIPsetIsZero(set, side) )
3180  {
3181  scale = 1.0;
3182  }
3183  else
3184  {
3185  scale = proofsetGetRhs(proofset) / side;
3186  assert(SCIPsetIsPositive(set, scale));
3187  }
3188  }
3189  updateside = TRUE;
3190  }
3191 
3192  /* add dual proof to storage */
3193  SCIP_CALL( SCIPconflictstoreAddDualsolcons(conflictstore, cons, blkmem, set, stat, transprob, reopt, scale, updateside, hasrelaxvar) );
3194  }
3195 
3196  if( applyglobal )
3197  {
3198  /* add the constraint to the global problem */
3199  SCIP_CALL( SCIPprobAddCons(transprob, set, stat, cons) );
3200  }
3201  else
3202  {
3203  SCIP_CALL( SCIPnodeAddCons(tree->path[proofset->validdepth], blkmem, set, stat, tree, cons) );
3204  }
3205 
3206  SCIPsetDebugMsg(set, "added proof-constraint to node %p (#%lld) in depth %d (nproofconss %d)\n",
3207  (void*)tree->path[proofset->validdepth], SCIPnodeGetNumber(tree->path[proofset->validdepth]),
3208  proofset->validdepth,
3209  (conflicttype == SCIP_CONFTYPE_INFEASLP || conflicttype == SCIP_CONFTYPE_ALTINFPROOF)
3211 
3212  /* release the constraint */
3213  SCIP_CALL( SCIPreleaseCons(set->scip, &cons) );
3214 
3215  UPDATESTATISTICS:
3216  /* update statistics */
3217  if( conflicttype == SCIP_CONFTYPE_INFEASLP || conflicttype == SCIP_CONFTYPE_ALTINFPROOF )
3218  {
3219  conflict->dualproofsinfnnonzeros += nnz;
3220  if( applyglobal )
3221  ++conflict->ndualproofsinfglobal;
3222  else
3223  ++conflict->ndualproofsinflocal;
3224  ++conflict->ndualproofsinfsuccess;
3225  }
3226  else
3227  {
3228  assert(conflicttype == SCIP_CONFTYPE_BNDEXCEEDING || conflicttype == SCIP_CONFTYPE_ALTBNDPROOF);
3229  conflict->dualproofsbndnnonzeros += nnz;
3230  if( applyglobal )
3231  ++conflict->ndualproofsbndglobal;
3232  else
3233  ++conflict->ndualproofsbndlocal;
3234 
3235  ++conflict->ndualproofsbndsuccess;
3236  }
3237  return SCIP_OKAY;
3238 }
3239 
3240 /* create proof constraints out of proof sets */
3241 static
3243  SCIP_CONFLICT* conflict, /**< conflict analysis data */
3244  SCIP_CONFLICTSTORE* conflictstore, /**< conflict store */
3245  BMS_BLKMEM* blkmem, /**< block memory */
3246  SCIP_SET* set, /**< global SCIP settings */
3247  SCIP_STAT* stat, /**< dynamic problem statistics */
3248  SCIP_PROB* transprob, /**< transformed problem after presolve */
3249  SCIP_PROB* origprob, /**< original problem */
3250  SCIP_TREE* tree, /**< branch and bound tree */
3251  SCIP_REOPT* reopt, /**< reoptimization data structure */
3252  SCIP_LP* lp, /**< current LP data */
3253  SCIP_BRANCHCAND* branchcand, /**< branching candidate storage */
3254  SCIP_EVENTQUEUE* eventqueue, /**< event queue */
3255  SCIP_CLIQUETABLE* cliquetable /**< clique table data structure */
3256  )
3257 {
3258  assert(conflict != NULL);
3259 
3261  {
3262  /* only one variable has a coefficient different to zero, we add this bound change instead of a constraint */
3263  if( proofsetGetNVars(conflict->proofset) == 1 )
3264  {
3265  SCIP_VAR** vars;
3266  SCIP_Real* coefs;
3267  int* inds;
3268  SCIP_Real rhs;
3269 
3270  vars = SCIPprobGetVars(transprob);
3271 
3272  coefs = proofsetGetVals(conflict->proofset);
3273  inds = proofsetGetInds(conflict->proofset);
3274  rhs = proofsetGetRhs(conflict->proofset);
3275 
3276  SCIP_CALL( tightenSingleVar(conflict, set, stat, tree, blkmem, origprob, transprob, reopt, lp, \
3277  branchcand, eventqueue, cliquetable, vars[inds[0]], coefs[0], rhs, conflict->proofset->conflicttype,
3278  conflict->proofset->validdepth) );
3279  }
3280  else
3281  {
3282  SCIP_Bool skipinitialproof = FALSE;
3283 
3284  /* prefer an infeasibility proof
3285  *
3286  * todo: check whether this is really what we want
3287  */
3288  if( set->conf_prefinfproof && proofsetGetConftype(conflict->proofset) == SCIP_CONFTYPE_BNDEXCEEDING )
3289  {
3290  int i;
3291 
3292  for( i = 0; i < conflict->nproofsets; i++ )
3293  {
3295  {
3296  skipinitialproof = TRUE;
3297  break;
3298  }
3299  }
3300  }
3301 
3302  if( !skipinitialproof )
3303  {
3304  /* create and add the original proof */
3305  SCIP_CALL( createAndAddProofcons(conflict, conflictstore, conflict->proofset, set, stat, origprob, transprob, \
3306  tree, reopt, lp, branchcand, eventqueue, cliquetable, blkmem) );
3307  }
3308  }
3309 
3310  /* clear the proof set anyway */
3311  proofsetClear(conflict->proofset);
3312  }
3313 
3314  if( conflict->nproofsets > 0 )
3315  {
3316  int i;
3317 
3318  for( i = 0; i < conflict->nproofsets; i++ )
3319  {
3320  assert(conflict->proofsets[i] != NULL);
3321  assert(proofsetGetConftype(conflict->proofsets[i]) != SCIP_CONFTYPE_UNKNOWN);
3322 
3323  /* only one variable has a coefficient different to zero, we add this bound change instead of a constraint */
3324  if( proofsetGetNVars(conflict->proofsets[i]) == 1 )
3325  {
3326  SCIP_VAR** vars;
3327  SCIP_Real* coefs;
3328  int* inds;
3329  SCIP_Real rhs;
3330 
3331  vars = SCIPprobGetVars(transprob);
3332 
3333  coefs = proofsetGetVals(conflict->proofsets[i]);
3334  inds = proofsetGetInds(conflict->proofsets[i]);
3335  rhs = proofsetGetRhs(conflict->proofsets[i]);
3336 
3337  SCIP_CALL( tightenSingleVar(conflict, set, stat, tree, blkmem, origprob, transprob, reopt, lp,
3338  branchcand, eventqueue, cliquetable, vars[inds[0]], coefs[0], rhs,
3339  conflict->proofsets[i]->conflicttype, conflict->proofsets[i]->validdepth) );
3340  }
3341  else
3342  {
3343  /* create and add proof constraint */
3344  SCIP_CALL( createAndAddProofcons(conflict, conflictstore, conflict->proofsets[i], set, stat, origprob, \
3345  transprob, tree, reopt, lp, branchcand, eventqueue, cliquetable, blkmem) );
3346  }
3347  }
3348 
3349  /* free all proofsets */
3350  for( i = 0; i < conflict->nproofsets; i++ )
3351  proofsetFree(&conflict->proofsets[i], blkmem);
3352 
3353  conflict->nproofsets = 0;
3354  }
3355 
3356  return SCIP_OKAY;
3357 }
3358 
3359 /** adds the given conflict set as conflict constraint to the problem */
3360 static
3362  SCIP_CONFLICT* conflict, /**< conflict analysis data */
3363  BMS_BLKMEM* blkmem, /**< block memory */
3364  SCIP_SET* set, /**< global SCIP settings */
3365  SCIP_STAT* stat, /**< dynamic problem statistics */
3366  SCIP_PROB* transprob, /**< transformed problem after presolve */
3367  SCIP_PROB* origprob, /**< original problem */
3368  SCIP_TREE* tree, /**< branch and bound tree */
3369  SCIP_REOPT* reopt, /**< reoptimization data structure */
3370  SCIP_LP* lp, /**< current LP data */
3371  SCIP_BRANCHCAND* branchcand, /**< branching candidate storage */
3372  SCIP_EVENTQUEUE* eventqueue, /**< event queue */
3373  SCIP_CLIQUETABLE* cliquetable, /**< clique table data structure */
3374  SCIP_CONFLICTSET* conflictset, /**< conflict set to add to the tree */
3375  int insertdepth, /**< depth level at which the conflict set should be added */
3376  SCIP_Bool* success /**< pointer to store whether the addition was successful */
3377  )
3378 {
3379  SCIP_Bool redundant;
3380  int h;
3381 
3382  assert(conflict != NULL);
3383  assert(tree != NULL);
3384  assert(tree->path != NULL);
3385  assert(conflictset != NULL);
3386  assert(conflictset->validdepth <= insertdepth);
3387  assert(success != NULL);
3388 
3389  *success = FALSE;
3390  redundant = FALSE;
3391 
3392  /* try to derive global bound changes and shorten the conflictset by using implication and clique and variable bound
3393  * information
3394  */
3395  if( conflictset->nbdchginfos > 1 && insertdepth == 0 && !lp->strongbranching )
3396  {
3397  int nbdchgs;
3398  int nredvars;
3399 #ifdef SCIP_DEBUG
3400  int oldnbdchginfos = conflictset->nbdchginfos;
3401 #endif
3402  assert(conflictset->validdepth == 0);
3403 
3404  /* check conflict set on debugging solution */
3405  SCIP_CALL( SCIPdebugCheckConflict(blkmem, set, tree->root, conflictset->bdchginfos, conflictset->relaxedbds, conflictset->nbdchginfos) );
3406 
3407  SCIPclockStart(conflict->dIBclock, set);
3408 
3409  /* find global bound changes which can be derived from the new conflict set */
3410  SCIP_CALL( detectImpliedBounds(set, transprob, conflictset, &nbdchgs, &nredvars, &redundant) );
3411 
3412  /* all variables where removed, we have an infeasibility proof */
3413  if( conflictset->nbdchginfos == 0 )
3414  return SCIP_OKAY;
3415 
3416  /* debug check for reduced conflict set */
3417  if( nredvars > 0 )
3418  {
3419  /* check conflict set on debugging solution */
3420  SCIP_CALL( SCIPdebugCheckConflict(blkmem, set, tree->root, conflictset->bdchginfos, conflictset->relaxedbds, conflictset->nbdchginfos) ); /*lint !e506 !e774*/
3421  }
3422 
3423 #ifdef SCIP_DEBUG
3424  SCIPsetDebugMsg(set, " -> conflict set removed %d redundant variables (old nvars %d, new nvars = %d)\n", nredvars, oldnbdchginfos, conflictset->nbdchginfos);
3425  SCIPsetDebugMsg(set, " -> conflict set led to %d global bound changes %s(cdpt:%d, fdpt:%d, confdpt:%d, len:%d):\n",
3426  nbdchgs, redundant ? "(conflict became redundant) " : "", SCIPtreeGetCurrentDepth(tree), SCIPtreeGetFocusDepth(tree),
3427  conflictset->conflictdepth, conflictset->nbdchginfos);
3428  conflictsetPrint(conflictset);
3429 #endif
3430 
3431  SCIPclockStop(conflict->dIBclock, set);
3432 
3433  if( redundant )
3434  {
3435  if( nbdchgs > 0 )
3436  *success = TRUE;
3437 
3438  return SCIP_OKAY;
3439  }
3440  }
3441 
3442  /* in case the conflict set contains only one bound change which is globally valid we apply that bound change
3443  * directly (except if we are in strong branching or diving - in this case a bound change would yield an unflushed LP
3444  * and is not handled when restoring the information)
3445  *
3446  * @note A bound change can only be applied if it is are related to the active node or if is a global bound
3447  * change. Bound changes which are related to any other node cannot be handled at point due to the internal
3448  * data structure
3449  */
3450  if( conflictset->nbdchginfos == 1 && insertdepth == 0 && !lp->strongbranching && !lp->diving )
3451  {
3452  SCIP_VAR* var;
3453  SCIP_Real bound;
3454  SCIP_BOUNDTYPE boundtype;
3455 
3456  var = conflictset->bdchginfos[0]->var;
3457  assert(var != NULL);
3458 
3459  boundtype = SCIPboundtypeOpposite((SCIP_BOUNDTYPE) conflictset->bdchginfos[0]->boundtype);
3460  bound = conflictset->relaxedbds[0];
3461 
3462  /* for continuous variables, we can only use the relaxed version of the bounds negation: !(x <= u) -> x >= u */
3463  if( SCIPvarIsIntegral(var) )
3464  {
3465  assert(SCIPsetIsIntegral(set, bound));
3466  bound += (boundtype == SCIP_BOUNDTYPE_LOWER ? +1.0 : -1.0);
3467  }
3468 
3469  SCIPsetDebugMsg(set, " -> apply global bound change: <%s> %s %g\n",
3470  SCIPvarGetName(var), boundtype == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=", bound);
3471 
3472  SCIP_CALL( SCIPnodeAddBoundchg(tree->path[conflictset->validdepth], blkmem, set, stat, transprob, origprob, tree,
3473  reopt, lp, branchcand, eventqueue, cliquetable, var, bound, boundtype, FALSE) );
3474 
3475  *success = TRUE;
3476  SCIP_CALL( updateStatistics(conflict, blkmem, set, stat, conflictset, insertdepth) );
3477  }
3478  else
3479  {
3480  /* sort conflict handlers by priority */
3482 
3483  /* call conflict handlers to create a conflict constraint */
3484  for( h = 0; h < set->nconflicthdlrs; ++h )
3485  {
3486  SCIP_RESULT result;
3487 
3488  assert(conflictset->conflicttype != SCIP_CONFTYPE_UNKNOWN);
3489 
3490  SCIP_CALL( SCIPconflicthdlrExec(set->conflicthdlrs[h], set, tree->path[insertdepth],
3491  tree->path[conflictset->validdepth], conflictset->bdchginfos, conflictset->relaxedbds,
3492  conflictset->nbdchginfos, conflictset->conflicttype, conflictset->usescutoffbound, *success, &result) );
3493  if( result == SCIP_CONSADDED )
3494  {
3495  *success = TRUE;
3496  SCIP_CALL( updateStatistics(conflict, blkmem, set, stat, conflictset, insertdepth) );
3497  }
3498 
3499  SCIPsetDebugMsg(set, " -> call conflict handler <%s> (prio=%d) to create conflict set with %d bounds returned result %d\n",
3500  SCIPconflicthdlrGetName(set->conflicthdlrs[h]), SCIPconflicthdlrGetPriority(set->conflicthdlrs[h]),
3501  conflictset->nbdchginfos, result);
3502  }
3503  }
3504 
3505  return SCIP_OKAY;
3506 }
3507 
3508 /** adds the collected conflict constraints to the corresponding nodes; the best set->conf_maxconss conflict constraints
3509  * are added to the node of their validdepth; additionally (if not yet added, and if repropagation is activated), the
3510  * conflict constraint that triggers the earliest repropagation is added to the node of its validdepth
3511  */
3513  SCIP_CONFLICT* conflict, /**< conflict analysis data */
3514  BMS_BLKMEM* blkmem, /**< block memory of transformed problem */
3515  SCIP_SET* set, /**< global SCIP settings */
3516  SCIP_STAT* stat, /**< dynamic problem statistics */
3517  SCIP_PROB* transprob, /**< transformed problem */
3518  SCIP_PROB* origprob, /**< original problem */
3519  SCIP_TREE* tree, /**< branch and bound tree */
3520  SCIP_REOPT* reopt, /**< reoptimization data structure */
3521  SCIP_LP* lp, /**< current LP data */
3522  SCIP_BRANCHCAND* branchcand, /**< branching candidate storage */
3523  SCIP_EVENTQUEUE* eventqueue, /**< event queue */
3524  SCIP_CLIQUETABLE* cliquetable /**< clique table data structure */
3525  )
3526 {
3527  assert(conflict != NULL);
3528  assert(set != NULL);
3529  assert(stat != NULL);
3530  assert(transprob != NULL);
3531  assert(tree != NULL);
3532 
3533  /* is there anything to do? */
3534  if( conflict->nconflictsets > 0 )
3535  {
3536  SCIP_CONFLICTSET* repropconflictset;
3537  int nconflictsetsused;
3538  int focusdepth;
3539 #ifndef NDEBUG
3540  int currentdepth;
3541 #endif
3542  int cutoffdepth;
3543  int repropdepth;
3544  int maxconflictsets;
3545  int maxsize;
3546  int i;
3547 
3548  /* calculate the maximal number of conflict sets to accept, and the maximal size of each accepted conflict set */
3549  maxconflictsets = (set->conf_maxconss == -1 ? INT_MAX : set->conf_maxconss);
3550  maxsize = conflictCalcMaxsize(set, transprob);
3551 
3552  focusdepth = SCIPtreeGetFocusDepth(tree);
3553 #ifndef NDEBUG
3554  currentdepth = SCIPtreeGetCurrentDepth(tree);
3555  assert(focusdepth <= currentdepth);
3556  assert(currentdepth == tree->pathlen-1);
3557 #endif
3558 
3559  SCIPsetDebugMsg(set, "flushing %d conflict sets at focus depth %d (maxconflictsets: %d, maxsize: %d)\n",
3560  conflict->nconflictsets, focusdepth, maxconflictsets, maxsize);
3561 
3562  /* mark the focus node to have produced conflict sets in the visualization output */
3563  SCIPvisualFoundConflict(stat->visual, stat, tree->path[focusdepth]);
3564 
3565  /* insert the conflict sets at the corresponding nodes */
3566  nconflictsetsused = 0;
3567  cutoffdepth = INT_MAX;
3568  repropdepth = INT_MAX;
3569  repropconflictset = NULL;
3570  for( i = 0; i < conflict->nconflictsets && nconflictsetsused < maxconflictsets; ++i )
3571  {
3572  SCIP_CONFLICTSET* conflictset;
3573 
3574  conflictset = conflict->conflictsets[i];
3575  assert(conflictset != NULL);
3576  assert(0 <= conflictset->validdepth);
3577  assert(conflictset->validdepth <= conflictset->insertdepth);
3578  assert(conflictset->insertdepth <= focusdepth);
3579  assert(conflictset->insertdepth <= conflictset->repropdepth);
3580  assert(conflictset->repropdepth <= currentdepth || conflictset->repropdepth == INT_MAX); /* INT_MAX for dive/probing/strong */
3581  assert(conflictset->conflictdepth <= currentdepth || conflictset->conflictdepth == INT_MAX); /* INT_MAX for dive/probing/strong */
3582 
3583  /* ignore conflict sets that are only valid at a node that was already cut off */
3584  if( conflictset->insertdepth >= cutoffdepth )
3585  {
3586  SCIPsetDebugMsg(set, " -> ignoring conflict set with insertdepth %d >= cutoffdepth %d\n",
3587  conflictset->validdepth, cutoffdepth);
3588  continue;
3589  }
3590 
3591  /* if no conflict bounds exist, the node and its sub tree in the conflict set's valid depth can be
3592  * cut off completely
3593  */
3594  if( conflictset->nbdchginfos == 0 )
3595  {
3596  SCIPsetDebugMsg(set, " -> empty conflict set in depth %d cuts off sub tree at depth %d\n",
3597  focusdepth, conflictset->validdepth);
3598 
3599  SCIP_CALL( SCIPnodeCutoff(tree->path[conflictset->validdepth], set, stat, tree, transprob, origprob, reopt, lp, blkmem) );
3600  cutoffdepth = conflictset->validdepth;
3601  continue;
3602  }
3603 
3604  /* if the conflict set is too long, use the conflict set only if it decreases the repropagation depth */
3605  if( conflictset->nbdchginfos > maxsize )
3606  {
3607  SCIPsetDebugMsg(set, " -> conflict set is too long: %d > %d literals\n", conflictset->nbdchginfos, maxsize);
3608  if( set->conf_keepreprop && conflictset->repropagate && conflictset->repropdepth < repropdepth )
3609  {
3610  repropdepth = conflictset->repropdepth;
3611  repropconflictset = conflictset;
3612  }
3613  }
3614  else
3615  {
3616  SCIP_Bool success;
3617 
3618  /* call conflict handlers to create a conflict constraint */
3619  SCIP_CALL( conflictAddConflictCons(conflict, blkmem, set, stat, transprob, origprob, tree, reopt, lp, \
3620  branchcand, eventqueue, cliquetable, conflictset, conflictset->insertdepth, &success) );
3621 
3622  /* if no conflict bounds exist, the node and its sub tree in the conflict set's valid depth can be
3623  * cut off completely
3624  */
3625  if( conflictset->nbdchginfos == 0 )
3626  {
3627  assert(!success);
3628 
3629  SCIPsetDebugMsg(set, " -> empty conflict set in depth %d cuts off sub tree at depth %d\n",
3630  focusdepth, conflictset->validdepth);
3631 
3632  SCIP_CALL( SCIPnodeCutoff(tree->path[conflictset->validdepth], set, stat, tree, transprob, origprob, \
3633  reopt, lp, blkmem) );
3634  cutoffdepth = conflictset->validdepth;
3635  continue;
3636  }
3637 
3638  if( success )
3639  {
3640  SCIPsetDebugMsg(set, " -> conflict set %d/%d added (cdpt:%d, fdpt:%d, insert:%d, valid:%d, conf:%d, reprop:%d, len:%d):\n",
3641  nconflictsetsused+1, maxconflictsets, SCIPtreeGetCurrentDepth(tree), SCIPtreeGetFocusDepth(tree),
3642  conflictset->insertdepth, conflictset->validdepth, conflictset->conflictdepth, conflictset->repropdepth,
3643  conflictset->nbdchginfos);
3644  SCIPdebug(conflictsetPrint(conflictset));
3645 
3646  if( conflictset->repropagate && conflictset->repropdepth <= repropdepth )
3647  {
3648  repropdepth = conflictset->repropdepth;
3649  repropconflictset = NULL;
3650  }
3651  nconflictsetsused++;
3652  }
3653  }
3654  }
3655 
3656  /* reactivate propagation on the first node where one of the new conflict sets trigger a deduction */
3657  if( set->conf_repropagate && repropdepth < cutoffdepth && repropdepth < tree->pathlen )
3658  {
3659  assert(0 <= repropdepth && repropdepth < tree->pathlen);
3660  assert((int) tree->path[repropdepth]->depth == repropdepth);
3661 
3662  /* if the conflict constraint of smallest repropagation depth was not yet added, insert it now */
3663  if( repropconflictset != NULL )
3664  {
3665  SCIP_Bool success;
3666 
3667  assert(repropconflictset->repropagate);
3668  assert(repropconflictset->repropdepth == repropdepth);
3669 
3670  SCIP_CALL( conflictAddConflictCons(conflict, blkmem, set, stat, transprob, origprob, tree, reopt, lp, \
3671  branchcand, eventqueue, cliquetable, repropconflictset, repropdepth, &success) );
3672 
3673  /* if no conflict bounds exist, the node and its sub tree in the conflict set's valid depth can be
3674  * cut off completely
3675  */
3676  if( repropconflictset->nbdchginfos == 0 )
3677  {
3678  assert(!success);
3679 
3680  SCIPsetDebugMsg(set, " -> empty reprop conflict set in depth %d cuts off sub tree at depth %d\n",
3681  focusdepth, repropconflictset->validdepth);
3682 
3683  SCIP_CALL( SCIPnodeCutoff(tree->path[repropconflictset->validdepth], set, stat, tree, transprob, \
3684  origprob, reopt, lp, blkmem) );
3685  }
3686 
3687 #ifdef SCIP_DEBUG
3688  if( success )
3689  {
3690  SCIPsetDebugMsg(set, " -> additional reprop conflict set added (cdpt:%d, fdpt:%d, insert:%d, valid:%d, conf:%d, reprop:%d, len:%d):\n",
3692  repropconflictset->insertdepth, repropconflictset->validdepth, repropconflictset->conflictdepth,
3693  repropconflictset->repropdepth, repropconflictset->nbdchginfos);
3694  SCIPdebug(conflictsetPrint(repropconflictset));
3695  }
3696 #endif
3697  }
3698 
3699  /* mark the node in the repropdepth to be propagated again */
3700  SCIPnodePropagateAgain(tree->path[repropdepth], set, stat, tree);
3701 
3702  SCIPsetDebugMsg(set, "marked node %p in depth %d to be repropagated due to conflicts found in depth %d\n",
3703  (void*)tree->path[repropdepth], repropdepth, focusdepth);
3704  }
3705 
3706  /* free the conflict store */
3707  for( i = 0; i < conflict->nconflictsets; ++i )
3708  {
3709  conflictsetFree(&conflict->conflictsets[i], blkmem);
3710  }
3711  conflict->nconflictsets = 0;
3712  }
3713 
3714  /* free all temporarily created bound change information data */
3715  conflictFreeTmpBdchginfos(conflict, blkmem);
3716 
3717  return SCIP_OKAY;
3718 }
3719 
3720 /** returns the current number of conflict sets in the conflict set storage */
3722  SCIP_CONFLICT* conflict /**< conflict analysis data */
3723  )
3724 {
3725  assert(conflict != NULL);
3726 
3727  return conflict->nconflictsets;
3728 }
3729 
3730 /** returns the total number of conflict constraints that were added to the problem */
3732  SCIP_CONFLICT* conflict /**< conflict analysis data */
3733  )
3734 {
3735  assert(conflict != NULL);
3736 
3737  return conflict->nappliedglbconss + conflict->nappliedlocconss;
3738 }
3739 
3740 /** returns the total number of literals in conflict constraints that were added to the problem */
3742  SCIP_CONFLICT* conflict /**< conflict analysis data */
3743  )
3744 {
3745  assert(conflict != NULL);
3746 
3747  return conflict->nappliedglbliterals + conflict->nappliedlocliterals;
3748 }
3749 
3750 /** returns the total number of global bound changes applied by the conflict analysis */
3752  SCIP_CONFLICT* conflict /**< conflict analysis data */
3753  )
3754 {
3755  assert(conflict != NULL);
3756 
3757  return conflict->nglbchgbds;
3758 }
3759 
3760 /** returns the total number of conflict constraints that were added globally to the problem */
3762  SCIP_CONFLICT* conflict /**< conflict analysis data */
3763  )
3764 {
3765  assert(conflict != NULL);
3766 
3767  return conflict->nappliedglbconss;
3768 }
3769 
3770 /** returns the total number of literals in conflict constraints that were added globally to the problem */
3772  SCIP_CONFLICT* conflict /**< conflict analysis data */
3773  )
3774 {
3775  assert(conflict != NULL);
3776 
3777  return conflict->nappliedglbliterals;
3778 }
3779 
3780 /** returns the total number of local bound changes applied by the conflict analysis */
3782  SCIP_CONFLICT* conflict /**< conflict analysis data */
3783  )
3784 {
3785  assert(conflict != NULL);
3786 
3787  return conflict->nlocchgbds;
3788 }
3789 
3790 /** returns the total number of conflict constraints that were added locally to the problem */
3792  SCIP_CONFLICT* conflict /**< conflict analysis data */
3793  )
3794 {
3795  assert(conflict != NULL);
3796 
3797  return conflict->nappliedlocconss;
3798 }
3799 
3800 /** returns the total number of literals in conflict constraints that were added locally to the problem */
3802  SCIP_CONFLICT* conflict /**< conflict analysis data */
3803  )
3804 {
3805  assert(conflict != NULL);
3806 
3807  return conflict->nappliedlocliterals;
3808 }
3809 
3810 
3811 
3812 
3813 /*
3814  * Propagation Conflict Analysis
3815  */
3816 
3817 /** returns whether bound change has a valid reason that can be resolved in conflict analysis */
3818 static
3820  SCIP_BDCHGINFO* bdchginfo /**< bound change information */
3821  )
3822 {
3823  assert(bdchginfo != NULL);
3824  assert(!SCIPbdchginfoIsRedundant(bdchginfo));
3825 
3828  && SCIPbdchginfoGetInferProp(bdchginfo) != NULL));
3829 }
3830 
3831 /** compares two conflict set entries, such that bound changes infered later are
3832  * ordered prior to ones that were infered earlier
3833  */
3834 static
3835 SCIP_DECL_SORTPTRCOMP(conflictBdchginfoComp)
3836 { /*lint --e{715}*/
3837  SCIP_BDCHGINFO* bdchginfo1;
3838  SCIP_BDCHGINFO* bdchginfo2;
3839 
3840  bdchginfo1 = (SCIP_BDCHGINFO*)elem1;
3841  bdchginfo2 = (SCIP_BDCHGINFO*)elem2;
3842  assert(bdchginfo1 != NULL);
3843  assert(bdchginfo2 != NULL);
3844  assert(!SCIPbdchginfoIsRedundant(bdchginfo1));
3845  assert(!SCIPbdchginfoIsRedundant(bdchginfo2));
3846 
3847  if( bdchginfo1 == bdchginfo2 )
3848  return 0;
3849 
3851  return -1;
3852  else
3853  return +1;
3854 }
3855 
3856 /** return TRUE if conflict analysis is applicable; In case the function return FALSE there is no need to initialize the
3857  * conflict analysis since it will not be applied
3858  */
3860  SCIP_SET* set /**< global SCIP settings */
3861  )
3862 {
3863  /* check, if propagation conflict analysis is enabled */
3864  if( !set->conf_enable || !set->conf_useprop )
3865  return FALSE;
3866 
3867  /* check, if there are any conflict handlers to use a conflict set */
3868  if( set->nconflicthdlrs == 0 )
3869  return FALSE;
3870 
3871  return TRUE;
3872 }
3873 
3874 /** creates conflict analysis data for propagation conflicts */
3876  SCIP_CONFLICT** conflict, /**< pointer to conflict analysis data */
3877  BMS_BLKMEM* blkmem, /**< block memory of transformed problem */
3878  SCIP_SET* set /**< global SCIP settings */
3879  )
3880 {
3881  assert(conflict != NULL);
3882 
3883  SCIP_ALLOC( BMSallocMemory(conflict) );
3884 
3885  SCIP_CALL( SCIPclockCreate(&(*conflict)->dIBclock, SCIP_CLOCKTYPE_DEFAULT) );
3886  SCIP_CALL( SCIPclockCreate(&(*conflict)->propanalyzetime, SCIP_CLOCKTYPE_DEFAULT) );
3887  SCIP_CALL( SCIPclockCreate(&(*conflict)->inflpanalyzetime, SCIP_CLOCKTYPE_DEFAULT) );
3888  SCIP_CALL( SCIPclockCreate(&(*conflict)->boundlpanalyzetime, SCIP_CLOCKTYPE_DEFAULT) );
3889  SCIP_CALL( SCIPclockCreate(&(*conflict)->sbanalyzetime, SCIP_CLOCKTYPE_DEFAULT) );
3890  SCIP_CALL( SCIPclockCreate(&(*conflict)->pseudoanalyzetime, SCIP_CLOCKTYPE_DEFAULT) );
3891 
3892  /* enable or disable timing depending on the parameter statistic timing */
3893  SCIPconflictEnableOrDisableClocks((*conflict), set->time_statistictiming);
3894 
3895  SCIP_CALL( SCIPpqueueCreate(&(*conflict)->bdchgqueue, set->mem_arraygrowinit, set->mem_arraygrowfac,
3896  conflictBdchginfoComp, NULL) );
3897  SCIP_CALL( SCIPpqueueCreate(&(*conflict)->forcedbdchgqueue, set->mem_arraygrowinit, set->mem_arraygrowfac,
3898  conflictBdchginfoComp, NULL) );
3899  SCIP_CALL( conflictsetCreate(&(*conflict)->conflictset, blkmem) );
3900  (*conflict)->conflictsets = NULL;
3901  (*conflict)->conflictsetscores = NULL;
3902  (*conflict)->tmpbdchginfos = NULL;
3903  (*conflict)->conflictsetssize = 0;
3904  (*conflict)->nconflictsets = 0;
3905  (*conflict)->proofsets = NULL;
3906  (*conflict)->proofsetssize = 0;
3907  (*conflict)->nproofsets = 0;
3908  (*conflict)->tmpbdchginfossize = 0;
3909  (*conflict)->ntmpbdchginfos = 0;
3910  (*conflict)->count = 0;
3911  (*conflict)->nglbchgbds = 0;
3912  (*conflict)->nappliedglbconss = 0;
3913  (*conflict)->nappliedglbliterals = 0;
3914  (*conflict)->nlocchgbds = 0;
3915  (*conflict)->nappliedlocconss = 0;
3916  (*conflict)->nappliedlocliterals = 0;
3917  (*conflict)->npropcalls = 0;
3918  (*conflict)->npropsuccess = 0;
3919  (*conflict)->npropconfconss = 0;
3920  (*conflict)->npropconfliterals = 0;
3921  (*conflict)->npropreconvconss = 0;
3922  (*conflict)->npropreconvliterals = 0;
3923  (*conflict)->ninflpcalls = 0;
3924  (*conflict)->ninflpsuccess = 0;
3925  (*conflict)->ninflpconfconss = 0;
3926  (*conflict)->ninflpconfliterals = 0;
3927  (*conflict)->ninflpreconvconss = 0;
3928  (*conflict)->ninflpreconvliterals = 0;
3929  (*conflict)->ninflpiterations = 0;
3930  (*conflict)->nboundlpcalls = 0;
3931  (*conflict)->nboundlpsuccess = 0;
3932  (*conflict)->nboundlpconfconss = 0;
3933  (*conflict)->nboundlpconfliterals = 0;
3934  (*conflict)->nboundlpreconvconss = 0;
3935  (*conflict)->nboundlpreconvliterals = 0;
3936  (*conflict)->nboundlpiterations = 0;
3937  (*conflict)->nsbcalls = 0;
3938  (*conflict)->nsbsuccess = 0;
3939  (*conflict)->nsbconfconss = 0;
3940  (*conflict)->nsbconfliterals = 0;
3941  (*conflict)->nsbreconvconss = 0;
3942  (*conflict)->nsbreconvliterals = 0;
3943  (*conflict)->nsbiterations = 0;
3944  (*conflict)->npseudocalls = 0;
3945  (*conflict)->npseudosuccess = 0;
3946  (*conflict)->npseudoconfconss = 0;
3947  (*conflict)->npseudoconfliterals = 0;
3948  (*conflict)->npseudoreconvconss = 0;
3949  (*conflict)->npseudoreconvliterals = 0;
3950  (*conflict)->ndualproofsinfglobal = 0;
3951  (*conflict)->ndualproofsinflocal = 0;
3952  (*conflict)->ndualproofsinfsuccess = 0;
3953  (*conflict)->dualproofsinfnnonzeros = 0;
3954  (*conflict)->ndualproofsbndglobal = 0;
3955  (*conflict)->ndualproofsbndlocal = 0;
3956  (*conflict)->ndualproofsbndsuccess = 0;
3957  (*conflict)->dualproofsbndnnonzeros = 0;
3958 
3959  SCIP_CALL( conflictInitProofset((*conflict), blkmem) );
3960 
3961  return SCIP_OKAY;
3962 }
3963 
3964 /** frees conflict analysis data for propagation conflicts */
3966  SCIP_CONFLICT** conflict, /**< pointer to conflict analysis data */
3967  BMS_BLKMEM* blkmem /**< block memory of transformed problem */
3968  )
3969 {
3970  assert(conflict != NULL);
3971  assert(*conflict != NULL);
3972  assert((*conflict)->nconflictsets == 0);
3973  assert((*conflict)->ntmpbdchginfos == 0);
3974 
3975 #ifdef SCIP_CONFGRAPH
3976  confgraphFree();
3977 #endif
3978 
3979  SCIPclockFree(&(*conflict)->dIBclock);
3980  SCIPclockFree(&(*conflict)->propanalyzetime);
3981  SCIPclockFree(&(*conflict)->inflpanalyzetime);
3982  SCIPclockFree(&(*conflict)->boundlpanalyzetime);
3983  SCIPclockFree(&(*conflict)->sbanalyzetime);
3984  SCIPclockFree(&(*conflict)->pseudoanalyzetime);
3985  SCIPpqueueFree(&(*conflict)->bdchgqueue);
3986  SCIPpqueueFree(&(*conflict)->forcedbdchgqueue);
3987  conflictsetFree(&(*conflict)->conflictset, blkmem);
3988  proofsetFree(&(*conflict)->proofset, blkmem);
3989 
3990  BMSfreeMemoryArrayNull(&(*conflict)->conflictsets);
3991  BMSfreeMemoryArrayNull(&(*conflict)->conflictsetscores);
3992  BMSfreeMemoryArrayNull(&(*conflict)->proofsets);
3993  BMSfreeMemoryArrayNull(&(*conflict)->tmpbdchginfos);
3994  BMSfreeMemory(conflict);
3995 
3996  return SCIP_OKAY;
3997 }
3998 
3999 /** clears the conflict queue and the current conflict set */
4000 static
4002  SCIP_CONFLICT* conflict /**< conflict analysis data */
4003  )
4004 {
4005  assert(conflict != NULL);
4006 
4007  SCIPpqueueClear(conflict->bdchgqueue);
4008  SCIPpqueueClear(conflict->forcedbdchgqueue);
4009  conflictsetClear(conflict->conflictset);
4010 }
4011 
4012 /** initializes the propagation conflict analysis by clearing the conflict candidate queue */
4014  SCIP_CONFLICT* conflict, /**< conflict analysis data */
4015  SCIP_SET* set, /**< global SCIP settings */
4016  SCIP_STAT* stat, /**< problem statistics */
4017  SCIP_PROB* prob, /**< problem data */
4018  SCIP_CONFTYPE conftype, /**< type of the conflict */
4019  SCIP_Bool usescutoffbound /**< depends the conflict on a cutoff bound? */
4020  )
4021 {
4022  assert(conflict != NULL);
4023  assert(set != NULL);
4024  assert(stat != NULL);
4025  assert(prob != NULL);
4026 
4027  SCIPsetDebugMsg(set, "initializing conflict analysis\n");
4028 
4029  /* clear the conflict candidate queue and the conflict set */
4030  conflictClear(conflict);
4031 
4032  /* set conflict type */
4033  assert(conftype == SCIP_CONFTYPE_BNDEXCEEDING || conftype == SCIP_CONFTYPE_INFEASLP
4034  || conftype == SCIP_CONFTYPE_PROPAGATION);
4035  conflict->conflictset->conflicttype = conftype;
4036 
4037  /* set whether a cutoff bound is involved */
4038  conflict->conflictset->usescutoffbound = usescutoffbound;
4039 
4040  /* increase the conflict counter, such that binary variables of new conflict set and new conflict queue are labeled
4041  * with this new counter
4042  */
4043  conflict->count++;
4044  if( conflict->count == 0 ) /* make sure, 0 is not a valid conflict counter (may happen due to integer overflow) */
4045  conflict->count = 1;
4046 
4047  /* increase the conflict score weight for history updates of future conflict reasons */
4048  if( stat->nnodes > stat->lastconflictnode )
4049  {
4050  assert(0.0 < set->conf_scorefac && set->conf_scorefac <= 1.0);
4051  stat->vsidsweight /= set->conf_scorefac;
4052  assert(stat->vsidsweight > 0.0);
4053 
4054  /* if the conflict score for the next conflict exceeds 1000.0, rescale all history conflict scores */
4055  if( stat->vsidsweight >= 1000.0 )
4056  {
4057  int v;
4058 
4059  for( v = 0; v < prob->nvars; ++v )
4060  {
4061  SCIP_CALL( SCIPvarScaleVSIDS(prob->vars[v], 1.0/stat->vsidsweight) );
4062  }
4063  SCIPhistoryScaleVSIDS(stat->glbhistory, 1.0/stat->vsidsweight);
4065  stat->vsidsweight = 1.0;
4066  }
4067  stat->lastconflictnode = stat->nnodes;
4068  }
4069 
4070 #ifdef SCIP_CONFGRAPH
4071  confgraphFree();
4072  SCIP_CALL( confgraphCreate(set, conflict) );
4073 #endif
4074 
4075  return SCIP_OKAY;
4076 }
4077 
4078 /** marks bound to be present in the current conflict and returns whether a bound which is at least as tight was already
4079  * member of the current conflict (i.e., the given bound change does not need to be added)
4080  */
4081 static
4083  SCIP_CONFLICT* conflict, /**< conflict analysis data */
4084  SCIP_SET* set, /**< global SCIP settings */
4085  SCIP_BDCHGINFO* bdchginfo, /**< bound change to add to the conflict set */
4086  SCIP_Real relaxedbd /**< relaxed bound */
4087  )
4088 {
4089  SCIP_VAR* var;
4090  SCIP_Real newbound;
4091 
4092  assert(conflict != NULL);
4093 
4094  var = SCIPbdchginfoGetVar(bdchginfo);
4095  newbound = SCIPbdchginfoGetNewbound(bdchginfo);
4096  assert(var != NULL);
4097 
4098  switch( SCIPbdchginfoGetBoundtype(bdchginfo) )
4099  {
4100  case SCIP_BOUNDTYPE_LOWER:
4101  /* check if the variables lower bound is already member of the conflict */
4102  if( var->conflictlbcount == conflict->count )
4103  {
4104  /* the variable is already member of the conflict; hence check if the new bound is redundant */
4105  if( var->conflictlb > newbound )
4106  {
4107  SCIPsetDebugMsg(set, "ignoring redundant bound change <%s> >= %g since a stronger lower bound exist <%s> >= %g\n",
4108  SCIPvarGetName(var), newbound, SCIPvarGetName(var), var->conflictlb);
4109  return TRUE;
4110  }
4111  else if( var->conflictlb == newbound ) /*lint !e777*/
4112  {
4113  SCIPsetDebugMsg(set, "ignoring redundant bound change <%s> >= %g since this lower bound is already present\n", SCIPvarGetName(var), newbound);
4114  SCIPsetDebugMsg(set, "adjust relaxed lower bound <%g> -> <%g>\n", var->conflictlb, relaxedbd);
4115  var->conflictrelaxedlb = MAX(var->conflictrelaxedlb, relaxedbd);
4116  return TRUE;
4117  }
4118  }
4119 
4120  /* add the variable lower bound to the current conflict */
4121  var->conflictlbcount = conflict->count;
4122 
4123  /* remember the lower bound and relaxed bound to allow only better/tighter lower bounds for that variables
4124  * w.r.t. this conflict
4125  */
4126  var->conflictlb = newbound;
4127  var->conflictrelaxedlb = relaxedbd;
4128 
4129  return FALSE;
4130 
4131  case SCIP_BOUNDTYPE_UPPER:
4132  /* check if the variables upper bound is already member of the conflict */
4133  if( var->conflictubcount == conflict->count )
4134  {
4135  /* the variable is already member of the conflict; hence check if the new bound is redundant */
4136  if( var->conflictub < newbound )
4137  {
4138  SCIPsetDebugMsg(set, "ignoring redundant bound change <%s> <= %g since a stronger upper bound exist <%s> <= %g\n",
4139  SCIPvarGetName(var), newbound, SCIPvarGetName(var), var->conflictub);
4140  return TRUE;
4141  }
4142  else if( var->conflictub == newbound ) /*lint !e777*/
4143  {
4144  SCIPsetDebugMsg(set, "ignoring redundant bound change <%s> <= %g since this upper bound is already present\n", SCIPvarGetName(var), newbound);
4145  SCIPsetDebugMsg(set, "adjust relaxed upper bound <%g> -> <%g>\n", var->conflictub, relaxedbd);
4146  var->conflictrelaxedub = MIN(var->conflictrelaxedub, relaxedbd);
4147  return TRUE;
4148  }
4149  }
4150 
4151  /* add the variable upper bound to the current conflict */
4152  var->conflictubcount = conflict->count;
4153 
4154  /* remember the upper bound and relaxed bound to allow only better/tighter upper bounds for that variables
4155  * w.r.t. this conflict
4156  */
4157  var->conflictub = newbound;
4158  var->conflictrelaxedub = relaxedbd;
4159 
4160  return FALSE;
4161 
4162  default:
4163  SCIPerrorMessage("invalid bound type %d\n", SCIPbdchginfoGetBoundtype(bdchginfo));
4164  SCIPABORT();
4165  return FALSE; /*lint !e527*/
4166  }
4167 }
4168 
4169 /** puts bound change into the current conflict set */
4170 static
4172  SCIP_CONFLICT* conflict, /**< conflict analysis data */
4173  BMS_BLKMEM* blkmem, /**< block memory of transformed problem */
4174  SCIP_SET* set, /**< global SCIP settings */
4175  SCIP_BDCHGINFO* bdchginfo, /**< bound change to add to the conflict set */
4176  SCIP_Real relaxedbd /**< relaxed bound */
4177  )
4178 {
4179  assert(conflict != NULL);
4180  assert(!SCIPbdchginfoIsRedundant(bdchginfo));
4181 
4182  /* check if the relaxed bound is really a relaxed bound */
4183  assert(SCIPbdchginfoGetBoundtype(bdchginfo) == SCIP_BOUNDTYPE_LOWER || SCIPsetIsGE(set, relaxedbd, SCIPbdchginfoGetNewbound(bdchginfo)));
4184  assert(SCIPbdchginfoGetBoundtype(bdchginfo) == SCIP_BOUNDTYPE_UPPER || SCIPsetIsLE(set, relaxedbd, SCIPbdchginfoGetNewbound(bdchginfo)));
4185 
4186  SCIPsetDebugMsg(set, "putting bound change <%s> %s %g(%g) at depth %d to current conflict set\n",
4187  SCIPvarGetName(SCIPbdchginfoGetVar(bdchginfo)),
4188  SCIPbdchginfoGetBoundtype(bdchginfo) == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=", SCIPbdchginfoGetNewbound(bdchginfo),
4189  relaxedbd, SCIPbdchginfoGetDepth(bdchginfo));
4190 
4191  /* mark the bound to be member of the conflict and check if a bound which is at least as tight is already member of
4192  * the conflict
4193  */
4194  if( !conflictMarkBoundCheckPresence(conflict, set, bdchginfo, relaxedbd) )
4195  {
4196  /* add the bound change to the current conflict set */
4197  SCIP_CALL( conflictsetAddBound(conflict->conflictset, blkmem, set, bdchginfo, relaxedbd) );
4198 
4199 #ifdef SCIP_CONFGRAPH
4200  if( bdchginfo != confgraphcurrentbdchginfo )
4201  confgraphAddBdchg(bdchginfo);
4202 #endif
4203  }
4204 #ifdef SCIP_CONFGRAPH
4205  else
4206  confgraphLinkBdchg(bdchginfo);
4207 #endif
4208 
4209  return SCIP_OKAY;
4210 }
4211 
4212 /** returns whether the negation of the given bound change would lead to a globally valid literal */
4213 static
4215  SCIP_SET* set, /**< global SCIP settings */
4216  SCIP_BDCHGINFO* bdchginfo /**< bound change information */
4217  )
4218 {
4219  SCIP_VAR* var;
4220  SCIP_BOUNDTYPE boundtype;
4221  SCIP_Real bound;
4222 
4223  var = SCIPbdchginfoGetVar(bdchginfo);
4224  boundtype = SCIPbdchginfoGetBoundtype(bdchginfo);
4225  bound = SCIPbdchginfoGetNewbound(bdchginfo);
4226 
4227  return (SCIPvarGetType(var) == SCIP_VARTYPE_CONTINUOUS
4228  && ((boundtype == SCIP_BOUNDTYPE_LOWER && SCIPsetIsFeasGE(set, bound, SCIPvarGetUbGlobal(var)))
4229  || (boundtype == SCIP_BOUNDTYPE_UPPER && SCIPsetIsFeasLE(set, bound, SCIPvarGetLbGlobal(var)))));
4230 }
4231 
4232 /** adds given bound change information to the conflict candidate queue */
4233 static
4235  SCIP_CONFLICT* conflict, /**< conflict analysis data */
4236  SCIP_SET* set, /**< global SCIP settings */
4237  SCIP_BDCHGINFO* bdchginfo, /**< bound change information */
4238  SCIP_Real relaxedbd /**< relaxed bound */
4239  )
4240 {
4241  assert(conflict != NULL);
4242  assert(set != NULL);
4243  assert(bdchginfo != NULL);
4244  assert(!SCIPbdchginfoIsRedundant(bdchginfo));
4245 
4246  /* check if the relaxed bound is really a relaxed bound */
4247  assert(SCIPbdchginfoGetBoundtype(bdchginfo) == SCIP_BOUNDTYPE_LOWER || SCIPsetIsGE(set, relaxedbd, SCIPbdchginfoGetNewbound(bdchginfo)));
4248  assert(SCIPbdchginfoGetBoundtype(bdchginfo) == SCIP_BOUNDTYPE_UPPER || SCIPsetIsLE(set, relaxedbd, SCIPbdchginfoGetNewbound(bdchginfo)));
4249 
4250  /* mark the bound to be member of the conflict and check if a bound which is at least as tight is already member of
4251  * the conflict
4252  */
4253  if( !conflictMarkBoundCheckPresence(conflict, set, bdchginfo, relaxedbd) )
4254  {
4255  /* insert the bound change into the conflict queue */
4256  if( (!set->conf_preferbinary || SCIPvarIsBinary(SCIPbdchginfoGetVar(bdchginfo)))
4257  && !isBoundchgUseless(set, bdchginfo) )
4258  {
4259  SCIP_CALL( SCIPpqueueInsert(conflict->bdchgqueue, (void*)bdchginfo) );
4260  }
4261  else
4262  {
4263  SCIP_CALL( SCIPpqueueInsert(conflict->forcedbdchgqueue, (void*)bdchginfo) );
4264  }
4265 
4266 #ifdef SCIP_CONFGRAPH
4267  confgraphAddBdchg(bdchginfo);
4268 #endif
4269  }
4270 #ifdef SCIP_CONFGRAPH
4271  else
4272  confgraphLinkBdchg(bdchginfo);
4273 #endif
4274 
4275  return SCIP_OKAY;
4276 }
4277 
4278 /** convert variable and bound change to active variable */
4279 static
4281  SCIP_VAR** var, /**< pointer to variable */
4282  SCIP_SET* set, /**< global SCIP settings */
4283  SCIP_BOUNDTYPE* boundtype, /**< pointer to type of bound that was changed: lower or upper bound */
4284  SCIP_Real* bound /**< pointer to bound to convert, or NULL */
4285  )
4286 {
4287  SCIP_Real scalar;
4288  SCIP_Real constant;
4289 
4290  scalar = 1.0;
4291  constant = 0.0;
4292 
4293  /* transform given varibale to active varibale */
4294  SCIP_CALL( SCIPvarGetProbvarSum(var, set, &scalar, &constant) );
4295  assert(SCIPvarGetStatus(*var) == SCIP_VARSTATUS_FIXED || scalar != 0.0); /*lint !e777*/
4296 
4297  if( SCIPvarGetStatus(*var) == SCIP_VARSTATUS_FIXED )
4298  return SCIP_OKAY;
4299 
4300  /* if the scalar of the aggregation is negative, we have to switch the bound type */
4301  if( scalar < 0.0 )
4302  (*boundtype) = SCIPboundtypeOpposite(*boundtype);
4303 
4304  if( bound != NULL )
4305  {
4306  (*bound) -= constant;
4307  (*bound) /= scalar;
4308  }
4309 
4310  return SCIP_OKAY;
4311 }
4312 
4313 /** adds variable's bound to conflict candidate queue */
4314 static
4316  SCIP_CONFLICT* conflict, /**< conflict analysis data */
4317  BMS_BLKMEM* blkmem, /**< block memory */
4318  SCIP_SET* set, /**< global SCIP settings */
4319  SCIP_STAT* stat, /**< dynamic problem statistics */
4320  SCIP_VAR* var, /**< problem variable */
4321  SCIP_BOUNDTYPE boundtype, /**< type of bound that was changed: lower or upper bound */
4322  SCIP_BDCHGINFO* bdchginfo, /**< bound change info, or NULL */
4323  SCIP_Real relaxedbd /**< relaxed bound */
4324  )
4325 {
4326  assert(SCIPvarIsActive(var));
4327  assert(bdchginfo != NULL);
4328  assert(!SCIPbdchginfoIsRedundant(bdchginfo));
4329 
4330  SCIPsetDebugMsg(set, " -> adding bound <%s> %s %.15g(%.15g) [status:%d, type:%d, depth:%d, pos:%d, reason:<%s>, info:%d] to candidates\n",
4331  SCIPvarGetName(var),
4332  boundtype == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=",
4333  SCIPbdchginfoGetNewbound(bdchginfo), relaxedbd,
4334  SCIPvarGetStatus(var), SCIPvarGetType(var),
4335  SCIPbdchginfoGetDepth(bdchginfo), SCIPbdchginfoGetPos(bdchginfo),
4336  SCIPbdchginfoGetChgtype(bdchginfo) == SCIP_BOUNDCHGTYPE_BRANCHING ? "branch"
4340  : "none")),
4342 
4343  /* the local bound change may be resolved and has to be put on the candidate queue;
4344  * we even put bound changes without inference information on the queue in order to automatically
4345  * eliminate multiple insertions of the same bound change
4346  */
4347  assert(SCIPbdchginfoGetVar(bdchginfo) == var);
4348  assert(SCIPbdchginfoGetBoundtype(bdchginfo) == boundtype);
4349  assert(SCIPbdchginfoGetDepth(bdchginfo) >= 0);
4350  assert(SCIPbdchginfoGetPos(bdchginfo) >= 0);
4351 
4352  /* the relaxed bound should be a relaxation */
4353  assert(boundtype == SCIP_BOUNDTYPE_LOWER ? SCIPsetIsLE(set, relaxedbd, SCIPbdchginfoGetNewbound(bdchginfo)) : SCIPsetIsGE(set, relaxedbd, SCIPbdchginfoGetNewbound(bdchginfo)));
4354 
4355  /* the relaxed bound should be worse then the old bound of the bound change info */
4356  assert(boundtype == SCIP_BOUNDTYPE_LOWER ? SCIPsetIsGT(set, relaxedbd, SCIPbdchginfoGetOldbound(bdchginfo)) : SCIPsetIsLT(set, relaxedbd, SCIPbdchginfoGetOldbound(bdchginfo)));
4357 
4358  /* put bound change information into priority queue */
4359  SCIP_CALL( conflictQueueBound(conflict, set, bdchginfo, relaxedbd) );
4360 
4361  /* each variable which is add to the conflict graph gets an increase in the VSIDS
4362  *
4363  * @note That is different to the VSIDS preseted in the literature
4364  */
4365  SCIP_CALL( incVSIDS(var, blkmem, set, stat, boundtype, relaxedbd, set->conf_conflictgraphweight) );
4366 
4367  return SCIP_OKAY;
4368 }
4369 
4370 /** adds variable's bound to conflict candidate queue */
4372  SCIP_CONFLICT* conflict, /**< conflict analysis data */
4373  BMS_BLKMEM* blkmem, /**< block memory */
4374  SCIP_SET* set, /**< global SCIP settings */
4375  SCIP_STAT* stat, /**< dynamic problem statistics */
4376  SCIP_VAR* var, /**< problem variable */
4377  SCIP_BOUNDTYPE boundtype, /**< type of bound that was changed: lower or upper bound */
4378  SCIP_BDCHGIDX* bdchgidx /**< bound change index (time stamp of bound change), or NULL for current time */
4379  )
4380 {
4381  SCIP_BDCHGINFO* bdchginfo;
4382 
4383  assert(conflict != NULL);
4384  assert(stat != NULL);
4385  assert(var != NULL);
4386 
4387  /* convert bound to active problem variable */
4388  SCIP_CALL( convertToActiveVar(&var, set, &boundtype, NULL) );
4389 
4390  /* we can ignore fixed variables */
4392  return SCIP_OKAY;
4393 
4394  /* if the variable is multi-aggregated, add the bounds of all aggregation variables */
4396  {
4397  SCIP_VAR** vars;
4398  SCIP_Real* scalars;
4399  int nvars;
4400  int i;
4401 
4402  vars = SCIPvarGetMultaggrVars(var);
4403  scalars = SCIPvarGetMultaggrScalars(var);
4404  nvars = SCIPvarGetMultaggrNVars(var);
4405  for( i = 0; i < nvars; ++i )
4406  {
4407  SCIP_CALL( SCIPconflictAddBound(conflict, blkmem, set, stat, vars[i],
4408  (scalars[i] < 0.0 ? SCIPboundtypeOpposite(boundtype) : boundtype), bdchgidx) );
4409  }
4410 
4411  return SCIP_OKAY;
4412  }
4413  assert(SCIPvarIsActive(var));
4414 
4415  /* get bound change information */
4416  bdchginfo = SCIPvarGetBdchgInfo(var, boundtype, bdchgidx, FALSE);
4417 
4418  /* if bound of variable was not changed (this means it is still the global bound), we can ignore the conflicting
4419  * bound
4420  */
4421  if( bdchginfo == NULL )
4422  return SCIP_OKAY;
4423 
4424  assert(SCIPbdchgidxIsEarlier(SCIPbdchginfoGetIdx(bdchginfo), bdchgidx));
4425 
4426  SCIP_CALL( conflictAddBound(conflict, blkmem, set, stat, var, boundtype, bdchginfo, SCIPbdchginfoGetNewbound(bdchginfo)) );
4427 
4428  return SCIP_OKAY;
4429 }
4430 
4431 /** adds variable's bound to conflict candidate queue */
4433  SCIP_CONFLICT* conflict, /**< conflict analysis data */
4434  BMS_BLKMEM* blkmem, /**< block memory */
4435  SCIP_SET* set, /**< global SCIP settings */
4436  SCIP_STAT* stat, /**< dynamic problem statistics */
4437  SCIP_VAR* var, /**< problem variable */
4438  SCIP_BOUNDTYPE boundtype, /**< type of bound that was changed: lower or upper bound */
4439  SCIP_BDCHGIDX* bdchgidx, /**< bound change index (time stamp of bound change), or NULL for current time */
4440  SCIP_Real relaxedbd /**< the relaxed bound */
4441  )
4442 {
4443  SCIP_BDCHGINFO* bdchginfo;
4444  int nbdchgs;
4445 
4446  assert(conflict != NULL);
4447  assert(stat != NULL);
4448  assert(var != NULL);
4449 
4450  if( !SCIPvarIsActive(var) )
4451  {
4452  /* convert bound to active problem variable */
4453  SCIP_CALL( convertToActiveVar(&var, set, &boundtype, &relaxedbd) );
4454 
4455  /* we can ignore fixed variables */
4457  return SCIP_OKAY;
4458 
4459  /* if the variable is multi-aggregated, add the bounds of all aggregation variables */
4461  {
4462  SCIPsetDebugMsg(set, "ignoring relaxed bound information since variable <%s> is multi-aggregated active\n", SCIPvarGetName(var));
4463 
4464  SCIP_CALL( SCIPconflictAddBound(conflict, blkmem, set, stat, var, boundtype, bdchgidx) );
4465 
4466  return SCIP_OKAY;
4467  }
4468  }
4469  assert(SCIPvarIsActive(var));
4470 
4471  /* get bound change information */
4472  bdchginfo = SCIPvarGetBdchgInfo(var, boundtype, bdchgidx, FALSE);
4473 
4474  /* if bound of variable was not changed (this means it is still the global bound), we can ignore the conflicting
4475  * bound
4476  */
4477  if( bdchginfo == NULL )
4478  return SCIP_OKAY;
4479 
4480  /* check that the bound change info is not a temporary one */
4481  assert(SCIPbdchgidxGetPos(&bdchginfo->bdchgidx) >= 0);
4482 
4483  /* get the position of the bound change information within the bound change array of the variable */
4484  nbdchgs = (int) bdchginfo->pos;
4485  assert(nbdchgs >= 0);
4486 
4487  /* if the relaxed bound should be ignored, set the relaxed bound to the bound given by the bdchgidx; that ensures
4488  * that the loop(s) below will be skipped
4489  */
4490  if( set->conf_ignorerelaxedbd )
4491  relaxedbd = SCIPbdchginfoGetNewbound(bdchginfo);
4492 
4493  /* search for the bound change information which includes the relaxed bound */
4494  if( boundtype == SCIP_BOUNDTYPE_LOWER )
4495  {
4496  SCIP_Real newbound;
4497 
4498  /* adjust relaxed lower bound w.r.t. variable type */
4499  SCIPvarAdjustLb(var, set, &relaxedbd);
4500 
4501  /* due to numericis we compare the relaxed lower bound to the one present at the particular time point and take
4502  * the better one
4503  */
4504  newbound = SCIPbdchginfoGetNewbound(bdchginfo);
4505  relaxedbd = MIN(relaxedbd, newbound);
4506 
4507  /* check if relaxed lower bound is smaller or equal to global lower bound; if so we can ignore the conflicting
4508  * bound
4509  */
4510  if( SCIPsetIsLE(set, relaxedbd, SCIPvarGetLbGlobal(var)) )
4511  return SCIP_OKAY;
4512 
4513  while( nbdchgs > 0 )
4514  {
4515  assert(SCIPsetIsLE(set, relaxedbd, SCIPbdchginfoGetNewbound(bdchginfo)));
4516 
4517  /* check if the old lower bound is greater than or equal to relaxed lower bound; if not we found the bound
4518  * change info which we need to report
4519  */
4520  if( SCIPsetIsGT(set, relaxedbd, SCIPbdchginfoGetOldbound(bdchginfo)) )
4521  break;
4522 
4523  bdchginfo = SCIPvarGetBdchgInfoLb(var, nbdchgs-1);
4524 
4525  SCIPsetDebugMsg(set, "lower bound change %d oldbd=%.15g, newbd=%.15g, depth=%d, pos=%d, redundant=%u\n",
4526  nbdchgs, SCIPbdchginfoGetOldbound(bdchginfo), SCIPbdchginfoGetNewbound(bdchginfo),
4527  SCIPbdchginfoGetDepth(bdchginfo), SCIPbdchginfoGetPos(bdchginfo),
4528  SCIPbdchginfoIsRedundant(bdchginfo));
4529 
4530  /* if bound change is redundant (this means it now a global bound), we can ignore the conflicting bound */
4531  if( SCIPbdchginfoIsRedundant(bdchginfo) )
4532  return SCIP_OKAY;
4533 
4534  nbdchgs--;
4535  }
4536  assert(SCIPsetIsGT(set, relaxedbd, SCIPbdchginfoGetOldbound(bdchginfo)));
4537  }
4538  else
4539  {
4540  SCIP_Real newbound;
4541 
4542  assert(boundtype == SCIP_BOUNDTYPE_UPPER);
4543 
4544  /* adjust relaxed upper bound w.r.t. variable type */
4545  SCIPvarAdjustUb(var, set, &relaxedbd);
4546 
4547  /* due to numericis we compare the relaxed upper bound to the one present at the particular time point and take
4548  * the better one
4549  */
4550  newbound = SCIPbdchginfoGetNewbound(bdchginfo);
4551  relaxedbd = MAX(relaxedbd, newbound);
4552 
4553  /* check if relaxed upper bound is greater or equal to global upper bound; if so we can ignore the conflicting
4554  * bound
4555  */
4556  if( SCIPsetIsGE(set, relaxedbd, SCIPvarGetUbGlobal(var)) )
4557  return SCIP_OKAY;
4558 
4559  while( nbdchgs > 0 )
4560  {
4561  assert(SCIPsetIsGE(set, relaxedbd, SCIPbdchginfoGetNewbound(bdchginfo)));
4562 
4563  /* check if the old upper bound is smaller than or equal to the relaxed upper bound; if not we found the
4564  * bound change info which we need to report
4565  */
4566  if( SCIPsetIsLT(set, relaxedbd, SCIPbdchginfoGetOldbound(bdchginfo)) )
4567  break;
4568 
4569  bdchginfo = SCIPvarGetBdchgInfoUb(var, nbdchgs-1);
4570 
4571  SCIPsetDebugMsg(set, "upper bound change %d oldbd=%.15g, newbd=%.15g, depth=%d, pos=%d, redundant=%u\n",
4572  nbdchgs, SCIPbdchginfoGetOldbound(bdchginfo), SCIPbdchginfoGetNewbound(bdchginfo),
4573  SCIPbdchginfoGetDepth(bdchginfo), SCIPbdchginfoGetPos(bdchginfo),
4574  SCIPbdchginfoIsRedundant(bdchginfo));
4575 
4576  /* if bound change is redundant (this means it now a global bound), we can ignore the conflicting bound */
4577  if( SCIPbdchginfoIsRedundant(bdchginfo) )
4578  return SCIP_OKAY;
4579 
4580  nbdchgs--;
4581  }
4582  assert(SCIPsetIsLT(set, relaxedbd, SCIPbdchginfoGetOldbound(bdchginfo)));
4583  }
4584 
4585  assert(SCIPbdchgidxIsEarlier(SCIPbdchginfoGetIdx(bdchginfo), bdchgidx));
4586 
4587  /* put bound change information into priority queue */
4588  SCIP_CALL( conflictAddBound(conflict, blkmem, set, stat, var, boundtype, bdchginfo, relaxedbd) );
4589 
4590  return SCIP_OKAY;
4591 }
4592 
4593 /** checks if the given variable is already part of the current conflict set or queued for resolving with the same or
4594  * even stronger bound
4595  */
4597  SCIP_CONFLICT* conflict, /**< conflict analysis data */
4598  SCIP_VAR* var, /**< problem variable */
4599  SCIP_SET* set, /**< global SCIP settings */
4600  SCIP_BOUNDTYPE boundtype, /**< type of bound for which the score should be increased */
4601  SCIP_BDCHGIDX* bdchgidx, /**< bound change index (time stamp of bound change), or NULL for current time */
4602  SCIP_Bool* used /**< pointer to store if the variable is already used */
4603  )
4604 {
4605  SCIP_Real newbound;
4606 
4607  /* convert bound to active problem variable */
4608  SCIP_CALL( convertToActiveVar(&var, set, &boundtype, NULL) );
4609 
4611  *used = FALSE;
4612  else
4613  {
4614  assert(SCIPvarIsActive(var));
4615  assert(var != NULL);
4616 
4617  switch( boundtype )
4618  {
4619  case SCIP_BOUNDTYPE_LOWER:
4620 
4621  newbound = SCIPgetVarLbAtIndex(set->scip, var, bdchgidx, FALSE);
4622 
4623  if( var->conflictlbcount == conflict->count && var->conflictlb >= newbound )
4624  {
4625  SCIPsetDebugMsg(set, "already queued bound change <%s> >= %g\n", SCIPvarGetName(var), newbound);
4626  *used = TRUE;
4627  }
4628  else
4629  *used = FALSE;
4630  break;
4631  case SCIP_BOUNDTYPE_UPPER:
4632 
4633  newbound = SCIPgetVarUbAtIndex(set->scip, var, bdchgidx, FALSE);
4634 
4635  if( var->conflictubcount == conflict->count && var->conflictub <= newbound )
4636  {
4637  SCIPsetDebugMsg(set, "already queued bound change <%s> <= %g\n", SCIPvarGetName(var), newbound);
4638  *used = TRUE;
4639  }
4640  else
4641  *used = FALSE;
4642  break;
4643  default:
4644  SCIPerrorMessage("invalid bound type %d\n", boundtype);
4645  SCIPABORT();
4646  *used = FALSE; /*lint !e527*/
4647  }
4648  }
4649 
4650  return SCIP_OKAY;
4651 }
4652 
4653 /** returns the conflict lower bound if the variable is present in the current conflict set; otherwise the global lower
4654  * bound
4655  */
4657  SCIP_CONFLICT* conflict, /**< conflict analysis data */
4658  SCIP_VAR* var /**< problem variable */
4659  )
4660 {
4661  if( var->conflictlbcount == conflict->count )
4662  {
4663  assert(EPSGE(var->conflictlb, var->conflictrelaxedlb, 1e-09));
4664  return var->conflictrelaxedlb;
4665  }
4666 
4667  return SCIPvarGetLbGlobal(var);
4668 }
4669 
4670 /** returns the conflict upper bound if the variable is present in the current conflict set; otherwise the global upper
4671  * bound
4672  */
4674  SCIP_CONFLICT* conflict, /**< conflict analysis data */
4675  SCIP_VAR* var /**< problem variable */
4676  )
4677 {
4678  if( var->conflictubcount == conflict->count )
4679  {
4680  assert(EPSLE(var->conflictub, var->conflictrelaxedub, 1e-09));
4681  return var->conflictrelaxedub;
4682  }
4683 
4684  return SCIPvarGetUbGlobal(var);
4685 }
4686 
4687 /** removes and returns next conflict analysis candidate from the candidate queue */
4688 static
4690  SCIP_CONFLICT* conflict /**< conflict analysis data */
4691  )
4692 {
4693  SCIP_BDCHGINFO* bdchginfo;
4694  SCIP_VAR* var;
4695 
4696  assert(conflict != NULL);
4697 
4698  if( SCIPpqueueNElems(conflict->forcedbdchgqueue) > 0 )
4699  bdchginfo = (SCIP_BDCHGINFO*)(SCIPpqueueRemove(conflict->forcedbdchgqueue));
4700  else
4701  bdchginfo = (SCIP_BDCHGINFO*)(SCIPpqueueRemove(conflict->bdchgqueue));
4702 
4703  assert(!SCIPbdchginfoIsRedundant(bdchginfo));
4704 
4705  /* if we have a candidate this one should be valid for the current conflict analysis */
4706  assert(!bdchginfoIsInvalid(conflict, bdchginfo));
4707 
4708  /* mark the bound change to be no longer in the conflict (it will be either added again to the conflict set or
4709  * replaced by resolving, which might add a weaker change on the same bound to the queue)
4710  */
4711  var = SCIPbdchginfoGetVar(bdchginfo);
4713  {
4714  var->conflictlbcount = 0;
4716  }
4717  else
4718  {
4719  assert(SCIPbdchginfoGetBoundtype(bdchginfo) == SCIP_BOUNDTYPE_UPPER);
4720  var->conflictubcount = 0;
4722  }
4723 
4724 #ifdef SCIP_CONFGRAPH
4725  confgraphSetCurrentBdchg(bdchginfo);
4726 #endif
4727 
4728  return bdchginfo;
4729 }
4730 
4731 /** returns next conflict analysis candidate from the candidate queue without removing it */
4732 static
4734  SCIP_CONFLICT* conflict /**< conflict analysis data */
4735  )
4736 {
4737  SCIP_BDCHGINFO* bdchginfo;
4738 
4739  assert(conflict != NULL);
4740 
4741  if( SCIPpqueueNElems(conflict->forcedbdchgqueue) > 0 )
4742  {
4743  /* get next potetioal candidate */
4744  bdchginfo = (SCIP_BDCHGINFO*)(SCIPpqueueFirst(conflict->forcedbdchgqueue));
4745 
4746  /* check if this candidate is valid */
4747  if( bdchginfoIsInvalid(conflict, bdchginfo) )
4748  {
4749  SCIPdebugMessage("bound change info [%d:<%s> %s %g] is invaild -> pop it from the force queue\n", SCIPbdchginfoGetDepth(bdchginfo),
4750  SCIPvarGetName(SCIPbdchginfoGetVar(bdchginfo)),
4751  SCIPbdchginfoGetBoundtype(bdchginfo) == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=",
4752  SCIPbdchginfoGetNewbound(bdchginfo));
4753 
4754  /* pop the invalid bound change info from the queue */
4755  (void)(SCIPpqueueRemove(conflict->forcedbdchgqueue));
4756 
4757  /* call method recursively to get next conflict analysis candidate */
4758  bdchginfo = conflictFirstCand(conflict);
4759  }
4760  }
4761  else
4762  {
4763  bdchginfo = (SCIP_BDCHGINFO*)(SCIPpqueueFirst(conflict->bdchgqueue));
4764 
4765  /* check if this candidate is valid */
4766  if( bdchginfo != NULL && bdchginfoIsInvalid(conflict, bdchginfo) )
4767  {
4768  SCIPdebugMessage("bound change info [%d:<%s> %s %g] is invaild -> pop it from the queue\n", SCIPbdchginfoGetDepth(bdchginfo),
4769  SCIPvarGetName(SCIPbdchginfoGetVar(bdchginfo)),
4770  SCIPbdchginfoGetBoundtype(bdchginfo) == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=",
4771  SCIPbdchginfoGetNewbound(bdchginfo));
4772 
4773  /* pop the invalid bound change info from the queue */
4774  (void)(SCIPpqueueRemove(conflict->bdchgqueue));
4775 
4776  /* call method recursively to get next conflict analysis candidate */
4777  bdchginfo = conflictFirstCand(conflict);
4778  }
4779  }
4780  assert(bdchginfo == NULL || !SCIPbdchginfoIsRedundant(bdchginfo));
4781 
4782  return bdchginfo;
4783 }
4784 
4785 /** adds the current conflict set (extended by all remaining bound changes in the queue) to the pool of conflict sets */
4786 static
4788  SCIP_CONFLICT* conflict, /**< conflict analysis data */
4789  BMS_BLKMEM* blkmem, /**< block memory of transformed problem */
4790  SCIP_SET* set, /**< global SCIP settings */
4791  SCIP_STAT* stat, /**< dynamic problem statistics */
4792  SCIP_TREE* tree, /**< branch and bound tree */
4793  int validdepth, /**< minimal depth level at which the conflict set is valid */
4794  SCIP_Bool diving, /**< are we in strong branching or diving mode? */
4795  SCIP_Bool repropagate, /**< should the constraint trigger a repropagation? */
4796  SCIP_Bool* success, /**< pointer to store whether the conflict set is valid */
4797  int* nliterals /**< pointer to store the number of literals in the generated conflictset */
4798  )
4799 {
4800  SCIP_CONFLICTSET* conflictset;
4801  SCIP_BDCHGINFO** bdchginfos;
4802  int nbdchginfos;
4803  int currentdepth;
4804  int focusdepth;
4805 
4806  assert(conflict != NULL);
4807  assert(conflict->conflictset != NULL);
4808  assert(set != NULL);
4809  assert(stat != NULL);
4810  assert(tree != NULL);
4811  assert(success != NULL);
4812  assert(nliterals != NULL);
4813  assert(SCIPpqueueNElems(conflict->forcedbdchgqueue) == 0);
4814 
4815  *success = FALSE;
4816  *nliterals = 0;
4817 
4818  /* check, whether local conflicts are allowed */
4819  validdepth = MAX(validdepth, conflict->conflictset->validdepth);
4820  if( !set->conf_allowlocal && validdepth > 0 )
4821  return SCIP_OKAY;
4822 
4823  focusdepth = SCIPtreeGetFocusDepth(tree);
4824  currentdepth = SCIPtreeGetCurrentDepth(tree);
4825  assert(currentdepth == tree->pathlen-1);
4826  assert(focusdepth <= currentdepth);
4827  assert(0 <= conflict->conflictset->validdepth && conflict->conflictset->validdepth <= currentdepth);
4828  assert(0 <= validdepth && validdepth <= currentdepth);
4829 
4830  /* get the elements of the bound change queue */
4831  bdchginfos = (SCIP_BDCHGINFO**)SCIPpqueueElems(conflict->bdchgqueue);
4832  nbdchginfos = SCIPpqueueNElems(conflict->bdchgqueue);
4833 
4834  /* create a copy of the current conflict set, allocating memory for the additional elements of the queue */
4835  SCIP_CALL( conflictsetCopy(&conflictset, blkmem, conflict->conflictset, nbdchginfos) );
4836  conflictset->validdepth = validdepth;
4837  conflictset->repropagate = repropagate;
4838 
4839  /* add the valid queue elements to the conflict set */
4840  SCIPsetDebugMsg(set, "adding %d variables from the queue as temporary conflict variables\n", nbdchginfos);
4841  SCIP_CALL( conflictsetAddBounds(conflict, conflictset, blkmem, set, bdchginfos, nbdchginfos) );
4842 
4843  /* calculate the depth, at which the conflictset should be inserted */
4844  SCIP_CALL( conflictsetCalcInsertDepth(conflictset, set, tree) );
4845  assert(conflictset->validdepth <= conflictset->insertdepth && conflictset->insertdepth <= currentdepth);
4846  SCIPsetDebugMsg(set, " -> conflict with %d literals found at depth %d is active in depth %d and valid in depth %d\n",
4847  conflictset->nbdchginfos, currentdepth, conflictset->insertdepth, conflictset->validdepth);
4848 
4849  /* if all branching variables are in the conflict set, the conflict set is of no use;
4850  * don't use conflict sets that are only valid in the probing path but not in the problem tree
4851  */
4852  if( (diving || conflictset->insertdepth < currentdepth) && conflictset->insertdepth <= focusdepth )
4853  {
4854  /* if the conflict should not be located only in the subtree where it is useful, put it to its valid depth level */
4855  if( !set->conf_settlelocal )
4856  conflictset->insertdepth = conflictset->validdepth;
4857 
4858  *nliterals = conflictset->nbdchginfos;
4859  SCIPsetDebugMsg(set, " -> final conflict set has %d literals\n", *nliterals);
4860 
4861  /* check conflict set on debugging solution */
4862  SCIP_CALL( SCIPdebugCheckConflict(blkmem, set, tree->path[validdepth], \
4863  conflictset->bdchginfos, conflictset->relaxedbds, conflictset->nbdchginfos) ); /*lint !e506 !e774*/
4864 
4865  /* move conflictset to the conflictset storage */
4866  SCIP_CALL( conflictInsertConflictset(conflict, blkmem, set, &conflictset) );
4867  *success = TRUE;
4868  }
4869  else
4870  {
4871  /* free the temporary conflict set */
4872  conflictsetFree(&conflictset, blkmem);
4873  }
4874 
4875  return SCIP_OKAY;
4876 }
4877 
4878 /** tries to resolve given bound change
4879  * - resolutions on local constraints are only applied, if the constraint is valid at the
4880  * current minimal valid depth level, because this depth level is the topmost level to add the conflict
4881  * constraint to anyways
4882  *
4883  * @note it is sufficient to explain the relaxed bound change
4884  */
4885 static
4887  SCIP_CONFLICT* conflict, /**< conflict analysis data */
4888  SCIP_SET* set, /**< global SCIP settings */
4889  SCIP_BDCHGINFO* bdchginfo, /**< bound change to resolve */
4890  SCIP_Real relaxedbd, /**< the relaxed bound */
4891  int validdepth, /**< minimal depth level at which the conflict is valid */
4892  SCIP_Bool* resolved /**< pointer to store whether the bound change was resolved */
4893  )
4894 {
4895  SCIP_VAR* actvar;
4896  SCIP_CONS* infercons;
4897  SCIP_PROP* inferprop;
4898  SCIP_RESULT result;
4899 
4900 #ifndef NDEBUG
4901  int nforcedbdchgqueue;
4902  int nbdchgqueue;
4903 
4904  /* store the current size of the conflict queues */
4905  assert(conflict != NULL);
4906  nforcedbdchgqueue = SCIPpqueueNElems(conflict->forcedbdchgqueue);
4907  nbdchgqueue = SCIPpqueueNElems(conflict->bdchgqueue);
4908 #else
4909  assert(conflict != NULL);
4910 #endif
4911 
4912  assert(resolved != NULL);
4913  assert(!SCIPbdchginfoIsRedundant(bdchginfo));
4914 
4915  *resolved = FALSE;
4916 
4917  actvar = SCIPbdchginfoGetVar(bdchginfo);
4918  assert(actvar != NULL);
4919  assert(SCIPvarIsActive(actvar));
4920 
4921 #ifdef SCIP_DEBUG
4922  {
4923  int i;
4924  SCIPsetDebugMsg(set, "processing next conflicting bound (depth: %d, valid depth: %d, bdchgtype: %s [%s], vartype: %d): [<%s> %s %g(%g)]\n",
4925  SCIPbdchginfoGetDepth(bdchginfo), validdepth,
4926  SCIPbdchginfoGetChgtype(bdchginfo) == SCIP_BOUNDCHGTYPE_BRANCHING ? "branch"
4927  : SCIPbdchginfoGetChgtype(bdchginfo) == SCIP_BOUNDCHGTYPE_CONSINFER ? "cons" : "prop",
4931  : SCIPbdchginfoGetInferProp(bdchginfo) == NULL ? "-"
4933  SCIPvarGetType(actvar), SCIPvarGetName(actvar),
4934  SCIPbdchginfoGetBoundtype(bdchginfo) == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=",
4935  SCIPbdchginfoGetNewbound(bdchginfo), relaxedbd);
4936  SCIPsetDebugMsg(set, " - conflict set :");
4937 
4938  for( i = 0; i < conflict->conflictset->nbdchginfos; ++i )
4939  {
4940  SCIPsetDebugMsgPrint(set, " [%d:<%s> %s %g(%g)]", SCIPbdchginfoGetDepth(conflict->conflictset->bdchginfos[i]),
4942  SCIPbdchginfoGetBoundtype(conflict->conflictset->bdchginfos[i]) == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=",
4943  SCIPbdchginfoGetNewbound(conflict->conflictset->bdchginfos[i]), conflict->conflictset->relaxedbds[i]);
4944  }
4945  SCIPsetDebugMsgPrint(set, "\n");
4946  SCIPsetDebugMsg(set, " - forced candidates :");
4947 
4948  for( i = 0; i < SCIPpqueueNElems(conflict->forcedbdchgqueue); ++i )
4949  {
4951  SCIPsetDebugMsgPrint(set, " [%d:<%s> %s %g(%g)]", SCIPbdchginfoGetDepth(info), SCIPvarGetName(SCIPbdchginfoGetVar(info)),
4952  bdchginfoIsInvalid(conflict, info) ? "<!>" : SCIPbdchginfoGetBoundtype(info) == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=",
4954  }
4955  SCIPsetDebugMsgPrint(set, "\n");
4956  SCIPsetDebugMsg(set, " - optional candidates:");
4957 
4958  for( i = 0; i < SCIPpqueueNElems(conflict->bdchgqueue); ++i )
4959  {
4960  SCIP_BDCHGINFO* info = (SCIP_BDCHGINFO*)(SCIPpqueueElems(conflict->bdchgqueue)[i]);
4961  SCIPsetDebugMsgPrint(set, " [%d:<%s> %s %g(%g)]", SCIPbdchginfoGetDepth(info), SCIPvarGetName(SCIPbdchginfoGetVar(info)),
4962  bdchginfoIsInvalid(conflict, info) ? "<!>" : SCIPbdchginfoGetBoundtype(info) == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=",
4964  }
4965  SCIPsetDebugMsgPrint(set, "\n");
4966  }
4967 #endif
4968 
4969  /* check, if the bound change can and should be resolved:
4970  * - resolutions on local constraints should only be applied, if the constraint is valid at the
4971  * current minimal valid depth level (which is initialized with the valid depth level of the initial
4972  * conflict set), because this depth level is the topmost level to add the conflict constraint to anyways
4973  */
4974  switch( SCIPbdchginfoGetChgtype(bdchginfo) )
4975  {
4977  infercons = SCIPbdchginfoGetInferCons(bdchginfo);
4978  assert(infercons != NULL);
4979 
4980  if( SCIPconsIsGlobal(infercons) || SCIPconsGetValidDepth(infercons) <= validdepth )
4981  {
4982  SCIP_VAR* infervar;
4983  int inferinfo;
4984  SCIP_BOUNDTYPE inferboundtype;
4985  SCIP_BDCHGIDX* bdchgidx;
4986 
4987  /* resolve bound change by asking the constraint that infered the bound to put all bounds that were
4988  * the reasons for the conflicting bound change on the priority queue
4989  */
4990  infervar = SCIPbdchginfoGetInferVar(bdchginfo);
4991  inferinfo = SCIPbdchginfoGetInferInfo(bdchginfo);
4992  inferboundtype = SCIPbdchginfoGetInferBoundtype(bdchginfo);
4993  bdchgidx = SCIPbdchginfoGetIdx(bdchginfo);
4994  assert(infervar != NULL);
4995 
4996  SCIPsetDebugMsg(set, "resolving bound <%s> %s %g(%g) [status:%d, type:%d, depth:%d, pos:%d]: <%s> %s %g [cons:<%s>(%s), info:%d]\n",
4997  SCIPvarGetName(actvar),
4998  SCIPbdchginfoGetBoundtype(bdchginfo) == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=",
4999  SCIPbdchginfoGetNewbound(bdchginfo), relaxedbd,
5000  SCIPvarGetStatus(actvar), SCIPvarGetType(actvar),
5001  SCIPbdchginfoGetDepth(bdchginfo), SCIPbdchginfoGetPos(bdchginfo),
5002  SCIPvarGetName(infervar),
5003  inferboundtype == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=",
5004  SCIPgetVarBdAtIndex(set->scip, infervar, inferboundtype, bdchgidx, TRUE),
5005  SCIPconsGetName(infercons),
5006  SCIPconsIsGlobal(infercons) ? "global" : "local",
5007  inferinfo);
5008 
5009  /* in case the inference variables is not an active variables, we need to transform the relaxed bound */
5010  if( actvar != infervar )
5011  {
5012  SCIP_VAR* var;
5013  SCIP_Real scalar;
5014  SCIP_Real constant;
5015 
5016  assert(SCIPvarGetStatus(infervar) == SCIP_VARSTATUS_AGGREGATED
5018  || (SCIPvarGetStatus(infervar) == SCIP_VARSTATUS_MULTAGGR && SCIPvarGetMultaggrNVars(infervar) == 1));
5019 
5020  scalar = 1.0;
5021  constant = 0.0;
5022 
5023  var = infervar;
5024 
5025  /* transform given varibale to active varibale */
5026  SCIP_CALL( SCIPvarGetProbvarSum(&var, set, &scalar, &constant) );
5027  assert(var == actvar);
5028 
5029  relaxedbd *= scalar;
5030  relaxedbd += constant;
5031  }
5032 
5033  SCIP_CALL( SCIPconsResolvePropagation(infercons, set, infervar, inferinfo, inferboundtype, bdchgidx, relaxedbd, &result) );
5034  *resolved = (result == SCIP_SUCCESS);
5035  }
5036  break;
5037 
5039  inferprop = SCIPbdchginfoGetInferProp(bdchginfo);
5040  if( inferprop != NULL )
5041  {
5042  SCIP_VAR* infervar;
5043  int inferinfo;
5044  SCIP_BOUNDTYPE inferboundtype;
5045  SCIP_BDCHGIDX* bdchgidx;
5046 
5047  /* resolve bound change by asking the propagator that infered the bound to put all bounds that were
5048  * the reasons for the conflicting bound change on the priority queue
5049  */
5050  infervar = SCIPbdchginfoGetInferVar(bdchginfo);
5051  inferinfo = SCIPbdchginfoGetInferInfo(bdchginfo);
5052  inferboundtype = SCIPbdchginfoGetInferBoundtype(bdchginfo);
5053  bdchgidx = SCIPbdchginfoGetIdx(bdchginfo);
5054  assert(infervar != NULL);
5055 
5056  SCIPsetDebugMsg(set, "resolving bound <%s> %s %g(%g) [status:%d, depth:%d, pos:%d]: <%s> %s %g [prop:<%s>, info:%d]\n",
5057  SCIPvarGetName(actvar),
5058  SCIPbdchginfoGetBoundtype(bdchginfo) == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=",
5059  SCIPbdchginfoGetNewbound(bdchginfo), relaxedbd,
5060  SCIPvarGetStatus(actvar), SCIPbdchginfoGetDepth(bdchginfo), SCIPbdchginfoGetPos(bdchginfo),
5061  SCIPvarGetName(infervar),
5062  inferboundtype == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=",
5063  SCIPgetVarBdAtIndex(set->scip, infervar, inferboundtype, bdchgidx, TRUE),
5064  SCIPpropGetName(inferprop), inferinfo);
5065 
5066  SCIP_CALL( SCIPpropResolvePropagation(inferprop, set, infervar, inferinfo, inferboundtype, bdchgidx, relaxedbd, &result) );
5067  *resolved = (result == SCIP_SUCCESS);
5068  }
5069  break;
5070 
5072  assert(!(*resolved));
5073  break;
5074 
5075  default:
5076  SCIPerrorMessage("invalid bound change type <%d>\n", SCIPbdchginfoGetChgtype(bdchginfo));
5077  return SCIP_INVALIDDATA;
5078  }
5079 
5080  SCIPsetDebugMsg(set, "resolving status: %u\n", *resolved);
5081 
5082 #ifndef NDEBUG
5083  /* subtract the size of the conflicq queues */
5084  nforcedbdchgqueue -= SCIPpqueueNElems(conflict->forcedbdchgqueue);
5085  nbdchgqueue -= SCIPpqueueNElems(conflict->bdchgqueue);
5086 
5087  /* in case the bound change was not resolved, the conflict queues should have the same size (contents) */
5088  assert((*resolved) || (nforcedbdchgqueue == 0 && nbdchgqueue == 0));
5089 #endif
5090 
5091  return SCIP_OKAY;
5092 }
5093 
5094 /** if only one conflicting bound change of the last depth level was used, and if this can be resolved,
5095  * creates GRASP-like reconvergence conflict constraints in the conflict graph up to the branching variable of this
5096  * depth level
5097  */
5098 static
5100  SCIP_CONFLICT* conflict, /**< conflict analysis data */
5101  BMS_BLKMEM* blkmem, /**< block memory of transformed problem */
5102  SCIP_SET* set, /**< global SCIP settings */
5103  SCIP_STAT* stat, /**< problem statistics */
5104  SCIP_PROB* prob, /**< problem data */
5105  SCIP_TREE* tree, /**< branch and bound tree */
5106  SCIP_Bool diving, /**< are we in strong branching or diving mode? */
5107  int validdepth, /**< minimal depth level at which the initial conflict set is valid */
5108  SCIP_BDCHGINFO* firstuip, /**< first UIP of conflict graph */
5109  int* nreconvconss, /**< pointer to store the number of generated reconvergence constraints */
5110  int* nreconvliterals /**< pointer to store the number of literals generated reconvergence constraints */
5111  )
5112 {
5113  SCIP_BDCHGINFO* uip;
5114  SCIP_CONFTYPE conftype;
5115  SCIP_Bool usescutoffbound;
5116  int firstuipdepth;
5117  int focusdepth;
5118  int currentdepth;
5119  int maxvaliddepth;
5120 
5121  assert(conflict != NULL);
5122  assert(firstuip != NULL);
5123  assert(nreconvconss != NULL);
5124  assert(nreconvliterals != NULL);
5125  assert(!SCIPbdchginfoIsRedundant(firstuip));
5126 
5127  focusdepth = SCIPtreeGetFocusDepth(tree);
5128  currentdepth = SCIPtreeGetCurrentDepth(tree);
5129  assert(currentdepth == tree->pathlen-1);
5130  assert(focusdepth <= currentdepth);
5131 
5132  /* check, whether local constraints are allowed; however, don't generate reconvergence constraints that are only valid
5133  * in the probing path and not in the problem tree (i.e. that exceed the focusdepth)
5134  */
5135  maxvaliddepth = (set->conf_allowlocal ? MIN(currentdepth-1, focusdepth) : 0);
5136  if( validdepth > maxvaliddepth )
5137  return SCIP_OKAY;
5138 
5139  firstuipdepth = SCIPbdchginfoGetDepth(firstuip);
5140 
5141  conftype = conflict->conflictset->conflicttype;
5142  usescutoffbound = conflict->conflictset->usescutoffbound;
5143 
5144  /* for each succeeding UIP pair of the last depth level, create one reconvergence constraint */
5145  uip = firstuip;
5146  while( uip != NULL && SCIPbdchginfoGetDepth(uip) == SCIPbdchginfoGetDepth(firstuip) && bdchginfoIsResolvable(uip) )
5147  {
5148  SCIP_BDCHGINFO* oppositeuip;
5149  SCIP_BDCHGINFO* bdchginfo;
5150  SCIP_BDCHGINFO* nextuip;
5151  SCIP_VAR* uipvar;
5152  SCIP_Real oppositeuipbound;
5153  SCIP_BOUNDTYPE oppositeuipboundtype;
5154  int nresolutions;
5155 
5156  assert(!SCIPbdchginfoIsRedundant(uip));
5157 
5158  SCIPsetDebugMsg(set, "creating reconvergence constraint for UIP <%s> %s %g in depth %d pos %d\n",
5161 
5162  /* initialize conflict data */
5163  SCIP_CALL( SCIPconflictInit(conflict, set, stat, prob, conftype, usescutoffbound) );
5164 
5165  conflict->conflictset->conflicttype = conftype;
5166  conflict->conflictset->usescutoffbound = usescutoffbound;
5167 
5168  /* create a temporary bound change information for the negation of the UIP's bound change;
5169  * this bound change information is freed in the SCIPconflictFlushConss() call;
5170  * for reconvergence constraints for continuous variables we can only use the "negation" !(x <= u) == (x >= u);
5171  * during conflict analysis, we treat a continuous bound "x >= u" in the conflict set as "x > u", and in the
5172  * generated constraint this is negated again to "x <= u" which is correct.
5173  */
5174  uipvar = SCIPbdchginfoGetVar(uip);
5175  oppositeuipboundtype = SCIPboundtypeOpposite(SCIPbdchginfoGetBoundtype(uip));
5176  oppositeuipbound = SCIPbdchginfoGetNewbound(uip);
5177  if( SCIPvarIsIntegral(uipvar) )
5178  {
5179  assert(SCIPsetIsIntegral(set, oppositeuipbound));
5180  oppositeuipbound += (oppositeuipboundtype == SCIP_BOUNDTYPE_LOWER ? +1.0 : -1.0);
5181  }
5182  SCIP_CALL( conflictCreateTmpBdchginfo(conflict, blkmem, set, uipvar, oppositeuipboundtype, \
5183  oppositeuipboundtype == SCIP_BOUNDTYPE_LOWER ? SCIP_REAL_MIN : SCIP_REAL_MAX, oppositeuipbound, &oppositeuip) );
5184 
5185  /* put the negated UIP into the conflict set */
5186  SCIP_CALL( conflictAddConflictBound(conflict, blkmem, set, oppositeuip, oppositeuipbound) );
5187 
5188  /* put positive UIP into priority queue */
5189  SCIP_CALL( conflictQueueBound(conflict, set, uip, SCIPbdchginfoGetNewbound(uip) ) );
5190 
5191  /* resolve the queue until the next UIP is reached */
5192  bdchginfo = conflictFirstCand(conflict);
5193  nextuip = NULL;
5194  nresolutions = 0;
5195  while( bdchginfo != NULL && validdepth <= maxvaliddepth )
5196  {
5197  SCIP_BDCHGINFO* nextbdchginfo;
5198  SCIP_Real relaxedbd;
5199  SCIP_Bool forceresolve;
5200  int bdchgdepth;
5201 
5202  /* check if the next bound change must be resolved in every case */
5203  forceresolve = (SCIPpqueueNElems(conflict->forcedbdchgqueue) > 0);
5204 
5205  /* remove currently processed candidate and get next conflicting bound from the conflict candidate queue before
5206  * we remove the candidate we have to collect the relaxed bound since removing the candidate from the queue
5207  * invalidates the relaxed bound
5208  */
5209  assert(bdchginfo == conflictFirstCand(conflict));
5210  relaxedbd = SCIPbdchginfoGetRelaxedBound(bdchginfo);
5211  bdchginfo = conflictRemoveCand(conflict);
5212  nextbdchginfo = conflictFirstCand(conflict);
5213  bdchgdepth = SCIPbdchginfoGetDepth(bdchginfo);
5214  assert(bdchginfo != NULL);
5215  assert(!SCIPbdchginfoIsRedundant(bdchginfo));
5216  assert(nextbdchginfo == NULL || SCIPbdchginfoGetDepth(bdchginfo) >= SCIPbdchginfoGetDepth(nextbdchginfo)
5217  || forceresolve);
5218  assert(bdchgdepth <= firstuipdepth);
5219 
5220  /* bound changes that are higher in the tree than the valid depth of the conflict can be ignored;
5221  * multiple insertions of the same bound change can be ignored
5222  */
5223  if( bdchgdepth > validdepth && bdchginfo != nextbdchginfo )
5224  {
5225  SCIP_VAR* actvar;
5226  SCIP_Bool resolved;
5227 
5228  actvar = SCIPbdchginfoGetVar(bdchginfo);
5229  assert(actvar != NULL);
5230  assert(SCIPvarIsActive(actvar));
5231 
5232  /* check if we have to resolve the bound change in this depth level
5233  * - the starting uip has to be resolved
5234  * - a bound change should be resolved, if it is in the fuip's depth level and not the
5235  * next uip (i.e., if it is not the last bound change in the fuip's depth level)
5236  * - a forced bound change must be resolved in any case
5237  */
5238  resolved = FALSE;
5239  if( bdchginfo == uip
5240  || (bdchgdepth == firstuipdepth
5241  && nextbdchginfo != NULL
5242  && SCIPbdchginfoGetDepth(nextbdchginfo) == bdchgdepth)
5243  || forceresolve )
5244  {
5245  SCIP_CALL( conflictResolveBound(conflict, set, bdchginfo, relaxedbd, validdepth, &resolved) );
5246  }
5247 
5248  if( resolved )
5249  nresolutions++;
5250  else if( forceresolve )
5251  {
5252  /* variable cannot enter the conflict clause: we have to make the conflict clause local, s.t.
5253  * the unresolved bound change is active in the whole sub tree of the conflict clause
5254  */
5255  assert(bdchgdepth >= validdepth);
5256  validdepth = bdchgdepth;
5257 
5258  SCIPsetDebugMsg(set, "couldn't resolve forced bound change on <%s> -> new valid depth: %d\n",
5259  SCIPvarGetName(actvar), validdepth);
5260  }
5261  else if( bdchginfo != uip )
5262  {
5263  assert(conflict->conflictset != NULL);
5264  assert(conflict->conflictset->nbdchginfos >= 1); /* starting UIP is already member of the conflict set */
5265 
5266  /* if this is the first variable of the conflict set besides the current starting UIP, it is the next
5267  * UIP (or the first unresolvable bound change)
5268  */
5269  if( bdchgdepth == firstuipdepth && conflict->conflictset->nbdchginfos == 1 )
5270  {
5271  assert(nextuip == NULL);
5272  nextuip = bdchginfo;
5273  }
5274 
5275  /* put bound change into the conflict set */
5276  SCIP_CALL( conflictAddConflictBound(conflict, blkmem, set, bdchginfo, relaxedbd) );
5277  assert(conflict->conflictset->nbdchginfos >= 2);
5278  }
5279  else
5280  assert(conflictFirstCand(conflict) == NULL); /* the starting UIP was not resolved */
5281  }
5282 
5283  /* get next conflicting bound from the conflict candidate queue (this does not need to be nextbdchginfo, because
5284  * due to resolving the bound changes, a variable could be added to the queue which must be
5285  * resolved before nextbdchginfo)
5286  */
5287  bdchginfo = conflictFirstCand(conflict);
5288  }
5289  assert(nextuip != uip);
5290 
5291  /* if only one propagation was resolved, the reconvergence constraint is already member of the constraint set
5292  * (it is exactly the constraint that produced the propagation)
5293  */
5294  if( nextuip != NULL && nresolutions >= 2 && bdchginfo == NULL && validdepth <= maxvaliddepth )
5295  {
5296  int nlits;
5297  SCIP_Bool success;
5298 
5299  assert(SCIPbdchginfoGetDepth(nextuip) == SCIPbdchginfoGetDepth(uip));
5300 
5301  /* check conflict graph frontier on debugging solution */
5302  SCIP_CALL( SCIPdebugCheckConflictFrontier(blkmem, set, tree->path[validdepth], \
5303  bdchginfo, conflict->conflictset->bdchginfos, conflict->conflictset->relaxedbds, \
5304  conflict->conflictset->nbdchginfos, conflict->bdchgqueue, conflict->forcedbdchgqueue) ); /*lint !e506 !e774*/
5305 
5306  SCIPsetDebugMsg(set, "creating reconvergence constraint from UIP <%s> to UIP <%s> in depth %d with %d literals after %d resolutions\n",
5308  SCIPbdchginfoGetDepth(uip), conflict->conflictset->nbdchginfos, nresolutions);
5309 
5310  /* call the conflict handlers to create a conflict set */
5311  SCIP_CALL( conflictAddConflictset(conflict, blkmem, set, stat, tree, validdepth, diving, FALSE, &success, &nlits) );
5312  if( success )
5313  {
5314  (*nreconvconss)++;
5315  (*nreconvliterals) += nlits;
5316  }
5317  }
5318 
5319  /* clear the conflict candidate queue and the conflict set (to make sure, oppositeuip is not referenced anymore) */
5320  conflictClear(conflict);
5321 
5322  uip = nextuip;
5323  }
5324 
5325  conflict->conflictset->conflicttype = conftype;
5326  conflict->conflictset->usescutoffbound = usescutoffbound;
5327 
5328  return SCIP_OKAY;
5329 }
5330 
5331 /** analyzes conflicting bound changes that were added with calls to SCIPconflictAddBound() and
5332  * SCIPconflictAddRelaxedBound(), and on success, calls the conflict handlers to create a conflict constraint out of
5333  * the resulting conflict set; afterwards the conflict queue and the conflict set is cleared
5334  */
5335 static
5337  SCIP_CONFLICT* conflict, /**< conflict analysis data */
5338  BMS_BLKMEM* blkmem, /**< block memory of transformed problem */
5339  SCIP_SET* set, /**< global SCIP settings */
5340  SCIP_STAT* stat, /**< problem statistics */
5341  SCIP_PROB* prob, /**< problem data */
5342  SCIP_TREE* tree, /**< branch and bound tree */
5343  SCIP_Bool diving, /**< are we in strong branching or diving mode? */
5344  int validdepth, /**< minimal depth level at which the initial conflict set is valid */
5345  SCIP_Bool mustresolve, /**< should the conflict set only be used, if a resolution was applied? */
5346  int* nconss, /**< pointer to store the number of generated conflict constraints */
5347  int* nliterals, /**< pointer to store the number of literals in generated conflict constraints */
5348  int* nreconvconss, /**< pointer to store the number of generated reconvergence constraints */
5349  int* nreconvliterals /**< pointer to store the number of literals generated reconvergence constraints */
5350  )
5351 {
5352  SCIP_BDCHGINFO* bdchginfo;
5353  SCIP_BDCHGINFO** firstuips;
5354  SCIP_CONFTYPE conftype;
5355  int nfirstuips;
5356  int focusdepth;
5357  int currentdepth;
5358  int maxvaliddepth;
5359  int resolvedepth;
5360  int nresolutions;
5361  int lastconsnresolutions;
5362  int lastconsresoldepth;
5363 
5364  assert(conflict != NULL);
5365  assert(conflict->conflictset != NULL);
5366  assert(conflict->conflictset->nbdchginfos >= 0);
5367  assert(set != NULL);
5368  assert(stat != NULL);
5369  assert(0 <= validdepth && validdepth <= SCIPtreeGetCurrentDepth(tree));
5370  assert(nconss != NULL);
5371  assert(nliterals != NULL);
5372  assert(nreconvconss != NULL);
5373  assert(nreconvliterals != NULL);
5374 
5375  focusdepth = SCIPtreeGetFocusDepth(tree);
5376  currentdepth = SCIPtreeGetCurrentDepth(tree);
5377  assert(currentdepth == tree->pathlen-1);
5378  assert(focusdepth <= currentdepth);
5379 
5380  resolvedepth = ((set->conf_fuiplevels >= 0 && set->conf_fuiplevels <= currentdepth)
5381  ? currentdepth - set->conf_fuiplevels + 1 : 0);
5382  assert(0 <= resolvedepth && resolvedepth <= currentdepth + 1);
5383 
5384  /* if we must resolve at least one bound change, find the first UIP at least in the last depth level */
5385  if( mustresolve )
5386  resolvedepth = MIN(resolvedepth, currentdepth);
5387 
5388  SCIPsetDebugMsg(set, "analyzing conflict with %d+%d conflict candidates and starting conflict set of size %d in depth %d (resolvedepth=%d)\n",
5390  conflict->conflictset->nbdchginfos, currentdepth, resolvedepth);
5391 
5392  *nconss = 0;
5393  *nliterals = 0;
5394  *nreconvconss = 0;
5395  *nreconvliterals = 0;
5396 
5397  /* check, whether local conflicts are allowed; however, don't generate conflict constraints that are only valid in the
5398  * probing path and not in the problem tree (i.e. that exceed the focusdepth)
5399  */
5400  maxvaliddepth = (set->conf_allowlocal ? MIN(currentdepth-1, focusdepth) : 0);
5401  if( validdepth > maxvaliddepth )
5402  return SCIP_OKAY;
5403 
5404  /* allocate temporary memory for storing first UIPs (in each depth level, at most two bound changes can be flagged
5405  * as UIP, namely a binary and a non-binary bound change)
5406  */
5407  SCIP_CALL( SCIPsetAllocBufferArray(set, &firstuips, 2*(currentdepth+1)) ); /*lint !e647*/
5408 
5409  /* process all bound changes in the conflict candidate queue */
5410  nresolutions = 0;
5411  lastconsnresolutions = (mustresolve ? 0 : -1);
5412  lastconsresoldepth = (mustresolve ? currentdepth : INT_MAX);
5413  bdchginfo = conflictFirstCand(conflict);
5414  nfirstuips = 0;
5415 
5416  /* check if the initial reason on debugging solution */
5417  SCIP_CALL( SCIPdebugCheckConflictFrontier(blkmem, set, tree->path[validdepth], \
5418  NULL, conflict->conflictset->bdchginfos, conflict->conflictset->relaxedbds, conflict->conflictset->nbdchginfos, \
5419  conflict->bdchgqueue, conflict->forcedbdchgqueue) ); /*lint !e506 !e774*/
5420 
5421  while( bdchginfo != NULL && validdepth <= maxvaliddepth )
5422  {
5423  SCIP_BDCHGINFO* nextbdchginfo;
5424  SCIP_Real relaxedbd;
5425  SCIP_Bool forceresolve;
5426  int bdchgdepth;
5427 
5428  assert(!SCIPbdchginfoIsRedundant(bdchginfo));
5429 
5430  /* check if the next bound change must be resolved in every case */
5431  forceresolve = (SCIPpqueueNElems(conflict->forcedbdchgqueue) > 0);
5432 
5433  /* resolve next bound change in queue */
5434  bdchgdepth = SCIPbdchginfoGetDepth(bdchginfo);
5435  assert(0 <= bdchgdepth && bdchgdepth <= currentdepth);
5436  assert(SCIPvarIsActive(SCIPbdchginfoGetVar(bdchginfo)));
5437  assert(bdchgdepth < tree->pathlen);
5438  assert(tree->path[bdchgdepth] != NULL);
5439  assert(tree->path[bdchgdepth]->domchg != NULL);
5440  assert(SCIPbdchginfoGetPos(bdchginfo) < (int)tree->path[bdchgdepth]->domchg->domchgbound.nboundchgs);
5441  assert(tree->path[bdchgdepth]->domchg->domchgbound.boundchgs[SCIPbdchginfoGetPos(bdchginfo)].var
5442  == SCIPbdchginfoGetVar(bdchginfo));
5443  assert(tree->path[bdchgdepth]->domchg->domchgbound.boundchgs[SCIPbdchginfoGetPos(bdchginfo)].newbound
5444  == SCIPbdchginfoGetNewbound(bdchginfo)
5447  == SCIPbdchginfoGetNewbound(bdchginfo)); /*lint !e777*/
5448  assert((SCIP_BOUNDTYPE)tree->path[bdchgdepth]->domchg->domchgbound.boundchgs[SCIPbdchginfoGetPos(bdchginfo)].boundtype
5449  == SCIPbdchginfoGetBoundtype(bdchginfo));
5450 
5451  /* create intermediate conflict constraint */
5452  assert(nresolutions >= lastconsnresolutions);
5453  if( !forceresolve )
5454  {
5455  if( nresolutions == lastconsnresolutions )
5456  lastconsresoldepth = bdchgdepth; /* all intermediate depth levels consisted of only unresolved bound changes */
5457  else if( bdchgdepth < lastconsresoldepth && (set->conf_interconss == -1 || *nconss < set->conf_interconss) )
5458  {
5459  int nlits;
5460  SCIP_Bool success;
5461 
5462  /* call the conflict handlers to create a conflict set */
5463  SCIPsetDebugMsg(set, "creating intermediate conflictset after %d resolutions up to depth %d (valid at depth %d): %d conflict bounds, %d bounds in queue\n",
5464  nresolutions, bdchgdepth, validdepth, conflict->conflictset->nbdchginfos,
5465  SCIPpqueueNElems(conflict->bdchgqueue));
5466 
5467  SCIP_CALL( conflictAddConflictset(conflict, blkmem, set, stat, tree, validdepth, diving, TRUE, &success, &nlits) );
5468  lastconsnresolutions = nresolutions;
5469  lastconsresoldepth = bdchgdepth;
5470  if( success )
5471  {
5472  (*nconss)++;
5473  (*nliterals) += nlits;
5474  }
5475  }
5476  }
5477 
5478  /* remove currently processed candidate and get next conflicting bound from the conflict candidate queue before
5479  * we remove the candidate we have to collect the relaxed bound since removing the candidate from the queue
5480  * invalidates the relaxed bound
5481  */
5482  assert(bdchginfo == conflictFirstCand(conflict));
5483  relaxedbd = SCIPbdchginfoGetRelaxedBound(bdchginfo);
5484  bdchginfo = conflictRemoveCand(conflict);
5485  nextbdchginfo = conflictFirstCand(conflict);
5486  assert(bdchginfo != NULL);
5487  assert(!SCIPbdchginfoIsRedundant(bdchginfo));
5488  assert(nextbdchginfo == NULL || SCIPbdchginfoGetDepth(bdchginfo) >= SCIPbdchginfoGetDepth(nextbdchginfo)
5489  || forceresolve);
5490 
5491  /* we don't need to resolve bound changes that are already active in the valid depth of the current conflict set,
5492  * because the conflict set can only be added locally at the valid depth, and all bound changes applied in this
5493  * depth or earlier can be removed from the conflict constraint, since they are already applied in the constraint's
5494  * subtree;
5495  * if the next bound change on the remaining queue is equal to the current bound change,
5496