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