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-2021 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->hasrelaxonlyvar = FALSE;
1282  conflictset->conflicttype = SCIP_CONFTYPE_UNKNOWN;
1283 }
1284 
1285 /** creates an empty conflict set */
1286 static
1288  SCIP_CONFLICTSET** conflictset, /**< pointer to store the conflict set */
1289  BMS_BLKMEM* blkmem /**< block memory of transformed problem */
1290  )
1291 {
1292  assert(conflictset != NULL);
1293 
1294  SCIP_ALLOC( BMSallocBlockMemory(blkmem, conflictset) );
1295  (*conflictset)->bdchginfos = NULL;
1296  (*conflictset)->relaxedbds = NULL;
1297  (*conflictset)->sortvals = NULL;
1298  (*conflictset)->bdchginfossize = 0;
1299 
1300  conflictsetClear(*conflictset);
1301 
1302  return SCIP_OKAY;
1303 }
1304 
1305 /** creates a copy of the given conflict set, allocating an additional amount of memory */
1306 static
1308  SCIP_CONFLICTSET** targetconflictset, /**< pointer to store the conflict set */
1309  BMS_BLKMEM* blkmem, /**< block memory of transformed problem */
1310  SCIP_CONFLICTSET* sourceconflictset, /**< source conflict set */
1311  int nadditionalelems /**< number of additional elements to allocate memory for */
1312  )
1313 {
1314  int targetsize;
1315 
1316  assert(targetconflictset != NULL);
1317  assert(sourceconflictset != NULL);
1318 
1319  targetsize = sourceconflictset->nbdchginfos + nadditionalelems;
1320  SCIP_ALLOC( BMSallocBlockMemory(blkmem, targetconflictset) );
1321  SCIP_ALLOC( BMSallocBlockMemoryArray(blkmem, &(*targetconflictset)->bdchginfos, targetsize) );
1322  SCIP_ALLOC( BMSallocBlockMemoryArray(blkmem, &(*targetconflictset)->relaxedbds, targetsize) );
1323  SCIP_ALLOC( BMSallocBlockMemoryArray(blkmem, &(*targetconflictset)->sortvals, targetsize) );
1324  (*targetconflictset)->bdchginfossize = targetsize;
1325 
1326  BMScopyMemoryArray((*targetconflictset)->bdchginfos, sourceconflictset->bdchginfos, sourceconflictset->nbdchginfos);
1327  BMScopyMemoryArray((*targetconflictset)->relaxedbds, sourceconflictset->relaxedbds, sourceconflictset->nbdchginfos);
1328  BMScopyMemoryArray((*targetconflictset)->sortvals, sourceconflictset->sortvals, sourceconflictset->nbdchginfos);
1329 
1330  (*targetconflictset)->nbdchginfos = sourceconflictset->nbdchginfos;
1331  (*targetconflictset)->validdepth = sourceconflictset->validdepth;
1332  (*targetconflictset)->insertdepth = sourceconflictset->insertdepth;
1333  (*targetconflictset)->conflictdepth = sourceconflictset->conflictdepth;
1334  (*targetconflictset)->repropdepth = sourceconflictset->repropdepth;
1335  (*targetconflictset)->usescutoffbound = sourceconflictset->usescutoffbound;
1336  (*targetconflictset)->hasrelaxonlyvar = sourceconflictset->hasrelaxonlyvar;
1337  (*targetconflictset)->conflicttype = sourceconflictset->conflicttype;
1338 
1339  return SCIP_OKAY;
1340 }
1341 
1342 /** frees a conflict set */
1343 static
1345  SCIP_CONFLICTSET** conflictset, /**< pointer to the conflict set */
1346  BMS_BLKMEM* blkmem /**< block memory of transformed problem */
1347  )
1348 {
1349  assert(conflictset != NULL);
1350  assert(*conflictset != NULL);
1351 
1352  BMSfreeBlockMemoryArrayNull(blkmem, &(*conflictset)->bdchginfos, (*conflictset)->bdchginfossize);
1353  BMSfreeBlockMemoryArrayNull(blkmem, &(*conflictset)->relaxedbds, (*conflictset)->bdchginfossize);
1354  BMSfreeBlockMemoryArrayNull(blkmem, &(*conflictset)->sortvals, (*conflictset)->bdchginfossize);
1355  BMSfreeBlockMemory(blkmem, conflictset);
1356 }
1357 
1358 /** resizes the arrays of the conflict set to be able to store at least num bound change entries */
1359 static
1361  SCIP_CONFLICTSET* conflictset, /**< conflict set */
1362  BMS_BLKMEM* blkmem, /**< block memory of transformed problem */
1363  SCIP_SET* set, /**< global SCIP settings */
1364  int num /**< minimal number of slots in arrays */
1365  )
1366 {
1367  assert(conflictset != NULL);
1368  assert(set != NULL);
1369 
1370  if( num > conflictset->bdchginfossize )
1371  {
1372  int newsize;
1373 
1374  newsize = SCIPsetCalcMemGrowSize(set, num);
1375  SCIP_ALLOC( BMSreallocBlockMemoryArray(blkmem, &conflictset->bdchginfos, conflictset->bdchginfossize, newsize) );
1376  SCIP_ALLOC( BMSreallocBlockMemoryArray(blkmem, &conflictset->relaxedbds, conflictset->bdchginfossize, newsize) );
1377  SCIP_ALLOC( BMSreallocBlockMemoryArray(blkmem, &conflictset->sortvals, conflictset->bdchginfossize, newsize) );
1378  conflictset->bdchginfossize = newsize;
1379  }
1380  assert(num <= conflictset->bdchginfossize);
1381 
1382  return SCIP_OKAY;
1383 }
1384 
1385 /** calculates the score of the conflict set
1386  *
1387  * the score is weighted sum of number of bound changes, repropagation depth, and valid depth
1388  */
1389 static
1391  SCIP_CONFLICTSET* conflictset, /**< conflict set */
1392  SCIP_SET* set /**< global SCIP settings */
1393  )
1394 {
1395  assert(conflictset != NULL);
1396 
1397  return -(set->conf_weightsize * conflictset->nbdchginfos
1398  + set->conf_weightrepropdepth * conflictset->repropdepth
1399  + set->conf_weightvaliddepth * conflictset->validdepth);
1400 }
1401 
1402 /** calculates the score of a bound change within a conflict */
1403 static
1405  SCIP_Real prooflhs, /**< lhs of proof constraint */
1406  SCIP_Real proofact, /**< activity of the proof constraint */
1407  SCIP_Real proofactdelta, /**< activity change */
1408  SCIP_Real proofcoef, /**< coefficient in proof constraint */
1409  int depth, /**< bound change depth */
1410  int currentdepth, /**< current depth */
1411  SCIP_VAR* var, /**< variable corresponding to bound change */
1412  SCIP_SET* set /**< global SCIP settings */
1413  )
1414 {
1415  SCIP_COL* col;
1416  SCIP_Real score;
1417 
1418  score = set->conf_proofscorefac * (1.0 - proofactdelta/(prooflhs - proofact));
1419  score = MAX(score, 0.0);
1420  score += set->conf_depthscorefac * (SCIP_Real)(depth+1)/(SCIP_Real)(currentdepth+1);
1421 
1423  col = SCIPvarGetCol(var);
1424  else
1425  col = NULL;
1426 
1427  if( proofcoef > 0.0 )
1428  {
1429  if( col != NULL && SCIPcolGetNNonz(col) > 0 )
1430  score += set->conf_uplockscorefac
1432  else
1433  score += set->conf_uplockscorefac * SCIPvarGetNLocksUpType(var, SCIP_LOCKTYPE_MODEL);
1434  }
1435  else
1436  {
1437  if( col != NULL && SCIPcolGetNNonz(col) > 0 )
1438  score += set->conf_downlockscorefac
1440  else
1441  score += set->conf_downlockscorefac * SCIPvarGetNLocksDownType(var, SCIP_LOCKTYPE_MODEL);
1442  }
1443 
1444  return score;
1445 }
1446 
1447 /** check if the bound change info (which is the potential next candidate which is queued) is valid for the current
1448  * conflict analysis; a bound change info can get invalid if after this one was added to the queue, a weaker bound
1449  * change was added to the queue (due the bound widening idea) which immediately makes this bound change redundant; due
1450  * to the priority we did not removed that bound change info since that cost O(log(n)); hence we have to skip/ignore it
1451  * now
1452  *
1453  * The following situations can occur before for example the bound change info (x >= 3) is potentially popped from the
1454  * queue.
1455  *
1456  * Postcondition: the reason why (x >= 3) was queued is that at this time point no lower bound of x was involved yet in
1457  * the current conflict or the lower bound which was involved until then was stronger, e.g., (x >= 2).
1458  *
1459  * 1) during the time until (x >= 3) gets potentially popped no weaker lower bound was added to the queue, in that case
1460  * the conflictlbcount is valid and conflictlb is 3; that is (var->conflictlbcount == conflict->count &&
1461  * var->conflictlb == 3)
1462  *
1463  * 2) a weaker bound change info gets queued (e.g., x >= 4); this bound change is popped before (x >= 3) since it has
1464  * higher priority (which is the time stamp of the bound change info and (x >= 4) has to be done after (x >= 3)
1465  * during propagation or branching)
1466  *
1467  * a) if (x >= 4) is popped and added to the conflict set the conflictlbcount is still valid and conflictlb is at
1468  * most 4; that is (var->conflictlbcount == conflict->count && var->conflictlb >= 4); it follows that any bound
1469  * change info which is stronger than (x >= 4) gets ignored (for example x >= 2)
1470  *
1471  * b) if (x >= 4) is popped and resolved without introducing a new lower bound on x until (x >= 3) is a potentially
1472  * candidate the conflictlbcount indicates that bound change is currently not present; that is
1473  * (var->conflictlbcount != conflict->count)
1474  *
1475  * 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
1476  * pooped, the conflictlbcount indicates that bound change is currently present; that is (var->conflictlbcount ==
1477  * conflict->count); however the (x >= 3) only has be explained if conflictlb matches that one; that is
1478  * (var->conflictlb == bdchginfo->newbound); otherwise it redundant/invalid.
1479  */
1480 static
1482  SCIP_CONFLICT* conflict, /**< conflict analysis data */
1483  SCIP_BDCHGINFO* bdchginfo /**< bound change information */
1484  )
1485 {
1486  SCIP_VAR* var;
1487 
1488  assert(bdchginfo != NULL);
1489 
1490  var = SCIPbdchginfoGetVar(bdchginfo);
1491  assert(var != NULL);
1492 
1493  /* the bound change info of a binary (domained) variable can never be invalid since the concepts of relaxed bounds
1494  * and bound widening do not make sense for these type of variables
1495  */
1496  if( SCIPvarIsBinary(var) )
1497  return FALSE;
1498 
1499  /* check if the bdchginfo is invaild since a tight/weaker bound change was already explained */
1501  {
1502  if( var->conflictlbcount != conflict->count || var->conflictlb != SCIPbdchginfoGetNewbound(bdchginfo) ) /*lint !e777*/
1503  {
1504  assert(!SCIPvarIsBinary(var));
1505  return TRUE;
1506  }
1507  }
1508  else
1509  {
1510  assert(SCIPbdchginfoGetBoundtype(bdchginfo) == SCIP_BOUNDTYPE_UPPER);
1511 
1512  if( var->conflictubcount != conflict->count || var->conflictub != SCIPbdchginfoGetNewbound(bdchginfo) ) /*lint !e777*/
1513  {
1514  assert(!SCIPvarIsBinary(var));
1515  return TRUE;
1516  }
1517  }
1518 
1519  return FALSE;
1520 }
1521 
1522 /** adds a bound change to a conflict set */
1523 static
1525  SCIP_CONFLICTSET* conflictset, /**< conflict set */
1526  BMS_BLKMEM* blkmem, /**< block memory of transformed problem */
1527  SCIP_SET* set, /**< global SCIP settings */
1528  SCIP_BDCHGINFO* bdchginfo, /**< bound change to add to the conflict set */
1529  SCIP_Real relaxedbd /**< relaxed bound */
1530  )
1531 {
1532  SCIP_BDCHGINFO** bdchginfos;
1533  SCIP_Real* relaxedbds;
1534  int* sortvals;
1535  SCIP_VAR* var;
1536  SCIP_BOUNDTYPE boundtype;
1537  int idx;
1538  int sortval;
1539  int pos;
1540 
1541  assert(conflictset != NULL);
1542  assert(bdchginfo != NULL);
1543 
1544  /* allocate memory for additional element */
1545  SCIP_CALL( conflictsetEnsureBdchginfosMem(conflictset, blkmem, set, conflictset->nbdchginfos+1) );
1546 
1547  /* insert the new bound change in the arrays sorted by increasing variable index and by bound type */
1548  bdchginfos = conflictset->bdchginfos;
1549  relaxedbds = conflictset->relaxedbds;
1550  sortvals = conflictset->sortvals;
1551  var = SCIPbdchginfoGetVar(bdchginfo);
1552  boundtype = SCIPbdchginfoGetBoundtype(bdchginfo);
1553  idx = SCIPvarGetIndex(var);
1554  assert(idx < INT_MAX/2);
1555  assert((int)boundtype == 0 || (int)boundtype == 1);
1556  sortval = 2*idx + (int)boundtype; /* first sorting criteria: variable index, second criteria: boundtype */
1557 
1558  /* insert new element into the sorted arrays; if an element exits with the same value insert the new element afterwards
1559  *
1560  * @todo check if it better (faster) to first search for the position O(log n) and compare the sort values and if
1561  * they are equal just replace the element and if not run the insert method O(n)
1562  */
1563 
1564  SCIPsortedvecInsertIntPtrReal(sortvals, (void**)bdchginfos, relaxedbds, sortval, (void*)bdchginfo, relaxedbd, &conflictset->nbdchginfos, &pos);
1565  assert(pos == conflictset->nbdchginfos - 1 || sortval < sortvals[pos+1]);
1566 
1567  /* merge multiple bound changes */
1568  if( pos > 0 && sortval == sortvals[pos-1] )
1569  {
1570  /* this is a multiple bound change */
1571  if( SCIPbdchginfoIsTighter(bdchginfo, bdchginfos[pos-1]) )
1572  {
1573  /* remove the "old" bound change since the "new" one in tighter */
1574  SCIPsortedvecDelPosIntPtrReal(sortvals, (void**)bdchginfos, relaxedbds, pos-1, &conflictset->nbdchginfos);
1575  }
1576  else if( SCIPbdchginfoIsTighter(bdchginfos[pos-1], bdchginfo) )
1577  {
1578  /* remove the "new" bound change since the "old" one is tighter */
1579  SCIPsortedvecDelPosIntPtrReal(sortvals, (void**)bdchginfos, relaxedbds, pos, &conflictset->nbdchginfos);
1580  }
1581  else
1582  {
1583  /* both bound change are equivalent; hence, keep the worse relaxed bound and remove one of them */
1584  relaxedbds[pos-1] = boundtype == SCIP_BOUNDTYPE_LOWER ? MAX(relaxedbds[pos-1], relaxedbd) : MIN(relaxedbds[pos-1], relaxedbd);
1585  SCIPsortedvecDelPosIntPtrReal(sortvals, (void**)bdchginfos, relaxedbds, pos, &conflictset->nbdchginfos);
1586  }
1587  }
1588 
1589  if( SCIPvarIsRelaxationOnly(var) )
1590  conflictset->hasrelaxonlyvar = TRUE;
1591 
1592  return SCIP_OKAY;
1593 }
1594 
1595 /** adds given bound changes to a conflict set */
1596 static
1598  SCIP_CONFLICT* conflict, /**< conflict analysis data */
1599  SCIP_CONFLICTSET* conflictset, /**< conflict set */
1600  BMS_BLKMEM* blkmem, /**< block memory of transformed problem */
1601  SCIP_SET* set, /**< global SCIP settings */
1602  SCIP_BDCHGINFO** bdchginfos, /**< bound changes to add to the conflict set */
1603  int nbdchginfos /**< number of bound changes to add */
1604  )
1605 {
1606  SCIP_BDCHGINFO** confbdchginfos;
1607  SCIP_BDCHGINFO* bdchginfo;
1608  SCIP_Real* confrelaxedbds;
1609  int* confsortvals;
1610  int confnbdchginfos;
1611  int idx;
1612  int sortval;
1613  int i;
1614  SCIP_BOUNDTYPE boundtype;
1615 
1616  assert(conflict != NULL);
1617  assert(conflictset != NULL);
1618  assert(blkmem != NULL);
1619  assert(set != NULL);
1620  assert(bdchginfos != NULL || nbdchginfos == 0);
1621 
1622  /* nothing to add */
1623  if( nbdchginfos == 0 )
1624  return SCIP_OKAY;
1625 
1626  assert(bdchginfos != NULL);
1627 
1628  /* only one element to add, use the single insertion method */
1629  if( nbdchginfos == 1 )
1630  {
1631  bdchginfo = bdchginfos[0];
1632  assert(bdchginfo != NULL);
1633 
1634  if( !bdchginfoIsInvalid(conflict, bdchginfo) )
1635  {
1636  SCIP_CALL( conflictsetAddBound(conflictset, blkmem, set, bdchginfo, SCIPbdchginfoGetRelaxedBound(bdchginfo)) );
1637  }
1638  else
1639  {
1640  SCIPsetDebugMsg(set, "-> bound change info [%d:<%s> %s %g] is invaild -> ignore it\n", SCIPbdchginfoGetDepth(bdchginfo),
1641  SCIPvarGetName(SCIPbdchginfoGetVar(bdchginfo)),
1642  SCIPbdchginfoGetBoundtype(bdchginfo) == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=",
1643  SCIPbdchginfoGetNewbound(bdchginfo));
1644  }
1645 
1646  return SCIP_OKAY;
1647  }
1648 
1649  confnbdchginfos = conflictset->nbdchginfos;
1650 
1651  /* allocate memory for additional element */
1652  SCIP_CALL( conflictsetEnsureBdchginfosMem(conflictset, blkmem, set, confnbdchginfos + nbdchginfos) );
1653 
1654  confbdchginfos = conflictset->bdchginfos;
1655  confrelaxedbds = conflictset->relaxedbds;
1656  confsortvals = conflictset->sortvals;
1657 
1658  assert(SCIP_BOUNDTYPE_LOWER == FALSE); /*lint !e641 !e506*/
1659  assert(SCIP_BOUNDTYPE_UPPER == TRUE); /*lint !e641 !e506*/
1660 
1661  for( i = 0; i < nbdchginfos; ++i )
1662  {
1663  bdchginfo = bdchginfos[i];
1664  assert(bdchginfo != NULL);
1665 
1666  /* add only valid bound change infos */
1667  if( !bdchginfoIsInvalid(conflict, bdchginfo) )
1668  {
1669  /* calculate sorting value */
1670  boundtype = SCIPbdchginfoGetBoundtype(bdchginfo);
1671  assert(SCIPbdchginfoGetVar(bdchginfo) != NULL);
1672 
1673  idx = SCIPvarGetIndex(SCIPbdchginfoGetVar(bdchginfo));
1674  assert(idx < INT_MAX/2);
1675 
1676  assert((int)boundtype == 0 || (int)boundtype == 1);
1677  sortval = 2*idx + (int)boundtype; /* first sorting criteria: variable index, second criteria: boundtype */
1678 
1679  /* add new element */
1680  confbdchginfos[confnbdchginfos] = bdchginfo;
1681  confrelaxedbds[confnbdchginfos] = SCIPbdchginfoGetRelaxedBound(bdchginfo);
1682  confsortvals[confnbdchginfos] = sortval;
1683  ++confnbdchginfos;
1684 
1686  conflictset->hasrelaxonlyvar = TRUE;
1687  }
1688  else
1689  {
1690  SCIPsetDebugMsg(set, "-> bound change info [%d:<%s> %s %g] is invaild -> ignore it\n", SCIPbdchginfoGetDepth(bdchginfo),
1691  SCIPvarGetName(SCIPbdchginfoGetVar(bdchginfo)),
1692  SCIPbdchginfoGetBoundtype(bdchginfo) == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=",
1693  SCIPbdchginfoGetNewbound(bdchginfo));
1694  }
1695  }
1696  assert(confnbdchginfos <= conflictset->nbdchginfos + nbdchginfos);
1697 
1698  /* sort and merge the new conflict set */
1699  if( confnbdchginfos > conflictset->nbdchginfos )
1700  {
1701  int k = 0;
1702 
1703  /* sort array */
1704  SCIPsortIntPtrReal(confsortvals, (void**)confbdchginfos, confrelaxedbds, confnbdchginfos);
1705 
1706  i = 1;
1707  /* merge multiple bound changes */
1708  while( i < confnbdchginfos )
1709  {
1710  assert(i > k);
1711 
1712  /* is this a multiple bound change */
1713  if( confsortvals[k] == confsortvals[i] )
1714  {
1715  if( SCIPbdchginfoIsTighter(confbdchginfos[k], confbdchginfos[i]) )
1716  ++i;
1717  else if( SCIPbdchginfoIsTighter(confbdchginfos[i], confbdchginfos[k]) )
1718  {
1719  /* replace worse bound change info by tighter bound change info */
1720  confbdchginfos[k] = confbdchginfos[i];
1721  confrelaxedbds[k] = confrelaxedbds[i];
1722  confsortvals[k] = confsortvals[i];
1723  ++i;
1724  }
1725  else
1726  {
1727  assert(confsortvals[k] == confsortvals[i]);
1728 
1729  /* both bound change are equivalent; hence, keep the worse relaxed bound and remove one of them */
1730  confrelaxedbds[k] = (confsortvals[k] % 2 == 0) ? MAX(confrelaxedbds[k], confrelaxedbds[i]) : MIN(confrelaxedbds[k], confrelaxedbds[i]);
1731  ++i;
1732  }
1733  }
1734  else
1735  {
1736  /* all bound change infos must be valid */
1737  assert(!bdchginfoIsInvalid(conflict, confbdchginfos[k]));
1738 
1739  ++k;
1740  /* move next comparison element to the correct position */
1741  if( k != i )
1742  {
1743  confbdchginfos[k] = confbdchginfos[i];
1744  confrelaxedbds[k] = confrelaxedbds[i];
1745  confsortvals[k] = confsortvals[i];
1746  }
1747  ++i;
1748  }
1749  }
1750  /* last bound change infos must also be valid */
1751  assert(!bdchginfoIsInvalid(conflict, confbdchginfos[k]));
1752  /* the number of bound change infos cannot be decreased, it would mean that the conflict set was not merged
1753  * before
1754  */
1755  assert(conflictset->nbdchginfos <= k + 1 );
1756  assert(k + 1 <= confnbdchginfos);
1757 
1758  conflictset->nbdchginfos = k + 1;
1759  }
1760 
1761  return SCIP_OKAY;
1762 }
1763 
1764 /** calculates the conflict and the repropagation depths of the conflict set */
1765 static
1767  SCIP_CONFLICTSET* conflictset /**< conflict set */
1768  )
1769 {
1770  int maxdepth[2];
1771  int i;
1772 
1773  assert(conflictset != NULL);
1774  assert(conflictset->validdepth <= conflictset->insertdepth);
1775 
1776  /* get the depth of the last and last but one bound change */
1777  maxdepth[0] = conflictset->validdepth;
1778  maxdepth[1] = conflictset->validdepth;
1779  for( i = 0; i < conflictset->nbdchginfos; ++i )
1780  {
1781  int depth;
1782 
1783  depth = SCIPbdchginfoGetDepth(conflictset->bdchginfos[i]);
1784  assert(depth >= 0);
1785  if( depth > maxdepth[0] )
1786  {
1787  maxdepth[1] = maxdepth[0];
1788  maxdepth[0] = depth;
1789  }
1790  else if( depth > maxdepth[1] )
1791  maxdepth[1] = depth;
1792  }
1793  assert(maxdepth[0] >= maxdepth[1]);
1794 
1795  conflictset->conflictdepth = maxdepth[0];
1796  conflictset->repropdepth = maxdepth[1];
1797 }
1798 
1799 /** identifies the depth, at which the conflict set should be added:
1800  * - if the branching rule operates on variables only, and if all branching variables up to a certain
1801  * depth level are member of the conflict, the conflict constraint can only be violated in the subtree
1802  * of the node at that depth, because in all other nodes, at least one of these branching variables
1803  * violates its conflicting bound, such that the conflict constraint is feasible
1804  * - if there is at least one branching variable in a node, we assume, that this branching was performed
1805  * on variables, and that the siblings of this node are disjunct w.r.t. the branching variables' fixings
1806  * - we have to add the conflict set at least in the valid depth of the initial conflict set,
1807  * so we start searching at the first branching after this depth level, i.e. validdepth+1
1808  */
1809 static
1811  SCIP_CONFLICTSET* conflictset, /**< conflict set */
1812  SCIP_SET* set, /**< global SCIP settings */
1813  SCIP_TREE* tree /**< branch and bound tree */
1814  )
1815 {
1816  SCIP_Bool* branchingincluded;
1817  int currentdepth;
1818  int i;
1819 
1820  assert(conflictset != NULL);
1821  assert(set != NULL);
1822  assert(tree != NULL);
1823 
1824  /* the conflict set must not be inserted prior to its valid depth */
1825  conflictset->insertdepth = conflictset->validdepth;
1826  assert(conflictset->insertdepth >= 0);
1827 
1828  currentdepth = SCIPtreeGetCurrentDepth(tree);
1829  assert(currentdepth == tree->pathlen-1);
1830 
1831  /* mark the levels for which a branching variable is included in the conflict set */
1832  SCIP_CALL( SCIPsetAllocBufferArray(set, &branchingincluded, currentdepth+2) );
1833  BMSclearMemoryArray(branchingincluded, currentdepth+2);
1834  for( i = 0; i < conflictset->nbdchginfos; ++i )
1835  {
1836  int depth;
1837 
1838  depth = SCIPbdchginfoGetDepth(conflictset->bdchginfos[i]);
1839  depth = MIN(depth, currentdepth+1); /* put diving/probing/strong branching changes in this depth level */
1840  branchingincluded[depth] = TRUE;
1841  }
1842 
1843  /* skip additional depth levels where branching on the conflict variables was applied */
1844  while( conflictset->insertdepth < currentdepth && branchingincluded[conflictset->insertdepth+1] )
1845  conflictset->insertdepth++;
1846 
1847  /* free temporary memory */
1848  SCIPsetFreeBufferArray(set, &branchingincluded);
1849 
1850  assert(conflictset->validdepth <= conflictset->insertdepth && conflictset->insertdepth <= currentdepth);
1851 
1852  return SCIP_OKAY;
1853 }
1854 
1855 /** checks whether the first conflict set is redundant to the second one */
1856 static
1858  SCIP_CONFLICTSET* conflictset1, /**< first conflict conflict set */
1859  SCIP_CONFLICTSET* conflictset2 /**< second conflict conflict set */
1860  )
1861 {
1862  int i1;
1863  int i2;
1864 
1865  assert(conflictset1 != NULL);
1866  assert(conflictset2 != NULL);
1867 
1868  /* if conflictset1 has smaller validdepth, it is definitely not redundant to conflictset2 */
1869  if( conflictset1->validdepth < conflictset2->validdepth )
1870  return FALSE;
1871 
1872  /* check, if all bound changes in conflictset2 are also present at least as tight in conflictset1;
1873  * we can stop immediately, if more bound changes are remaining in conflictset2 than in conflictset1
1874  */
1875  for( i1 = 0, i2 = 0; i2 < conflictset2->nbdchginfos && conflictset1->nbdchginfos - i1 >= conflictset2->nbdchginfos - i2;
1876  ++i1, ++i2 )
1877  {
1878  int sortval;
1879 
1880  assert(i2 == 0 || conflictset2->sortvals[i2-1] < conflictset2->sortvals[i2]);
1881 
1882  sortval = conflictset2->sortvals[i2];
1883  for( ; i1 < conflictset1->nbdchginfos && conflictset1->sortvals[i1] < sortval; ++i1 ) /*lint !e445*/
1884  {
1885  /* while scanning conflictset1, check consistency */
1886  assert(i1 == 0 || conflictset1->sortvals[i1-1] < conflictset1->sortvals[i1]);
1887  }
1888  if( i1 >= conflictset1->nbdchginfos || conflictset1->sortvals[i1] > sortval
1889  || SCIPbdchginfoIsTighter(conflictset2->bdchginfos[i2], conflictset1->bdchginfos[i1]) )
1890  return FALSE;
1891  }
1892 
1893  return (i2 == conflictset2->nbdchginfos);
1894 }
1895 
1896 #ifdef SCIP_DEBUG
1897 /** prints a conflict set to the screen */
1898 static
1899 void conflictsetPrint(
1900  SCIP_CONFLICTSET* conflictset /**< conflict set */
1901  )
1902 {
1903  int i;
1904 
1905  assert(conflictset != NULL);
1906  for( i = 0; i < conflictset->nbdchginfos; ++i )
1907  {
1908  SCIPdebugPrintf(" [%d:<%s> %s %g(%g)]", SCIPbdchginfoGetDepth(conflictset->bdchginfos[i]),
1909  SCIPvarGetName(SCIPbdchginfoGetVar(conflictset->bdchginfos[i])),
1910  SCIPbdchginfoGetBoundtype(conflictset->bdchginfos[i]) == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=",
1911  SCIPbdchginfoGetNewbound(conflictset->bdchginfos[i]), conflictset->relaxedbds[i]);
1912  }
1913  SCIPdebugPrintf("\n");
1914 }
1915 #endif
1916 
1917 /** resizes proofsets array to be able to store at least num entries */
1918 static
1920  SCIP_CONFLICT* conflict, /**< conflict analysis data */
1921  SCIP_SET* set, /**< global SCIP settings */
1922  int num /**< minimal number of slots in array */
1923  )
1924 {
1925  assert(conflict != NULL);
1926  assert(set != NULL);
1927 
1928  if( num > conflict->proofsetssize )
1929  {
1930  int newsize;
1931 
1932  newsize = SCIPsetCalcMemGrowSize(set, num);
1933  SCIP_ALLOC( BMSreallocMemoryArray(&conflict->proofsets, newsize) );
1934  conflict->proofsetssize = newsize;
1935  }
1936  assert(num <= conflict->proofsetssize);
1937 
1938  return SCIP_OKAY;
1939 }
1940 
1941 /** resizes conflictsets array to be able to store at least num entries */
1942 static
1944  SCIP_CONFLICT* conflict, /**< conflict analysis data */
1945  SCIP_SET* set, /**< global SCIP settings */
1946  int num /**< minimal number of slots in array */
1947  )
1948 {
1949  assert(conflict != NULL);
1950  assert(set != NULL);
1951 
1952  if( num > conflict->conflictsetssize )
1953  {
1954  int newsize;
1955 
1956  newsize = SCIPsetCalcMemGrowSize(set, num);
1957  SCIP_ALLOC( BMSreallocMemoryArray(&conflict->conflictsets, newsize) );
1958  SCIP_ALLOC( BMSreallocMemoryArray(&conflict->conflictsetscores, newsize) );
1959  conflict->conflictsetssize = newsize;
1960  }
1961  assert(num <= conflict->conflictsetssize);
1962 
1963  return SCIP_OKAY;
1964 }
1965 
1966 /** add a proofset to the list of all proofsets */
1967 static
1969  SCIP_CONFLICT* conflict, /**< conflict analysis data */
1970  SCIP_SET* set, /**< global SCIP settings */
1971  SCIP_PROOFSET* proofset /**< proof set to add */
1972  )
1973 {
1974  assert(conflict != NULL);
1975  assert(proofset != NULL);
1976 
1977  /* insert proofset into the sorted proofsets array */
1978  SCIP_CALL( conflictEnsureProofsetsMem(conflict, set, conflict->nproofsets + 1) );
1979 
1980  conflict->proofsets[conflict->nproofsets] = proofset;
1981  ++conflict->nproofsets;
1982 
1983  return SCIP_OKAY;
1984 }
1985 
1986 /** inserts conflict set into sorted conflictsets array and deletes the conflict set pointer */
1987 static
1989  SCIP_CONFLICT* conflict, /**< conflict analysis data */
1990  BMS_BLKMEM* blkmem, /**< block memory of transformed problem */
1991  SCIP_SET* set, /**< global SCIP settings */
1992  SCIP_CONFLICTSET** conflictset /**< pointer to conflict set to insert */
1993  )
1994 {
1995  SCIP_Real score;
1996  int pos;
1997  int i;
1998  int j;
1999 
2000  assert(conflict != NULL);
2001  assert(set != NULL);
2002  assert(conflictset != NULL);
2003  assert(*conflictset != NULL);
2004  assert((*conflictset)->validdepth <= (*conflictset)->insertdepth);
2005  assert(set->conf_allowlocal || (*conflictset)->validdepth == 0);
2006 
2007  /* calculate conflict and repropagation depth */
2008  conflictsetCalcConflictDepth(*conflictset);
2009 
2010  /* if we apply repropagations, the conflict set should be inserted at most at its repropdepth */
2011  if( set->conf_repropagate )
2012  (*conflictset)->insertdepth = MIN((*conflictset)->insertdepth, (*conflictset)->repropdepth);
2013  else
2014  (*conflictset)->repropdepth = INT_MAX;
2015  assert((*conflictset)->insertdepth <= (*conflictset)->repropdepth);
2016 
2017  SCIPsetDebugMsg(set, "inserting conflict set (valid: %d, insert: %d, conf: %d, reprop: %d):\n",
2018  (*conflictset)->validdepth, (*conflictset)->insertdepth, (*conflictset)->conflictdepth, (*conflictset)->repropdepth);
2019  SCIPdebug(conflictsetPrint(*conflictset));
2020 
2021  /* get the score of the conflict set */
2022  score = conflictsetCalcScore(*conflictset, set);
2023 
2024  /* check, if conflict set is redundant to a better conflict set */
2025  for( pos = 0; pos < conflict->nconflictsets && score < conflict->conflictsetscores[pos]; ++pos )
2026  {
2027  /* check if conflict set is redundant with respect to conflictsets[pos] */
2028  if( conflictsetIsRedundant(*conflictset, conflict->conflictsets[pos]) )
2029  {
2030  SCIPsetDebugMsg(set, " -> conflict set is redundant to: ");
2031  SCIPdebug(conflictsetPrint(conflict->conflictsets[pos]));
2032  conflictsetFree(conflictset, blkmem);
2033  return SCIP_OKAY;
2034  }
2035 
2036  /**@todo like in sepastore.c: calculate overlap between conflictsets -> large overlap reduces score */
2037  }
2038 
2039  /* insert conflictset into the sorted conflictsets array */
2040  SCIP_CALL( conflictEnsureConflictsetsMem(conflict, set, conflict->nconflictsets + 1) );
2041  for( i = conflict->nconflictsets; i > pos; --i )
2042  {
2043  assert(score >= conflict->conflictsetscores[i-1]);
2044  conflict->conflictsets[i] = conflict->conflictsets[i-1];
2045  conflict->conflictsetscores[i] = conflict->conflictsetscores[i-1];
2046  }
2047  conflict->conflictsets[pos] = *conflictset;
2048  conflict->conflictsetscores[pos] = score;
2049  conflict->nconflictsets++;
2050 
2051  /* remove worse conflictsets that are redundant to the new conflictset */
2052  for( i = pos+1, j = pos+1; i < conflict->nconflictsets; ++i )
2053  {
2054  if( conflictsetIsRedundant(conflict->conflictsets[i], *conflictset) )
2055  {
2056  SCIPsetDebugMsg(set, " -> conflict set dominates: ");
2057  SCIPdebug(conflictsetPrint(conflict->conflictsets[i]));
2058  conflictsetFree(&conflict->conflictsets[i], blkmem);
2059  }
2060  else
2061  {
2062  assert(j <= i);
2063  conflict->conflictsets[j] = conflict->conflictsets[i];
2064  conflict->conflictsetscores[j] = conflict->conflictsetscores[i];
2065  j++;
2066  }
2067  }
2068  assert(j <= conflict->nconflictsets);
2069  conflict->nconflictsets = j;
2070 
2071 #ifdef SCIP_CONFGRAPH
2072  confgraphMarkConflictset(*conflictset);
2073 #endif
2074 
2075  *conflictset = NULL; /* ownership of pointer is now in the conflictsets array */
2076 
2077  return SCIP_OKAY;
2078 }
2079 
2080 /** calculates the maximal size of conflict sets to be used */
2081 static
2083  SCIP_SET* set, /**< global SCIP settings */
2084  SCIP_PROB* prob /**< problem data */
2085  )
2086 {
2087  int maxsize;
2088 
2089  assert(set != NULL);
2090  assert(prob != NULL);
2091 
2092  maxsize = (int)(set->conf_maxvarsfac * (prob->nvars - prob->ncontvars));
2093  maxsize = MAX(maxsize, set->conf_minmaxvars);
2094 
2095  return maxsize;
2096 }
2097 
2098 /** increases the conflict score of the variable in the given direction */
2099 static
2101  SCIP_VAR* var, /**< problem variable */
2102  BMS_BLKMEM* blkmem, /**< block memory */
2103  SCIP_SET* set, /**< global SCIP settings */
2104  SCIP_STAT* stat, /**< dynamic problem statistics */
2105  SCIP_BOUNDTYPE boundtype, /**< type of bound for which the score should be increased */
2106  SCIP_Real value, /**< value of the bound */
2107  SCIP_Real weight /**< weight of this VSIDS updates */
2108  )
2109 {
2110  SCIP_BRANCHDIR branchdir;
2111 
2112  assert(var != NULL);
2113  assert(stat != NULL);
2114 
2115  /* weight the VSIDS by the given weight */
2116  weight *= stat->vsidsweight;
2117 
2118  if( SCIPsetIsZero(set, weight) )
2119  return SCIP_OKAY;
2120 
2121  branchdir = (boundtype == SCIP_BOUNDTYPE_LOWER ? SCIP_BRANCHDIR_UPWARDS : SCIP_BRANCHDIR_DOWNWARDS); /*lint !e641*/
2122  SCIP_CALL( SCIPvarIncVSIDS(var, blkmem, set, stat, branchdir, value, weight) );
2123  SCIPhistoryIncVSIDS(stat->glbhistory, branchdir, weight);
2124  SCIPhistoryIncVSIDS(stat->glbhistorycrun, branchdir, weight);
2125 
2126  return SCIP_OKAY;
2127 }
2128 
2129 /** update conflict statistics */
2130 static
2132  SCIP_CONFLICT* conflict, /**< conflict analysis data */
2133  BMS_BLKMEM* blkmem, /**< block memory */
2134  SCIP_SET* set, /**< global SCIP settings */
2135  SCIP_STAT* stat, /**< dynamic problem statistics */
2136  SCIP_CONFLICTSET* conflictset, /**< conflict set to add to the tree */
2137  int insertdepth /**< depth level at which the conflict set should be added */
2138  )
2139 {
2140  if( insertdepth > 0 )
2141  {
2142  conflict->nappliedlocconss++;
2143  conflict->nappliedlocliterals += conflictset->nbdchginfos;
2144  }
2145  else
2146  {
2147  int i;
2148  int conflictlength;
2149  conflictlength = conflictset->nbdchginfos;
2150 
2151  for( i = 0; i < conflictlength; i++ )
2152  {
2153  SCIP_VAR* var;
2154  SCIP_BRANCHDIR branchdir;
2155  SCIP_BOUNDTYPE boundtype;
2156  SCIP_Real bound;
2157 
2158  assert(stat != NULL);
2159 
2160  var = conflictset->bdchginfos[i]->var;
2161  boundtype = SCIPbdchginfoGetBoundtype(conflictset->bdchginfos[i]);
2162  bound = conflictset->relaxedbds[i];
2163 
2164  branchdir = (boundtype == SCIP_BOUNDTYPE_LOWER ? SCIP_BRANCHDIR_UPWARDS : SCIP_BRANCHDIR_DOWNWARDS); /*lint !e641*/
2165 
2166  SCIP_CALL( SCIPvarIncNActiveConflicts(var, blkmem, set, stat, branchdir, bound, (SCIP_Real)conflictlength) );
2167  SCIPhistoryIncNActiveConflicts(stat->glbhistory, branchdir, (SCIP_Real)conflictlength);
2168  SCIPhistoryIncNActiveConflicts(stat->glbhistorycrun, branchdir, (SCIP_Real)conflictlength);
2169 
2170  /* each variable which is part of the conflict gets an increase in the VSIDS */
2171  SCIP_CALL( incVSIDS(var, blkmem, set, stat, boundtype, bound, set->conf_conflictweight) );
2172  }
2173  conflict->nappliedglbconss++;
2174  conflict->nappliedglbliterals += conflictset->nbdchginfos;
2175  }
2176 
2177  return SCIP_OKAY;
2178 }
2179 
2180 
2181 /** check conflict set for redundancy, other conflicts in the same conflict analysis could have led to global reductions
2182  * an made this conflict set redundant
2183  */
2184 static
2186  SCIP_SET* set, /**< global SCIP settings */
2187  SCIP_CONFLICTSET* conflictset /**< conflict set */
2188  )
2189 {
2190  SCIP_BDCHGINFO** bdchginfos;
2191  SCIP_VAR* var;
2192  SCIP_Real* relaxedbds;
2193  SCIP_Real bound;
2194  int v;
2195 
2196  assert(set != NULL);
2197  assert(conflictset != NULL);
2198 
2199  bdchginfos = conflictset->bdchginfos;
2200  relaxedbds = conflictset->relaxedbds;
2201  assert(bdchginfos != NULL);
2202  assert(relaxedbds != NULL);
2203 
2204  /* check all boundtypes and bounds for redundancy */
2205  for( v = conflictset->nbdchginfos - 1; v >= 0; --v )
2206  {
2207  var = SCIPbdchginfoGetVar(bdchginfos[v]);
2208  assert(var != NULL);
2209  assert(SCIPvarGetProbindex(var) >= 0);
2210 
2211  /* check if the relaxed bound is really a relaxed bound */
2212  assert(SCIPbdchginfoGetBoundtype(bdchginfos[v]) == SCIP_BOUNDTYPE_LOWER || SCIPsetIsGE(set, relaxedbds[v], SCIPbdchginfoGetNewbound(bdchginfos[v])));
2213  assert(SCIPbdchginfoGetBoundtype(bdchginfos[v]) == SCIP_BOUNDTYPE_UPPER || SCIPsetIsLE(set, relaxedbds[v], SCIPbdchginfoGetNewbound(bdchginfos[v])));
2214 
2215  bound = relaxedbds[v];
2216 
2217  if( SCIPbdchginfoGetBoundtype(bdchginfos[v]) == SCIP_BOUNDTYPE_UPPER )
2218  {
2220  {
2221  assert(SCIPsetIsIntegral(set, bound));
2222  bound += 1.0;
2223  }
2224 
2225  /* check if the bound is already fulfilled globally */
2226  if( SCIPsetIsFeasGE(set, SCIPvarGetLbGlobal(var), bound) )
2227  return TRUE;
2228  }
2229  else
2230  {
2231  assert(SCIPbdchginfoGetBoundtype(bdchginfos[v]) == SCIP_BOUNDTYPE_LOWER);
2232 
2234  {
2235  assert(SCIPsetIsIntegral(set, bound));
2236  bound -= 1.0;
2237  }
2238 
2239  /* check if the bound is already fulfilled globally */
2240  if( SCIPsetIsFeasLE(set, SCIPvarGetUbGlobal(var), bound) )
2241  return TRUE;
2242  }
2243  }
2244 
2245  return FALSE;
2246 }
2247 
2248 /** find global fixings which can be derived from the new conflict set */
2249 static
2251  SCIP_SET* set, /**< global SCIP settings */
2252  SCIP_PROB* prob, /**< transformed problem after presolve */
2253  SCIP_CONFLICTSET* conflictset, /**< conflict set to add to the tree */
2254  int* nbdchgs, /**< number of global deducted bound changes due to the conflict set */
2255  int* nredvars, /**< number of redundant and removed variables from conflict set */
2256  SCIP_Bool* redundant /**< did we found a global reduction on a conflict set variable, which makes this conflict redundant */
2257  )
2258 {
2259  SCIP_BDCHGINFO** bdchginfos;
2260  SCIP_Real* relaxedbds;
2261  SCIP_VAR* var;
2262  SCIP_Bool* boundtypes;
2263  SCIP_Real* bounds;
2264  SCIP_Longint* nbinimpls;
2265  int* sortvals;
2266  SCIP_Real bound;
2267  SCIP_Bool isupper;
2268  int ntrivialredvars;
2269  int nbdchginfos;
2270  int nzeroimpls;
2271  int v;
2272 
2273  assert(set != NULL);
2274  assert(prob != NULL);
2275  assert(SCIPprobIsTransformed(prob));
2276  assert(conflictset != NULL);
2277  assert(nbdchgs != NULL);
2278  assert(nredvars != NULL);
2279  /* only check conflict sets with more than one variable */
2280  assert(conflictset->nbdchginfos > 1);
2281 
2282  *nbdchgs = 0;
2283  *nredvars = 0;
2284 
2285  /* due to other conflict in the same conflict analysis, this conflict set might have become redundant */
2286  *redundant = checkRedundancy(set, conflictset);
2287 
2288  if( *redundant )
2289  return SCIP_OKAY;
2290 
2291  bdchginfos = conflictset->bdchginfos;
2292  relaxedbds = conflictset->relaxedbds;
2293  nbdchginfos = conflictset->nbdchginfos;
2294  sortvals = conflictset->sortvals;
2295 
2296  assert(bdchginfos != NULL);
2297  assert(relaxedbds != NULL);
2298  assert(sortvals != NULL);
2299 
2300  /* check if the boolean representation of boundtypes matches the 'standard' definition */
2301  assert(SCIP_BOUNDTYPE_LOWER == FALSE); /*lint !e641 !e506*/
2302  assert(SCIP_BOUNDTYPE_UPPER == TRUE); /*lint !e641 !e506*/
2303 
2304  ntrivialredvars = 0;
2305 
2306  /* due to multiple conflict sets for one conflict, it can happen, that we already have redundant information in the
2307  * conflict set
2308  */
2309  for( v = nbdchginfos - 1; v >= 0; --v )
2310  {
2311  var = SCIPbdchginfoGetVar(bdchginfos[v]);
2312  bound = relaxedbds[v];
2313  isupper = (SCIP_Bool) SCIPboundtypeOpposite(SCIPbdchginfoGetBoundtype(bdchginfos[v]));
2314 
2315  /* for integral variable we can increase/decrease the conflicting bound */
2316  if( SCIPvarIsIntegral(var) )
2317  bound += (isupper ? -1.0 : +1.0);
2318 
2319  /* if conflict variable cannot fulfill the conflict we can remove it */
2320  if( (isupper && SCIPsetIsFeasLT(set, bound, SCIPvarGetLbGlobal(var))) ||
2321  (!isupper && SCIPsetIsFeasGT(set, bound, SCIPvarGetUbGlobal(var))) )
2322  {
2323  SCIPsetDebugMsg(set, "remove redundant variable <%s> from conflict set\n", SCIPvarGetName(var));
2324 
2325  bdchginfos[v] = bdchginfos[nbdchginfos - 1];
2326  relaxedbds[v] = relaxedbds[nbdchginfos - 1];
2327  sortvals[v] = sortvals[nbdchginfos - 1];
2328 
2329  --nbdchginfos;
2330  ++ntrivialredvars;
2331  }
2332  }
2333  assert(ntrivialredvars + nbdchginfos == conflictset->nbdchginfos);
2334 
2335  SCIPsetDebugMsg(set, "trivially removed %d redundant of %d variables from conflictset (%p)\n", ntrivialredvars, conflictset->nbdchginfos, (void*)conflictset);
2336  conflictset->nbdchginfos = nbdchginfos;
2337 
2338  /* all variables where removed, the conflict cannot be fulfilled, i.e., we have an infeasibility proof */
2339  if( conflictset->nbdchginfos == 0 )
2340  return SCIP_OKAY;
2341 
2342  /* do not check to big or trivial conflicts */
2343  if( conflictset->nbdchginfos > set->conf_maxvarsdetectimpliedbounds || conflictset->nbdchginfos == 1 )
2344  {
2345  *nredvars = ntrivialredvars;
2346  return SCIP_OKAY;
2347  }
2348 
2349  /* create array of boundtypes, and bound values in conflict set */
2350  SCIP_CALL( SCIPsetAllocBufferArray(set, &boundtypes, nbdchginfos) );
2351  SCIP_CALL( SCIPsetAllocBufferArray(set, &bounds, nbdchginfos) );
2352  /* memory for the estimates for binary implications used for sorting */
2353  SCIP_CALL( SCIPsetAllocBufferArray(set, &nbinimpls, nbdchginfos) );
2354 
2355  nzeroimpls = 0;
2356 
2357  /* collect estimates and initialize variables, boundtypes, and bounds array */
2358  for( v = 0; v < nbdchginfos; ++v )
2359  {
2360  var = SCIPbdchginfoGetVar(bdchginfos[v]);
2361  boundtypes[v] = (SCIP_Bool) SCIPboundtypeOpposite(SCIPbdchginfoGetBoundtype(bdchginfos[v]));
2362  bounds[v] = relaxedbds[v];
2363 
2364  assert(SCIPvarGetProbindex(var) >= 0);
2365 
2366  /* check if the relaxed bound is really a relaxed bound */
2367  assert(SCIPbdchginfoGetBoundtype(bdchginfos[v]) == SCIP_BOUNDTYPE_LOWER || SCIPsetIsGE(set, relaxedbds[v], SCIPbdchginfoGetNewbound(bdchginfos[v])));
2368  assert(SCIPbdchginfoGetBoundtype(bdchginfos[v]) == SCIP_BOUNDTYPE_UPPER || SCIPsetIsLE(set, relaxedbds[v], SCIPbdchginfoGetNewbound(bdchginfos[v])));
2369 
2370  /* for continuous variables, we can only use the relaxed version of the bounds negation: !(x <= u) -> x >= u */
2371  if( SCIPvarIsBinary(var) )
2372  {
2373  if( !boundtypes[v] )
2374  {
2375  assert(SCIPsetIsZero(set, bounds[v]));
2376  bounds[v] = 1.0;
2377  nbinimpls[v] = (SCIP_Longint)SCIPvarGetNCliques(var, TRUE) * 2;
2378  }
2379  else
2380  {
2381  assert(SCIPsetIsEQ(set, bounds[v], 1.0));
2382  bounds[v] = 0.0;
2383  nbinimpls[v] = (SCIP_Longint)SCIPvarGetNCliques(var, FALSE) * 2;
2384  }
2385  }
2386  else if( SCIPvarIsIntegral(var) )
2387  {
2388  assert(SCIPsetIsIntegral(set, bounds[v]));
2389 
2390  bounds[v] += ((!boundtypes[v]) ? +1.0 : -1.0);
2391  nbinimpls[v] = (boundtypes[v] ? SCIPvarGetNVlbs(var) : SCIPvarGetNVubs(var));
2392  }
2393  else if( ((!boundtypes[v]) && SCIPsetIsFeasEQ(set, SCIPvarGetLbGlobal(var), bounds[v]))
2394  || ((boundtypes[v]) && SCIPsetIsFeasEQ(set, SCIPvarGetUbGlobal(var), bounds[v])) )
2395  {
2396  /* the literal is satisfied in global bounds (may happen due to weak "negation" of continuous variables)
2397  * -> discard the conflict constraint
2398  */
2399  break;
2400  }
2401  else
2402  {
2403  nbinimpls[v] = (boundtypes[v] ? SCIPvarGetNVlbs(var) : SCIPvarGetNVubs(var));
2404  }
2405 
2406  if( nbinimpls[v] == 0 )
2407  ++nzeroimpls;
2408  }
2409 
2410  /* starting to derive global bound changes */
2411  if( v == nbdchginfos && ((!set->conf_fullshortenconflict && nzeroimpls < 2) || (set->conf_fullshortenconflict && nzeroimpls < nbdchginfos)) )
2412  {
2413  SCIP_VAR** vars;
2414  SCIP_Bool* redundants;
2415  SCIP_Bool glbinfeas;
2416 
2417  /* sort variables in increasing order of binary implications to gain speed later on */
2418  SCIPsortLongPtrRealRealBool(nbinimpls, (void**)bdchginfos, relaxedbds, bounds, boundtypes, v);
2419 
2420  SCIPsetDebugMsg(set, "checking for global reductions and redundant conflict variables(in %s) on conflict:\n", SCIPprobGetName(prob));
2421  SCIPsetDebugMsg(set, "[");
2422  for( v = 0; v < nbdchginfos; ++v )
2423  {
2424  SCIPsetDebugMsgPrint(set, "%s %s %g", SCIPvarGetName(SCIPbdchginfoGetVar(bdchginfos[v])), (!boundtypes[v]) ? ">=" : "<=", bounds[v]);
2425  if( v < nbdchginfos - 1 )
2426  SCIPsetDebugMsgPrint(set, ", ");
2427  }
2428  SCIPsetDebugMsgPrint(set, "]\n");
2429 
2430  SCIP_CALL( SCIPsetAllocBufferArray(set, &vars, v) );
2431  SCIP_CALL( SCIPsetAllocCleanBufferArray(set, &redundants, v) );
2432 
2433  /* initialize conflict variable data */
2434  for( v = 0; v < nbdchginfos; ++v )
2435  vars[v] = SCIPbdchginfoGetVar(bdchginfos[v]);
2436 
2437  SCIP_CALL( SCIPshrinkDisjunctiveVarSet(set->scip, vars, bounds, boundtypes, redundants, nbdchginfos, nredvars, \
2438  nbdchgs, redundant, &glbinfeas, set->conf_fullshortenconflict) );
2439 
2440  if( glbinfeas )
2441  {
2442  SCIPsetDebugMsg(set, "conflict set (%p) led to global infeasibility\n", (void*) conflictset);
2443 
2444  /* clear the memory array before freeing it */
2445  BMSclearMemoryArray(redundants, nbdchginfos);
2446  goto TERMINATE;
2447  }
2448 
2449 #ifdef SCIP_DEBUG
2450  if( *nbdchgs > 0 )
2451  {
2452  SCIPsetDebugMsg(set, "conflict set (%p) led to %d global bound reductions\n", (void*) conflictset, *nbdchgs);
2453  }
2454 #endif
2455 
2456  /* remove as redundant marked variables */
2457  if( *redundant )
2458  {
2459  SCIPsetDebugMsg(set, "conflict set (%p) is redundant because at least one global reduction, fulfills the conflict constraint\n", (void*)conflictset);
2460 
2461  /* clear the memory array before freeing it */
2462  BMSclearMemoryArray(redundants, nbdchginfos);
2463  }
2464  else if( *nredvars > 0 )
2465  {
2466  assert(bdchginfos == conflictset->bdchginfos);
2467  assert(relaxedbds == conflictset->relaxedbds);
2468  assert(sortvals == conflictset->sortvals);
2469 
2470  for( v = nbdchginfos - 1; v >= 0; --v )
2471  {
2472  /* if conflict variable was marked to be redundant remove it */
2473  if( redundants[v] )
2474  {
2475  SCIPsetDebugMsg(set, "remove redundant variable <%s> from conflict set\n", SCIPvarGetName(SCIPbdchginfoGetVar(bdchginfos[v])));
2476 
2477  bdchginfos[v] = bdchginfos[nbdchginfos - 1];
2478  relaxedbds[v] = relaxedbds[nbdchginfos - 1];
2479  sortvals[v] = sortvals[nbdchginfos - 1];
2480 
2481  /* reset redundants[v] to 0 */
2482  redundants[v] = 0;
2483 
2484  --nbdchginfos;
2485  }
2486  }
2487  assert((*nredvars) + nbdchginfos == conflictset->nbdchginfos);
2488 
2489  SCIPsetDebugMsg(set, "removed %d redundant of %d variables from conflictset (%p)\n", (*nredvars), conflictset->nbdchginfos, (void*)conflictset);
2490  conflictset->nbdchginfos = nbdchginfos;
2491  }
2492  else
2493  {
2494  /* clear the memory array before freeing it */
2495  BMSclearMemoryArray(redundants, nbdchginfos);
2496  }
2497 
2498  TERMINATE:
2499  SCIPsetFreeCleanBufferArray(set, &redundants);
2500  SCIPsetFreeBufferArray(set, &vars);
2501  }
2502 
2503  /* free temporary memory */
2504  SCIPsetFreeBufferArray(set, &nbinimpls);
2505  SCIPsetFreeBufferArray(set, &bounds);
2506  SCIPsetFreeBufferArray(set, &boundtypes);
2507 
2508  *nredvars += ntrivialredvars;
2509 
2510  return SCIP_OKAY;
2511 }
2512 
2513 /** tighten the bound of a singleton variable in a constraint
2514  *
2515  * if the bound is contradicting with a global bound we cannot tighten the bound directly.
2516  * in this case we need to create and add a constraint of size one such that propagating this constraint will
2517  * enforce the infeasibility.
2518  */
2519 static
2521  SCIP_CONFLICT* conflict, /**< conflict analysis data */
2522  SCIP_SET* set, /**< global SCIP settings */
2523  SCIP_STAT* stat, /**< dynamic SCIP statistics */
2524  SCIP_TREE* tree, /**< tree data */
2525  BMS_BLKMEM* blkmem, /**< block memory */
2526  SCIP_PROB* origprob, /**< original problem */
2527  SCIP_PROB* transprob, /**< transformed problem */
2528  SCIP_REOPT* reopt, /**< reoptimization data */
2529  SCIP_LP* lp, /**< LP data */
2530  SCIP_BRANCHCAND* branchcand, /**< branching candidates */
2531  SCIP_EVENTQUEUE* eventqueue, /**< event queue */
2532  SCIP_CLIQUETABLE* cliquetable, /**< clique table */
2533  SCIP_VAR* var, /**< problem variable */
2534  SCIP_Real val, /**< coefficient of the variable */
2535  SCIP_Real rhs, /**< rhs of the constraint */
2536  SCIP_CONFTYPE prooftype, /**< type of the proof */
2537  int validdepth /**< depth where the bound change is valid */
2538  )
2539 {
2540  SCIP_Real newbound;
2541  SCIP_Bool applyglobal;
2542  SCIP_BOUNDTYPE boundtype;
2543 
2544  assert(tree != NULL);
2545  assert(validdepth >= 0);
2546 
2547  applyglobal = (validdepth <= SCIPtreeGetEffectiveRootDepth(tree));
2548 
2549  /* if variable and coefficient are integral the rhs can be rounded down */
2550  if( SCIPvarIsIntegral(var) && SCIPsetIsIntegral(set, val) )
2551  newbound = SCIPsetFeasFloor(set, rhs)/val;
2552  else
2553  newbound = rhs/val;
2554 
2555  boundtype = (val > 0.0 ? SCIP_BOUNDTYPE_UPPER : SCIP_BOUNDTYPE_LOWER);
2556  SCIPvarAdjustBd(var, set, boundtype, &newbound);
2557 
2558  /* skip numerical unstable bound changes */
2559  if( applyglobal
2560  && ((boundtype == SCIP_BOUNDTYPE_LOWER && SCIPsetIsLE(set, newbound, SCIPvarGetLbGlobal(var)))
2561  || (boundtype == SCIP_BOUNDTYPE_UPPER && SCIPsetIsGE(set, newbound, SCIPvarGetUbGlobal(var)))) )
2562  {
2563  return SCIP_OKAY;
2564  }
2565 
2566  /* the new bound contradicts a global bound, we can cutoff the root node immediately */
2567  if( applyglobal
2568  && ((boundtype == SCIP_BOUNDTYPE_LOWER && SCIPsetIsGT(set, newbound, SCIPvarGetUbGlobal(var)))
2569  || (boundtype == SCIP_BOUNDTYPE_UPPER && SCIPsetIsLT(set, newbound, SCIPvarGetLbGlobal(var)))) )
2570  {
2571  SCIPsetDebugMsg(set, "detected global infeasibility at var <%s>: locdom=[%g,%g] glbdom=[%g,%g] new %s bound=%g\n",
2572  SCIPvarGetName(var), SCIPvarGetLbLocal(var),
2574  (boundtype == SCIP_BOUNDTYPE_LOWER ? "lower" : "upper"), newbound);
2575  SCIP_CALL( SCIPnodeCutoff(tree->path[0], set, stat, tree, transprob, origprob, reopt, lp, blkmem) );
2576  }
2577  else
2578  {
2579  if( lp->strongbranching || !applyglobal )
2580  {
2581  SCIP_CONS* cons;
2582  SCIP_Real conslhs;
2583  SCIP_Real consrhs;
2584  char name[SCIP_MAXSTRLEN];
2585 
2586  SCIPsetDebugMsg(set, "add constraint <%s>[%c] %s %g to node #%lld in depth %d\n",
2587  SCIPvarGetName(var), varGetChar(var), boundtype == SCIP_BOUNDTYPE_UPPER ? "<=" : ">=", newbound,
2588  SCIPnodeGetNumber(tree->path[validdepth]), validdepth);
2589 
2590  (void)SCIPsnprintf(name, SCIP_MAXSTRLEN, "pc_fix_%s", SCIPvarGetName(var));
2591 
2592  if( boundtype == SCIP_BOUNDTYPE_UPPER )
2593  {
2594  conslhs = -SCIPsetInfinity(set);
2595  consrhs = newbound;
2596  }
2597  else
2598  {
2599  conslhs = newbound;
2600  consrhs = SCIPsetInfinity(set);
2601  }
2602 
2603  SCIP_CALL( SCIPcreateConsLinear(set->scip, &cons, name, 0, NULL, NULL, conslhs, consrhs,
2605 
2606  SCIP_CALL( SCIPaddCoefLinear(set->scip, cons, var, 1.0) );
2607 
2608  if( applyglobal )
2609  {
2610  SCIP_CALL( SCIPprobAddCons(transprob, set, stat, cons) );
2611  }
2612  else
2613  {
2614  SCIP_CALL( SCIPnodeAddCons(tree->path[validdepth], blkmem, set, stat, tree, cons) );
2615  }
2616 
2617  SCIP_CALL( SCIPconsRelease(&cons, blkmem, set) );
2618  }
2619  else
2620  {
2621  assert(applyglobal);
2622 
2623  SCIPsetDebugMsg(set, "change global %s bound of <%s>[%c]: %g -> %g\n",
2624  (boundtype == SCIP_BOUNDTYPE_LOWER ? "lower" : "upper"),
2625  SCIPvarGetName(var), varGetChar(var),
2626  (boundtype == SCIP_BOUNDTYPE_LOWER ? SCIPvarGetLbGlobal(var) : SCIPvarGetUbGlobal(var)),
2627  newbound);
2628 
2629  SCIP_CALL( SCIPnodeAddBoundchg(tree->path[0], blkmem, set, stat, transprob, origprob, tree, reopt, lp, branchcand, \
2630  eventqueue, cliquetable, var, newbound, boundtype, FALSE) );
2631 
2632  /* mark the node in the validdepth to be propagated again */
2633  SCIPnodePropagateAgain(tree->path[0], set, stat, tree);
2634  }
2635  }
2636 
2637  if( applyglobal )
2638  ++conflict->nglbchgbds;
2639  else
2640  ++conflict->nlocchgbds;
2641 
2642  if( prooftype == SCIP_CONFTYPE_INFEASLP || prooftype == SCIP_CONFTYPE_ALTINFPROOF )
2643  {
2644  ++conflict->dualproofsinfnnonzeros; /* we count a global bound reduction as size 1 */
2645  ++conflict->ndualproofsinfsuccess;
2646  ++conflict->ninflpsuccess;
2647 
2648  if( applyglobal )
2649  ++conflict->ndualproofsinfglobal;
2650  else
2651  ++conflict->ndualproofsinflocal;
2652  }
2653  else
2654  {
2655  ++conflict->dualproofsbndnnonzeros; /* we count a global bound reduction as size 1 */
2656  ++conflict->ndualproofsbndsuccess;
2657  ++conflict->nboundlpsuccess;
2658 
2659  if( applyglobal )
2660  ++conflict->ndualproofsbndglobal;
2661  else
2662  ++conflict->ndualproofsbndlocal;
2663  }
2664 
2665  return SCIP_OKAY;
2666 }
2667 
2668 /** calculates the minimal activity of a given aggregation row */
2669 static
2671  SCIP_SET* set, /**< global SCIP settings */
2672  SCIP_PROB* transprob, /**< transformed problem data */
2673  SCIP_AGGRROW* aggrrow, /**< aggregation row */
2674  SCIP_Real* curvarlbs, /**< current lower bounds of active problem variables (or NULL for global bounds) */
2675  SCIP_Real* curvarubs, /**< current upper bounds of active problem variables (or NULL for global bounds) */
2676  SCIP_Bool* infdelta /**< pointer to store whether at least one variable contributes with an infinite value */
2677  )
2678 {
2679  SCIP_VAR** vars;
2680  SCIP_Real QUAD(minact);
2681  int* inds;
2682  int nnz;
2683  int i;
2684 
2685  vars = SCIPprobGetVars(transprob);
2686  assert(vars != NULL);
2687 
2688  nnz = SCIPaggrRowGetNNz(aggrrow);
2689  inds = SCIPaggrRowGetInds(aggrrow);
2690 
2691  QUAD_ASSIGN(minact, 0.0);
2692 
2693  if( infdelta != NULL )
2694  *infdelta = FALSE;
2695 
2696  for( i = 0; i < nnz; i++ )
2697  {
2698  SCIP_Real val;
2699  SCIP_Real QUAD(delta);
2700  int v = inds[i];
2701 
2702  assert(SCIPvarGetProbindex(vars[v]) == v);
2703 
2704  val = SCIPaggrRowGetProbvarValue(aggrrow, v);
2705 
2706  if( val > 0.0 )
2707  {
2708  SCIP_Real bnd = (curvarlbs == NULL ? SCIPvarGetLbGlobal(vars[v]) : curvarlbs[v]);
2709  SCIPquadprecProdDD(delta, val, bnd);
2710  }
2711  else
2712  {
2713  SCIP_Real bnd = (curvarubs == NULL ? SCIPvarGetUbGlobal(vars[v]) : curvarubs[v]);
2714  SCIPquadprecProdDD(delta, val, bnd);
2715  }
2716 
2717  /* update minimal activity */
2718  SCIPquadprecSumQQ(minact, minact, delta);
2719 
2720  if( infdelta != NULL && SCIPsetIsInfinity(set, REALABS(QUAD_TO_DBL(delta))) )
2721  {
2722  *infdelta = TRUE;
2723  goto TERMINATE;
2724  }
2725  }
2726 
2727  TERMINATE:
2728  /* check whether the minimal activity is infinite */
2729  if( SCIPsetIsInfinity(set, QUAD_TO_DBL(minact)) )
2730  return SCIPsetInfinity(set);
2731  if( SCIPsetIsInfinity(set, -QUAD_TO_DBL(minact)) )
2732  return -SCIPsetInfinity(set);
2733 
2734  return QUAD_TO_DBL(minact);
2735 }
2736 
2737 /** calculates the minimal activity of a given set of bounds and coefficients */
2738 static
2740  SCIP_SET* set, /**< global SCIP settings */
2741  SCIP_PROB* transprob, /**< transformed problem data */
2742  SCIP_Real* coefs, /**< coefficients in sparse representation */
2743  int* inds, /**< non-zero indices */
2744  int nnz, /**< number of non-zero indices */
2745  SCIP_Real* curvarlbs, /**< current lower bounds of active problem variables (or NULL for global bounds) */
2746  SCIP_Real* curvarubs /**< current upper bounds of active problem variables (or NULL for global bounds) */
2747  )
2748 {
2749  SCIP_VAR** vars;
2750  SCIP_Real QUAD(minact);
2751  int i;
2752 
2753  assert(coefs != NULL);
2754  assert(inds != NULL);
2755 
2756  vars = SCIPprobGetVars(transprob);
2757  assert(vars != NULL);
2758 
2759  QUAD_ASSIGN(minact, 0.0);
2760 
2761  for( i = 0; i < nnz; i++ )
2762  {
2763  SCIP_Real val;
2764  SCIP_Real QUAD(delta);
2765  int v = inds[i];
2766 
2767  assert(SCIPvarGetProbindex(vars[v]) == v);
2768 
2769  val = coefs[i];
2770 
2771  if( val > 0.0 )
2772  {
2773  SCIP_Real bnd;
2774 
2775  assert(curvarlbs == NULL || !SCIPsetIsInfinity(set, -curvarlbs[v]));
2776 
2777  bnd = (curvarlbs == NULL ? SCIPvarGetLbGlobal(vars[v]) : curvarlbs[v]);
2778  SCIPquadprecProdDD(delta, val, bnd);
2779  }
2780  else
2781  {
2782  SCIP_Real bnd;
2783 
2784  assert(curvarubs == NULL || !SCIPsetIsInfinity(set, curvarubs[v]));
2785 
2786  bnd = (curvarubs == NULL ? SCIPvarGetUbGlobal(vars[v]) : curvarubs[v]);
2787  SCIPquadprecProdDD(delta, val, bnd);
2788  }
2789 
2790  /* update minimal activity */
2791  SCIPquadprecSumQQ(minact, minact, delta);
2792  }
2793 
2794  /* check whether the minmal activity is infinite */
2795  if( SCIPsetIsInfinity(set, QUAD_TO_DBL(minact)) )
2796  return SCIPsetInfinity(set);
2797  if( SCIPsetIsInfinity(set, -QUAD_TO_DBL(minact)) )
2798  return -SCIPsetInfinity(set);
2799 
2800  return QUAD_TO_DBL(minact);
2801 }
2802 
2803 /** calculates the minimal activity of a given set of bounds and coefficients */
2804 static
2806  SCIP_SET* set, /**< global SCIP settings */
2807  SCIP_PROB* transprob, /**< transformed problem data */
2808  SCIP_Real* coefs, /**< coefficients in sparse representation */
2809  int* inds, /**< non-zero indices */
2810  int nnz, /**< number of non-zero indices */
2811  SCIP_Real* curvarlbs, /**< current lower bounds of active problem variables (or NULL for global bounds) */
2812  SCIP_Real* curvarubs /**< current upper bounds of active problem variables (or NULL for global bounds) */
2813  )
2814 {
2815  SCIP_VAR** vars;
2816  SCIP_Real QUAD(maxact);
2817  int i;
2818 
2819  assert(coefs != NULL);
2820  assert(inds != NULL);
2821 
2822  vars = SCIPprobGetVars(transprob);
2823  assert(vars != NULL);
2824 
2825  QUAD_ASSIGN(maxact, 0.0);
2826 
2827  for( i = 0; i < nnz; i++ )
2828  {
2829  SCIP_Real val;
2830  SCIP_Real QUAD(delta);
2831  int v = inds[i];
2832 
2833  assert(SCIPvarGetProbindex(vars[v]) == v);
2834 
2835  val = coefs[i];
2836 
2837  if( val < 0.0 )
2838  {
2839  SCIP_Real bnd;
2840 
2841  assert(curvarlbs == NULL || !SCIPsetIsInfinity(set, -curvarlbs[v]));
2842 
2843  bnd = (curvarlbs == NULL ? SCIPvarGetLbGlobal(vars[v]) : curvarlbs[v]);
2844  SCIPquadprecProdDD(delta, val, bnd);
2845  }
2846  else
2847  {
2848  SCIP_Real bnd;
2849 
2850  assert(curvarubs == NULL || !SCIPsetIsInfinity(set, curvarubs[v]));
2851 
2852  bnd = (curvarubs == NULL ? SCIPvarGetUbGlobal(vars[v]) : curvarubs[v]);
2853  SCIPquadprecProdDD(delta, val, bnd);
2854  }
2855 
2856  /* update maximal activity */
2857  SCIPquadprecSumQQ(maxact, maxact, delta);
2858  }
2859 
2860  /* check whether the maximal activity got infinite */
2861  if( SCIPsetIsInfinity(set, QUAD_TO_DBL(maxact)) )
2862  return SCIPsetInfinity(set);
2863  if( SCIPsetIsInfinity(set, -QUAD_TO_DBL(maxact)) )
2864  return -SCIPsetInfinity(set);
2865 
2866  return QUAD_TO_DBL(maxact);
2867 }
2868 
2869 static
2871  SCIP_CONFLICT* conflict, /**< conflict analysis data */
2872  SCIP_SET* set, /**< global SCIP settings */
2873  SCIP_STAT* stat, /**< dynamic SCIP statistics */
2874  SCIP_REOPT* reopt, /**< reoptimization data */
2875  SCIP_TREE* tree, /**< tree data */
2876  BMS_BLKMEM* blkmem, /**< block memory */
2877  SCIP_PROB* origprob, /**< original problem */
2878  SCIP_PROB* transprob, /**< transformed problem */
2879  SCIP_LP* lp, /**< LP data */
2880  SCIP_BRANCHCAND* branchcand, /**< branching candidate storage */
2881  SCIP_EVENTQUEUE* eventqueue, /**< event queue */
2882  SCIP_CLIQUETABLE* cliquetable, /**< clique table data structure */
2883  SCIP_Real* coefs, /**< coefficients in sparse representation */
2884  int* inds, /**< non-zero indices */
2885  int nnz, /**< number of non-zero indices */
2886  SCIP_Real rhs, /**< right-hand side */
2887  SCIP_CONFTYPE conflicttype, /**< type of the conflict */
2888  int validdepth /**< depth where the proof is valid */
2889  )
2890 {
2891  SCIP_VAR** vars;
2892  SCIP_Real minact;
2893  int i;
2894 
2895  assert(coefs != NULL);
2896  assert(inds != NULL);
2897  assert(nnz >= 0);
2898 
2899  vars = SCIPprobGetVars(transprob);
2900  minact = getMinActivity(set, transprob, coefs, inds, nnz, NULL, NULL);
2901 
2902  /* we cannot find global tightenings */
2903  if( SCIPsetIsInfinity(set, -minact) )
2904  return SCIP_OKAY;
2905 
2906  for( i = 0; i < nnz; i++ )
2907  {
2908  SCIP_VAR* var;
2909  SCIP_Real val;
2910  SCIP_Real resminact;
2911  SCIP_Real lb;
2912  SCIP_Real ub;
2913  int pos;
2914 
2915  pos = inds[i];
2916  val = coefs[i];
2917  var = vars[pos];
2918  lb = SCIPvarGetLbGlobal(var);
2919  ub = SCIPvarGetUbGlobal(var);
2920 
2921  assert(!SCIPsetIsZero(set, val));
2922 
2923  resminact = minact;
2924 
2925  /* we got a potential new upper bound */
2926  if( val > 0.0 )
2927  {
2928  SCIP_Real newub;
2929 
2930  resminact -= (val * lb);
2931  newub = (rhs - resminact)/val;
2932 
2933  if( SCIPsetIsInfinity(set, newub) )
2934  continue;
2935 
2936  /* we cannot tighten the upper bound */
2937  if( SCIPsetIsGE(set, newub, ub) )
2938  continue;
2939 
2940  SCIP_CALL( tightenSingleVar(conflict, set, stat, tree, blkmem, origprob, transprob, reopt, lp, branchcand, \
2941  eventqueue, cliquetable, var, val, rhs-resminact, conflicttype, validdepth) );
2942  }
2943  /* we got a potential new lower bound */
2944  else
2945  {
2946  SCIP_Real newlb;
2947 
2948  resminact -= (val * ub);
2949  newlb = (rhs - resminact)/val;
2950 
2951  if( SCIPsetIsInfinity(set, -newlb) )
2952  continue;
2953 
2954  /* we cannot tighten the lower bound */
2955  if( SCIPsetIsLE(set, newlb, lb) )
2956  continue;
2957 
2958  SCIP_CALL( tightenSingleVar(conflict, set, stat, tree, blkmem, origprob, transprob, reopt, lp, branchcand, \
2959  eventqueue, cliquetable, var, val, rhs-resminact, conflicttype, validdepth) );
2960  }
2961 
2962  /* the minimal activity should stay unchanged because we tightened the bound that doesn't contribute to the
2963  * minimal activity
2964  */
2965  assert(SCIPsetIsEQ(set, minact, getMinActivity(set, transprob, coefs, inds, nnz, NULL, NULL)));
2966  }
2967 
2968  return SCIP_OKAY;
2969 }
2970 
2971 
2972 /** creates a proof constraint and tries to add it to the storage */
2973 static
2975  SCIP_CONFLICT* conflict, /**< conflict analysis data */
2976  SCIP_CONFLICTSTORE* conflictstore, /**< conflict pool data */
2977  SCIP_PROOFSET* proofset, /**< proof set */
2978  SCIP_SET* set, /**< global SCIP settings */
2979  SCIP_STAT* stat, /**< dynamic SCIP statistics */
2980  SCIP_PROB* origprob, /**< original problem */
2981  SCIP_PROB* transprob, /**< transformed problem */
2982  SCIP_TREE* tree, /**< tree data */
2983  SCIP_REOPT* reopt, /**< reoptimization data */
2984  SCIP_LP* lp, /**< LP data */
2985  SCIP_BRANCHCAND* branchcand, /**< branching candidate storage */
2986  SCIP_EVENTQUEUE* eventqueue, /**< event queue */
2987  SCIP_CLIQUETABLE* cliquetable, /**< clique table data structure */
2988  BMS_BLKMEM* blkmem /**< block memory */
2989  )
2990 {
2991  SCIP_CONS* cons;
2992  SCIP_CONS* upgdcons;
2993  SCIP_VAR** vars;
2994  SCIP_Real* coefs;
2995  int* inds;
2996  SCIP_Real rhs;
2997  SCIP_Real fillin;
2998  SCIP_Real globalminactivity;
2999  SCIP_Bool applyglobal;
3000  SCIP_Bool toolong;
3001  SCIP_Bool contonly;
3002  SCIP_Bool hasrelaxvar;
3003  SCIP_CONFTYPE conflicttype;
3004  char name[SCIP_MAXSTRLEN];
3005  int nnz;
3006  int i;
3007 
3008  assert(conflict != NULL);
3009  assert(conflictstore != NULL);
3010  assert(proofset != NULL);
3011  assert(proofset->validdepth == 0 || proofset->validdepth < SCIPtreeGetFocusDepth(tree));
3012 
3013  nnz = proofsetGetNVars(proofset);
3014 
3015  if( nnz == 0 )
3016  return SCIP_OKAY;
3017 
3018  vars = SCIPprobGetVars(transprob);
3019 
3020  rhs = proofsetGetRhs(proofset);
3021  assert(!SCIPsetIsInfinity(set, rhs));
3022 
3023  coefs = proofsetGetVals(proofset);
3024  assert(coefs != NULL);
3025 
3026  inds = proofsetGetInds(proofset);
3027  assert(inds != NULL);
3028 
3029  conflicttype = proofsetGetConftype(proofset);
3030 
3031  applyglobal = (proofset->validdepth <= SCIPtreeGetEffectiveRootDepth(tree));
3032 
3033  if( applyglobal )
3034  {
3035  SCIP_Real globalmaxactivity = getMaxActivity(set, transprob, coefs, inds, nnz, NULL, NULL);
3036 
3037  /* check whether the alternative proof is redundant */
3038  if( SCIPsetIsLE(set, globalmaxactivity, rhs) )
3039  return SCIP_OKAY;
3040 
3041  /* check whether the constraint proves global infeasibility */
3042  globalminactivity = getMinActivity(set, transprob, coefs, inds, nnz, NULL, NULL);
3043  if( SCIPsetIsGT(set, globalminactivity, rhs) )
3044  {
3045  SCIPsetDebugMsg(set, "detect global infeasibility: minactivity=%g, rhs=%g\n", globalminactivity, rhs);
3046 
3047  SCIP_CALL( SCIPnodeCutoff(tree->path[proofset->validdepth], set, stat, tree, transprob, origprob, reopt, lp, blkmem) );
3048 
3049  goto UPDATESTATISTICS;
3050  }
3051  }
3052 
3053  if( set->conf_minmaxvars >= nnz )
3054  toolong = FALSE;
3055  else
3056  {
3057  SCIP_Real maxnnz;
3058 
3059  if( transprob->startnconss < 100 )
3060  maxnnz = 0.85 * transprob->nvars;
3061  else
3062  maxnnz = (SCIP_Real)transprob->nvars;
3063 
3064  fillin = nnz;
3065  if( conflicttype == SCIP_CONFTYPE_INFEASLP || conflicttype == SCIP_CONFTYPE_ALTINFPROOF )
3066  {
3067  fillin += SCIPconflictstoreGetNDualInfProofs(conflictstore) * SCIPconflictstoreGetAvgNnzDualInfProofs(conflictstore);
3068  fillin /= (SCIPconflictstoreGetNDualInfProofs(conflictstore) + 1.0);
3069  toolong = (fillin > MIN(2.0 * stat->avgnnz, maxnnz));
3070  }
3071  else
3072  {
3073  assert(conflicttype == SCIP_CONFTYPE_BNDEXCEEDING || conflicttype == SCIP_CONFTYPE_ALTBNDPROOF);
3074 
3075  fillin += SCIPconflictstoreGetNDualBndProofs(conflictstore) * SCIPconflictstoreGetAvgNnzDualBndProofs(conflictstore);
3076  fillin /= (SCIPconflictstoreGetNDualBndProofs(conflictstore) + 1.0);
3077  toolong = (fillin > MIN(1.5 * stat->avgnnz, maxnnz));
3078  }
3079 
3080  toolong = (toolong && (nnz > set->conf_maxvarsfac * transprob->nvars));
3081  }
3082 
3083  /* don't store global dual proofs that are too long / have too many non-zeros */
3084  if( toolong )
3085  {
3086  if( applyglobal )
3087  {
3088  SCIP_CALL( propagateLongProof(conflict, set, stat, reopt, tree, blkmem, origprob, transprob, lp, branchcand,
3089  eventqueue, cliquetable, coefs, inds, nnz, rhs, conflicttype, proofset->validdepth) );
3090  }
3091  return SCIP_OKAY;
3092  }
3093 
3094  /* check if conflict contains variables that are invalid after a restart to label it appropriately */
3095  hasrelaxvar = FALSE;
3096  contonly = TRUE;
3097  for( i = 0; i < nnz && (!hasrelaxvar || contonly); ++i )
3098  {
3099  hasrelaxvar |= SCIPvarIsRelaxationOnly(vars[inds[i]]);
3100 
3101  if( SCIPvarIsIntegral(vars[inds[i]]) )
3102  contonly = FALSE;
3103  }
3104 
3105  if( !applyglobal && contonly )
3106  return SCIP_OKAY;
3107 
3108  if( conflicttype == SCIP_CONFTYPE_INFEASLP || conflicttype == SCIP_CONFTYPE_ALTINFPROOF )
3109  (void)SCIPsnprintf(name, SCIP_MAXSTRLEN, "dualproof_inf_%" SCIP_LONGINT_FORMAT, conflict->ndualproofsinfsuccess);
3110  else if( conflicttype == SCIP_CONFTYPE_BNDEXCEEDING || conflicttype == SCIP_CONFTYPE_ALTBNDPROOF )
3111  (void)SCIPsnprintf(name, SCIP_MAXSTRLEN, "dualproof_bnd_%" SCIP_LONGINT_FORMAT, conflict->ndualproofsbndsuccess);
3112  else
3113  return SCIP_INVALIDCALL;
3114 
3115  SCIP_CALL( SCIPcreateConsLinear(set->scip, &cons, name, 0, NULL, NULL, -SCIPsetInfinity(set), rhs,
3116  FALSE, FALSE, FALSE, FALSE, TRUE, !applyglobal,
3117  FALSE, TRUE, TRUE, FALSE) );
3118 
3119  for( i = 0; i < nnz; i++ )
3120  {
3121  int v = inds[i];
3122  SCIP_CALL( SCIPaddCoefLinear(set->scip, cons, vars[v], coefs[i]) );
3123  }
3124 
3125  /* do not upgrade linear constraints of size 1 */
3126  if( nnz > 1 )
3127  {
3128  upgdcons = NULL;
3129  /* try to automatically convert a linear constraint into a more specific and more specialized constraint */
3130  SCIP_CALL( SCIPupgradeConsLinear(set->scip, cons, &upgdcons) );
3131  if( upgdcons != NULL )
3132  {
3133  SCIP_CALL( SCIPreleaseCons(set->scip, &cons) );
3134  cons = upgdcons;
3135 
3136  if( conflicttype == SCIP_CONFTYPE_INFEASLP )
3137  conflicttype = SCIP_CONFTYPE_ALTINFPROOF;
3138  else if( conflicttype == SCIP_CONFTYPE_BNDEXCEEDING )
3139  conflicttype = SCIP_CONFTYPE_ALTBNDPROOF;
3140  }
3141  }
3142 
3143  /* mark constraint to be a conflict */
3144  SCIPconsMarkConflict(cons);
3145 
3146  /* add constraint to storage */
3147  if( conflicttype == SCIP_CONFTYPE_INFEASLP || conflicttype == SCIP_CONFTYPE_ALTINFPROOF )
3148  {
3149  /* add dual proof to storage */
3150  SCIP_CALL( SCIPconflictstoreAddDualraycons(conflictstore, cons, blkmem, set, stat, transprob, reopt, hasrelaxvar) );
3151  }
3152  else
3153  {
3154  SCIP_Real scale = 1.0;
3155  SCIP_Bool updateside = FALSE;
3156 
3157  /* In some cases the constraint could not be updated to a more special type. However, it is possible that
3158  * constraint got scaled. Therefore, we need to be very careful when updating the lhs/rhs after the incumbent
3159  * solution has improved.
3160  */
3161  if( conflicttype == SCIP_CONFTYPE_BNDEXCEEDING )
3162  {
3163  SCIP_Real side;
3164 
3165 #ifndef NDEBUG
3166  SCIP_CONSHDLR* conshdlr = SCIPconsGetHdlr(cons);
3167 
3168  assert(conshdlr != NULL);
3169  assert(strcmp(SCIPconshdlrGetName(conshdlr), "linear") == 0);
3170 #endif
3171  side = SCIPgetLhsLinear(set->scip, cons);
3172 
3173  if( !SCIPsetIsInfinity(set, -side) )
3174  {
3175  if( SCIPsetIsZero(set, side) )
3176  {
3177  scale = -1.0;
3178  }
3179  else
3180  {
3181  scale = proofsetGetRhs(proofset) / side;
3182  assert(SCIPsetIsNegative(set, scale));
3183  }
3184  }
3185  else
3186  {
3187  side = SCIPgetRhsLinear(set->scip, cons);
3188  assert(!SCIPsetIsInfinity(set, side));
3189 
3190  if( SCIPsetIsZero(set, side) )
3191  {
3192  scale = 1.0;
3193  }
3194  else
3195  {
3196  scale = proofsetGetRhs(proofset) / side;
3197  assert(SCIPsetIsPositive(set, scale));
3198  }
3199  }
3200  updateside = TRUE;
3201  }
3202 
3203  /* add dual proof to storage */
3204  SCIP_CALL( SCIPconflictstoreAddDualsolcons(conflictstore, cons, blkmem, set, stat, transprob, reopt, scale, updateside, hasrelaxvar) );
3205  }
3206 
3207  if( applyglobal ) /*lint !e774*/
3208  {
3209  /* add the constraint to the global problem */
3210  SCIP_CALL( SCIPprobAddCons(transprob, set, stat, cons) );
3211  }
3212  else
3213  {
3214  SCIP_CALL( SCIPnodeAddCons(tree->path[proofset->validdepth], blkmem, set, stat, tree, cons) );
3215  }
3216 
3217  SCIPsetDebugMsg(set, "added proof-constraint to node %p (#%lld) in depth %d (nproofconss %d)\n",
3218  (void*)tree->path[proofset->validdepth], SCIPnodeGetNumber(tree->path[proofset->validdepth]),
3219  proofset->validdepth,
3220  (conflicttype == SCIP_CONFTYPE_INFEASLP || conflicttype == SCIP_CONFTYPE_ALTINFPROOF)
3222 
3223  /* release the constraint */
3224  SCIP_CALL( SCIPreleaseCons(set->scip, &cons) );
3225 
3226  UPDATESTATISTICS:
3227  /* update statistics */
3228  if( conflicttype == SCIP_CONFTYPE_INFEASLP || conflicttype == SCIP_CONFTYPE_ALTINFPROOF )
3229  {
3230  conflict->dualproofsinfnnonzeros += nnz;
3231  if( applyglobal ) /*lint !e774*/
3232  ++conflict->ndualproofsinfglobal;
3233  else
3234  ++conflict->ndualproofsinflocal;
3235  ++conflict->ndualproofsinfsuccess;
3236  }
3237  else
3238  {
3239  assert(conflicttype == SCIP_CONFTYPE_BNDEXCEEDING || conflicttype == SCIP_CONFTYPE_ALTBNDPROOF);
3240  conflict->dualproofsbndnnonzeros += nnz;
3241  if( applyglobal ) /*lint !e774*/
3242  ++conflict->ndualproofsbndglobal;
3243  else
3244  ++conflict->ndualproofsbndlocal;
3245 
3246  ++conflict->ndualproofsbndsuccess;
3247  }
3248  return SCIP_OKAY;
3249 }
3250 
3251 /* create proof constraints out of proof sets */
3252 static
3254  SCIP_CONFLICT* conflict, /**< conflict analysis data */
3255  SCIP_CONFLICTSTORE* conflictstore, /**< conflict store */
3256  BMS_BLKMEM* blkmem, /**< block memory */
3257  SCIP_SET* set, /**< global SCIP settings */
3258  SCIP_STAT* stat, /**< dynamic problem statistics */
3259  SCIP_PROB* transprob, /**< transformed problem after presolve */
3260  SCIP_PROB* origprob, /**< original problem */
3261  SCIP_TREE* tree, /**< branch and bound tree */
3262  SCIP_REOPT* reopt, /**< reoptimization data structure */
3263  SCIP_LP* lp, /**< current LP data */
3264  SCIP_BRANCHCAND* branchcand, /**< branching candidate storage */
3265  SCIP_EVENTQUEUE* eventqueue, /**< event queue */
3266  SCIP_CLIQUETABLE* cliquetable /**< clique table data structure */
3267  )
3268 {
3269  assert(conflict != NULL);
3270 
3272  {
3273  /* only one variable has a coefficient different to zero, we add this bound change instead of a constraint */
3274  if( proofsetGetNVars(conflict->proofset) == 1 )
3275  {
3276  SCIP_VAR** vars;
3277  SCIP_Real* coefs;
3278  int* inds;
3279  SCIP_Real rhs;
3280 
3281  vars = SCIPprobGetVars(transprob);
3282 
3283  coefs = proofsetGetVals(conflict->proofset);
3284  inds = proofsetGetInds(conflict->proofset);
3285  rhs = proofsetGetRhs(conflict->proofset);
3286 
3287  SCIP_CALL( tightenSingleVar(conflict, set, stat, tree, blkmem, origprob, transprob, reopt, lp, \
3288  branchcand, eventqueue, cliquetable, vars[inds[0]], coefs[0], rhs, conflict->proofset->conflicttype,
3289  conflict->proofset->validdepth) );
3290  }
3291  else
3292  {
3293  SCIP_Bool skipinitialproof = FALSE;
3294 
3295  /* prefer an infeasibility proof
3296  *
3297  * todo: check whether this is really what we want
3298  */
3299  if( set->conf_prefinfproof && proofsetGetConftype(conflict->proofset) == SCIP_CONFTYPE_BNDEXCEEDING )
3300  {
3301  int i;
3302 
3303  for( i = 0; i < conflict->nproofsets; i++ )
3304  {
3306  {
3307  skipinitialproof = TRUE;
3308  break;
3309  }
3310  }
3311  }
3312 
3313  if( !skipinitialproof )
3314  {
3315  /* create and add the original proof */
3316  SCIP_CALL( createAndAddProofcons(conflict, conflictstore, conflict->proofset, set, stat, origprob, transprob, \
3317  tree, reopt, lp, branchcand, eventqueue, cliquetable, blkmem) );
3318  }
3319  }
3320 
3321  /* clear the proof set anyway */
3322  proofsetClear(conflict->proofset);
3323  }
3324 
3325  if( conflict->nproofsets > 0 )
3326  {
3327  int i;
3328 
3329  for( i = 0; i < conflict->nproofsets; i++ )
3330  {
3331  assert(conflict->proofsets[i] != NULL);
3332  assert(proofsetGetConftype(conflict->proofsets[i]) != SCIP_CONFTYPE_UNKNOWN);
3333 
3334  /* only one variable has a coefficient different to zero, we add this bound change instead of a constraint */
3335  if( proofsetGetNVars(conflict->proofsets[i]) == 1 )
3336  {
3337  SCIP_VAR** vars;
3338  SCIP_Real* coefs;
3339  int* inds;
3340  SCIP_Real rhs;
3341 
3342  vars = SCIPprobGetVars(transprob);
3343 
3344  coefs = proofsetGetVals(conflict->proofsets[i]);
3345  inds = proofsetGetInds(conflict->proofsets[i]);
3346  rhs = proofsetGetRhs(conflict->proofsets[i]);
3347 
3348  SCIP_CALL( tightenSingleVar(conflict, set, stat, tree, blkmem, origprob, transprob, reopt, lp,
3349  branchcand, eventqueue, cliquetable, vars[inds[0]], coefs[0], rhs,
3350  conflict->proofsets[i]->conflicttype, conflict->proofsets[i]->validdepth) );
3351  }
3352  else
3353  {
3354  /* create and add proof constraint */
3355  SCIP_CALL( createAndAddProofcons(conflict, conflictstore, conflict->proofsets[i], set, stat, origprob, \
3356  transprob, tree, reopt, lp, branchcand, eventqueue, cliquetable, blkmem) );
3357  }
3358  }
3359 
3360  /* free all proofsets */
3361  for( i = 0; i < conflict->nproofsets; i++ )
3362  proofsetFree(&conflict->proofsets[i], blkmem);
3363 
3364  conflict->nproofsets = 0;
3365  }
3366 
3367  return SCIP_OKAY;
3368 }
3369 
3370 /** adds the given conflict set as conflict constraint to the problem */
3371 static
3373  SCIP_CONFLICT* conflict, /**< conflict analysis data */
3374  BMS_BLKMEM* blkmem, /**< block memory */
3375  SCIP_SET* set, /**< global SCIP settings */
3376  SCIP_STAT* stat, /**< dynamic problem statistics */
3377  SCIP_PROB* transprob, /**< transformed problem after presolve */
3378  SCIP_PROB* origprob, /**< original problem */
3379  SCIP_TREE* tree, /**< branch and bound tree */
3380  SCIP_REOPT* reopt, /**< reoptimization data structure */
3381  SCIP_LP* lp, /**< current LP data */
3382  SCIP_BRANCHCAND* branchcand, /**< branching candidate storage */
3383  SCIP_EVENTQUEUE* eventqueue, /**< event queue */
3384  SCIP_CLIQUETABLE* cliquetable, /**< clique table data structure */
3385  SCIP_CONFLICTSET* conflictset, /**< conflict set to add to the tree */
3386  int insertdepth, /**< depth level at which the conflict set should be added */
3387  SCIP_Bool* success /**< pointer to store whether the addition was successful */
3388  )
3389 {
3390  SCIP_Bool redundant;
3391  int h;
3392 
3393  assert(conflict != NULL);
3394  assert(tree != NULL);
3395  assert(tree->path != NULL);
3396  assert(conflictset != NULL);
3397  assert(conflictset->validdepth <= insertdepth);
3398  assert(success != NULL);
3399 
3400  *success = FALSE;
3401  redundant = FALSE;
3402 
3403  /* try to derive global bound changes and shorten the conflictset by using implication and clique and variable bound
3404  * information
3405  */
3406  if( conflictset->nbdchginfos > 1 && insertdepth == 0 && !lp->strongbranching )
3407  {
3408  int nbdchgs;
3409  int nredvars;
3410 #ifdef SCIP_DEBUG
3411  int oldnbdchginfos = conflictset->nbdchginfos;
3412 #endif
3413  assert(conflictset->validdepth == 0);
3414 
3415  /* check conflict set on debugging solution */
3416  SCIP_CALL( SCIPdebugCheckConflict(blkmem, set, tree->root, conflictset->bdchginfos, conflictset->relaxedbds, conflictset->nbdchginfos) );
3417 
3418  SCIPclockStart(conflict->dIBclock, set);
3419 
3420  /* find global bound changes which can be derived from the new conflict set */
3421  SCIP_CALL( detectImpliedBounds(set, transprob, conflictset, &nbdchgs, &nredvars, &redundant) );
3422 
3423  /* all variables where removed, we have an infeasibility proof */
3424  if( conflictset->nbdchginfos == 0 )
3425  return SCIP_OKAY;
3426 
3427  /* debug check for reduced conflict set */
3428  if( nredvars > 0 )
3429  {
3430  /* check conflict set on debugging solution */
3431  SCIP_CALL( SCIPdebugCheckConflict(blkmem, set, tree->root, conflictset->bdchginfos, conflictset->relaxedbds, conflictset->nbdchginfos) ); /*lint !e506 !e774*/
3432  }
3433 
3434 #ifdef SCIP_DEBUG
3435  SCIPsetDebugMsg(set, " -> conflict set removed %d redundant variables (old nvars %d, new nvars = %d)\n", nredvars, oldnbdchginfos, conflictset->nbdchginfos);
3436  SCIPsetDebugMsg(set, " -> conflict set led to %d global bound changes %s(cdpt:%d, fdpt:%d, confdpt:%d, len:%d):\n",
3437  nbdchgs, redundant ? "(conflict became redundant) " : "", SCIPtreeGetCurrentDepth(tree), SCIPtreeGetFocusDepth(tree),
3438  conflictset->conflictdepth, conflictset->nbdchginfos);
3439  conflictsetPrint(conflictset);
3440 #endif
3441 
3442  SCIPclockStop(conflict->dIBclock, set);
3443 
3444  if( redundant )
3445  {
3446  if( nbdchgs > 0 )
3447  *success = TRUE;
3448 
3449  return SCIP_OKAY;
3450  }
3451  }
3452 
3453  /* in case the conflict set contains only one bound change which is globally valid we apply that bound change
3454  * directly (except if we are in strong branching or diving - in this case a bound change would yield an unflushed LP
3455  * and is not handled when restoring the information)
3456  *
3457  * @note A bound change can only be applied if it is are related to the active node or if is a global bound
3458  * change. Bound changes which are related to any other node cannot be handled at point due to the internal
3459  * data structure
3460  */
3461  if( conflictset->nbdchginfos == 1 && insertdepth == 0 && !lp->strongbranching && !lp->diving )
3462  {
3463  SCIP_VAR* var;
3464  SCIP_Real bound;
3465  SCIP_BOUNDTYPE boundtype;
3466 
3467  var = conflictset->bdchginfos[0]->var;
3468  assert(var != NULL);
3469 
3470  boundtype = SCIPboundtypeOpposite((SCIP_BOUNDTYPE) conflictset->bdchginfos[0]->boundtype);
3471  bound = conflictset->relaxedbds[0];
3472 
3473  /* for continuous variables, we can only use the relaxed version of the bounds negation: !(x <= u) -> x >= u */
3474  if( SCIPvarIsIntegral(var) )
3475  {
3476  assert(SCIPsetIsIntegral(set, bound));
3477  bound += (boundtype == SCIP_BOUNDTYPE_LOWER ? +1.0 : -1.0);
3478  }
3479 
3480  SCIPsetDebugMsg(set, " -> apply global bound change: <%s> %s %g\n",
3481  SCIPvarGetName(var), boundtype == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=", bound);
3482 
3483  SCIP_CALL( SCIPnodeAddBoundchg(tree->path[conflictset->validdepth], blkmem, set, stat, transprob, origprob, tree,
3484  reopt, lp, branchcand, eventqueue, cliquetable, var, bound, boundtype, FALSE) );
3485 
3486  *success = TRUE;
3487  SCIP_CALL( updateStatistics(conflict, blkmem, set, stat, conflictset, insertdepth) );
3488  }
3489  else if( !conflictset->hasrelaxonlyvar )
3490  {
3491  /* sort conflict handlers by priority */
3493 
3494  /* call conflict handlers to create a conflict constraint */
3495  for( h = 0; h < set->nconflicthdlrs; ++h )
3496  {
3497  SCIP_RESULT result;
3498 
3499  assert(conflictset->conflicttype != SCIP_CONFTYPE_UNKNOWN);
3500 
3501  SCIP_CALL( SCIPconflicthdlrExec(set->conflicthdlrs[h], set, tree->path[insertdepth],
3502  tree->path[conflictset->validdepth], conflictset->bdchginfos, conflictset->relaxedbds,
3503  conflictset->nbdchginfos, conflictset->conflicttype, conflictset->usescutoffbound, *success, &result) );
3504  if( result == SCIP_CONSADDED )
3505  {
3506  *success = TRUE;
3507  SCIP_CALL( updateStatistics(conflict, blkmem, set, stat, conflictset, insertdepth) );
3508  }
3509 
3510  SCIPsetDebugMsg(set, " -> call conflict handler <%s> (prio=%d) to create conflict set with %d bounds returned result %d\n",
3511  SCIPconflicthdlrGetName(set->conflicthdlrs[h]), SCIPconflicthdlrGetPriority(set->conflicthdlrs[h]),
3512  conflictset->nbdchginfos, result);
3513  }
3514  }
3515  else
3516  {
3517  SCIPsetDebugMsg(set, " -> skip conflict set with relaxation-only variable\n");
3518  /* TODO would be nice to still create a constraint?, if we can make sure that we the constraint does not survive a restart */
3519  }
3520 
3521  return SCIP_OKAY;
3522 }
3523 
3524 /** adds the collected conflict constraints to the corresponding nodes; the best set->conf_maxconss conflict constraints
3525  * are added to the node of their validdepth; additionally (if not yet added, and if repropagation is activated), the
3526  * conflict constraint that triggers the earliest repropagation is added to the node of its validdepth
3527  */
3529  SCIP_CONFLICT* conflict, /**< conflict analysis data */
3530  BMS_BLKMEM* blkmem, /**< block memory of transformed problem */
3531  SCIP_SET* set, /**< global SCIP settings */
3532  SCIP_STAT* stat, /**< dynamic problem statistics */
3533  SCIP_PROB* transprob, /**< transformed problem */
3534  SCIP_PROB* origprob, /**< original problem */
3535  SCIP_TREE* tree, /**< branch and bound tree */
3536  SCIP_REOPT* reopt, /**< reoptimization data structure */
3537  SCIP_LP* lp, /**< current LP data */
3538  SCIP_BRANCHCAND* branchcand, /**< branching candidate storage */
3539  SCIP_EVENTQUEUE* eventqueue, /**< event queue */
3540  SCIP_CLIQUETABLE* cliquetable /**< clique table data structure */
3541  )
3542 {
3543  assert(conflict != NULL);
3544  assert(set != NULL);
3545  assert(stat != NULL);
3546  assert(transprob != NULL);
3547  assert(tree != NULL);
3548 
3549  /* is there anything to do? */
3550  if( conflict->nconflictsets > 0 )
3551  {
3552  SCIP_CONFLICTSET* repropconflictset;
3553  int nconflictsetsused;
3554  int focusdepth;
3555 #ifndef NDEBUG
3556  int currentdepth;
3557 #endif
3558  int cutoffdepth;
3559  int repropdepth;
3560  int maxconflictsets;
3561  int maxsize;
3562  int i;
3563 
3564  /* calculate the maximal number of conflict sets to accept, and the maximal size of each accepted conflict set */
3565  maxconflictsets = (set->conf_maxconss == -1 ? INT_MAX : set->conf_maxconss);
3566  maxsize = conflictCalcMaxsize(set, transprob);
3567 
3568  focusdepth = SCIPtreeGetFocusDepth(tree);
3569 #ifndef NDEBUG
3570  currentdepth = SCIPtreeGetCurrentDepth(tree);
3571  assert(focusdepth <= currentdepth);
3572  assert(currentdepth == tree->pathlen-1);
3573 #endif
3574 
3575  SCIPsetDebugMsg(set, "flushing %d conflict sets at focus depth %d (maxconflictsets: %d, maxsize: %d)\n",
3576  conflict->nconflictsets, focusdepth, maxconflictsets, maxsize);
3577 
3578  /* mark the focus node to have produced conflict sets in the visualization output */
3579  SCIPvisualFoundConflict(stat->visual, stat, tree->path[focusdepth]);
3580 
3581  /* insert the conflict sets at the corresponding nodes */
3582  nconflictsetsused = 0;
3583  cutoffdepth = INT_MAX;
3584  repropdepth = INT_MAX;
3585  repropconflictset = NULL;
3586  for( i = 0; i < conflict->nconflictsets && nconflictsetsused < maxconflictsets; ++i )
3587  {
3588  SCIP_CONFLICTSET* conflictset;
3589 
3590  conflictset = conflict->conflictsets[i];
3591  assert(conflictset != NULL);
3592  assert(0 <= conflictset->validdepth);
3593  assert(conflictset->validdepth <= conflictset->insertdepth);
3594  assert(conflictset->insertdepth <= focusdepth);
3595  assert(conflictset->insertdepth <= conflictset->repropdepth);
3596  assert(conflictset->repropdepth <= currentdepth || conflictset->repropdepth == INT_MAX); /* INT_MAX for dive/probing/strong */
3597  assert(conflictset->conflictdepth <= currentdepth || conflictset->conflictdepth == INT_MAX); /* INT_MAX for dive/probing/strong */
3598 
3599  /* ignore conflict sets that are only valid at a node that was already cut off */
3600  if( conflictset->insertdepth >= cutoffdepth )
3601  {
3602  SCIPsetDebugMsg(set, " -> ignoring conflict set with insertdepth %d >= cutoffdepth %d\n",
3603  conflictset->validdepth, cutoffdepth);
3604  continue;
3605  }
3606 
3607  /* if no conflict bounds exist, the node and its sub tree in the conflict set's valid depth can be
3608  * cut off completely
3609  */
3610  if( conflictset->nbdchginfos == 0 )
3611  {
3612  SCIPsetDebugMsg(set, " -> empty conflict set in depth %d cuts off sub tree at depth %d\n",
3613  focusdepth, conflictset->validdepth);
3614 
3615  SCIP_CALL( SCIPnodeCutoff(tree->path[conflictset->validdepth], set, stat, tree, transprob, origprob, reopt, lp, blkmem) );
3616  cutoffdepth = conflictset->validdepth;
3617  continue;
3618  }
3619 
3620  /* if the conflict set is too long, use the conflict set only if it decreases the repropagation depth */
3621  if( conflictset->nbdchginfos > maxsize )
3622  {
3623  SCIPsetDebugMsg(set, " -> conflict set is too long: %d > %d literals\n", conflictset->nbdchginfos, maxsize);
3624  if( set->conf_keepreprop && conflictset->repropagate && conflictset->repropdepth < repropdepth )
3625  {
3626  repropdepth = conflictset->repropdepth;
3627  repropconflictset = conflictset;
3628  }
3629  }
3630  else
3631  {
3632  SCIP_Bool success;
3633 
3634  /* call conflict handlers to create a conflict constraint */
3635  SCIP_CALL( conflictAddConflictCons(conflict, blkmem, set, stat, transprob, origprob, tree, reopt, lp, \
3636  branchcand, eventqueue, cliquetable, conflictset, conflictset->insertdepth, &success) );
3637 
3638  /* if no conflict bounds exist, the node and its sub tree in the conflict set's valid depth can be
3639  * cut off completely
3640  */
3641  if( conflictset->nbdchginfos == 0 )
3642  {
3643  assert(!success);
3644 
3645  SCIPsetDebugMsg(set, " -> empty conflict set in depth %d cuts off sub tree at depth %d\n",
3646  focusdepth, conflictset->validdepth);
3647 
3648  SCIP_CALL( SCIPnodeCutoff(tree->path[conflictset->validdepth], set, stat, tree, transprob, origprob, \
3649  reopt, lp, blkmem) );
3650  cutoffdepth = conflictset->validdepth;
3651  continue;
3652  }
3653 
3654  if( success )
3655  {
3656  SCIPsetDebugMsg(set, " -> conflict set %d/%d added (cdpt:%d, fdpt:%d, insert:%d, valid:%d, conf:%d, reprop:%d, len:%d):\n",
3657  nconflictsetsused+1, maxconflictsets, SCIPtreeGetCurrentDepth(tree), SCIPtreeGetFocusDepth(tree),
3658  conflictset->insertdepth, conflictset->validdepth, conflictset->conflictdepth, conflictset->repropdepth,
3659  conflictset->nbdchginfos);
3660  SCIPdebug(conflictsetPrint(conflictset));
3661 
3662  if( conflictset->repropagate && conflictset->repropdepth <= repropdepth )
3663  {
3664  repropdepth = conflictset->repropdepth;
3665  repropconflictset = NULL;
3666  }
3667  nconflictsetsused++;
3668  }
3669  }
3670  }
3671 
3672  /* reactivate propagation on the first node where one of the new conflict sets trigger a deduction */
3673  if( set->conf_repropagate && repropdepth < cutoffdepth && repropdepth < tree->pathlen )
3674  {
3675  assert(0 <= repropdepth && repropdepth < tree->pathlen);
3676  assert((int) tree->path[repropdepth]->depth == repropdepth);
3677 
3678  /* if the conflict constraint of smallest repropagation depth was not yet added, insert it now */
3679  if( repropconflictset != NULL )
3680  {
3681  SCIP_Bool success;
3682 
3683  assert(repropconflictset->repropagate);
3684  assert(repropconflictset->repropdepth == repropdepth);
3685 
3686  SCIP_CALL( conflictAddConflictCons(conflict, blkmem, set, stat, transprob, origprob, tree, reopt, lp, \
3687  branchcand, eventqueue, cliquetable, repropconflictset, repropdepth, &success) );
3688 
3689  /* if no conflict bounds exist, the node and its sub tree in the conflict set's valid depth can be
3690  * cut off completely
3691  */
3692  if( repropconflictset->nbdchginfos == 0 )
3693  {
3694  assert(!success);
3695 
3696  SCIPsetDebugMsg(set, " -> empty reprop conflict set in depth %d cuts off sub tree at depth %d\n",
3697  focusdepth, repropconflictset->validdepth);
3698 
3699  SCIP_CALL( SCIPnodeCutoff(tree->path[repropconflictset->validdepth], set, stat, tree, transprob, \
3700  origprob, reopt, lp, blkmem) );
3701  }
3702 
3703 #ifdef SCIP_DEBUG
3704  if( success )
3705  {
3706  SCIPsetDebugMsg(set, " -> additional reprop conflict set added (cdpt:%d, fdpt:%d, insert:%d, valid:%d, conf:%d, reprop:%d, len:%d):\n",
3708  repropconflictset->insertdepth, repropconflictset->validdepth, repropconflictset->conflictdepth,
3709  repropconflictset->repropdepth, repropconflictset->nbdchginfos);
3710  SCIPdebug(conflictsetPrint(repropconflictset));
3711  }
3712 #endif
3713  }
3714 
3715  /* mark the node in the repropdepth to be propagated again */
3716  SCIPnodePropagateAgain(tree->path[repropdepth], set, stat, tree);
3717 
3718  SCIPsetDebugMsg(set, "marked node %p in depth %d to be repropagated due to conflicts found in depth %d\n",
3719  (void*)tree->path[repropdepth], repropdepth, focusdepth);
3720  }
3721 
3722  /* free the conflict store */
3723  for( i = 0; i < conflict->nconflictsets; ++i )
3724  {
3725  conflictsetFree(&conflict->conflictsets[i], blkmem);
3726  }
3727  conflict->nconflictsets = 0;
3728  }
3729 
3730  /* free all temporarily created bound change information data */
3731  conflictFreeTmpBdchginfos(conflict, blkmem);
3732 
3733  return SCIP_OKAY;
3734 }
3735 
3736 /** returns the current number of conflict sets in the conflict set storage */
3738  SCIP_CONFLICT* conflict /**< conflict analysis data */
3739  )
3740 {
3741  assert(conflict != NULL);
3742 
3743  return conflict->nconflictsets;
3744 }
3745 
3746 /** returns the total number of conflict constraints that were added to the problem */
3748  SCIP_CONFLICT* conflict /**< conflict analysis data */
3749  )
3750 {
3751  assert(conflict != NULL);
3752 
3753  return conflict->nappliedglbconss + conflict->nappliedlocconss;
3754 }
3755 
3756 /** returns the total number of literals in conflict constraints that were added to the problem */
3758  SCIP_CONFLICT* conflict /**< conflict analysis data */
3759  )
3760 {
3761  assert(conflict != NULL);
3762 
3763  return conflict->nappliedglbliterals + conflict->nappliedlocliterals;
3764 }
3765 
3766 /** returns the total number of global bound changes applied by the conflict analysis */
3768  SCIP_CONFLICT* conflict /**< conflict analysis data */
3769  )
3770 {
3771  assert(conflict != NULL);
3772 
3773  return conflict->nglbchgbds;
3774 }
3775 
3776 /** returns the total number of conflict constraints that were added globally to the problem */
3778  SCIP_CONFLICT* conflict /**< conflict analysis data */
3779  )
3780 {
3781  assert(conflict != NULL);
3782 
3783  return conflict->nappliedglbconss;
3784 }
3785 
3786 /** returns the total number of literals in conflict constraints that were added globally to the problem */
3788  SCIP_CONFLICT* conflict /**< conflict analysis data */
3789  )
3790 {
3791  assert(conflict != NULL);
3792 
3793  return conflict->nappliedglbliterals;
3794 }
3795 
3796 /** returns the total number of local bound changes applied by the conflict analysis */
3798  SCIP_CONFLICT* conflict /**< conflict analysis data */
3799  )
3800 {
3801  assert(conflict != NULL);
3802 
3803  return conflict->nlocchgbds;
3804 }
3805 
3806 /** returns the total number of conflict constraints that were added locally to the problem */
3808  SCIP_CONFLICT* conflict /**< conflict analysis data */
3809  )
3810 {
3811  assert(conflict != NULL);
3812 
3813  return conflict->nappliedlocconss;
3814 }
3815 
3816 /** returns the total number of literals in conflict constraints that were added locally to the problem */
3818  SCIP_CONFLICT* conflict /**< conflict analysis data */
3819  )
3820 {
3821  assert(conflict != NULL);
3822 
3823  return conflict->nappliedlocliterals;
3824 }
3825 
3826 
3827 
3828 
3829 /*
3830  * Propagation Conflict Analysis
3831  */
3832 
3833 /** returns whether bound change has a valid reason that can be resolved in conflict analysis */
3834 static
3836  SCIP_BDCHGINFO* bdchginfo /**< bound change information */
3837  )
3838 {
3839  assert(bdchginfo != NULL);
3840  assert(!SCIPbdchginfoIsRedundant(bdchginfo));
3841 
3844  && SCIPbdchginfoGetInferProp(bdchginfo) != NULL));
3845 }
3846 
3847 /** compares two conflict set entries, such that bound changes infered later are
3848  * ordered prior to ones that were infered earlier
3849  */
3850 static
3851 SCIP_DECL_SORTPTRCOMP(conflictBdchginfoComp)
3852 { /*lint --e{715}*/
3853  SCIP_BDCHGINFO* bdchginfo1;
3854  SCIP_BDCHGINFO* bdchginfo2;
3855 
3856  bdchginfo1 = (SCIP_BDCHGINFO*)elem1;
3857  bdchginfo2 = (SCIP_BDCHGINFO*)elem2;
3858  assert(bdchginfo1 != NULL);
3859  assert(bdchginfo2 != NULL);
3860  assert(!SCIPbdchginfoIsRedundant(bdchginfo1));
3861  assert(!SCIPbdchginfoIsRedundant(bdchginfo2));
3862 
3863  if( bdchginfo1 == bdchginfo2 )
3864  return 0;
3865 
3867  return -1;
3868  else
3869  return +1;
3870 }
3871 
3872 /** return TRUE if conflict analysis is applicable; In case the function return FALSE there is no need to initialize the
3873  * conflict analysis since it will not be applied
3874  */
3876  SCIP_SET* set /**< global SCIP settings */
3877  )
3878 {
3879  /* check, if propagation conflict analysis is enabled */
3880  if( !set->conf_enable || !set->conf_useprop )
3881  return FALSE;
3882 
3883  /* check, if there are any conflict handlers to use a conflict set */
3884  if( set->nconflicthdlrs == 0 )
3885  return FALSE;
3886 
3887  return TRUE;
3888 }
3889 
3890 /** creates conflict analysis data for propagation conflicts */
3892  SCIP_CONFLICT** conflict, /**< pointer to conflict analysis data */
3893  BMS_BLKMEM* blkmem, /**< block memory of transformed problem */
3894  SCIP_SET* set /**< global SCIP settings */
3895  )
3896 {
3897  assert(conflict != NULL);
3898 
3899  SCIP_ALLOC( BMSallocMemory(conflict) );
3900 
3901  SCIP_CALL( SCIPclockCreate(&(*conflict)->dIBclock, SCIP_CLOCKTYPE_DEFAULT) );
3902  SCIP_CALL( SCIPclockCreate(&(*conflict)->propanalyzetime, SCIP_CLOCKTYPE_DEFAULT) );
3903  SCIP_CALL( SCIPclockCreate(&(*conflict)->inflpanalyzetime, SCIP_CLOCKTYPE_DEFAULT) );
3904  SCIP_CALL( SCIPclockCreate(&(*conflict)->boundlpanalyzetime, SCIP_CLOCKTYPE_DEFAULT) );
3905  SCIP_CALL( SCIPclockCreate(&(*conflict)->sbanalyzetime, SCIP_CLOCKTYPE_DEFAULT) );
3906  SCIP_CALL( SCIPclockCreate(&(*conflict)->pseudoanalyzetime, SCIP_CLOCKTYPE_DEFAULT) );
3907 
3908  /* enable or disable timing depending on the parameter statistic timing */
3909  SCIPconflictEnableOrDisableClocks((*conflict), set->time_statistictiming);
3910 
3911  SCIP_CALL( SCIPpqueueCreate(&(*conflict)->bdchgqueue, set->mem_arraygrowinit, set->mem_arraygrowfac,
3912  conflictBdchginfoComp, NULL) );
3913  SCIP_CALL( SCIPpqueueCreate(&(*conflict)->forcedbdchgqueue, set->mem_arraygrowinit, set->mem_arraygrowfac,
3914  conflictBdchginfoComp, NULL) );
3915  SCIP_CALL( conflictsetCreate(&(*conflict)->conflictset, blkmem) );
3916  (*conflict)->conflictsets = NULL;
3917  (*conflict)->conflictsetscores = NULL;
3918  (*conflict)->tmpbdchginfos = NULL;
3919  (*conflict)->conflictsetssize = 0;
3920  (*conflict)->nconflictsets = 0;
3921  (*conflict)->proofsets = NULL;
3922  (*conflict)->proofsetssize = 0;
3923  (*conflict)->nproofsets = 0;
3924  (*conflict)->tmpbdchginfossize = 0;
3925  (*conflict)->ntmpbdchginfos = 0;
3926  (*conflict)->count = 0;
3927  (*conflict)->nglbchgbds = 0;
3928  (*conflict)->nappliedglbconss = 0;
3929  (*conflict)->nappliedglbliterals = 0;
3930  (*conflict)->nlocchgbds = 0;
3931  (*conflict)->nappliedlocconss = 0;
3932  (*conflict)->nappliedlocliterals = 0;
3933  (*conflict)->npropcalls = 0;
3934  (*conflict)->npropsuccess = 0;
3935  (*conflict)->npropconfconss = 0;
3936  (*conflict)->npropconfliterals = 0;
3937  (*conflict)->npropreconvconss = 0;
3938  (*conflict)->npropreconvliterals = 0;
3939  (*conflict)->ninflpcalls = 0;
3940  (*conflict)->ninflpsuccess = 0;
3941  (*conflict)->ninflpconfconss = 0;
3942  (*conflict)->ninflpconfliterals = 0;
3943  (*conflict)->ninflpreconvconss = 0;
3944  (*conflict)->ninflpreconvliterals = 0;
3945  (*conflict)->ninflpiterations = 0;
3946  (*conflict)->nboundlpcalls = 0;
3947  (*conflict)->nboundlpsuccess = 0;
3948  (*conflict)->nboundlpconfconss = 0;
3949  (*conflict)->nboundlpconfliterals = 0;
3950  (*conflict)->nboundlpreconvconss = 0;
3951  (*conflict)->nboundlpreconvliterals = 0;
3952  (*conflict)->nboundlpiterations = 0;
3953  (*conflict)->nsbcalls = 0;
3954  (*conflict)->nsbsuccess = 0;
3955  (*conflict)->nsbconfconss = 0;
3956  (*conflict)->nsbconfliterals = 0;
3957  (*conflict)->nsbreconvconss = 0;
3958  (*conflict)->nsbreconvliterals = 0;
3959  (*conflict)->nsbiterations = 0;
3960  (*conflict)->npseudocalls = 0;
3961  (*conflict)->npseudosuccess = 0;
3962  (*conflict)->npseudoconfconss = 0;
3963  (*conflict)->npseudoconfliterals = 0;
3964  (*conflict)->npseudoreconvconss = 0;
3965  (*conflict)->npseudoreconvliterals = 0;
3966  (*conflict)->ndualproofsinfglobal = 0;
3967  (*conflict)->ndualproofsinflocal = 0;
3968  (*conflict)->ndualproofsinfsuccess = 0;
3969  (*conflict)->dualproofsinfnnonzeros = 0;
3970  (*conflict)->ndualproofsbndglobal = 0;
3971  (*conflict)->ndualproofsbndlocal = 0;
3972  (*conflict)->ndualproofsbndsuccess = 0;
3973  (*conflict)->dualproofsbndnnonzeros = 0;
3974 
3975  SCIP_CALL( conflictInitProofset((*conflict), blkmem) );
3976 
3977  return SCIP_OKAY;
3978 }
3979 
3980 /** frees conflict analysis data for propagation conflicts */
3982  SCIP_CONFLICT** conflict, /**< pointer to conflict analysis data */
3983  BMS_BLKMEM* blkmem /**< block memory of transformed problem */
3984  )
3985 {
3986  assert(conflict != NULL);
3987  assert(*conflict != NULL);
3988  assert((*conflict)->nconflictsets == 0);
3989  assert((*conflict)->ntmpbdchginfos == 0);
3990 
3991 #ifdef SCIP_CONFGRAPH
3992  confgraphFree();
3993 #endif
3994 
3995  SCIPclockFree(&(*conflict)->dIBclock);
3996  SCIPclockFree(&(*conflict)->propanalyzetime);
3997  SCIPclockFree(&(*conflict)->inflpanalyzetime);
3998  SCIPclockFree(&(*conflict)->boundlpanalyzetime);
3999  SCIPclockFree(&(*conflict)->sbanalyzetime);
4000  SCIPclockFree(&(*conflict)->pseudoanalyzetime);
4001  SCIPpqueueFree(&(*conflict)->bdchgqueue);
4002  SCIPpqueueFree(&(*conflict)->forcedbdchgqueue);
4003  conflictsetFree(&(*conflict)->conflictset, blkmem);
4004  proofsetFree(&(*conflict)->proofset, blkmem);
4005 
4006  BMSfreeMemoryArrayNull(&(*conflict)->conflictsets);
4007  BMSfreeMemoryArrayNull(&(*conflict)->conflictsetscores);
4008  BMSfreeMemoryArrayNull(&(*conflict)->proofsets);
4009  BMSfreeMemoryArrayNull(&(*conflict)->tmpbdchginfos);
4010  BMSfreeMemory(conflict);
4011 
4012  return SCIP_OKAY;
4013 }
4014 
4015 /** clears the conflict queue and the current conflict set */
4016 static
4018  SCIP_CONFLICT* conflict /**< conflict analysis data */
4019  )
4020 {
4021  assert(conflict != NULL);
4022 
4023  SCIPpqueueClear(conflict->bdchgqueue);
4024  SCIPpqueueClear(conflict->forcedbdchgqueue);
4025  conflictsetClear(conflict->conflictset);
4026 }
4027 
4028 /** initializes the propagation conflict analysis by clearing the conflict candidate queue */
4030  SCIP_CONFLICT* conflict, /**< conflict analysis data */
4031  SCIP_SET* set, /**< global SCIP settings */
4032  SCIP_STAT* stat, /**< problem statistics */
4033  SCIP_PROB* prob, /**< problem data */
4034  SCIP_CONFTYPE conftype, /**< type of the conflict */
4035  SCIP_Bool usescutoffbound /**< depends the conflict on a cutoff bound? */
4036  )
4037 {
4038  assert(conflict != NULL);
4039  assert(set != NULL);
4040  assert(stat != NULL);
4041  assert(prob != NULL);
4042 
4043  SCIPsetDebugMsg(set, "initializing conflict analysis\n");
4044 
4045  /* clear the conflict candidate queue and the conflict set */
4046  conflictClear(conflict);
4047 
4048  /* set conflict type */
4049  assert(conftype == SCIP_CONFTYPE_BNDEXCEEDING || conftype == SCIP_CONFTYPE_INFEASLP
4050  || conftype == SCIP_CONFTYPE_PROPAGATION);
4051  conflict->conflictset->conflicttype = conftype;
4052 
4053  /* set whether a cutoff bound is involved */
4054  conflict->conflictset->usescutoffbound = usescutoffbound;
4055 
4056  /* increase the conflict counter, such that binary variables of new conflict set and new conflict queue are labeled
4057  * with this new counter
4058  */
4059  conflict->count++;
4060  if( conflict->count == 0 ) /* make sure, 0 is not a valid conflict counter (may happen due to integer overflow) */
4061  conflict->count = 1;
4062 
4063  /* increase the conflict score weight for history updates of future conflict reasons */
4064  if( stat->nnodes > stat->lastconflictnode )
4065  {
4066  assert(0.0 < set->conf_scorefac && set->conf_scorefac <= 1.0);
4067  stat->vsidsweight /= set->conf_scorefac;
4068  assert(stat->vsidsweight > 0.0);
4069 
4070  /* if the conflict score for the next conflict exceeds 1000.0, rescale all history conflict scores */
4071  if( stat->vsidsweight >= 1000.0 )
4072  {
4073  int v;
4074 
4075  for( v = 0; v < prob->nvars; ++v )
4076  {
4077  SCIP_CALL( SCIPvarScaleVSIDS(prob->vars[v], 1.0/stat->vsidsweight) );
4078  }
4079  SCIPhistoryScaleVSIDS(stat->glbhistory, 1.0/stat->vsidsweight);
4081  stat->vsidsweight = 1.0;
4082  }
4083  stat->lastconflictnode = stat->nnodes;
4084  }
4085 
4086 #ifdef SCIP_CONFGRAPH
4087  confgraphFree();
4088  SCIP_CALL( confgraphCreate(set, conflict) );
4089 #endif
4090 
4091  return SCIP_OKAY;
4092 }
4093 
4094 /** marks bound to be present in the current conflict and returns whether a bound which is at least as tight was already
4095  * member of the current conflict (i.e., the given bound change does not need to be added)
4096  */
4097 static
4099  SCIP_CONFLICT* conflict, /**< conflict analysis data */
4100  SCIP_SET* set, /**< global SCIP settings */
4101  SCIP_BDCHGINFO* bdchginfo, /**< bound change to add to the conflict set */
4102  SCIP_Real relaxedbd /**< relaxed bound */
4103  )
4104 {
4105  SCIP_VAR* var;
4106  SCIP_Real newbound;
4107 
4108  assert(conflict != NULL);
4109 
4110  var = SCIPbdchginfoGetVar(bdchginfo);
4111  newbound = SCIPbdchginfoGetNewbound(bdchginfo);
4112  assert(var != NULL);
4113 
4114  switch( SCIPbdchginfoGetBoundtype(bdchginfo) )
4115  {
4116  case SCIP_BOUNDTYPE_LOWER:
4117  /* check if the variables lower bound is already member of the conflict */
4118  if( var->conflictlbcount == conflict->count )
4119  {
4120  /* the variable is already member of the conflict; hence check if the new bound is redundant */
4121  if( var->conflictlb > newbound )
4122  {
4123  SCIPsetDebugMsg(set, "ignoring redundant bound change <%s> >= %g since a stronger lower bound exist <%s> >= %g\n",
4124  SCIPvarGetName(var), newbound, SCIPvarGetName(var), var->conflictlb);
4125  return TRUE;
4126  }
4127  else if( var->conflictlb == newbound ) /*lint !e777*/
4128  {
4129  SCIPsetDebugMsg(set, "ignoring redundant bound change <%s> >= %g since this lower bound is already present\n", SCIPvarGetName(var), newbound);
4130  SCIPsetDebugMsg(set, "adjust relaxed lower bound <%g> -> <%g>\n", var->conflictlb, relaxedbd);
4131  var->conflictrelaxedlb = MAX(var->conflictrelaxedlb, relaxedbd);
4132  return TRUE;
4133  }
4134  }
4135 
4136  /* add the variable lower bound to the current conflict */
4137  var->conflictlbcount = conflict->count;
4138 
4139  /* remember the lower bound and relaxed bound to allow only better/tighter lower bounds for that variables
4140  * w.r.t. this conflict
4141  */
4142  var->conflictlb = newbound;
4143  var->conflictrelaxedlb = relaxedbd;
4144 
4145  return FALSE;
4146 
4147  case SCIP_BOUNDTYPE_UPPER:
4148  /* check if the variables upper bound is already member of the conflict */
4149  if( var->conflictubcount == conflict->count )
4150  {
4151  /* the variable is already member of the conflict; hence check if the new bound is redundant */
4152  if( var->conflictub < newbound )
4153  {
4154  SCIPsetDebugMsg(set, "ignoring redundant bound change <%s> <= %g since a stronger upper bound exist <%s> <= %g\n",
4155  SCIPvarGetName(var), newbound, SCIPvarGetName(var), var->conflictub);
4156  return TRUE;
4157  }
4158  else if( var->conflictub == newbound ) /*lint !e777*/
4159  {
4160  SCIPsetDebugMsg(set, "ignoring redundant bound change <%s> <= %g since this upper bound is already present\n", SCIPvarGetName(var), newbound);
4161  SCIPsetDebugMsg(set, "adjust relaxed upper bound <%g> -> <%g>\n", var->conflictub, relaxedbd);
4162  var->conflictrelaxedub = MIN(var->conflictrelaxedub, relaxedbd);
4163  return TRUE;
4164  }
4165  }
4166 
4167  /* add the variable upper bound to the current conflict */
4168  var->conflictubcount = conflict->count;
4169 
4170  /* remember the upper bound and relaxed bound to allow only better/tighter upper bounds for that variables
4171  * w.r.t. this conflict
4172  */
4173  var->conflictub = newbound;
4174  var->conflictrelaxedub = relaxedbd;
4175 
4176  return FALSE;
4177 
4178  default:
4179  SCIPerrorMessage("invalid bound type %d\n", SCIPbdchginfoGetBoundtype(bdchginfo));
4180  SCIPABORT();
4181  return FALSE; /*lint !e527*/
4182  }
4183 }
4184 
4185 /** puts bound change into the current conflict set */
4186 static
4188  SCIP_CONFLICT* conflict, /**< conflict analysis data */
4189  BMS_BLKMEM* blkmem, /**< block memory of transformed problem */
4190  SCIP_SET* set, /**< global SCIP settings */
4191  SCIP_BDCHGINFO* bdchginfo, /**< bound change to add to the conflict set */
4192  SCIP_Real relaxedbd /**< relaxed bound */
4193  )
4194 {
4195  assert(conflict != NULL);
4196  assert(!SCIPbdchginfoIsRedundant(bdchginfo));
4197 
4198  /* check if the relaxed bound is really a relaxed bound */
4199  assert(SCIPbdchginfoGetBoundtype(bdchginfo) == SCIP_BOUNDTYPE_LOWER || SCIPsetIsGE(set, relaxedbd, SCIPbdchginfoGetNewbound(bdchginfo)));
4200  assert(SCIPbdchginfoGetBoundtype(bdchginfo) == SCIP_BOUNDTYPE_UPPER || SCIPsetIsLE(set, relaxedbd, SCIPbdchginfoGetNewbound(bdchginfo)));
4201 
4202  SCIPsetDebugMsg(set, "putting bound change <%s> %s %g(%g) at depth %d to current conflict set\n",
4203  SCIPvarGetName(SCIPbdchginfoGetVar(bdchginfo)),
4204  SCIPbdchginfoGetBoundtype(bdchginfo) == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=", SCIPbdchginfoGetNewbound(bdchginfo),
4205  relaxedbd, SCIPbdchginfoGetDepth(bdchginfo));
4206 
4207  /* mark the bound to be member of the conflict and check if a bound which is at least as tight is already member of
4208  * the conflict
4209  */
4210  if( !conflictMarkBoundCheckPresence(conflict, set, bdchginfo, relaxedbd) )
4211  {
4212  /* add the bound change to the current conflict set */
4213  SCIP_CALL( conflictsetAddBound(conflict->conflictset, blkmem, set, bdchginfo, relaxedbd) );
4214 
4215 #ifdef SCIP_CONFGRAPH
4216  if( bdchginfo != confgraphcurrentbdchginfo )
4217  confgraphAddBdchg(bdchginfo);
4218 #endif
4219  }
4220 #ifdef SCIP_CONFGRAPH
4221  else
4222  confgraphLinkBdchg(bdchginfo);
4223 #endif
4224 
4225  return SCIP_OKAY;
4226 }
4227 
4228 /** returns whether the negation of the given bound change would lead to a globally valid literal */
4229 static
4231  SCIP_SET* set, /**< global SCIP settings */
4232  SCIP_BDCHGINFO* bdchginfo /**< bound change information */
4233  )
4234 {
4235  SCIP_VAR* var;
4236  SCIP_BOUNDTYPE boundtype;
4237  SCIP_Real bound;
4238 
4239  var = SCIPbdchginfoGetVar(bdchginfo);
4240  boundtype = SCIPbdchginfoGetBoundtype(bdchginfo);
4241  bound = SCIPbdchginfoGetNewbound(bdchginfo);
4242 
4243  return (SCIPvarGetType(var) == SCIP_VARTYPE_CONTINUOUS
4244  && ((boundtype == SCIP_BOUNDTYPE_LOWER && SCIPsetIsFeasGE(set, bound, SCIPvarGetUbGlobal(var)))
4245  || (boundtype == SCIP_BOUNDTYPE_UPPER && SCIPsetIsFeasLE(set, bound, SCIPvarGetLbGlobal(var)))));
4246 }
4247 
4248 /** adds given bound change information to the conflict candidate queue */
4249 static
4251  SCIP_CONFLICT* conflict, /**< conflict analysis data */
4252  SCIP_SET* set, /**< global SCIP settings */
4253  SCIP_BDCHGINFO* bdchginfo, /**< bound change information */
4254  SCIP_Real relaxedbd /**< relaxed bound */
4255  )
4256 {
4257  assert(conflict != NULL);
4258  assert(set != NULL);
4259  assert(bdchginfo != NULL);
4260  assert(!SCIPbdchginfoIsRedundant(bdchginfo));
4261 
4262  /* check if the relaxed bound is really a relaxed bound */
4263  assert(SCIPbdchginfoGetBoundtype(bdchginfo) == SCIP_BOUNDTYPE_LOWER || SCIPsetIsGE(set, relaxedbd, SCIPbdchginfoGetNewbound(bdchginfo)));
4264  assert(SCIPbdchginfoGetBoundtype(bdchginfo) == SCIP_BOUNDTYPE_UPPER || SCIPsetIsLE(set, relaxedbd, SCIPbdchginfoGetNewbound(bdchginfo)));
4265 
4266  /* mark the bound to be member of the conflict and check if a bound which is at least as tight is already member of
4267  * the conflict
4268  */
4269  if( !conflictMarkBoundCheckPresence(conflict, set, bdchginfo, relaxedbd) )
4270  {
4271  /* insert the bound change into the conflict queue */
4272  if( (!set->conf_preferbinary || SCIPvarIsBinary(SCIPbdchginfoGetVar(bdchginfo)))
4273  && !isBoundchgUseless(set, bdchginfo) )
4274  {
4275  SCIP_CALL( SCIPpqueueInsert(conflict->bdchgqueue, (void*)bdchginfo) );
4276  }
4277  else
4278  {
4279  SCIP_CALL( SCIPpqueueInsert(conflict->forcedbdchgqueue, (void*)bdchginfo) );
4280  }
4281 
4282 #ifdef SCIP_CONFGRAPH
4283  confgraphAddBdchg(bdchginfo);
4284 #endif
4285  }
4286 #ifdef SCIP_CONFGRAPH
4287  else
4288  confgraphLinkBdchg(bdchginfo);
4289 #endif
4290 
4291  return SCIP_OKAY;
4292 }
4293 
4294 /** convert variable and bound change to active variable */
4295 static
4297  SCIP_VAR** var, /**< pointer to variable */
4298  SCIP_SET* set, /**< global SCIP settings */
4299  SCIP_BOUNDTYPE* boundtype, /**< pointer to type of bound that was changed: lower or upper bound */
4300  SCIP_Real* bound /**< pointer to bound to convert, or NULL */
4301  )
4302 {
4303  SCIP_Real scalar;
4304  SCIP_Real constant;
4305 
4306  scalar = 1.0;
4307  constant = 0.0;
4308 
4309  /* transform given varibale to active varibale */
4310  SCIP_CALL( SCIPvarGetProbvarSum(var, set, &scalar, &constant) );
4311  assert(SCIPvarGetStatus(*var) == SCIP_VARSTATUS_FIXED || scalar != 0.0); /*lint !e777*/
4312 
4313  if( SCIPvarGetStatus(*var) == SCIP_VARSTATUS_FIXED )
4314  return SCIP_OKAY;
4315 
4316  /* if the scalar of the aggregation is negative, we have to switch the bound type */
4317  if( scalar < 0.0 )
4318  (*boundtype) = SCIPboundtypeOpposite(*boundtype);
4319 
4320  if( bound != NULL )
4321  {
4322  (*bound) -= constant;
4323  (*bound) /= scalar;
4324  }
4325 
4326  return SCIP_OKAY;
4327 }
4328 
4329 /** adds variable's bound to conflict candidate queue */
4330 static
4332  SCIP_CONFLICT* conflict, /**< conflict analysis data */
4333  BMS_BLKMEM* blkmem, /**< block memory */
4334  SCIP_SET* set, /**< global SCIP settings */
4335  SCIP_STAT* stat, /**< dynamic problem statistics */
4336  SCIP_VAR* var, /**< problem variable */
4337  SCIP_BOUNDTYPE boundtype, /**< type of bound that was changed: lower or upper bound */
4338  SCIP_BDCHGINFO* bdchginfo, /**< bound change info, or NULL */
4339  SCIP_Real relaxedbd /**< relaxed bound */
4340  )
4341 {
4342  assert(SCIPvarIsActive(var));
4343  assert(bdchginfo != NULL);
4344  assert(!SCIPbdchginfoIsRedundant(bdchginfo));
4345 
4346  SCIPsetDebugMsg(set, " -> adding bound <%s> %s %.15g(%.15g) [status:%d, type:%d, depth:%d, pos:%d, reason:<%s>, info:%d] to candidates\n",
4347  SCIPvarGetName(var),
4348  boundtype == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=",
4349  SCIPbdchginfoGetNewbound(bdchginfo), relaxedbd,
4350  SCIPvarGetStatus(var), SCIPvarGetType(var),
4351  SCIPbdchginfoGetDepth(bdchginfo), SCIPbdchginfoGetPos(bdchginfo),
4352  SCIPbdchginfoGetChgtype(bdchginfo) == SCIP_BOUNDCHGTYPE_BRANCHING ? "branch"
4356  : "none")),
4358 
4359  /* the local bound change may be resolved and has to be put on the candidate queue;
4360  * we even put bound changes without inference information on the queue in order to automatically
4361  * eliminate multiple insertions of the same bound change
4362  */
4363  assert(SCIPbdchginfoGetVar(bdchginfo) == var);
4364  assert(SCIPbdchginfoGetBoundtype(bdchginfo) == boundtype);
4365  assert(SCIPbdchginfoGetDepth(bdchginfo) >= 0);
4366  assert(SCIPbdchginfoGetPos(bdchginfo) >= 0);
4367 
4368  /* the relaxed bound should be a relaxation */
4369  assert(boundtype == SCIP_BOUNDTYPE_LOWER ? SCIPsetIsLE(set, relaxedbd, SCIPbdchginfoGetNewbound(bdchginfo)) : SCIPsetIsGE(set, relaxedbd, SCIPbdchginfoGetNewbound(bdchginfo)));
4370 
4371  /* the relaxed bound should be worse then the old bound of the bound change info */
4372  assert(boundtype == SCIP_BOUNDTYPE_LOWER ? SCIPsetIsGT(set, relaxedbd, SCIPbdchginfoGetOldbound(bdchginfo)) : SCIPsetIsLT(set, relaxedbd, SCIPbdchginfoGetOldbound(bdchginfo)));
4373 
4374  /* put bound change information into priority queue */
4375  SCIP_CALL( conflictQueueBound(conflict, set, bdchginfo, relaxedbd) );
4376 
4377  /* each variable which is add to the conflict graph gets an increase in the VSIDS
4378  *
4379  * @note That is different to the VSIDS preseted in the literature
4380  */
4381  SCIP_CALL( incVSIDS(var, blkmem, set, stat, boundtype, relaxedbd, set->conf_conflictgraphweight) );
4382 
4383  return SCIP_OKAY;
4384 }
4385 
4386 /** adds variable's bound to conflict candidate queue */
4388  SCIP_CONFLICT* conflict, /**< conflict analysis data */
4389  BMS_BLKMEM* blkmem, /**< block memory */
4390  SCIP_SET* set, /**< global SCIP settings */
4391  SCIP_STAT* stat, /**< dynamic problem statistics */
4392  SCIP_VAR* var, /**< problem variable */
4393  SCIP_BOUNDTYPE boundtype, /**< type of bound that was changed: lower or upper bound */
4394  SCIP_BDCHGIDX* bdchgidx /**< bound change index (time stamp of bound change), or NULL for current time */
4395  )
4396 {
4397  SCIP_BDCHGINFO* bdchginfo;
4398 
4399  assert(conflict != NULL);
4400  assert(stat != NULL);
4401  assert(var != NULL);
4402 
4403  /* convert bound to active problem variable */
4404  SCIP_CALL( convertToActiveVar(&var, set, &boundtype, NULL) );
4405 
4406  /* we can ignore fixed variables */
4408  return SCIP_OKAY;
4409 
4410  /* if the variable is multi-aggregated, add the bounds of all aggregation variables */
4412  {
4413  SCIP_VAR** vars;
4414  SCIP_Real* scalars;
4415  int nvars;
4416  int i;
4417 
4418  vars = SCIPvarGetMultaggrVars(var);
4419  scalars = SCIPvarGetMultaggrScalars(var);
4420  nvars = SCIPvarGetMultaggrNVars(var);
4421  for( i = 0; i < nvars; ++i )
4422  {
4423  SCIP_CALL( SCIPconflictAddBound(conflict, blkmem, set, stat, vars[i],
4424  (scalars[i] < 0.0 ? SCIPboundtypeOpposite(boundtype) : boundtype), bdchgidx) );
4425  }
4426 
4427  return SCIP_OKAY;
4428  }
4429  assert(SCIPvarIsActive(var));
4430 
4431  /* get bound change information */
4432  bdchginfo = SCIPvarGetBdchgInfo(var, boundtype, bdchgidx, FALSE);
4433 
4434  /* if bound of variable was not changed (this means it is still the global bound), we can ignore the conflicting
4435  * bound
4436  */
4437  if( bdchginfo == NULL )
4438  return SCIP_OKAY;
4439 
4440  assert(SCIPbdchgidxIsEarlier(SCIPbdchginfoGetIdx(bdchginfo), bdchgidx));
4441 
4442  SCIP_CALL( conflictAddBound(conflict, blkmem, set, stat, var, boundtype, bdchginfo, SCIPbdchginfoGetNewbound(bdchginfo)) );
4443 
4444  return SCIP_OKAY;
4445 }
4446 
4447 /** adds variable's bound to conflict candidate queue */
4449  SCIP_CONFLICT* conflict, /**< conflict analysis data */
4450  BMS_BLKMEM* blkmem, /**< block memory */
4451  SCIP_SET* set, /**< global SCIP settings */
4452  SCIP_STAT* stat, /**< dynamic problem statistics */
4453  SCIP_VAR* var, /**< problem variable */
4454  SCIP_BOUNDTYPE boundtype, /**< type of bound that was changed: lower or upper bound */
4455  SCIP_BDCHGIDX* bdchgidx, /**< bound change index (time stamp of bound change), or NULL for current time */
4456  SCIP_Real relaxedbd /**< the relaxed bound */
4457  )
4458 {
4459  SCIP_BDCHGINFO* bdchginfo;
4460  int nbdchgs;
4461 
4462  assert(conflict != NULL);
4463  assert(stat != NULL);
4464  assert(var != NULL);
4465 
4466  if( !SCIPvarIsActive(var) )
4467  {
4468  /* convert bound to active problem variable */
4469  SCIP_CALL( convertToActiveVar(&var, set, &boundtype, &relaxedbd) );
4470 
4471  /* we can ignore fixed variables */
4473  return SCIP_OKAY;
4474 
4475  /* if the variable is multi-aggregated, add the bounds of all aggregation variables */
4477  {
4478  SCIPsetDebugMsg(set, "ignoring relaxed bound information since variable <%s> is multi-aggregated active\n", SCIPvarGetName(var));
4479 
4480  SCIP_CALL( SCIPconflictAddBound(conflict, blkmem, set, stat, var, boundtype, bdchgidx) );
4481 
4482  return SCIP_OKAY;
4483  }
4484  }
4485  assert(SCIPvarIsActive(var));
4486 
4487  /* get bound change information */
4488  bdchginfo = SCIPvarGetBdchgInfo(var, boundtype, bdchgidx, FALSE);
4489 
4490  /* if bound of variable was not changed (this means it is still the global bound), we can ignore the conflicting
4491  * bound
4492  */
4493  if( bdchginfo == NULL )
4494  return SCIP_OKAY;
4495 
4496  /* check that the bound change info is not a temporary one */
4497  assert(SCIPbdchgidxGetPos(&bdchginfo->bdchgidx) >= 0);
4498 
4499  /* get the position of the bound change information within the bound change array of the variable */
4500  nbdchgs = (int) bdchginfo->pos;
4501  assert(nbdchgs >= 0);
4502 
4503  /* if the relaxed bound should be ignored, set the relaxed bound to the bound given by the bdchgidx; that ensures
4504  * that the loop(s) below will be skipped
4505  */
4506  if( set->conf_ignorerelaxedbd )
4507  relaxedbd = SCIPbdchginfoGetNewbound(bdchginfo);
4508 
4509  /* search for the bound change information which includes the relaxed bound */
4510  if( boundtype == SCIP_BOUNDTYPE_LOWER )
4511  {
4512  SCIP_Real newbound;
4513 
4514  /* adjust relaxed lower bound w.r.t. variable type */
4515  SCIPvarAdjustLb(var, set, &relaxedbd);
4516 
4517  /* due to numericis we compare the relaxed lower bound to the one present at the particular time point and take
4518  * the better one
4519  */
4520  newbound = SCIPbdchginfoGetNewbound(bdchginfo);
4521  relaxedbd = MIN(relaxedbd, newbound);
4522 
4523  /* check if relaxed lower bound is smaller or equal to global lower bound; if so we can ignore the conflicting
4524  * bound
4525  */
4526  if( SCIPsetIsLE(set, relaxedbd, SCIPvarGetLbGlobal(var)) )
4527  return SCIP_OKAY;
4528 
4529  while( nbdchgs > 0 )
4530  {
4531  assert(SCIPsetIsLE(set, relaxedbd, SCIPbdchginfoGetNewbound(bdchginfo)));
4532 
4533  /* check if the old lower bound is greater than or equal to relaxed lower bound; if not we found the bound
4534  * change info which we need to report
4535  */
4536  if( SCIPsetIsGT(set, relaxedbd, SCIPbdchginfoGetOldbound(bdchginfo)) )
4537  break;
4538 
4539  bdchginfo = SCIPvarGetBdchgInfoLb(var, nbdchgs-1);
4540 
4541  SCIPsetDebugMsg(set, "lower bound change %d oldbd=%.15g, newbd=%.15g, depth=%d, pos=%d, redundant=%u\n",
4542  nbdchgs, SCIPbdchginfoGetOldbound(bdchginfo), SCIPbdchginfoGetNewbound(bdchginfo),
4543  SCIPbdchginfoGetDepth(bdchginfo), SCIPbdchginfoGetPos(bdchginfo),
4544  SCIPbdchginfoIsRedundant(bdchginfo));
4545 
4546  /* if bound change is redundant (this means it now a global bound), we can ignore the conflicting bound */
4547  if( SCIPbdchginfoIsRedundant(bdchginfo) )
4548  return SCIP_OKAY;
4549 
4550  nbdchgs--;
4551  }
4552  assert(SCIPsetIsGT(set, relaxedbd, SCIPbdchginfoGetOldbound(bdchginfo)));
4553  }
4554  else
4555  {
4556  SCIP_Real newbound;
4557 
4558  assert(boundtype == SCIP_BOUNDTYPE_UPPER);
4559 
4560  /* adjust relaxed upper bound w.r.t. variable type */
4561  SCIPvarAdjustUb(var, set, &relaxedbd);
4562 
4563  /* due to numericis we compare the relaxed upper bound to the one present at the particular time point and take
4564  * the better one
4565  */
4566  newbound = SCIPbdchginfoGetNewbound(bdchginfo);
4567  relaxedbd = MAX(relaxedbd, newbound);
4568 
4569  /* check if relaxed upper bound is greater or equal to global upper bound; if so we can ignore the conflicting
4570  * bound
4571  */
4572  if( SCIPsetIsGE(set, relaxedbd, SCIPvarGetUbGlobal(var)) )
4573  return SCIP_OKAY;
4574 
4575  while( nbdchgs > 0 )
4576  {
4577  assert(SCIPsetIsGE(set, relaxedbd, SCIPbdchginfoGetNewbound(bdchginfo)));
4578 
4579  /* check if the old upper bound is smaller than or equal to the relaxed upper bound; if not we found the
4580  * bound change info which we need to report
4581  */
4582  if( SCIPsetIsLT(set, relaxedbd, SCIPbdchginfoGetOldbound(bdchginfo)) )
4583  break;
4584 
4585  bdchginfo = SCIPvarGetBdchgInfoUb(var, nbdchgs-1);
4586 
4587  SCIPsetDebugMsg(set, "upper bound change %d oldbd=%.15g, newbd=%.15g, depth=%d, pos=%d, redundant=%u\n",
4588  nbdchgs, SCIPbdchginfoGetOldbound(bdchginfo), SCIPbdchginfoGetNewbound(bdchginfo),
4589  SCIPbdchginfoGetDepth(bdchginfo), SCIPbdchginfoGetPos(bdchginfo),
4590  SCIPbdchginfoIsRedundant(bdchginfo));
4591 
4592  /* if bound change is redundant (this means it now a global bound), we can ignore the conflicting bound */
4593  if( SCIPbdchginfoIsRedundant(bdchginfo) )
4594  return SCIP_OKAY;
4595 
4596  nbdchgs--;
4597  }
4598  assert(SCIPsetIsLT(set, relaxedbd, SCIPbdchginfoGetOldbound(bdchginfo)));
4599  }
4600 
4601  assert(SCIPbdchgidxIsEarlier(SCIPbdchginfoGetIdx(bdchginfo), bdchgidx));
4602 
4603  /* put bound change information into priority queue */
4604  SCIP_CALL( conflictAddBound(conflict, blkmem, set, stat, var, boundtype, bdchginfo, relaxedbd) );
4605 
4606  return SCIP_OKAY;
4607 }
4608 
4609 /** checks if the given variable is already part of the current conflict set or queued for resolving with the same or
4610  * even stronger bound
4611  */
4613  SCIP_CONFLICT* conflict, /**< conflict analysis data */
4614  SCIP_VAR* var, /**< problem variable */
4615  SCIP_SET* set, /**< global SCIP settings */
4616  SCIP_BOUNDTYPE boundtype, /**< type of bound for which the score should be increased */
4617  SCIP_BDCHGIDX* bdchgidx, /**< bound change index (time stamp of bound change), or NULL for current time */
4618  SCIP_Bool* used /**< pointer to store if the variable is already used */
4619  )
4620 {
4621  SCIP_Real newbound;
4622 
4623  /* convert bound to active problem variable */
4624  SCIP_CALL( convertToActiveVar(&var, set, &boundtype, NULL) );
4625 
4627  *used = FALSE;
4628  else
4629  {
4630  assert(SCIPvarIsActive(var));
4631  assert(var != NULL);
4632 
4633  switch( boundtype )
4634  {
4635  case SCIP_BOUNDTYPE_LOWER:
4636 
4637  newbound = SCIPgetVarLbAtIndex(set->scip, var, bdchgidx, FALSE);
4638 
4639  if( var->conflictlbcount == conflict->count && var->conflictlb >= newbound )
4640  {
4641  SCIPsetDebugMsg(set, "already queued bound change <%s> >= %g\n", SCIPvarGetName(var), newbound);
4642  *used = TRUE;
4643  }
4644  else
4645  *used = FALSE;
4646  break;
4647  case SCIP_BOUNDTYPE_UPPER:
4648 
4649  newbound = SCIPgetVarUbAtIndex(set->scip, var, bdchgidx, FALSE);
4650 
4651  if( var->conflictubcount == conflict->count && var->conflictub <= newbound )
4652  {
4653  SCIPsetDebugMsg(set, "already queued bound change <%s> <= %g\n", SCIPvarGetName(var), newbound);
4654  *used = TRUE;
4655  }
4656  else
4657  *used = FALSE;
4658  break;
4659  default:
4660  SCIPerrorMessage("invalid bound type %d\n", boundtype);
4661  SCIPABORT();
4662  *used = FALSE; /*lint !e527*/
4663  }
4664  }
4665 
4666  return SCIP_OKAY;
4667 }
4668 
4669 /** returns the conflict lower bound if the variable is present in the current conflict set; otherwise the global lower
4670  * bound
4671  */
4673  SCIP_CONFLICT* conflict, /**< conflict analysis data */
4674  SCIP_VAR* var /**< problem variable */
4675  )
4676 {
4677  if( var->conflictlbcount == conflict->count )
4678  {
4679  assert(EPSGE(var->conflictlb, var->conflictrelaxedlb, 1e-09));
4680  return var->conflictrelaxedlb;
4681  }
4682 
4683  return SCIPvarGetLbGlobal(var);
4684 }
4685 
4686 /** returns the conflict upper bound if the variable is present in the current conflict set; otherwise the global upper
4687  * bound
4688  */
4690  SCIP_CONFLICT* conflict, /**< conflict analysis data */
4691  SCIP_VAR* var /**< problem variable */
4692  )
4693 {
4694  if( var->conflictubcount == conflict->count )
4695  {
4696  assert(EPSLE(var->conflictub, var->conflictrelaxedub, 1e-09));
4697  return var->conflictrelaxedub;
4698  }
4699 
4700  return SCIPvarGetUbGlobal(var);
4701 }
4702 
4703 /** removes and returns next conflict analysis candidate from the candidate queue */
4704 static
4706  SCIP_CONFLICT* conflict /**< conflict analysis data */
4707  )
4708 {
4709  SCIP_BDCHGINFO* bdchginfo;
4710  SCIP_VAR* var;
4711 
4712  assert(conflict != NULL);
4713 
4714  if( SCIPpqueueNElems(conflict->forcedbdchgqueue) > 0 )
4715  bdchginfo = (SCIP_BDCHGINFO*)(SCIPpqueueRemove(conflict->forcedbdchgqueue));
4716  else
4717  bdchginfo = (SCIP_BDCHGINFO*)(SCIPpqueueRemove(conflict->bdchgqueue));
4718 
4719  assert(!SCIPbdchginfoIsRedundant(bdchginfo));
4720 
4721  /* if we have a candidate this one should be valid for the current conflict analysis */
4722  assert(!bdchginfoIsInvalid(conflict, bdchginfo));
4723 
4724  /* mark the bound change to be no longer in the conflict (it will be either added again to the conflict set or
4725  * replaced by resolving, which might add a weaker change on the same bound to the queue)
4726  */
4727  var = SCIPbdchginfoGetVar(bdchginfo);
4729  {
4730  var->conflictlbcount = 0;
4732  }
4733  else
4734  {
4735  assert(SCIPbdchginfoGetBoundtype(bdchginfo) == SCIP_BOUNDTYPE_UPPER);
4736  var->conflictubcount = 0;
4738  }
4739 
4740 #ifdef SCIP_CONFGRAPH
4741  confgraphSetCurrentBdchg(bdchginfo);
4742 #endif
4743 
4744  return bdchginfo;
4745 }
4746 
4747 /** returns next conflict analysis candidate from the candidate queue without removing it */
4748 static
4750  SCIP_CONFLICT* conflict /**< conflict analysis data */
4751  )
4752 {
4753  SCIP_BDCHGINFO* bdchginfo;
4754 
4755  assert(conflict != NULL);
4756 
4757  if( SCIPpqueueNElems(conflict->forcedbdchgqueue) > 0 )
4758  {
4759  /* get next potetioal candidate */
4760  bdchginfo = (SCIP_BDCHGINFO*)(SCIPpqueueFirst(conflict->forcedbdchgqueue));
4761 
4762  /* check if this candidate is valid */
4763  if( bdchginfoIsInvalid(conflict, bdchginfo) )
4764  {
4765  SCIPdebugMessage("bound change info [%d:<%s> %s %g] is invaild -> pop it from the force queue\n", SCIPbdchginfoGetDepth(bdchginfo),
4766  SCIPvarGetName(SCIPbdchginfoGetVar(bdchginfo)),
4767  SCIPbdchginfoGetBoundtype(bdchginfo) == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=",
4768  SCIPbdchginfoGetNewbound(bdchginfo));
4769 
4770  /* pop the invalid bound change info from the queue */
4771  (void)(SCIPpqueueRemove(conflict->forcedbdchgqueue));
4772 
4773  /* call method recursively to get next conflict analysis candidate */
4774  bdchginfo = conflictFirstCand(conflict);
4775  }
4776  }
4777  else
4778  {
4779  bdchginfo = (SCIP_BDCHGINFO*)(SCIPpqueueFirst(conflict->bdchgqueue));
4780 
4781  /* check if this candidate is valid */
4782  if( bdchginfo != NULL && bdchginfoIsInvalid(conflict, bdchginfo) )
4783  {
4784  SCIPdebugMessage("bound change info [%d:<%s> %s %g] is invaild -> pop it from the queue\n", SCIPbdchginfoGetDepth(bdchginfo),
4785  SCIPvarGetName(SCIPbdchginfoGetVar(bdchginfo)),
4786  SCIPbdchginfoGetBoundtype(bdchginfo) == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=",
4787  SCIPbdchginfoGetNewbound(bdchginfo));
4788 
4789  /* pop the invalid bound change info from the queue */
4790  (void)(SCIPpqueueRemove(conflict->bdchgqueue));
4791 
4792  /* call method recursively to get next conflict analysis candidate */
4793  bdchginfo = conflictFirstCand(conflict);
4794  }
4795  }
4796  assert(bdchginfo == NULL || !SCIPbdchginfoIsRedundant(bdchginfo));
4797 
4798  return bdchginfo;
4799 }
4800 
4801 /** adds the current conflict set (extended by all remaining bound changes in the queue) to the pool of conflict sets */
4802 static
4804  SCIP_CONFLICT* conflict, /**< conflict analysis data */
4805  BMS_BLKMEM* blkmem, /**< block memory of transformed problem */
4806  SCIP_SET* set, /**< global SCIP settings */
4807  SCIP_STAT* stat, /**< dynamic problem statistics */
4808  SCIP_TREE* tree, /**< branch and bound tree */
4809  int validdepth, /**< minimal depth level at which the conflict set is valid */
4810  SCIP_Bool diving, /**< are we in strong branching or diving mode? */
4811  SCIP_Bool repropagate, /**< should the constraint trigger a repropagation? */
4812  SCIP_Bool* success, /**< pointer to store whether the conflict set is valid */
4813  int* nliterals /**< pointer to store the number of literals in the generated conflictset */
4814  )
4815 {
4816  SCIP_CONFLICTSET* conflictset;
4817  SCIP_BDCHGINFO** bdchginfos;
4818  int nbdchginfos;
4819  int currentdepth;
4820  int focusdepth;
4821 
4822  assert(conflict != NULL);
4823  assert(conflict->conflictset != NULL);
4824  assert(set != NULL);
4825  assert(stat != NULL);
4826  assert(tree != NULL);
4827  assert(success != NULL);
4828  assert(nliterals != NULL);
4829  assert(SCIPpqueueNElems(conflict->forcedbdchgqueue) == 0);
4830 
4831  *success = FALSE;
4832  *nliterals = 0;
4833 
4834  /* check, whether local conflicts are allowed */
4835  validdepth = MAX(validdepth, conflict->conflictset->validdepth);
4836  if( !set->conf_allowlocal && validdepth > 0 )
4837  return SCIP_OKAY;
4838 
4839  focusdepth = SCIPtreeGetFocusDepth(tree);
4840  currentdepth = SCIPtreeGetCurrentDepth(tree);
4841  assert(currentdepth == tree->pathlen-1);
4842  assert(focusdepth <= currentdepth);
4843  assert(0 <= conflict->conflictset->validdepth && conflict->conflictset->validdepth <= currentdepth);
4844  assert(0 <= validdepth && validdepth <= currentdepth);
4845 
4846  /* get the elements of the bound change queue */
4847  bdchginfos = (SCIP_BDCHGINFO**)SCIPpqueueElems(conflict->bdchgqueue);
4848  nbdchginfos = SCIPpqueueNElems(conflict->bdchgqueue);
4849 
4850  /* create a copy of the current conflict set, allocating memory for the additional elements of the queue */
4851  SCIP_CALL( conflictsetCopy(&conflictset, blkmem, conflict->conflictset, nbdchginfos) );
4852  conflictset->validdepth = validdepth;
4853  conflictset->repropagate = repropagate;
4854 
4855  /* add the valid queue elements to the conflict set */
4856  SCIPsetDebugMsg(set, "adding %d variables from the queue as temporary conflict variables\n", nbdchginfos);
4857  SCIP_CALL( conflictsetAddBounds(conflict, conflictset, blkmem, set, bdchginfos, nbdchginfos) );
4858 
4859  /* calculate the depth, at which the conflictset should be inserted */
4860  SCIP_CALL( conflictsetCalcInsertDepth(conflictset, set, tree) );
4861  assert(conflictset->validdepth <= conflictset->insertdepth && conflictset->insertdepth <= currentdepth);
4862  SCIPsetDebugMsg(set, " -> conflict with %d literals found at depth %d is active in depth %d and valid in depth %d\n",
4863  conflictset->nbdchginfos, currentdepth, conflictset->insertdepth, conflictset->validdepth);
4864 
4865  /* if all branching variables are in the conflict set, the conflict set is of no use;
4866  * don't use conflict sets that are only valid in the probing path but not in the problem tree
4867  */
4868  if( (diving || conflictset->insertdepth < currentdepth) && conflictset->insertdepth <= focusdepth )
4869  {
4870  /* if the conflict should not be located only in the subtree where it is useful, put it to its valid depth level */
4871  if( !set->conf_settlelocal )
4872  conflictset->insertdepth = conflictset->validdepth;
4873 
4874  *nliterals = conflictset->nbdchginfos;
4875  SCIPsetDebugMsg(set, " -> final conflict set has %d literals\n", *nliterals);
4876 
4877  /* check conflict set on debugging solution */
4878  SCIP_CALL( SCIPdebugCheckConflict(blkmem, set, tree->path[validdepth], \
4879  conflictset->bdchginfos, conflictset->relaxedbds, conflictset->nbdchginfos) ); /*lint !e506 !e774*/
4880 
4881  /* move conflictset to the conflictset storage */
4882  SCIP_CALL( conflictInsertConflictset(conflict, blkmem, set, &conflictset) );
4883  *success = TRUE;
4884  }
4885  else
4886  {
4887  /* free the temporary conflict set */
4888  conflictsetFree(&conflictset, blkmem);
4889  }
4890 
4891  return SCIP_OKAY;
4892 }
4893 
4894 /** tries to resolve given bound change
4895  * - resolutions on local constraints are only applied, if the constraint is valid at the
4896  * current minimal valid depth level, because this depth level is the topmost level to add the conflict
4897  * constraint to anyways
4898  *
4899  * @note it is sufficient to explain the relaxed bound change
4900  */
4901 static
4903  SCIP_CONFLICT* conflict, /**< conflict analysis data */
4904  SCIP_SET* set, /**< global SCIP settings */
4905  SCIP_BDCHGINFO* bdchginfo, /**< bound change to resolve */
4906  SCIP_Real relaxedbd, /**< the relaxed bound */
4907  int validdepth, /**< minimal depth level at which the conflict is valid */
4908  SCIP_Bool* resolved /**< pointer to store whether the bound change was resolved */
4909  )
4910 {
4911  SCIP_VAR* actvar;
4912  SCIP_CONS* infercons;
4913  SCIP_PROP* inferprop;
4914  SCIP_RESULT result;
4915 
4916 #ifndef NDEBUG
4917  int nforcedbdchgqueue;
4918  int nbdchgqueue;
4919 
4920  /* store the current size of the conflict queues */
4921  assert(conflict != NULL);
4922  nforcedbdchgqueue = SCIPpqueueNElems(conflict->forcedbdchgqueue);
4923  nbdchgqueue = SCIPpqueueNElems(conflict->bdchgqueue);
4924 #else
4925  assert(conflict != NULL);
4926 #endif
4927 
4928  assert(resolved != NULL);
4929  assert(!SCIPbdchginfoIsRedundant(bdchginfo));
4930 
4931  *resolved = FALSE;
4932 
4933  actvar = SCIPbdchginfoGetVar(bdchginfo);
4934  assert(actvar != NULL);
4935  assert(SCIPvarIsActive(actvar));
4936 
4937 #ifdef SCIP_DEBUG
4938  {
4939  int i;
4940  SCIPsetDebugMsg(set, "processing next conflicting bound (depth: %d, valid depth: %d, bdchgtype: %s [%s], vartype: %d): [<%s> %s %g(%g)]\n",
4941  SCIPbdchginfoGetDepth(bdchginfo), validdepth,
4942  SCIPbdchginfoGetChgtype(bdchginfo) == SCIP_BOUNDCHGTYPE_BRANCHING ? "branch"
4943  : SCIPbdchginfoGetChgtype(bdchginfo) == SCIP_BOUNDCHGTYPE_CONSINFER ? "cons" : "prop",
4947  : SCIPbdchginfoGetInferProp(bdchginfo) == NULL ? "-"
4949  SCIPvarGetType(actvar), SCIPvarGetName(actvar),
4950  SCIPbdchginfoGetBoundtype(bdchginfo) == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=",
4951  SCIPbdchginfoGetNewbound(bdchginfo), relaxedbd);
4952  SCIPsetDebugMsg(set, " - conflict set :");
4953 
4954  for( i = 0; i < conflict->conflictset->nbdchginfos; ++i )
4955  {
4956  SCIPsetDebugMsgPrint(set, " [%d:<%s> %s %g(%g)]", SCIPbdchginfoGetDepth(conflict->conflictset->bdchginfos[i]),
4958  SCIPbdchginfoGetBoundtype(conflict->conflictset->bdchginfos[i]) == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=",
4959  SCIPbdchginfoGetNewbound(conflict->conflictset->bdchginfos[i]), conflict->conflictset->relaxedbds[i]);
4960  }
4961  SCIPsetDebugMsgPrint(set, "\n");
4962  SCIPsetDebugMsg(set, " - forced candidates :");
4963 
4964  for( i = 0; i < SCIPpqueueNElems(conflict->forcedbdchgqueue); ++i )
4965  {
4967  SCIPsetDebugMsgPrint(set, " [%d:<%s> %s %g(%g)]", SCIPbdchginfoGetDepth(info), SCIPvarGetName(SCIPbdchginfoGetVar(info)),
4968  bdchginfoIsInvalid(conflict, info) ? "<!>" : SCIPbdchginfoGetBoundtype(info) == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=",
4970  }
4971  SCIPsetDebugMsgPrint(set, "\n");
4972  SCIPsetDebugMsg(set, " - optional candidates:");
4973 
4974  for( i = 0; i < SCIPpqueueNElems(conflict->bdchgqueue); ++i )
4975  {
4976  SCIP_BDCHGINFO* info = (SCIP_BDCHGINFO*)(SCIPpqueueElems(conflict->bdchgqueue)[i]);
4977  SCIPsetDebugMsgPrint(set, " [%d:<%s> %s %g(%g)]", SCIPbdchginfoGetDepth(info), SCIPvarGetName(SCIPbdchginfoGetVar(info)),
4978  bdchginfoIsInvalid(conflict, info) ? "<!>" : SCIPbdchginfoGetBoundtype(info) == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=",
4980  }
4981  SCIPsetDebugMsgPrint(set, "\n");
4982  }
4983 #endif
4984 
4985  /* check, if the bound change can and should be resolved:
4986  * - resolutions on local constraints should only be applied, if the constraint is valid at the
4987  * current minimal valid depth level (which is initialized with the valid depth level of the initial
4988  * conflict set), because this depth level is the topmost level to add the conflict constraint to anyways
4989  */
4990  switch( SCIPbdchginfoGetChgtype(bdchginfo) )
4991  {
4993  infercons = SCIPbdchginfoGetInferCons(bdchginfo);
4994  assert(infercons != NULL);
4995 
4996  if( SCIPconsIsGlobal(infercons) || SCIPconsGetValidDepth(infercons) <= validdepth )
4997  {
4998  SCIP_VAR* infervar;
4999  int inferinfo;
5000  SCIP_BOUNDTYPE inferboundtype;
5001  SCIP_BDCHGIDX* bdchgidx;
5002 
5003  /* resolve bound change by asking the constraint that infered the bound to put all bounds that were
5004  * the reasons for the conflicting bound change on the priority queue
5005  */
5006  infervar = SCIPbdchginfoGetInferVar(bdchginfo);
5007  inferinfo = SCIPbdchginfoGetInferInfo(bdchginfo);
5008  inferboundtype = SCIPbdchginfoGetInferBoundtype(bdchginfo);
5009  bdchgidx = SCIPbdchginfoGetIdx(bdchginfo);
5010  assert(infervar != NULL);
5011 
5012  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",
5013  SCIPvarGetName(actvar),
5014  SCIPbdchginfoGetBoundtype(bdchginfo) == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=",
5015  SCIPbdchginfoGetNewbound(bdchginfo), relaxedbd,
5016  SCIPvarGetStatus(actvar), SCIPvarGetType(actvar),
5017  SCIPbdchginfoGetDepth(bdchginfo), SCIPbdchginfoGetPos(bdchginfo),
5018  SCIPvarGetName(infervar),
5019  inferboundtype == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=",
5020  SCIPgetVarBdAtIndex(set->scip, infervar, inferboundtype, bdchgidx, TRUE),
5021  SCIPconsGetName(infercons),
5022  SCIPconsIsGlobal(infercons) ? "global" : "local",
5023  inferinfo);
5024 
5025  /* in case the inference variables is not an active variables, we need to transform the relaxed bound */
5026  if( actvar != infervar )
5027  {
5028  SCIP_VAR* var;
5029  SCIP_Real scalar;
5030  SCIP_Real constant;
5031 
5032  assert(SCIPvarGetStatus(infervar) == SCIP_VARSTATUS_AGGREGATED
5034  || (SCIPvarGetStatus(infervar) == SCIP_VARSTATUS_MULTAGGR && SCIPvarGetMultaggrNVars(infervar) == 1));
5035 
5036  scalar = 1.0;
5037  constant = 0.0;
5038 
5039  var = infervar;
5040 
5041  /* transform given varibale to active varibale */
5042  SCIP_CALL( SCIPvarGetProbvarSum(&var, set, &scalar, &constant) );
5043  assert(var == actvar);
5044 
5045  relaxedbd *= scalar;
5046  relaxedbd += constant;
5047  }
5048 
5049  SCIP_CALL( SCIPconsResolvePropagation(infercons, set, infervar, inferinfo, inferboundtype, bdchgidx, relaxedbd, &result) );
5050  *resolved = (result == SCIP_SUCCESS);
5051  }
5052  break;
5053 
5055  inferprop = SCIPbdchginfoGetInferProp(bdchginfo);
5056  if( inferprop != NULL )
5057  {
5058  SCIP_VAR* infervar;
5059  int inferinfo;
5060  SCIP_BOUNDTYPE inferboundtype;
5061  SCIP_BDCHGIDX* bdchgidx;
5062 
5063  /* resolve bound change by asking the propagator that infered the bound to put all bounds that were
5064  * the reasons for the conflicting bound change on the priority queue
5065  */
5066  infervar = SCIPbdchginfoGetInferVar(bdchginfo);
5067  inferinfo = SCIPbdchginfoGetInferInfo(bdchginfo);
5068  inferboundtype = SCIPbdchginfoGetInferBoundtype(bdchginfo);
5069  bdchgidx = SCIPbdchginfoGetIdx(bdchginfo);
5070  assert(infervar != NULL);
5071 
5072  SCIPsetDebugMsg(set, "resolving bound <%s> %s %g(%g) [status:%d, depth:%d, pos:%d]: <%s> %s %g [prop:<%s>, info:%d]\n",
5073  SCIPvarGetName(actvar),
5074  SCIPbdchginfoGetBoundtype(bdchginfo) == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=",
5075  SCIPbdchginfoGetNewbound(bdchginfo), relaxedbd,
5076  SCIPvarGetStatus(actvar), SCIPbdchginfoGetDepth(bdchginfo), SCIPbdchginfoGetPos(bdchginfo),
5077  SCIPvarGetName(infervar),
5078  inferboundtype == SCIP_BOUNDTYPE_LOWER ? ">=" : "<=",
5079  SCIPgetVarBdAtIndex(set->scip, infervar, inferboundtype, bdchgidx, TRUE),
5080  SCIPpropGetName(inferprop), inferinfo);
5081 
5082  SCIP_CALL( SCIPpropResolvePropagation(inferprop, set, infervar, inferinfo, inferboundtype, bdchgidx, relaxedbd, &result) );
5083  *resolved = (result == SCIP_SUCCESS);
5084  }
5085  break;
5086 
5088  assert(!(*resolved));
5089  break;
5090 
5091  default:
5092  SCIPerrorMessage("invalid bound change type <%d>\n", SCIPbdchginfoGetChgtype(bdchginfo));
5093  return SCIP_INVALIDDATA;
5094  }
5095 
5096  SCIPsetDebugMsg(set, "resolving status: %u\n", *resolved);
5097 
5098 #ifndef NDEBUG
5099  /* subtract the size of the conflicq queues */
5100  nforcedbdchgqueue -= SCIPpqueueNElems(conflict->forcedbdchgqueue);
5101  nbdchgqueue -= SCIPpqueueNElems(conflict->bdchgqueue);
5102 
5103  /* in case the bound change was not resolved, the conflict queues should have the same size (contents) */
5104  assert((*resolved) || (nforcedbdchgqueue == 0 && nbdchgqueue == 0));
5105 #endif
5106 
5107  return SCIP_OKAY;
5108 }
5109 
5110 /** if only one conflicting bound change of the last depth level was used, and if this can be resolved,
5111  * creates GRASP-like reconvergence conflict constraints in the conflict graph up to the branching variable of this
5112  * depth level
5113  */
5114 static
5116  SCIP_CONFLICT* conflict, /**< conflict analysis data */
5117  BMS_BLKMEM* blkmem, /**< block memory of transformed problem */
5118  SCIP_SET* set, /**< global SCIP settings */
5119  SCIP_STAT* stat, /**< problem statistics */
5120  SCIP_PROB* prob, /**< problem data */
5121  SCIP_TREE* tree, /**< branch and bound tree */
5122  SCIP_Bool diving, /**< are we in strong branching or diving mode? */
5123  int validdepth, /**< minimal depth level at which the initial conflict set is valid */
5124  SCIP_BDCHGINFO* firstuip, /**< first UIP of conflict graph */
5125  int* nreconvconss, /**< pointer to store the number of generated reconvergence constraints */
5126  int* nreconvliterals /**< pointer to store the number of literals generated reconvergence constraints */
5127  )
5128 {
5129  SCIP_BDCHGINFO* uip;
5130  SCIP_CONFTYPE conftype;
5131  SCIP_Bool usescutoffbound;
5132  int firstuipdepth;
5133  int focusdepth;
5134  int currentdepth;
5135  int maxvaliddepth;
5136 
5137  assert(conflict != NULL);
5138  assert(firstuip != NULL);
5139  assert(nreconvconss != NULL);
5140  assert(nreconvliterals != NULL);
5141  assert(!SCIPbdchginfoIsRedundant(firstuip));
5142 
5143  focusdepth = SCIPtreeGetFocusDepth(tree);
5144  currentdepth = SCIPtreeGetCurrentDepth(tree);
5145  assert(currentdepth == tree->pathlen-1);
5146  assert(focusdepth <= currentdepth);
5147 
5148  /* check, whether local constraints are allowed; however, don't generate reconvergence constraints that are only valid
5149  * in the probing path and not in the problem tree (i.e. that exceed the focusdepth)
5150  */
5151  maxvaliddepth = (set->conf_allowlocal ? MIN(currentdepth-1, focusdepth) : 0);
5152  if( validdepth > maxvaliddepth )
5153  return SCIP_OKAY;
5154 
5155  firstuipdepth = SCIPbdchginfoGetDepth(firstuip);
5156 
5157  conftype = conflict->conflictset->conflicttype;
5158  usescutoffbound = conflict->conflictset->usescutoffbound;
5159 
5160  /* for each succeeding UIP pair of the last depth level, create one reconvergence constraint */
5161  uip = firstuip;
5162  while( uip != NULL && SCIPbdchginfoGetDepth(uip) == SCIPbdchginfoGetDepth(firstuip) && bdchginfoIsResolvable(uip) )
5163  {
5164  SCIP_BDCHGINFO* oppositeuip;
5165  SCIP_BDCHGINFO* bdchginfo;
5166  SCIP_BDCHGINFO* nextuip;
5167  SCIP_VAR* uipvar;
5168  SCIP_Real oppositeuipbound;
5169  SCIP_BOUNDTYPE oppositeuipboundtype;
5170  int nresolutions;
5171 
5172  assert(!SCIPbdchginfoIsRedundant(uip));
5173 
5174  SCIPsetDebugMsg(set, "creating reconvergence constraint for UIP <%s> %s %g in depth %d pos %d\n",
5177 
5178  /* initialize conflict data */
5179  SCIP_CALL( SCIPconflictInit(conflict, set, stat, prob, conftype, usescutoffbound) );
5180 
5181  conflict->conflictset->conflicttype = conftype;
5182  conflict->conflictset->usescutoffbound = usescutoffbound;
5183 
5184  /* create a temporary bound change information for the negation of the UIP's bound change;
5185  * this bound change information is freed in the SCIPconflictFlushConss() call;
5186  * for reconvergence constraints for continuous variables we can only use the "negation" !(x <= u) == (x >= u);
5187  * during conflict analysis, we treat a continuous bound "x >= u" in the conflict set as "x > u", and in the
5188  * generated constraint this is negated again to "x <= u" which is correct.
5189  */
5190  uipvar = SCIPbdchginfoGetVar(uip);
5191  oppositeuipboundtype = SCIPboundtypeOpposite(SCIPbdchginfoGetBoundtype(uip));
5192  oppositeuipbound = SCIPbdchginfoGetNewbound(uip);
5193  if( SCIPvarIsIntegral(uipvar) )
5194  {
5195  assert(SCIPsetIsIntegral(set, oppositeuipbound));
5196  oppositeuipbound += (oppositeuipboundtype == SCIP_BOUNDTYPE_LOWER ? +1.0 : -1.0);
5197  }
5198  SCIP_CALL( conflictCreateTmpBdchginfo(conflict, blkmem, set, uipvar, oppositeuipboundtype, \
5199  oppositeuipboundtype == SCIP_BOUNDTYPE_LOWER ? SCIP_REAL_MIN : SCIP_REAL_MAX, oppositeuipbound, &oppositeuip) );
5200 
5201  /* put the negated UIP into the conflict set */
5202  SCIP_CALL( conflictAddConflictBound(conflict, blkmem, set, oppositeuip, oppositeuipbound) );
5203 
5204  /* put positive UIP into priority queue */
5205  SCIP_CALL( conflictQueueBound(conflict, set, uip, SCIPbdchginfoGetNewbound(uip) ) );
5206 
5207  /* resolve the queue until the next UIP is reached */
5208  bdchginfo = conflictFirstCand(conflict);
5209  nextuip = NULL;
5210  nresolutions = 0;
5211  while( bdchginfo != NULL && validdepth <= maxvaliddepth )
5212  {
5213  SCIP_BDCHGINFO* nextbdchginfo;
5214  SCIP_Real relaxedbd;
5215  SCIP_Bool forceresolve;
5216  int bdchgdepth;
5217 
5218  /* check if the next bound change must be resolved in every case */
5219  forceresolve = (SCIPpqueueNElems(conflict->forcedbdchgqueue) > 0);
5220 
5221  /* remove currently processed candidate and get next conflicting bound from the conflict candidate queue before
5222  * we remove the candidate we have to collect the relaxed bound since removing the candidate from the queue
5223  * invalidates the relaxed bound
5224  */
5225  assert(bdchginfo == conflictFirstCand(conflict));
5226  relaxedbd = SCIPbdchginfoGetRelaxedBound(bdchginfo);
5227  bdchginfo = conflictRemoveCand(conflict);
5228  nextbdchginfo = conflictFirstCand(conflict);
5229  bdchgdepth = SCIPbdchginfoGetDepth(bdchginfo);
5230  assert(bdchginfo != NULL);
5231  assert(!SCIPbdchginfoIsRedundant(bdchginfo));
5232  assert(nextbdchginfo == NULL || SCIPbdchginfoGetDepth(bdchginfo) >= SCIPbdchginfoGetDepth(nextbdchginfo)
5233  || forceresolve);
5234  assert(bdchgdepth <= firstuipdepth);
5235 
5236  /* bound changes that are higher in the tree than the valid depth of the conflict can be ignored;
5237  * multiple insertions of the same bound change can be ignored
5238  */
5239  if( bdchgdepth > validdepth && bdchginfo != nextbdchginfo )
5240  {
5241  SCIP_VAR* actvar;
5242  SCIP_Bool resolved;
5243 
5244  actvar = SCIPbdchginfoGetVar(bdchginfo);
5245  assert(actvar != NULL);
5246  assert(SCIPvarIsActive(actvar));
5247 
5248  /* check if we have to resolve the bound change in this depth level
5249  * - the starting uip has to be resolved
5250  * - a bound change should be resolved, if it is in the fuip's depth level and not the
5251  * next uip (i.e., if it is not the last bound change in the fuip's depth level)
5252  * - a forced bound change must be resolved in any case
5253  */
5254  resolved = FALSE;
5255  if( bdchginfo == uip
5256  || (bdchgdepth == firstuipdepth
5257  && nextbdchginfo != NULL
5258  && SCIPbdchginfoGetDepth(nextbdchginfo) == bdchgdepth)
5259  || forceresolve )
5260  {
5261  SCIP_CALL( conflictResolveBound(conflict, set, bdchginfo, relaxedbd, validdepth, &resolved) );
5262  }
5263 
5264  if( resolved )
5265  nresolutions++;
5266  else if( forceresolve )
5267  {
5268  /* variable cannot enter the conflict clause: we have to make the conflict clause local, s.t.
5269  * the unresolved bound change is active in the whole sub tree of the conflict clause
5270  */
5271  assert(bdchgdepth >= validdepth);
5272  validdepth = bdchgdepth;
5273 
5274  SCIPsetDebugMsg(set, "couldn't resolve forced bound change on <%s> -> new valid depth: %d\n",
5275  SCIPvarGetName(actvar), validdepth);
5276  }
5277  else if( bdchginfo != uip )
5278  {
5279  assert(conflict->conflictset != NULL);
5280  assert(conflict->conflictset->nbdchginfos >= 1); /* starting UIP is already member of the conflict set */
5281 
5282  /* if this is the first variable of the conflict set besides the current starting UIP, it is the next
5283  * UIP (or the first unresolvable bound change)
5284  */
5285  if( bdchgdepth == firstuipdepth && conflict->conflictset->nbdchginfos == 1 )
5286  {
5287  assert(nextuip == NULL);
5288  nextuip = bdchginfo;
5289  }
5290 
5291  /* put bound change into the conflict set */
5292  SCIP_CALL( conflictAddConflictBound(conflict, blkmem, set, bdchginfo, relaxedbd) );
5293  assert(conflict->conflictset->nbdchginfos >= 2);
5294  }
5295  else
5296  assert(conflictFirstCand(conflict) == NULL); /* the starting UIP was not resolved */
5297  }
5298 
5299  /* get next conflicting bound from the conflict candidate queue (this does not need to be nextbdchginfo, because
5300  * due to resolving the bound changes, a variable could be added to the queue which must be
5301  * resolved before nextbdchginfo)
5302  */
5303  bdchginfo = conflictFirstCand(conflict);
5304  }
5305  assert(nextuip != uip);
5306 
5307  /* if only one propagation was resolved, the reconvergence constraint is already member of the constraint set
5308  * (it is exactly the constraint that produced the propagation)
5309  */
5310  if( nextuip != NULL && nresolutions >= 2 && bdchginfo == NULL && validdepth <= maxvaliddepth )
5311  {
5312  int nlits;
5313  SCIP_Bool success;
5314 
5315  assert(SCIPbdchginfoGetDepth(nextuip) == SCIPbdchginfoGetDepth(uip));
5316 
5317  /* check conflict graph frontier on debugging solution */
5318  SCIP_CALL( SCIPdebugCheckConflictFrontier(blkmem, set, tree->path[validdepth], \
5319  bdchginfo, conflict->conflictset->bdchginfos, conflict->conflictset->relaxedbds, \
5320  conflict->conflictset->nbdchginfos, conflict->bdchgqueue, conflict->forcedbdchgqueue) ); /*lint !e506 !e774*/
5321 
5322  SCIPsetDebugMsg(set, "creating reconvergence constraint from UIP <%s> to UIP <%s> in depth %d with %d literals after %d resolutions\n",
5324  SCIPbdchginfoGetDepth(uip), conflict->conflictset->nbdchginfos, nresolutions);
5325 
5326  /* call the conflict handlers to create a conflict set */
5327  SCIP_CALL( conflictAddConflictset(conflict, blkmem, set, stat, tree, validdepth, diving, FALSE, &success, &nlits) );
5328  if( success )
5329  {
5330  (*nreconvconss)++;
5331  (*nreconvliterals) += nlits;
5332  }
5333  }
5334 
5335  /* clear the conflict candidate queue and the conflict set (to make sure, oppositeuip is not referenced anymore) */
5336  conflictClear(conflict);
5337 
5338  uip = nextuip;
5339  }
5340 
5341  conflict->conflictset->conflicttype = conftype;
5342  conflict->conflictset->usescutoffbound = usescutoffbound;
5343 
5344  return SCIP_OKAY;
5345 }
5346 
5347 /** analyzes conflicting bound changes that were added with calls to SCIPconflictAddBound() and
5348  * SCIPconflictAddRelaxedBound(), and on success, calls the conflict handlers to create a conflict constraint out of
5349  * the resulting conflict set; afterwards the conflict queue and the conflict set is cleared
5350  */
5351 static
5353  SCIP_CONFLICT* conflict, /**< conflict analysis data */
5354  BMS_BLKMEM* blkmem, /**< block memory of transformed problem */
5355  SCIP_SET* set, /**< global SCIP settings */
5356  SCIP_STAT* stat, /**< problem statistics */
5357  SCIP_PROB* prob, /**< problem data */
5358  SCIP_TREE* tree, /**< branch and bound tree */
5359  SCIP_Bool diving, /**< are we in strong branching or diving mode? */
5360  int validdepth, /**< minimal depth level at which the initial conflict set is valid */
5361  SCIP_Bool mustresolve, /**< should the conflict set only be used, if a resolution was applied? */
5362  int* nconss, /**< pointer to store the number of generated conflict constraints */
5363  int* nliterals, /**< pointer to store the number of literals in generated conflict constraints */
5364  int* nreconvconss, /**< pointer to store the number of generated reconvergence constraints */
5365  int* nreconvliterals /**< pointer to store the number of literals generated reconvergence constraints */
5366  )
5367 {
5368  SCIP_BDCHGINFO* bdchginfo;
5369  SCIP_BDCHGINFO** firstuips;
5370  SCIP_CONFTYPE conftype;
5371  int nfirstuips;
5372  int focusdepth;
5373  int currentdepth;
5374  int maxvaliddepth;
5375  int resolvedepth;
5376  int nresolutions;
5377  int lastconsnresolutions;
5378  int lastconsresoldepth;
5379 
5380  assert(conflict != NULL);
5381  assert(conflict->conflictset != NULL);
5382  assert(conflict->conflictset->nbdchginfos >= 0);
5383  assert(set != NULL);
5384  assert(stat != NULL);
5385  assert(0 <= validdepth && validdepth <= SCIPtreeGetCurrentDepth(tree));
5386  assert(nconss != NULL);
5387  assert(nliterals != NULL);
5388  assert(nreconvconss != NULL);
5389  assert(nreconvliterals != NULL);
5390 
5391  focusdepth = SCIPtreeGetFocusDepth(tree);
5392  currentdepth = SCIPtreeGetCurrentDepth(tree);
5393  assert(currentdepth == tree->pathlen-1);
5394  assert(focusdepth <= currentdepth);
5395 
5396  resolvedepth = ((set->conf_fuiplevels >= 0 && set->conf_fuiplevels <= currentdepth)
5397  ? currentdepth - set->conf_fuiplevels + 1 : 0);
5398  assert(0 <= resolvedepth && resolvedepth <= currentdepth + 1);
5399 
5400  /* if we must resolve at least one bound change, find the first UIP at least in the last depth level */
5401  if( mustresolve )
5402  resolvedepth = MIN(resolvedepth, currentdepth);
5403 
5404  SCIPsetDebugMsg(set, "analyzing conflict with %d+%d conflict candidates and starting conflict set of size %d in depth %d (resolvedepth=%d)\n",
5406  conflict->conflictset->nbdchginfos, currentdepth, resolvedepth);
5407 
5408  *nconss = 0;
5409  *nliterals = 0;
5410  *nreconvconss = 0;
5411  *nreconvliterals = 0;
5412 
5413  /* check, whether local conflicts are allowed; however, don't generate conflict constraints that are only valid in the
5414  * probing path and not in the problem tree (i.e. that exceed the focusdepth)
5415  */
5416  maxvaliddepth = (set->conf_allowlocal ? MIN(currentdepth-1, focusdepth) : 0);
5417  if( validdepth > maxvaliddepth )
5418  return SCIP_OKAY;
5419 
5420  /* allocate temporary memory for storing first UIPs (in each depth level, at most two bound changes can be flagged
5421  * as UIP, namely a binary and a non-binary bound change)
5422  */
5423  SCIP_CALL( SCIPsetAllocBufferArray(set, &firstuips, 2*(currentdepth+1)) ); /*lint !e647*/
5424 
5425  /* process all bound changes in the conflict candidate queue */
5426  nresolutions = 0;
5427  lastconsnresolutions = (mustresolve ? 0 : -1);
5428  lastconsresoldepth = (mustresolve ? currentdepth : INT_MAX);
5429  bdchginfo = conflictFirstCand(conflict);
5430  nfirstuips = 0;
5431 
5432  /* check if the initial reason on debugging solution */
5433  SCIP_CALL( SCIPdebugCheckConflictFrontier(blkmem, set, tree->path[validdepth], \
5434  NULL, conflict->conflictset->bdchginfos, conflict->conflictset->relaxedbds, conflict->conflictset->nbdchginfos, \
5435  conflict->bdchgqueue, conflict->forcedbdchgqueue) ); /*lint !e506 !e774*/
5436 
5437  while( bdchginfo != NULL && validdepth <= maxvaliddepth )
5438  {
5439  SCIP_BDCHGINFO* nextbdchginfo;
5440  SCIP_Real relaxedbd;
5441  SCIP_Bool forceresolve;
5442  int bdchgdepth;
5443 
5444  assert(!SCIPbdchginfoIsRedundant(bdchginfo));
5445 
5446  /* check if the next bound change must be resolved in every case */
5447  forceresolve = (SCIPpqueueNElems(conflict->forcedbdchgqueue) > 0);
5448 
5449  /* resolve next bound change in queue */
5450  bdchgdepth = SCIPbdchginfoGetDepth(bdchginfo);
5451  assert(0 <= bdchgdepth && bdchgdepth <= currentdepth);
5452  assert(SCIPvarIsActive(SCIPbdchginfoGetVar(bdchginfo)));
5453  assert(bdchgdepth < tree->pathlen);
5454  assert(tree->path[bdchgdepth] != NULL);
5455  assert(tree->path[bdchgdepth]->domchg != NULL);
5456  assert(SCIPbdchginfoGetPos(bdchginfo) < (int)tree->path[bdchgdepth]->domchg->domchgbound.nboundchgs);
5457  assert(tree->path[bdchgdepth]->domchg->domchgbound.boundchgs[SCIPbdchginfoGetPos(bdchginfo)].var
5458  == SCIPbdchginfoGetVar(bdchginfo));
5459  assert(tree->path[bdchgdepth]->domchg->domchgbound.boundchgs[SCIPbdchginfoGetPos(bdchginfo)].newbound
5460  == SCIPbdchginfoGetNewbound(bdchginfo)
5463  == SCIPbdchginfoGetNewbound(bdchginfo)); /*lint !e777*/
5464  assert((SCIP_BOUNDTYPE)tree->path[bdchgdepth]->domchg->domchgbound.boundchgs[SCIPbdchginfoGetPos(bdchginfo)].boundtype
5465  == SCIPbdchginfoGetBoundtype(bdchginfo));
5466 
5467  /* create intermediate conflict constraint */
5468  assert(nresolutions >= lastconsnresolutions);
5469  if( !forceresolve )
5470  {
5471  if( nresolutions == lastconsnresolutions )
5472  lastconsresoldepth = bdchgdepth; /* all intermediate depth levels consisted of only unresolved bound changes */
5473  else if( bdchgdepth < lastconsresoldepth && (set->conf_interconss == -1 || *nconss < set->conf_interconss) )
5474  {
5475  int nlits;
5476  SCIP_Bool success;
5477 
5478  /* call the conflict handlers to create a conflict set */
5479  SCIPsetDebugMsg(set, "creating intermediate conflictset after %d resolutions up to depth %d (valid at depth %d): %d conflict bounds, %d bounds in queue\n",
5480  nresolutions, bdchgdepth, validdepth, conflict->conflictset->nbdchginfos,
5481  SCIPpqueueNElems(conflict->bdchgqueue));
5482 
5483  SCIP_CALL( conflictAddConflictset(conflict, blkmem, set, stat, tree, validdepth, diving, TRUE, &success, &nlits) );
5484  lastconsnresolutions = nresolutions;
5485  lastconsresoldepth = bdchgdepth;
5486  if( success )
5487  {
5488  (*nconss)++;
5489  (*nliterals) += nlits;
5490  }
5491  }
5492  }
5493 
5494  /* remove currently processed candidate and get nex