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