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   	
25   	/**@file   prop_vbounds.c
26   	 * @ingroup DEFPLUGINS_PROP
27   	 * @brief  variable upper and lower bound propagator
28   	 * @author Stefan Heinz
29   	 * @author Jens Schulz
30   	 * @author Gerald Gamrath
31   	 * @author Marc Pfetsch
32   	 *
33   	 * This propagator uses global bound information provided by SCIP to deduce global and local bound changes.
34   	 * It can take into account
35   	 * - implications (bound change following from specific value of a binary variable)
36   	 * - cliques (set of binary variables, each with a corresponding value, of which at most one variable can get the value)
37   	 * - variable lower/upper bounds (bounds of arbitrary variables that depend linearly on the value of another variable)
38   	 *
39   	 * The propagator does not look at a variable in whole, but at one point in time only handles one specific bound (lower
40   	 * or upper) of a variable and deduces changes for lower or upper bounds of other variables. The concept is as follows:
41   	 *
42   	 * 1) Extract variable bound data
43   	 *
44   	 *    Implications and cliques are stored in a way such that given a variable and its new value, we can access all bound
45   	 *    changes that can be deduced from setting the variable to that value. However, for variable bounds, this currently
46   	 *    does not hold, they are only stored in the other direction, i.e. for a bound of a given variable, we have a list
47   	 *    of all other bounds of variables that directly influence the bound of the given variable and a linear function
48   	 *    describing how they do this.
49   	 *    For the propagation, we need the other direction, thus we store it in the propagator data when the branch-and-bound
50   	 *    solving process is about to begin.
51   	 *
52   	 * 2) Topological sorting of bounds of variable
53   	 *
54   	 *    We compute a topological order of the bounds of variables. This is needed to define an order in which we will
55   	 *    regard bounds of variables in the propagation process in order to avoid unneccessarily regarding the same variable
56   	 *    bound multiple times because it was changed in the meantime when propagating another bound of a variable.
57   	 *    Therefore, we implictly regard a directed graph, in which each node corresponds to a bound of a variable and there
58   	 *    exists a directed edge from one node to another, if the bound corresponding to the former node influences the
59   	 *    bound corresponding to the latter node. This is done by iteratively running a DFS until all nodes were visited.
60   	 *    Note that there might be cycles in the graph, which are randomly broken, so the order is only almost topological.
61   	 *
62   	 * 3) Collecting bound changes
63   	 *
64   	 *    For each bound of a variable, which can trigger bound changes of other variables, the propagator catches all
65   	 *    events informing about a global change of the bound or a local tightening of the bound. The event handler
66   	 *    then adds the bound of the variable to a priority queue, with the key in the priority queue corresponding
67   	 *    to the position of the bound in the topological sort.
68   	 *
69   	 * 4) Propagating Bounds
70   	 *
71   	 *    As long as there are bounds contained in the priority queue, the propagator pops one bound from the queue, which
72   	 *    is the one most at the beginning of the topological sort, so it should not be influenced by propagating other
73   	 *    bounds currently contained in the queue. Starting at this bound, all implication, clique, and variable bound
74   	 *    information is used to deduce tigther bounds for other variables and change the bounds, if a tighter one is found.
75   	 *    These bound changes trigger an event that will lead to adding the corresponding bound to the priority queue,
76   	 *    if it is not contained, yet. The process is iterated until the priority queue contains no more bounds.
77   	 *
78   	 * Additionally, the propagator analyzes the conflict/clique graph during presolving. It uses Tarjan's algorithm to
79   	 * search for strongly connected components, for each of which all variables can be aggregated to one. Additionally,
80   	 * it may detect invalid assignments of binary variables and fix the variable to the only possible value left.
81   	 */
82   	
83   	/*---+----1----+----2----+----3----+----4----+----5----+----6----+----7----+----8----+----9----+----0----+----1----+----2*/
84   	
85   	#include "blockmemshell/memory.h"
86   	#include "scip/prop_vbounds.h"
87   	#include "scip/pub_event.h"
88   	#include "scip/pub_implics.h"
89   	#include "scip/pub_message.h"
90   	#include "scip/pub_misc.h"
91   	#include "scip/pub_prop.h"
92   	#include "scip/pub_var.h"
93   	#include "scip/scip_conflict.h"
94   	#include "scip/scip_event.h"
95   	#include "scip/scip_general.h"
96   	#include "scip/scip_mem.h"
97   	#include "scip/scip_message.h"
98   	#include "scip/scip_numerics.h"
99   	#include "scip/scip_param.h"
100  	#include "scip/scip_prob.h"
101  	#include "scip/scip_prop.h"
102  	#include "scip/scip_tree.h"
103  	#include "scip/scip_var.h"
104  	#include <string.h>
105  	
106  	/**@name Propagator properties
107  	 *
108  	 * @{
109  	 */
110  	
111  	#define PROP_NAME              "vbounds"
112  	#define PROP_DESC              "propagates variable upper and lower bounds"
113  	#define PROP_TIMING             SCIP_PROPTIMING_BEFORELP | SCIP_PROPTIMING_AFTERLPLOOP
114  	#define PROP_PRIORITY           3000000 /**< propagator priority */
115  	#define PROP_FREQ                     1 /**< propagator frequency */
116  	#define PROP_DELAY                FALSE /**< should propagation method be delayed, if other propagators found reductions? */
117  	
118  	#define PROP_PRESOL_PRIORITY     -90000 /**< priority of the presolving method (>= 0: before, < 0: after constraint handlers); combined with presolvers */
119  	#define PROP_PRESOLTIMING       SCIP_PRESOLTIMING_MEDIUM | SCIP_PRESOLTIMING_EXHAUSTIVE
120  	#define PROP_PRESOL_MAXROUNDS        -1 /**< maximal number of presolving rounds the presolver participates in (-1: no
121  	                                         *   limit) */
122  	/**@} */
123  	
124  	/**@name Event handler properties
125  	 *
126  	 * @{
127  	 */
128  	
129  	#define EVENTHDLR_NAME         "vbounds"
130  	#define EVENTHDLR_DESC         "bound change event handler for for vbounds propagator"
131  	
132  	/**@} */
133  	
134  	/**@name Default parameter values
135  	 *
136  	 * @{
137  	 */
138  	
139  	#define DEFAULT_USEBDWIDENING      TRUE      /**< should bound widening be used to initialize conflict analysis? */
140  	#define DEFAULT_USEIMPLICS         FALSE     /**< should implications be propagated? */
141  	#define DEFAULT_USECLIQUES         FALSE     /**< should cliques be propagated? */
142  	#define DEFAULT_USEVBOUNDS         TRUE      /**< should variable bounds be propagated? */
143  	#define DEFAULT_DOTOPOSORT         TRUE      /**< should the bounds be topologically sorted in advance? */
144  	#define DEFAULT_SORTCLIQUES        FALSE     /**< should cliques be regarded for the topological sort? */
145  	#define DEFAULT_DETECTCYCLES       FALSE     /**< should cycles in the variable bound graph be identified? */
146  	#define DEFAULT_MINNEWCLIQUES      0.1       /**< minimum number of new cliques to trigger another clique table analysis */
147  	#define DEFAULT_MAXCLIQUESMEDIUM   50.0      /**< maximum number of cliques per variable to run clique table analysis in
148  	                                              *   medium presolving */
149  	#define DEFAULT_MAXCLIQUESEXHAUSTIVE 100.0   /**< maximum number of cliques per variable to run clique table analysis in
150  	                                              *   exhaustive presolving */
151  	
152  	/**@} */
153  	
154  	/**@name Propagator defines
155  	 *
156  	 * @{
157  	 *
158  	 * The propagator works on indices representing a bound of a variable. This index will be called bound index in the
159  	 * following. For a given active variable with problem index i (note that active variables have problem indices
160  	 * between 0 and nactivevariable - 1), the bound index of its lower bound is 2*i, the bound index of its upper
161  	 * bound is 2*i + 1. The other way around, a given bound index i corresponds to the variable with problem index
162  	 * i/2 (rounded down), and to the lower bound, if i is even, to the upper bound if i is odd.
163  	 * The following macros can be used to convert bound index into variable problem index and boundtype and vice versa.
164  	 */
165  	#define getLbIndex(idx) (2*(idx))
166  	#define getUbIndex(idx) (2*(idx)+1)
167  	#define getVarIndex(idx) ((idx)/2)
168  	#define getBoundtype(idx) (((idx) % 2 == 0) ? SCIP_BOUNDTYPE_LOWER : SCIP_BOUNDTYPE_UPPER)
169  	#define isIndexLowerbound(idx) ((idx) % 2 == 0)
170  	#define getBoundString(lower) ((lower) ? "lb" : "ub")
171  	#define getBoundtypeString(type) ((type) == SCIP_BOUNDTYPE_LOWER ? "lower" : "upper")
172  	#define indexGetBoundString(idx) (getBoundString(isIndexLowerbound(idx)))
173  	#define getOtherBoundIndex(idx) ((idx) + 1 - 2 * ((idx) % 2))
174  	
175  	/**@} */
176  	
177  	/*
178  	 * Data structures
179  	 */
180  	
181  	/** propagator data */
182  	struct SCIP_PropData
183  	{
184  	   SCIP_EVENTHDLR*       eventhdlr;          /**< event handler for catching bound changes */
185  	   SCIP_VAR**            vars;               /**< array containing all variable which are considered within the propagator */
186  	   SCIP_HASHMAP*         varhashmap;         /**< hashmap mapping from variable to index in the vars array */
187  	   int*                  topoorder;          /**< array mapping on the bounds of variables in topological order;
188  	                                              *   or -1, if the bound that should be at that position has no outgoing
189  	                                              *   implications, cliques, or vbounds;
190  	                                              *   i.e., for i < j and topoorder[i] != -1 != topoorder[j], the variable
191  	                                              *   and boundtype represented by index topoorder[i] are earlier in the
192  	                                              *   topological order than those represented by index topoorder[j]
193  	                                              */
194  	   int**                 vboundboundedidx;   /**< array storing for each bound index the bound indices of all bounds
195  	                                              *   influenced by this bound through variable bounds */
196  	   SCIP_Real**           vboundcoefs;        /**< array storing for each bound index the coefficients in the variable
197  	                                              *   bounds influencing the corresponding bound index stored in
198  	                                              *   vboundboundedidx */
199  	   SCIP_Real**           vboundconstants;    /**< array storing for each bound index the constants in the variable
200  	                                              *   bounds influencing the corresponding bound index stored in
201  	                                              *   vboundboundedidx */
202  	   int*                  nvbounds;           /**< array storing for each bound index the number of vbounds stored */
203  	   int*                  vboundsize;         /**< array with sizes of vbound arrays for the nodes */
204  	   int                   nbounds;            /**< number of bounds of variables regarded (two times number of active variables) */
205  	   int                   lastpresolncliques; /**< number of cliques created until the last call to the presolver */
206  	   SCIP_PQUEUE*          propqueue;          /**< priority queue to handle the bounds of variables that were changed and have to be propagated */
207  	   SCIP_Bool*            inqueue;            /**< boolean array to store whether a bound of a variable is already contained in propqueue */
208  	   SCIP_Bool             initialized;        /**< was the data for propagation already initialized? */
209  	   SCIP_Real             minnewcliques;      /**< minimum percentage of new cliques to trigger another clique table analysis */
210  	   SCIP_Real             maxcliquesmedium;   /**< maximum number of cliques per variable to run clique table analysis in medium presolving */
211  	   SCIP_Real             maxcliquesexhaustive;/**< maximum number of cliques per variable to run clique table analysis in exhaustive presolving */
212  	   SCIP_Bool             usebdwidening;      /**< should bound widening be used to initialize conflict analysis? */
213  	   SCIP_Bool             useimplics;         /**< should implications be propagated? */
214  	   SCIP_Bool             usecliques;         /**< should cliques be propagated? */
215  	   SCIP_Bool             usevbounds;         /**< should variable bounds be propagated? */
216  	   SCIP_Bool             dotoposort;         /**< should the bounds be topologically sorted in advance? */
217  	   SCIP_Bool             sortcliques;        /**< should cliques be regarded for the topological sort? */
218  	   SCIP_Bool             detectcycles;       /**< should cycles in the variable bound graph be identified? */
219  	};
220  	
221  	/** inference information */
222  	struct InferInfo
223  	{
224  	   union
225  	   {
226  	      struct
227  	      {
228  	         unsigned int    pos:31;             /**< position of the variable which forced that propagation */
229  	         unsigned int    boundtype:1;        /**< bound type which was the reason (0: lower, 1: upper) */
230  	      } asbits;
231  	      int                asint;              /**< inference information as a single int value */
232  	   } val;
233  	};
234  	typedef struct InferInfo INFERINFO;
235  	
236  	/** converts an integer into an inference information */
237  	static
238  	INFERINFO intToInferInfo(
239  	   int                   i                   /**< integer to convert */
240  	   )
241  	{
242  	   INFERINFO inferinfo;
243  	
244  	   inferinfo.val.asint = i;
245  	
246  	   return inferinfo;
247  	}
248  	
249  	/** converts an inference information into an int */
250  	static
251  	int inferInfoToInt(
252  	   INFERINFO             inferinfo           /**< inference information to convert */
253  	   )
254  	{
255  	   return inferinfo.val.asint;
256  	}
257  	
258  	/** returns the propagation rule stored in the inference information */
259  	static
260  	SCIP_BOUNDTYPE inferInfoGetBoundtype(
261  	   INFERINFO             inferinfo           /**< inference information to convert */
262  	   )
263  	{
264  	   assert((SCIP_BOUNDTYPE)inferinfo.val.asbits.boundtype == SCIP_BOUNDTYPE_LOWER
265  	      || (SCIP_BOUNDTYPE)inferinfo.val.asbits.boundtype == SCIP_BOUNDTYPE_UPPER);
266  	   return (SCIP_BOUNDTYPE)inferinfo.val.asbits.boundtype;
267  	}
268  	
269  	/** returns the position stored in the inference information */
270  	static
271  	int inferInfoGetPos(
272  	   INFERINFO             inferinfo           /**< inference information to convert */
273  	   )
274  	{
275  	   return (int) inferinfo.val.asbits.pos;
276  	}
277  	
278  	/** constructs an inference information out of a position of a variable and a boundtype */
279  	static
280  	INFERINFO getInferInfo(
281  	   int                   pos,                /**< position of the variable which forced that propagation */
282  	   SCIP_BOUNDTYPE        boundtype           /**< propagation rule that deduced the value */
283  	   )
284  	{
285  	   INFERINFO inferinfo;
286  	
287  	   assert(boundtype == SCIP_BOUNDTYPE_LOWER || boundtype == SCIP_BOUNDTYPE_UPPER);
288  	   assert(pos >= 0);
289  	
290  	   inferinfo.val.asbits.pos = (unsigned int) pos; /*lint !e732*/
291  	   inferinfo.val.asbits.boundtype = (unsigned int) boundtype; /*lint !e641*/
292  	
293  	   return inferinfo;
294  	}
295  	
296  	/*
297  	 * Local methods
298  	 */
299  	
300  	/* returns the lower bound index of a variable */
301  	static
302  	int varGetLbIndex(
303  	   SCIP_PROPDATA*        propdata,           /**< propagator data */
304  	   SCIP_VAR*             var                 /**< variable to get the index for */
305  	   )
306  	{
307  	   int i;
308  	
309  	   i = SCIPhashmapGetImageInt(propdata->varhashmap, var);
310  	
311  	   assert(SCIPhashmapExists(propdata->varhashmap, var) == (i != INT_MAX));
312  	   assert(i >= 0);
313  	
314  	   return getLbIndex(i == INT_MAX ? -1 : i);
315  	}
316  	
317  	/* returns the upper bound index of a variable */
318  	static
319  	int varGetUbIndex(
320  	   SCIP_PROPDATA*        propdata,           /**< propagator data */
321  	   SCIP_VAR*             var                 /**< variable to get the index for */
322  	   )
323  	{
324  	   int i;
325  	
326  	   i = SCIPhashmapGetImageInt(propdata->varhashmap, var);
327  	
328  	   assert(SCIPhashmapExists(propdata->varhashmap, var) == (i != INT_MAX));
329  	   assert(i >= 0);
330  	
331  	   return getUbIndex(i == INT_MAX ? -1 : i);
332  	}
333  	
334  	/** reset propagation data */
335  	static
336  	void resetPropdata(
337  	   SCIP_PROPDATA*        propdata            /**< propagator data */
338  	   )
339  	{
340  	   propdata->vars = NULL;
341  	   propdata->varhashmap = NULL;
342  	   propdata->topoorder = NULL;
343  	   propdata->vboundboundedidx = NULL;
344  	   propdata->vboundcoefs = NULL;
345  	   propdata->vboundconstants = NULL;
346  	   propdata->nvbounds = NULL;
347  	   propdata->vboundsize = NULL;
348  	   propdata->nbounds = 0;
349  	   propdata->initialized = FALSE;
350  	}
351  	
352  	/** catches events for variables */
353  	static
354  	SCIP_RETCODE catchEvents(
355  	   SCIP*                 scip,               /**< SCIP data structure */
356  	   SCIP_PROPDATA*        propdata            /**< propagator data */
357  	   )
358  	{
359  	   SCIP_EVENTHDLR* eventhdlr;
360  	   SCIP_EVENTTYPE eventtype;
361  	   SCIP_VAR** vars;
362  	   SCIP_VAR* var;
363  	   SCIP_Bool lower;
364  	   int nbounds;
365  	   int v;
366  	   int idx;
367  	
368  	   assert(scip != NULL);
369  	   assert(propdata != NULL);
370  	   assert(propdata->vars != NULL);
371  	   assert(propdata->topoorder != NULL);
372  	
373  	   /* catch variable events according to computed eventtypes */
374  	   eventhdlr = propdata->eventhdlr;
375  	   assert(eventhdlr != NULL);
376  	
377  	   vars = propdata->vars;
378  	   nbounds = propdata->nbounds;
379  	
380  	   /* setup events */
381  	   for( v = 0; v < nbounds; ++v )
382  	   {
383  	      idx = propdata->topoorder[v];
384  	      assert(idx >= 0 && idx < nbounds);
385  	
386  	      var = vars[getVarIndex(idx)];
387  	      lower = isIndexLowerbound(idx);
388  	
389  	      /* if the bound does not influence another bound by implications, cliques, or vbounds,
390  	       * we do not create an event and do not catch changes of the bound;
391  	       * we mark this by setting the value in topoorder to -1
392  	       */
393  	      if( propdata->nvbounds[idx] == 0 && SCIPvarGetNImpls(var, lower) == 0 && SCIPvarGetNCliques(var, lower) == 0 )
394  	      {
395  	         propdata->topoorder[v] = -1;
396  	         continue;
397  	      }
398  	
399  	      /* determine eventtype that we want to catch depending on boundtype of variable */
400  	      if( lower )
401  	         eventtype = SCIP_EVENTTYPE_LBTIGHTENED | SCIP_EVENTTYPE_GLBCHANGED;
402  	      else
403  	         eventtype = SCIP_EVENTTYPE_UBTIGHTENED | SCIP_EVENTTYPE_GUBCHANGED;
404  	
405  	      SCIP_CALL( SCIPcatchVarEvent(scip, var, eventtype, eventhdlr, (SCIP_EVENTDATA*) (uintptr_t) v, NULL) ); /*lint !e571*/
406  	   }
407  	
408  	   return SCIP_OKAY;
409  	}
410  	
411  	/** drops events for variables */
412  	static
413  	SCIP_RETCODE dropEvents(
414  	   SCIP*                 scip,               /**< SCIP data structure */
415  	   SCIP_PROPDATA*        propdata            /**< propagator data */
416  	   )
417  	{
418  	   SCIP_EVENTHDLR* eventhdlr;
419  	   SCIP_EVENTTYPE eventtype;
420  	   SCIP_VAR** vars;
421  	   SCIP_VAR* var;
422  	   SCIP_Bool lower;
423  	   int nbounds;
424  	   int v;
425  	   int idx;
426  	
427  	   assert(propdata != NULL);
428  	
429  	   eventhdlr = propdata->eventhdlr;
430  	   assert(eventhdlr != NULL);
431  	
432  	   vars = propdata->vars;
433  	   nbounds = propdata->nbounds;
434  	
435  	   for( v = 0; v < nbounds; ++v )
436  	   {
437  	      idx = propdata->topoorder[v];
438  	
439  	      if( idx == -1 )
440  	         continue;
441  	
442  	      assert(idx >= 0 && idx < nbounds);
443  	
444  	      var = vars[getVarIndex(idx)];
445  	      lower = isIndexLowerbound(idx);
446  	
447  	      /* determine eventtype that we catch and now want to drop depending on boundtype of variable */
448  	      if( lower )
449  	         eventtype = SCIP_EVENTTYPE_LBTIGHTENED | SCIP_EVENTTYPE_GLBCHANGED;
450  	      else
451  	         eventtype = SCIP_EVENTTYPE_UBTIGHTENED | SCIP_EVENTTYPE_GUBCHANGED;
452  	
453  	      SCIP_CALL( SCIPdropVarEvent(scip, var, eventtype, eventhdlr, (SCIP_EVENTDATA*) (uintptr_t) v, -1) ); /*lint !e571*/
454  	   }
455  	
456  	   return SCIP_OKAY;
457  	}
458  	
459  	#define INITMEMSIZE 5
460  	
461  	/* adds a vbound to the propagator data to store it internally and allow forward propagation */
462  	static
463  	SCIP_RETCODE addVbound(
464  	   SCIP*                 scip,               /**< SCIP data structure */
465  	   SCIP_PROPDATA*        propdata,           /**< propagator data */
466  	   int                   startidx,           /**< index of bound of variable influencing the other variable */
467  	   int                   endidx,             /**< index of bound of variable which is influenced */
468  	   SCIP_Real             coef,               /**< coefficient in the variable bound */
469  	   SCIP_Real             constant            /**< constant in the variable bound */
470  	   )
471  	{
472  	   int nvbounds;
473  	
474  	   assert(scip != NULL);
475  	   assert(propdata != NULL);
476  	
477  	   if( propdata->vboundsize[startidx] == 0 )
478  	   {
479  	      /* allocate memory for storing vbounds */
480  	      propdata->vboundsize[startidx] = INITMEMSIZE;
481  	
482  	      SCIP_CALL( SCIPreallocMemoryArray(scip, &propdata->vboundboundedidx[startidx], propdata->vboundsize[startidx]) ); /*lint !e866*/
483  	      SCIP_CALL( SCIPreallocMemoryArray(scip, &propdata->vboundcoefs[startidx], propdata->vboundsize[startidx]) ); /*lint !e866*/
484  	      SCIP_CALL( SCIPreallocMemoryArray(scip, &propdata->vboundconstants[startidx], propdata->vboundsize[startidx]) ); /*lint !e866*/
485  	   }
486  	   else if( propdata->nvbounds[startidx] >= propdata->vboundsize[startidx] )
487  	   {
488  	      /* reallocate memory for storing vbounds */
489  	      propdata->vboundsize[startidx] = SCIPcalcMemGrowSize(scip, propdata->nvbounds[startidx] + 1);
490  	      assert(propdata->nvbounds[startidx] < propdata->vboundsize[startidx]);
491  	
492  	      SCIP_CALL( SCIPreallocMemoryArray(scip, &propdata->vboundboundedidx[startidx], propdata->vboundsize[startidx]) ); /*lint !e866*/
493  	      SCIP_CALL( SCIPreallocMemoryArray(scip, &propdata->vboundcoefs[startidx], propdata->vboundsize[startidx]) ); /*lint !e866*/
494  	      SCIP_CALL( SCIPreallocMemoryArray(scip, &propdata->vboundconstants[startidx], propdata->vboundsize[startidx]) ); /*lint !e866*/
495  	   }
496  	
497  	   nvbounds = propdata->nvbounds[startidx];
498  	   propdata->vboundboundedidx[startidx][nvbounds] = endidx;
499  	   propdata->vboundcoefs[startidx][nvbounds] = coef;
500  	   propdata->vboundconstants[startidx][nvbounds] = constant;
501  	   (propdata->nvbounds[startidx])++;
502  	
503  	   return SCIP_OKAY;
504  	}
505  	
506  	/** comparison method for two indices in the topoorder array, preferring higher indices because the order is reverse
507  	 *  topological
508  	 */
509  	static
510  	SCIP_DECL_SORTPTRCOMP(compVarboundIndices)
511  	{
512  	   int idx1 = (int)(size_t)elem1;
513  	   int idx2 = (int)(size_t)elem2;
514  	
515  	   return idx2 - idx1;
516  	}
517  	
518  	/* extract bound changes or infeasibility information from a cycle in the variable bound graph detected during
519  	 * depth-first search
520  	 */
521  	static
522  	SCIP_RETCODE extractCycle(
523  	   SCIP*                 scip,               /**< SCIP data structure */
524  	   SCIP_PROPDATA*        propdata,           /**< propagator data */
525  	   int*                  dfsstack,           /**< array of size number of nodes to store the stack;
526  	                                              *   only needed for performance reasons */
527  	   int*                  stacknextedge,      /**< array storing the next edge to be visited in dfs for all nodes on the
528  	                                              *   stack/in the current path; negative numbers represent a clique,
529  	                                              *   positive numbers an implication (smaller numbers) or a variable bound */
530  	   int                   stacksize,          /**< current stack size */
531  	   SCIP_Bool             samebound,          /**< does the cycle contain the same bound twice or both bounds of the same variable? */
532  	   SCIP_Bool*            infeasible          /**< pointer to store whether an infeasibility was detected */
533  	
534  	   )
535  	{
536  	   SCIP_VAR** vars;
537  	   SCIP_VAR* currvar;
538  	   SCIP_Bool currlower;
539  	
540  	   SCIP_Real coef = 1.0;
541  	   SCIP_Real constant = 0.0;
542  	   SCIP_Bool islower;
543  	   SCIP_Real newbound;
544  	   int cycleidx;
545  	   int startidx;
546  	   int ntmpimpls;
547  	   int j;
548  	   int k;
549  	
550  	   assert(scip != NULL);
551  	   assert(propdata != NULL);
552  	
553  	   vars = propdata->vars;
554  	
555  	   /* the last element on the stack is the end-point of the cycle */
556  	   cycleidx = dfsstack[stacksize - 1];
557  	
558  	   /* the same bound of the variable was visited already earlier on the current path, so the start-point of the cycle
559  	    * has the same index
560  	    */
561  	   if( samebound )
562  	      startidx = cycleidx;
563  	   /* the other bound of the variable was visited earlier on the current path, so the start-point of the cycle
564  	    * has the index of the other bound
565  	    */
566  	   else
567  	      startidx = getOtherBoundIndex(cycleidx);
568  	
569  	   /* search for the start-point of the cycle; since the endpoint is at position stacksize - 1 we start at stacksize - 2
570  	    * and go backwards
571  	    */
572  	   for( j = stacksize - 2; dfsstack[j] != startidx && j >= 0; --j ){};
573  	   assert(j >= 0);
574  	
575  	   for( ; j < stacksize - 1; ++j )
576  	   {
577  	      currvar = vars[getVarIndex(dfsstack[j])];
578  	      currlower = isIndexLowerbound(dfsstack[j]);
579  	
580  	      /* if we do not use implications, we assume the number of implications to be 0 (as we did before) */
581  	      ntmpimpls = (propdata->useimplics ? SCIPvarGetNImpls(currvar, currlower) : 0);
582  	
583  	      /* stacknextedge[j] <= 0 --> the last outgoing edge traversed during dfs starting from node dfsstack[j] was given
584  	       * by a clique
585  	       */
586  	      if( stacknextedge[j] <= 0 )
587  	      {
588  	         SCIP_Bool nextlower = isIndexLowerbound(dfsstack[j+1]);
589  	#if defined(SCIP_DEBUG) || defined(SCIP_MORE_DEBUG)
590  	         SCIP_CLIQUE** tmpcliques = SCIPvarGetCliques(currvar, currlower);
591  	         SCIP_VAR** cliquevars;
592  	         SCIP_Bool* cliquevals;
593  	         int ntmpcliques = SCIPvarGetNCliques(currvar, currlower);
594  	         int ncliquevars;
595  	         int v;
596  	#endif
597  	         /* there are four cases:
598  	          * a) lb(x) -> ub(y)   ==>   clique(x,y,...)    ==>   y <= 1 - x
599  	          * b) lb(x) -> lb(y)   ==>   clique(x,~y,...)   ==>   y >= x
600  	          * c) ub(x) -> ub(y)   ==>   clique(~x,y,...)   ==>   y <= x
601  	          * d) ub(x) -> lb(y)   ==>   clique(~x,~y,...)  ==>   y >= 1 - x
602  	          *
603  	          * in cases b) and c), coef=1.0 and constant=0.0; these are the cases where both nodes represent
604  	          * the same type of bound
605  	          * in cases a) and d), coef=-1.0 and constant=1.0; both nodes represent different types of bounds
606  	          *
607  	          * we do not need to change the overall coef and constant in cases b) and c), but for the others
608  	          */
609  	         if( currlower != nextlower )
610  	         {
611  	            coef = -coef;
612  	            constant = -constant + 1.0;
613  	         }
614  	
615  	         /* since the coefficient and constant only depend on the type of bounds of the two nodes (see below), we do not
616  	          * need to search for the variable in the clique; however, if debug output is enabled, we want to print the
617  	          * clique, if more debugging is enabled, we explicitly check that the variable and bound we expect are in the
618  	          * clique
619  	          */
620  	#if defined(SCIP_DEBUG) || defined(SCIP_MORE_DEBUG)
621  	         if( stacknextedge[j] == 0 )
622  	         {
623  	            k = ntmpcliques - 1;
624  	         }
625  	         else
626  	         {
627  	            /* we processed at least one edge, so the next one should be -2 or smaller (we have a -1 offset) */
628  	            assert(stacknextedge[j] <= -2);
629  	
630  	            k = -stacknextedge[j] - 2;
631  	
632  	            assert(k < ntmpcliques);
633  	         }
634  	
635  	         cliquevars = SCIPcliqueGetVars(tmpcliques[k]);
636  	         cliquevals = SCIPcliqueGetValues(tmpcliques[k]);
637  	         ncliquevars = SCIPcliqueGetNVars(tmpcliques[k]);
638  	#ifdef SCIP_DEBUG
639  	         SCIPdebugMsg(scip, "clique: ");
640  	         for( v = 0; v < ncliquevars; ++v )
641  	         {
642  	            SCIPdebugMsg(scip, "%s%s ", cliquevals[v] ? "" : "~", SCIPvarGetName(cliquevars[v]));
643  	         }
644  	         SCIPdebugMsg(scip, "(equation:%d)\n", SCIPcliqueIsEquation(tmpcliques[k]));
645  	#endif
646  	#ifdef SCIP_MORE_DEBUG
647  	         for( v = 0; v < ncliquevars; ++v )
648  	         {
649  	            if( cliquevars[v] == vars[getVarIndex(dfsstack[j+1])] && cliquevals[v] == !nextlower )
650  	               break;
651  	         }
652  	         assert(v < ncliquevars);
653  	#endif
654  	
655  	         SCIPdebugMsg(scip, "%s(%s) -- (*%g + %g)[clique(<%s%s>,<%s%s>,...)] --> %s(%s)\n",
656  	            indexGetBoundString(dfsstack[j]), SCIPvarGetName(currvar),
657  	            (currlower != nextlower ? -1.0 : 1.0),
658  	            (currlower != nextlower ? 1.0 : 0.0),
659  	            (currlower ? "" : "~"), SCIPvarGetName(currvar),
660  	            (nextlower ? "~" : ""), SCIPvarGetName(vars[getVarIndex(dfsstack[j+1])]),
661  	            indexGetBoundString(dfsstack[j+1]), SCIPvarGetName(currvar));
662  	#endif
663  	      }
664  	      /* stacknextedge[j] > 0 --> the last outgoing edge traversed during dfs starting from node dfsstack[j] was given
665  	       * by an implication or vbound. Implications are looked at first, so if stacknextedge[j] <= ntmpimpls, it comes
666  	       * from an implication
667  	       */
668  	      else if( stacknextedge[j] <= ntmpimpls )
669  	      {
670  	#ifndef NDEBUG
671  	         SCIP_VAR** implvars = SCIPvarGetImplVars(currvar, currlower);
672  	#endif
673  	         SCIP_BOUNDTYPE* impltypes = SCIPvarGetImplTypes(currvar, currlower);
674  	         SCIP_Real* implbounds = SCIPvarGetImplBounds(currvar, currlower);
675  	         SCIP_VAR* nextvar = vars[getVarIndex(dfsstack[j+1])];
676  	         SCIP_Real newconstant;
677  	         SCIP_Real newcoef;
678  	
679  	         k = stacknextedge[j] - 1;
680  	
681  	         assert(dfsstack[j+1] == (impltypes[k] == SCIP_BOUNDTYPE_LOWER ?
682  	               varGetLbIndex(propdata, implvars[k]) : varGetUbIndex(propdata, implvars[k])));
683  	
684  	         if( impltypes[k] == SCIP_BOUNDTYPE_LOWER )
685  	         {
686  	            newcoef = implbounds[k] - SCIPvarGetLbLocal(nextvar);
687  	
688  	            if( currlower )
689  	            {
690  	               newconstant = SCIPvarGetLbLocal(nextvar);
691  	            }
692  	            else
693  	            {
694  	               newconstant = implbounds[k];
695  	               newcoef *= -1.0;
696  	            }
697  	         }
698  	         else
699  	         {
700  	            assert(impltypes[k] == SCIP_BOUNDTYPE_UPPER);
701  	
702  	            newcoef = SCIPvarGetUbLocal(nextvar) - implbounds[k];
703  	
704  	            if( currlower )
705  	            {
706  	               newconstant = SCIPvarGetUbLocal(nextvar);
707  	               newcoef *= -1.0;
708  	            }
709  	            else
710  	            {
711  	               newconstant = implbounds[k];
712  	            }
713  	         }
714  	
715  	         coef = coef * newcoef;
716  	         constant = constant * newcoef + newconstant;
717  	
718  	         SCIPdebugMsg(scip, "%s(%s) -- (*%g + %g) --> %s(%s)\n",
719  	            indexGetBoundString(dfsstack[j]), SCIPvarGetName(vars[getVarIndex(dfsstack[j])]),
720  	            newcoef, newconstant,
721  	            indexGetBoundString(dfsstack[j+1]), SCIPvarGetName(vars[getVarIndex(dfsstack[j+1])]));
722  	      }
723  	      /* the edge was given by a variable bound relation */
724  	      else
725  	      {
726  	         assert(stacknextedge[j] > ntmpimpls);
727  	
728  	         k = stacknextedge[j] - ntmpimpls - 1;
729  	         assert(k < propdata->nvbounds[dfsstack[j]]);
730  	         assert(propdata->vboundboundedidx[dfsstack[j]][k] == dfsstack[j+1]);
731  	
732  	         SCIPdebugMsg(scip, "%s(%s) -- (*%g + %g) --> %s(%s)\n",
733  	            indexGetBoundString(dfsstack[j]), SCIPvarGetName(vars[getVarIndex(dfsstack[j])]),
734  	            propdata->vboundcoefs[dfsstack[j]][k], propdata->vboundconstants[dfsstack[j]][k],
735  	            indexGetBoundString(dfsstack[j+1]), SCIPvarGetName(vars[getVarIndex(dfsstack[j+1])]));
736  	
737  	         coef = coef * propdata->vboundcoefs[dfsstack[j]][k];
738  	         constant = constant * propdata->vboundcoefs[dfsstack[j]][k] + propdata->vboundconstants[dfsstack[j]][k];
739  	      }
740  	   }
741  	
742  	   SCIPdebugMsg(scip, "==> %s(%s) -- (*%g + %g) --> %s(%s)\n",
743  	      indexGetBoundString(startidx), SCIPvarGetName(vars[getVarIndex(startidx)]),
744  	      coef, constant,
745  	      indexGetBoundString(cycleidx), SCIPvarGetName(vars[getVarIndex(cycleidx)]));
746  	
747  	   islower = isIndexLowerbound(cycleidx);
748  	
749  	   /* we have a relation x <=/>= coef * x + constant now
750  	    * (the relation depends on islower, i.e., whether the last node in the cycle is a lower or upper bound)
751  	    * case 1) coef is 1.0 --> x cancels out and we have a statement 0 <=/>= constant.
752  	    *         if we have a >= relation and constant is positive, we have a contradiction 0 >= constant
753  	    *         if we have a <= relation and constant is negative, we have a contradiction 0 <= constant
754  	    * case 2) coef != 1.0 --> we have a relation x - coef * x <=/>= constant
755  	    *                                      <=> (1 - coef) * x <=/>= constant
756  	    *         if coef < 1.0 this gives us x >= constant / (1 - coef) (if islower=TRUE)
757  	    *                                  or x <= constant / (1 - coef) (if islower=FALSE)
758  	    *         if coef > 1.0, the relation signs need to be switched.
759  	    */
760  	   if( SCIPisEQ(scip, coef, 1.0) )
761  	   {
762  	      if( islower && SCIPisFeasPositive(scip, constant) )
763  	      {
764  	         SCIPdebugMsg(scip, "-> infeasible aggregated variable bound relation 0 >= %g\n", constant);
765  	         *infeasible = TRUE;
766  	      }
767  	      else if( !islower && SCIPisFeasNegative(scip, constant) )
768  	      {
769  	         SCIPdebugMsg(scip, "-> infeasible aggregated variable bound relation 0 <= %g\n", constant);
770  	         *infeasible = TRUE;
771  	      }
772  	   }
773  	   else
774  	   {
775  	      SCIP_Bool tightened;
776  	
777  	      newbound = constant / (1.0 - coef);
778  	
779  	      if( SCIPisGT(scip, coef, 1.0) )
780  	         islower = !islower;
781  	
782  	      if( islower )
783  	      {
784  	         SCIPdebugMsg(scip, "-> found new lower bound: <%s>[%g,%g] >= %g\n", SCIPvarGetName(vars[getVarIndex(cycleidx)]),
785  	            SCIPvarGetLbLocal(vars[getVarIndex(cycleidx)]), SCIPvarGetUbLocal(vars[getVarIndex(cycleidx)]), newbound);
786  	         SCIP_CALL( SCIPtightenVarLb(scip, vars[getVarIndex(cycleidx)], newbound, FALSE, infeasible, &tightened) );
787  	      }
788  	      else
789  	      {
790  	         SCIPdebugMsg(scip, "-> found new upper bound: <%s>[%g,%g] <= %g\n", SCIPvarGetName(vars[getVarIndex(cycleidx)]),
791  	            SCIPvarGetLbLocal(vars[getVarIndex(cycleidx)]), SCIPvarGetUbLocal(vars[getVarIndex(cycleidx)]), newbound);
792  	         SCIP_CALL( SCIPtightenVarUb(scip, vars[getVarIndex(cycleidx)], newbound, FALSE, infeasible, &tightened) );
793  	      }
794  	
795  	      if( tightened )
796  	         SCIPdebugMsg(scip, "---> applied new bound\n");
797  	   }
798  	
799  	   return SCIP_OKAY;
800  	}
801  	
802  	#define VISITED 1
803  	#define ACTIVE  2
804  	/** performs depth-first-search in the implicitly given directed graph from the given start index */
805  	static
806  	SCIP_RETCODE dfs(
807  	   SCIP*                 scip,               /**< SCIP data structure */
808  	   SCIP_PROPDATA*        propdata,           /**< propagator data */
809  	   int                   startnode,          /**< node to start the depth-first-search */
810  	   int*                  visited,            /**< array to store for each node, whether it was already visited */
811  	   int*                  dfsstack,           /**< array of size number of nodes to store the stack;
812  	                                              *   only needed for performance reasons */
813  	   int*                  stacknextedge,      /**< array of size number of nodes to store the next edge to be visited in
814  	                                              *   dfs for all nodes on the stack/in the current path; only needed for
815  	                                              *   performance reasons */
816  	   int*                  dfsnodes,           /**< array of nodes that can be reached starting at startnode, in reverse
817  	                                              *   dfs order */
818  	   int*                  ndfsnodes,          /**< pointer to store number of nodes that can be reached starting at
819  	                                              *   startnode */
820  	   SCIP_Bool*            infeasible          /**< pointer to store whether an infeasibility was detected */
821  	   )
822  	{
823  	   SCIP_VAR** vars;
824  	   SCIP_VAR* startvar;
825  	   SCIP_Bool lower;
826  	   int stacksize;
827  	   int curridx;
828  	   int nimpls;
829  	   int idx;
830  	   /* for cycle detection, we need to mark currently active nodes, otherwise we just mark them as visited */
831  	   int visitedflag = (propdata->detectcycles ? ACTIVE : VISITED);
832  	
833  	   assert(startnode >= 0);
834  	   assert(startnode < propdata->nbounds);
835  	   assert(visited != NULL);
836  	   assert(visited[startnode] == 0);
837  	   assert(dfsstack != NULL);
838  	   assert(dfsnodes != NULL);
839  	   assert(ndfsnodes != NULL);
840  	   assert(infeasible != NULL);
841  	
842  	   *infeasible = FALSE;
843  	
844  	   vars = propdata->vars;
845  	
846  	   /* put start node on the stack */
847  	   dfsstack[0] = startnode;
848  	   stacknextedge[0] = 0;
849  	   stacksize = 1;
850  	   idx = -1;
851  	
852  	   /* we run until no more bounds indices are on the stack, i.e. all changed bounds were propagated */
853  	   while( stacksize > 0 )
854  	   {
855  	      /* get next node from stack */
856  	      curridx = dfsstack[stacksize - 1];
857  	
858  	      /* mark current node as visited */
859  	      assert((visited[curridx] != 0) == (stacknextedge[stacksize - 1] != 0));
860  	      visited[curridx] = visitedflag;
861  	
862  	      startvar = vars[getVarIndex(curridx)];
863  	      lower = isIndexLowerbound(curridx);
864  	
865  	      /* if the variable was fixed in the meantime, it is a loose end in the variable bound graph */
866  	      if( SCIPisFeasGE(scip, SCIPvarGetLbGlobal(startvar), SCIPvarGetUbGlobal(startvar)) )
867  	         goto REMOVE;
868  	
869  	      nimpls = 0;
870  	
871  	      if( propdata->sortcliques && propdata->usecliques && stacknextedge[stacksize - 1] == 0 )
872  	         stacknextedge[stacksize - 1] = -1;
873  	
874  	      /* stacknextedge is negative, if the last visited edge from the current node belongs to a clique;
875  	       * the index of the clique in the variable's clique list equals abs(stacknextedge) - 1
876  	       */
877  	      if( propdata->sortcliques && propdata->usecliques && stacknextedge[stacksize - 1] < 0 )
878  	      {
879  	         SCIP_CLIQUE** cliques;
880  	         int ncliques;
881  	         int j;
882  	         int i;
883  	         SCIP_Bool found;
884  	
885  	         ncliques = SCIPvarGetNCliques(startvar, lower);
886  	         cliques = SCIPvarGetCliques(startvar, lower);
887  	         found = FALSE;
888  	
889  	         assert(stacknextedge[stacksize - 1] == -1 || -stacknextedge[stacksize - 1] - 1 <= ncliques);
890  	
891  	         /* iterate over all not yet handled cliques and search for an unvisited node */
892  	         for( j = -stacknextedge[stacksize - 1] - 1; j < ncliques; ++j )
893  	         {
894  	            SCIP_VAR** cliquevars;
895  	            SCIP_Bool* cliquevals;
896  	            int ncliquevars;
897  	
898  	            cliquevars = SCIPcliqueGetVars(cliques[j]);
899  	            cliquevals = SCIPcliqueGetValues(cliques[j]);
900  	            ncliquevars = SCIPcliqueGetNVars(cliques[j]);
901  	
902  	            for( i = 0; i < ncliquevars; ++i )
903  	            {
904  	               if( cliquevars[i] == startvar )
905  	                  continue;
906  	
907  	               if( cliquevals[i] )
908  	                  idx = varGetUbIndex(propdata, cliquevars[i]);
909  	               else
910  	                  idx = varGetLbIndex(propdata, cliquevars[i]);
911  	
912  	               /* we reached a variable that was already visited on the active path, so we have a cycle in the variable
913  	                * bound graph and try to extract valid bound changes from it or detect infeasibility
914  	                */
915  	               if( idx >= 0 && (visited[idx] == ACTIVE || visited[getOtherBoundIndex(idx)] == ACTIVE)
916  	                  && !SCIPisFeasGE(scip, SCIPvarGetLbGlobal(cliquevars[i]), SCIPvarGetUbGlobal(cliquevars[i])) )
917  	               {
918  	                  SCIPdebugMsg(scip, "found cycle\n");
919  	
920  	                  dfsstack[stacksize] = idx;
921  	                  stacknextedge[stacksize - 1] = -j - 2;
922  	
923  	                  SCIP_CALL( extractCycle(scip, propdata, dfsstack, stacknextedge, stacksize + 1,
924  	                        visited[idx] == ACTIVE, infeasible) );
925  	
926  	                  if( *infeasible )
927  	                     break;
928  	               }
929  	
930  	               /* break when the first unvisited node is reached */
931  	               if( idx >= 0 && !visited[idx] )
932  	               {
933  	                  found = TRUE;
934  	                  break;
935  	               }
936  	            }
937  	            if( found )
938  	               break;
939  	         }
940  	
941  	         /* we stopped because we found an unhandled node and not because we reached the end of the list */
942  	         if( found )
943  	         {
944  	            assert(idx >= 0);
945  	            assert(!visited[idx]);
946  	            assert(j < ncliques);
947  	
948  	            SCIPdebugMsg(scip, "clique: %s(%s) -> %s(%s)\n", getBoundString(lower), SCIPvarGetName(startvar),
949  	               indexGetBoundString(idx), SCIPvarGetName(vars[getVarIndex(idx)]));
950  	
951  	            /* put the adjacent node onto the stack */
952  	            dfsstack[stacksize] = idx;
953  	            stacknextedge[stacksize] = 0;
954  	            stacknextedge[stacksize - 1] = -j - 2;
955  	            stacksize++;
956  	            assert(stacksize <= propdata->nbounds);
957  	
958  	            /* restart while loop, get next index from stack */
959  	            continue;
960  	         }
961  	         else
962  	         {
963  	            /* we did not find an edge to an unhandled node given by a clique */
964  	            stacknextedge[stacksize - 1] = 0;
965  	         }
966  	      }
967  	      assert(stacknextedge[stacksize - 1] >= 0);
968  	
969  	      /* go over edges given by implications */
970  	      if( propdata->useimplics )
971  	      {
972  	         nimpls = SCIPvarGetNImpls(startvar, lower);
973  	
974  	         if( stacknextedge[stacksize - 1] < nimpls )
975  	         {
976  	            SCIP_VAR** implvars;
977  	            SCIP_BOUNDTYPE* impltypes;
978  	            int* implids;
979  	            int i;
980  	
981  	            implvars = SCIPvarGetImplVars(startvar, lower);
982  	            impltypes = SCIPvarGetImplTypes(startvar, lower);
983  	            implids = SCIPvarGetImplIds(startvar, lower);
984  	
985  	            for( i = stacknextedge[stacksize - 1]; i < nimpls; ++i )
986  	            {
987  	               /* it might happen that implications point to inactive variables (normally, those are removed when a
988  	                * variable becomes inactive, but in some cases, it cannot be done), we have to ignore these variables
989  	                */
990  	               if( !SCIPvarIsActive(implvars[i]) )
991  	                  continue;
992  	
993  	               /* implication is just a shortcut, so we dont regard it now, because will later go the long way, anyway;
994  	                * however, if we do regard cliques for the topological order, we use them to get a better order
995  	                */
996  	               if( propdata->usecliques && !propdata->sortcliques && implids[i] < 0 )
997  	                  continue;
998  	
999  	               idx = (impltypes[i] == SCIP_BOUNDTYPE_LOWER ?
1000 	                  varGetLbIndex(propdata, implvars[i]) : varGetUbIndex(propdata, implvars[i]));
1001 	
1002 	               /* we reached a variable that was already visited on the active path, so we have a cycle in the variable
1003 	                * bound graph and try to extract valid bound changes from it or detect infeasibility
1004 	                */
1005 	               if( idx >= 0 && (visited[idx] == ACTIVE || visited[getOtherBoundIndex(idx)] == ACTIVE)
1006 	                  && !SCIPisFeasGE(scip, SCIPvarGetLbGlobal(implvars[i]), SCIPvarGetUbGlobal(implvars[i])) )
1007 	               {
1008 	                  SCIPdebugMsg(scip, "found cycle\n");
1009 	
1010 	                  dfsstack[stacksize] = idx;
1011 	                  stacknextedge[stacksize - 1] = i + 1;
1012 	
1013 	                  SCIP_CALL( extractCycle(scip, propdata, dfsstack, stacknextedge, stacksize + 1,
1014 	                        visited[idx] == ACTIVE, infeasible) );
1015 	
1016 	                  if( *infeasible )
1017 	                     break;
1018 	               }
1019 	
1020 	               /* break when the first unvisited node is reached */
1021 	               if( idx >= 0 && !visited[idx] )
1022 	                  break;
1023 	            }
1024 	
1025 	            /* we stopped because we found an unhandled node and not because we reached the end of the list */
1026 	            if( i < nimpls )
1027 	            {
1028 	               assert(!visited[idx]);
1029 	
1030 	               SCIPdebugMsg(scip, "impl: %s(%s) -> %s(%s)\n", getBoundString(lower), SCIPvarGetName(startvar),
1031 	                  indexGetBoundString(idx), SCIPvarGetName(vars[getVarIndex(idx)]));
1032 	
1033 	               /* put the adjacent node onto the stack */
1034 	               dfsstack[stacksize] = idx;
1035 	               stacknextedge[stacksize] = 0;
1036 	               stacknextedge[stacksize - 1] = i + 1;
1037 	               stacksize++;
1038 	               assert(stacksize <= propdata->nbounds);
1039 	
1040 	               /* restart while loop, get next index from stack */
1041 	               continue;
1042 	            }
1043 	            else
1044 	            {
1045 	               stacknextedge[stacksize - 1] = nimpls;
1046 	            }
1047 	         }
1048 	      }
1049 	      assert(stacknextedge[stacksize - 1] >= nimpls);
1050 	
1051 	      /* go over edges corresponding to varbounds */
1052 	      if( propdata->usevbounds )
1053 	      {
1054 	         int nvbounds;
1055 	         int* vboundidx;
1056 	         int i;
1057 	
1058 	         nvbounds = propdata->nvbounds[curridx];
1059 	         vboundidx = propdata->vboundboundedidx[curridx];
1060 	
1061 	         /* iterate over all vbounds for the given bound */
1062 	         for( i = stacknextedge[stacksize - 1] - nimpls; i < nvbounds; ++i )
1063 	         {
1064 	            idx = vboundidx[i];
1065 	            assert(idx >= 0);
1066 	
1067 	            if( (visited[idx] == ACTIVE || visited[getOtherBoundIndex(idx)] == ACTIVE)
1068 	               && !SCIPisFeasGE(scip, SCIPvarGetLbGlobal(vars[getVarIndex(idx)]), SCIPvarGetUbGlobal(vars[getVarIndex(idx)])) )
1069 	            {
1070 	               SCIPdebugMsg(scip, "found cycle\n");
1071 	
1072 	               dfsstack[stacksize] = idx;
1073 	               stacknextedge[stacksize - 1] = nimpls + i + 1;
1074 	
1075 	               /* we reached a variable that was already visited on the active path, so we have a cycle in the variable
1076 	                * bound graph and try to extract valid bound changes from it or detect infeasibility
1077 	                */
1078 	               SCIP_CALL( extractCycle(scip, propdata, dfsstack, stacknextedge, stacksize + 1,
1079 	                     visited[idx] == ACTIVE, infeasible) );
1080 	
1081 	               if( *infeasible )
1082 	                  break;
1083 	            }
1084 	
1085 	            /* break when the first unvisited node is reached */
1086 	            if( !visited[idx] )
1087 	               break;
1088 	         }
1089 	
1090 	         if( *infeasible )
1091 	            break;
1092 	
1093 	         /* we stopped because we found an unhandled node and not because we reached the end of the list */
1094 	         if( i < nvbounds )
1095 	         {
1096 	            assert(!visited[idx]);
1097 	
1098 	            SCIPdebugMsg(scip, "vbound: %s(%s) -> %s(%s)\n", getBoundString(lower), SCIPvarGetName(startvar),
1099 	               indexGetBoundString(idx), SCIPvarGetName(vars[getVarIndex(idx)]));
1100 	
1101 	            /* put the adjacent node onto the stack */
1102 	            dfsstack[stacksize] = idx;
1103 	            stacknextedge[stacksize] = 0;
1104 	            stacknextedge[stacksize - 1] = nimpls + i + 1;
1105 	            stacksize++;
1106 	            assert(stacksize <= propdata->nbounds);
1107 	
1108 	            /* restart while loop, get next index from stack */
1109 	            continue;
1110 	         }
1111 	      }
1112 	   REMOVE:
1113 	      /* the current node was completely handled, remove it from stack */
1114 	      stacksize--;
1115 	
1116 	      SCIPdebugMsg(scip, "topoorder[%d] = %s(%s)\n", *ndfsnodes, getBoundString(lower), SCIPvarGetName(startvar));
1117 	
1118 	      /* store node in the sorted nodes array */
1119 	      dfsnodes[(*ndfsnodes)] = curridx;
1120 	      assert(visited[curridx] == visitedflag);
1121 	      visited[curridx] = VISITED;
1122 	      (*ndfsnodes)++;
1123 	   }
1124 	
1125 	   return SCIP_OKAY;
1126 	}
1127 	
1128 	/** sort the bounds of variables topologically */
1129 	static
1130 	SCIP_RETCODE topologicalSort(
1131 	   SCIP*                 scip,               /**< SCIP data structure */
1132 	   SCIP_PROPDATA*        propdata,           /**< propagator data */
1133 	   SCIP_Bool*            infeasible          /**< pointer to store whether an infeasibility was detected */
1134 	   )
1135 	{
1136 	   int* dfsstack;
1137 	   int* stacknextedge;
1138 	   int* visited;
1139 	   int nsortednodes;
1140 	   int nbounds;
1141 	   int i;
1142 	
1143 	   assert(scip != NULL);
1144 	   assert(propdata != NULL);
1145 	   assert(infeasible != NULL);
1146 	
1147 	   nbounds = propdata->nbounds;
1148 	
1149 	   SCIP_CALL( SCIPallocBufferArray(scip, &dfsstack, nbounds) );
1150 	   SCIP_CALL( SCIPallocBufferArray(scip, &stacknextedge, nbounds) );
1151 	   SCIP_CALL( SCIPallocClearBufferArray(scip, &visited, nbounds) );
1152 	
1153 	   nsortednodes = 0;
1154 	
1155 	   /* while there are unvisited nodes, run dfs starting from one of these nodes; the dfs orders are stored in the
1156 	    * topoorder array, later dfs calls are just appended after the stacks of previous dfs calls, which gives us a
1157 	    * reverse topological order
1158 	    */
1159 	   for( i = 0; i < nbounds && !(*infeasible); ++i )
1160 	   {
1161 	      if( !visited[i] )
1162 	      {
1163 	         SCIP_CALL( dfs(scip, propdata, i, visited, dfsstack, stacknextedge, propdata->topoorder, &nsortednodes, infeasible) );
1164 	      }
1165 	   }
1166 	   assert((nsortednodes == nbounds) || (*infeasible));
1167 	
1168 	   SCIPfreeBufferArray(scip, &visited);
1169 	   SCIPfreeBufferArray(scip, &stacknextedge);
1170 	   SCIPfreeBufferArray(scip, &dfsstack);
1171 	
1172 	   return SCIP_OKAY;
1173 	}
1174 	
1175 	/** initializes the internal data for the variable bounds propagator */
1176 	static
1177 	SCIP_RETCODE initData(
1178 	   SCIP*                 scip,               /**< SCIP data structure */
1179 	   SCIP_PROP*            prop,               /**< vbounds propagator */
1180 	   SCIP_Bool*            infeasible          /**< pointer to store whether an infeasibility was detected */
1181 	   )
1182 	{
1183 	   SCIP_PROPDATA* propdata;
1184 	   SCIP_VAR** vars;
1185 	   int nvars;
1186 	   int nbounds;
1187 	   int startidx;
1188 	   int v;
1189 	   int n;
1190 	
1191 	   assert(scip != NULL);
1192 	   assert(prop != NULL);
1193 	   assert(infeasible != NULL);
1194 	
1195 	   /* get propagator data */
1196 	   propdata = SCIPpropGetData(prop);
1197 	   assert(propdata != NULL);
1198 	   assert(!propdata->initialized);
1199 	
1200 	   SCIPdebugMsg(scip, "initialize vbounds propagator for problem <%s>\n", SCIPgetProbName(scip));
1201 	
1202 	   vars = SCIPgetVars(scip);
1203 	   nvars = SCIPgetNVars(scip);
1204 	   nbounds = 2 * nvars;
1205 	
1206 	   *infeasible = FALSE;
1207 	
1208 	   /* store size of the bounds of variables array */
1209 	   propdata->nbounds = nbounds;
1210 	
1211 	   if( nbounds == 0 )
1212 	      return SCIP_OKAY;
1213 	
1214 	   propdata->initialized = TRUE;
1215 	
1216 	   /* prepare priority queue structure */
1217 	   SCIP_CALL( SCIPpqueueCreate(&propdata->propqueue, nvars, 2.0, compVarboundIndices, NULL) );
1218 	   SCIP_CALL( SCIPallocBlockMemoryArray(scip, &propdata->inqueue, nbounds) );
1219 	   BMSclearMemoryArray(propdata->inqueue, nbounds);
1220 	
1221 	   /* we need to copy the variable since this array is the basis of the propagator and the corresponding variable array
1222 	    * within SCIP might change during the search
1223 	    */
1224 	   SCIP_CALL( SCIPduplicateBlockMemoryArray(scip, &propdata->vars, vars, nvars) );
1225 	   SCIP_CALL( SCIPhashmapCreate(&propdata->varhashmap, SCIPblkmem(scip), nvars) );
1226 	
1227 	   for( v = 0; v < nvars; ++v )
1228 	   {
1229 	      SCIP_CALL( SCIPhashmapInsertInt(propdata->varhashmap, propdata->vars[v], v) );
1230 	   }
1231 	
1232 	   /* allocate memory for the arrays of the propdata */
1233 	   SCIP_CALL( SCIPallocBlockMemoryArray(scip, &propdata->topoorder, nbounds) );
1234 	   SCIP_CALL( SCIPallocBlockMemoryArray(scip, &propdata->vboundboundedidx, nbounds) );
1235 	   SCIP_CALL( SCIPallocBlockMemoryArray(scip, &propdata->vboundcoefs, nbounds) );
1236 	   SCIP_CALL( SCIPallocBlockMemoryArray(scip, &propdata->vboundconstants, nbounds) );
1237 	   SCIP_CALL( SCIPallocBlockMemoryArray(scip, &propdata->nvbounds, nbounds) );
1238 	   SCIP_CALL( SCIPallocBlockMemoryArray(scip, &propdata->vboundsize, nbounds) );
1239 	   BMSclearMemoryArray(propdata->vboundboundedidx, nbounds);
1240 	   BMSclearMemoryArray(propdata->vboundcoefs, nbounds);
1241 	   BMSclearMemoryArray(propdata->vboundconstants, nbounds);
1242 	   BMSclearMemoryArray(propdata->nvbounds, nbounds);
1243 	   BMSclearMemoryArray(propdata->vboundsize, nbounds);
1244 	
1245 	   for( v = 0; v < nbounds; ++v )
1246 	   {
1247 	      propdata->topoorder[v] = v;
1248 	      propdata->vboundboundedidx[v] = NULL;
1249 	      propdata->vboundcoefs[v] = NULL;
1250 	      propdata->vboundconstants[v] = NULL;
1251 	      propdata->nvbounds[v] = 0;
1252 	      propdata->vboundsize[v] = 0;
1253 	   }
1254 	
1255 	   /* collect information about varbounds */
1256 	   for( v = 0; v < nbounds; ++v )
1257 	   {
1258 	      SCIP_VAR** vbvars;
1259 	      SCIP_VAR* var;
1260 	      SCIP_Real* coefs;
1261 	      SCIP_Real* constants;
1262 	      SCIP_Bool lower;
1263 	      int nvbvars;
1264 	
1265 	      var = vars[getVarIndex(v)];
1266 	      lower = isIndexLowerbound(v);
1267 	
1268 	      /* get the variable bound informations for the current variable */
1269 	      if( lower )
1270 	      {
1271 	         vbvars = SCIPvarGetVlbVars(var);
1272 	         coefs = SCIPvarGetVlbCoefs(var);
1273 	         constants = SCIPvarGetVlbConstants(var);
1274 	         nvbvars = SCIPvarGetNVlbs(var);
1275 	      }
1276 	      else
1277 	      {
1278 	         vbvars = SCIPvarGetVubVars(var);
1279 	         coefs = SCIPvarGetVubCoefs(var);
1280 	         constants = SCIPvarGetVubConstants(var);
1281 	         nvbvars = SCIPvarGetNVubs(var);
1282 	      }
1283 	
1284 	      /* loop over all variable bounds; a variable lower bound has the form: x >= b*y + d,
1285 	       * a variable upper bound the form x <= b*y + d */
1286 	      for( n = 0; n < nvbvars; ++n )
1287 	      {
1288 	         SCIP_VAR* vbvar;
1289 	         SCIP_Real coef;
1290 	         SCIP_Real constant;
1291 	
1292 	         vbvar = vbvars[n];
1293 	         coef = coefs[n];
1294 	         constant = constants[n];
1295 	         assert(vbvar != NULL);
1296 	
1297 	         /* transform variable bound variable to an active variable, if possible */
1298 	         SCIP_CALL( SCIPgetProbvarSum(scip, &vbvar, &coef, &constant) );
1299 	         assert(vbvar != NULL);
1300 	
1301 	         if( !SCIPvarIsActive(vbvar) )
1302 	            continue;
1303 	
1304 	         /* if the coefficient is positive, the type of bound is the same for the bounded and the bounding variable */
1305 	         if( SCIPisPositive(scip, coef) )
1306 	            startidx = (lower ? varGetLbIndex(propdata, vbvar) : varGetUbIndex(propdata, vbvar));
1307 	         else
1308 	            startidx = (lower ? varGetUbIndex(propdata, vbvar) : varGetLbIndex(propdata, vbvar));
1309 	         assert(startidx >= 0);
1310 	
1311 	         /* If the vbvar is binary, the vbound should be stored as an implication already.
1312 	          * However, it might happen that vbvar was integer when the variable bound was added, but was converted
1313 	          * to a binary variable later during presolving when its upper bound was changed to 1. In this case,
1314 	          * the implication might not have been created.
1315 	          */
1316 	         if( SCIPvarGetType(vbvar) == SCIP_VARTYPE_BINARY
1317 	            && SCIPvarHasImplic(vbvar, isIndexLowerbound(startidx), var, getBoundtype(v)) )
1318 	         {
1319 	            SCIPdebugMsg(scip, "varbound <%s> %s %g * <%s> + %g not added to propagator data due to reverse implication\n",
1320 	               SCIPvarGetName(var), (lower ? ">=" : "<="), coef,
1321 	               SCIPvarGetName(vbvar), constant);
1322 	         }
1323 	         else
1324 	         {
1325 	            SCIP_CALL( addVbound(scip, propdata, startidx, v, coef, constant) );
1326 	
1327 	            SCIPdebugMsg(scip, "varbound <%s> %s %g * <%s> + %g added to propagator data\n",
1328 	               SCIPvarGetName(var), (lower ? ">=" : "<="), coef,
1329 	               SCIPvarGetName(vbvar), constant);
1330 	         }
1331 	      }
1332 	   }
1333 	
1334 	   /* sort the bounds topologically */
1335 	   if( propdata->dotoposort )
1336 	   {
1337 	      SCIP_CALL( topologicalSort(scip, propdata, infeasible) );
1338 	   }
1339 	
1340 	   /* catch variable events */
1341 	   SCIP_CALL( catchEvents(scip, propdata) );
1342 	
1343 	   return SCIP_OKAY;
1344 	}
1345 	
1346 	/** resolves a propagation by adding the variable which implied that bound change */
1347 	static
1348 	SCIP_RETCODE resolvePropagation(
1349 	   SCIP*                 scip,               /**< SCIP data structure */
1350 	   SCIP_PROPDATA*        propdata,           /**< propagator data */
1351 	   SCIP_VAR*             var,                /**< variable to be reported */
1352 	   SCIP_BOUNDTYPE        boundtype,          /**< bound to be reported */
1353 	   SCIP_BDCHGIDX*        bdchgidx            /**< the index of the bound change, representing the point of time where
1354 	                                              *   the change took place, or NULL for the current local bounds */
1355 	   )
1356 	{
1357 	   assert(propdata != NULL);
1358 	   assert(boundtype == SCIP_BOUNDTYPE_LOWER || boundtype == SCIP_BOUNDTYPE_UPPER);
1359 	
1360 	   SCIPdebugMsg(scip, " -> add %s bound of variable <%s> as reason\n",
1361 	      getBoundtypeString(boundtype), SCIPvarGetName(var));
1362 	
1363 	   switch( boundtype )
1364 	   {
1365 	   case SCIP_BOUNDTYPE_LOWER:
1366 	      SCIP_CALL( SCIPaddConflictLb(scip, var, bdchgidx) );
1367 	      break;
1368 	   case SCIP_BOUNDTYPE_UPPER:
1369 	      SCIP_CALL( SCIPaddConflictUb(scip, var, bdchgidx) );
1370 	      break;
1371 	   default:
1372 	      SCIPerrorMessage("invalid bound type <%d>\n", boundtype);
1373 	      SCIPABORT();
1374 	      return SCIP_INVALIDDATA; /*lint !e527*/
1375 	   }
1376 	
1377 	   return SCIP_OKAY;
1378 	}
1379 	
1380 	/** relaxes bound of give variable as long as the given inference bound still leads to a cutoff and add that bound
1381 	 *  change to the conflict set
1382 	 */
1383 	static
1384 	SCIP_RETCODE relaxVbdvar(
1385 	   SCIP*                 scip,               /**< SCIP data structure */
1386 	   SCIP_VAR*             var,                /**< variable for which the upper bound should be relaxed */
1387 	   SCIP_BOUNDTYPE        boundtype,          /**< boundtype used for the variable bound variable */
1388 	   SCIP_BDCHGIDX*        bdchgidx,           /**< the index of the bound change, representing the point of time where
1389 	                                              *   the change took place, or NULL for the current local bounds */
1390 	   SCIP_Real             relaxedbd           /**< relaxed bound */
1391 	   )
1392 	{
1393 	   if( boundtype == SCIP_BOUNDTYPE_LOWER )
1394 	   {
1395 	      SCIP_CALL( SCIPaddConflictRelaxedLb(scip, var, bdchgidx, relaxedbd) );
1396 	   }
1397 	   else
1398 	   {
1399 	      assert(boundtype == SCIP_BOUNDTYPE_UPPER);
1400 	      SCIP_CALL( SCIPaddConflictRelaxedUb(scip, var, bdchgidx, relaxedbd) );
1401 	   }
1402 	
1403 	   return SCIP_OKAY;
1404 	}
1405 	
1406 	/** compute the relaxed bound which is sufficient to propagate the inference lower bound of given variable */
1407 	static
1408 	SCIP_Real computeRelaxedLowerbound(
1409 	   SCIP*                 scip,               /**< SCIP data structure */
1410 	   SCIP_VAR*             var,                /**< variable which was propagated */
1411 	   SCIP_Real             inferlb,            /**< inference lower bound */
1412 	   SCIP_Real             coef,               /**< inference variable bound coefficient used */
1413 	   SCIP_Real             constant            /**< inference variable bound constant used */
1414 	   )
1415 	{
1416 	   SCIP_Real relaxedbd;
1417 	
1418 	   if( SCIPvarIsIntegral(var) && inferlb < SCIPgetHugeValue(scip) * SCIPfeastol(scip) )
1419 	      relaxedbd = (inferlb - 1.0 + 2*SCIPfeastol(scip) - constant) / coef;
1420 	   else
1421 	      relaxedbd = (inferlb - constant) / coef;
1422 	
1423 	   /* check the computed relaxed lower/upper bound is a proper reason for the inference bound which has to be explained */
1424 	   assert(SCIPisEQ(scip, inferlb, SCIPadjustedVarLb(scip, var, relaxedbd * coef + constant)));
1425 	
1426 	   if( coef > 0.0 )
1427 	      relaxedbd += SCIPfeastol(scip);
1428 	   else
1429 	      relaxedbd -= SCIPfeastol(scip);
1430 	
1431 	   return relaxedbd;
1432 	}
1433 	
1434 	/** analyzes an infeasibility which was reached by updating the lower bound of the inference variable above its upper
1435 	 *  bound
1436 	 */
1437 	static
1438 	SCIP_RETCODE analyzeConflictLowerbound(
1439 	   SCIP*                 scip,               /**< SCIP data structure */
1440 	   SCIP_PROPDATA*        propdata,           /**< propagator data */
1441 	   SCIP_VAR*             infervar,           /**< variable which led to a cutoff */
1442 	   SCIP_Real             inferlb,            /**< lower bound which led to infeasibility */
1443 	   SCIP_VAR*             vbdvar,             /**< variable which is the reason for the lower bound change */
1444 	   SCIP_BOUNDTYPE        boundtype,          /**< bound which is the reason for the lower bound change */
1445 	   SCIP_Real             coef,               /**< inference variable bound coefficient used */
1446 	   SCIP_Real             constant,           /**< inference variable bound constant used */
1447 	   SCIP_Bool             canwide             /**< can bound widening be used (for vbounds) or not
1448 	                                              *   (for implications or cliques) */
1449 	   )
1450 	{
1451 	   assert(scip != NULL);
1452 	   assert(propdata != NULL);
1453 	   assert(infervar != NULL);
1454 	   assert(SCIPisEQ(scip, SCIPvarGetUbLocal(infervar), SCIPgetVarUbAtIndex(scip, infervar, NULL, FALSE)));
1455 	   assert(SCIPisEQ(scip, SCIPgetVarUbAtIndex(scip, infervar, NULL, TRUE), SCIPgetVarUbAtIndex(scip, infervar, NULL, FALSE)));
1456 	   assert(SCIPisGT(scip, inferlb, SCIPvarGetUbLocal(infervar)));
1457 	   assert(SCIPgetStage(scip) == SCIP_STAGE_SOLVING);
1458 	
1459 	   /* check if conflict analysis is applicable */
1460 	   if( !SCIPisConflictAnalysisApplicable(scip) )
1461 	      return SCIP_OKAY;
1462 	
1463 	   if( canwide && propdata->usebdwidening )
1464 	   {
1465 	      SCIP_Real relaxedbd;
1466 	      SCIP_Real relaxedub;
1467 	
1468 	      SCIPdebugMsg(scip, "try to create conflict using bound widening order: inference variable, variable bound variable\n");
1469 	
1470 	      /* initialize conflict analysis, and add all variables of infeasible constraint to conflict candidate queue */
1471 	      SCIP_CALL( SCIPinitConflictAnalysis(scip, SCIP_CONFTYPE_PROPAGATION, FALSE) );
1472 	
1473 	      /* adjust lower bound */
1474 	      inferlb = SCIPadjustedVarLb(scip, infervar, inferlb);
1475 	
1476 	      /* compute a relaxed upper bound which would be sufficient to be still infeasible */
1477 	      if( SCIPvarIsIntegral(infervar) )
1478 	         relaxedub = inferlb - 1.0;
1479 	      else
1480 	         relaxedub = inferlb - 2*SCIPfeastol(scip);
1481 	
1482 	      /* try to relax inference variable upper bound such that the infeasibility is still given */
1483 	      SCIP_CALL( SCIPaddConflictRelaxedUb(scip, infervar, NULL, relaxedub) );
1484 	
1485 	      /* collect the upper bound which is reported to the conflict analysis */
1486 	      relaxedub = SCIPgetConflictVarUb(scip, infervar);
1487 	
1488 	      /* adjust inference bound with respect to the upper bound reported to the conflict analysis */
1489 	      if( SCIPvarIsIntegral(infervar) )
1490 	         relaxedub = relaxedub + 1.0;
1491 	      else
1492 	         relaxedub = relaxedub + 2*SCIPfeastol(scip);
1493 	
1494 	      /* compute the relaxed bound which is sufficient to propagate the inference lower bound of given variable */
1495 	      relaxedbd = computeRelaxedLowerbound(scip, infervar, relaxedub, coef, constant);
1496 	
1497 	      /* try to relax variable bound variable */
1498 	      SCIP_CALL( relaxVbdvar(scip, vbdvar, boundtype, NULL, relaxedbd) );
1499 	
1500 	      /* analyze the conflict */
1501 	      SCIP_CALL( SCIPanalyzeConflict(scip, 0, NULL) );
1502 	   }
1503 	   else
1504 	   {
1505 	      /* initialize conflict analysis, and add all variables of infeasible constraint to conflict candidate queue */
1506 	      SCIP_CALL( SCIPinitConflictAnalysis(scip, SCIP_CONFTYPE_PROPAGATION, FALSE) );
1507 	
1508 	      /* add upper bound of the variable for which we tried to change the lower bound */
1509 	      SCIP_CALL( SCIPaddConflictUb(scip, infervar, NULL) );
1510 	
1511 	      /* add (correct) bound of the variable which let to the new lower bound */
1512 	      SCIP_CALL( resolvePropagation(scip, propdata, vbdvar, boundtype, NULL) );
1513 	
1514 	      /* analyze the conflict */
1515 	      SCIP_CALL( SCIPanalyzeConflict(scip, 0, NULL) );
1516 	   }
1517 	
1518 	   return SCIP_OKAY;
1519 	}
1520 	
1521 	/** compute the relaxed bound which is sufficient to propagate the inference upper bound of given variable */
1522 	static
1523 	SCIP_Real computeRelaxedUpperbound(
1524 	   SCIP*                 scip,               /**< SCIP data structure */
1525 	   SCIP_VAR*             var,                /**< variable which was propagated */
1526 	   SCIP_Real             inferub,            /**< inference upper bound */
1527 	   SCIP_Real             coef,               /**< inference variable bound coefficient used */
1528 	   SCIP_Real             constant            /**< inference variable bound constant used */
1529 	   )
1530 	{
1531 	   SCIP_Real relaxedbd;
1532 	
1533 	   if( SCIPvarIsIntegral(var) && inferub < SCIPgetHugeValue(scip) * SCIPfeastol(scip) )
1534 	      relaxedbd = (inferub + 1.0 - 2*SCIPfeastol(scip) - constant) / coef;
1535 	   else
1536 	      relaxedbd = (inferub - constant) / coef;
1537 	
1538 	   /* check the computed relaxed lower/upper bound is a proper reason for the inference bound which has to be explained */
1539 	   assert(SCIPisEQ(scip, inferub, SCIPadjustedVarUb(scip, var, relaxedbd * coef + constant)));
1540 	
1541 	   if( coef > 0.0 )
1542 	      relaxedbd -= SCIPfeastol(scip);
1543 	   else
1544 	      relaxedbd += SCIPfeastol(scip);
1545 	
1546 	   return relaxedbd;
1547 	}
1548 	
1549 	/** analyzes an infeasibility which was reached by updating the upper bound of the inference variable below its lower
1550 	 *  bound
1551 	 */
1552 	static
1553 	SCIP_RETCODE analyzeConflictUpperbound(
1554 	   SCIP*                 scip,               /**< SCIP data structure */
1555 	   SCIP_PROPDATA*        propdata,           /**< propagator data */
1556 	   SCIP_VAR*             infervar,           /**< variable which led to a cutoff */
1557 	   SCIP_Real             inferub,            /**< upper bound which led to infeasibility */
1558 	   SCIP_VAR*             vbdvar,             /**< variable which is the reason for the upper bound change */
1559 	   SCIP_BOUNDTYPE        boundtype,          /**< bound which is the reason for the upper bound change */
1560 	   SCIP_Real             coef,               /**< inference variable bound coefficient used */
1561 	   SCIP_Real             constant,           /**< inference variable bound constant used */
1562 	   SCIP_Bool             canwide             /**< can bound widening be used (for vbounds) or not (for inplications or cliques) */
1563 	   )
1564 	{
1565 	   assert(scip != NULL);
1566 	   assert(propdata != NULL);
1567 	   assert(infervar != NULL);
1568 	   assert(SCIPisEQ(scip, SCIPvarGetLbLocal(infervar), SCIPgetVarLbAtIndex(scip, infervar, NULL, FALSE)));
1569 	   assert(SCIPisEQ(scip, SCIPgetVarLbAtIndex(scip, infervar, NULL, TRUE), SCIPgetVarLbAtIndex(scip, infervar, NULL, FALSE)));
1570 	   assert(SCIPisLT(scip, inferub, SCIPvarGetLbLocal(infervar)));
1571 	   assert(SCIPgetStage(scip) == SCIP_STAGE_SOLVING);
1572 	
1573 	   /* check if conflict analysis is applicable */
1574 	   if( !SCIPisConflictAnalysisApplicable(scip) )
1575 	      return SCIP_OKAY;
1576 	
1577 	   if( canwide && propdata->usebdwidening )
1578 	   {
1579 	      SCIP_Real relaxedbd;
1580 	      SCIP_Real relaxedlb;
1581 	
1582 	      SCIPdebugMsg(scip, "try to create conflict using bound widening order: inference variable, variable bound variable\n");
1583 	
1584 	      /* initialize conflict analysis, and add all variables of infeasible constraint to conflict candidate queue */
1585 	      SCIP_CALL( SCIPinitConflictAnalysis(scip, SCIP_CONFTYPE_PROPAGATION, FALSE) );
1586 	
1587 	      /* adjust upper bound */
1588 	      inferub = SCIPadjustedVarUb(scip, infervar, inferub);
1589 	
1590 	      /* compute a relaxed lower bound which would be sufficient to be still infeasible */
1591 	      if( SCIPvarIsIntegral(infervar) )
1592 	         relaxedlb = inferub + 1.0;
1593 	      else
1594 	         relaxedlb = inferub + 2*SCIPfeastol(scip);
1595 	
1596 	      /* try to relax inference variable lower bound such that the infeasibility is still given */
1597 	      SCIP_CALL( SCIPaddConflictRelaxedLb(scip, infervar, NULL, relaxedlb) );
1598 	
1599 	      /* collect the lower bound which is reported to the conflict analysis */
1600 	      relaxedlb = SCIPgetConflictVarLb(scip, infervar);
1601 	
1602 	      /* adjust inference bound with respect to the upper bound reported to the conflict analysis */
1603 	      if( SCIPvarIsIntegral(infervar) )
1604 	         relaxedlb = relaxedlb - 1.0;
1605 	      else
1606 	         relaxedlb = relaxedlb - 2*SCIPfeastol(scip);
1607 	
1608 	      /* compute the relaxed bound which is sufficient to propagate the inference upper bound of given variable */
1609 	      relaxedbd = computeRelaxedUpperbound(scip, infervar, relaxedlb, coef, constant);
1610 	
1611 	      /* try to relax variable bound variable */
1612 	      SCIP_CALL( relaxVbdvar(scip, vbdvar, boundtype, NULL, relaxedbd) );
1613 	
1614 	      /* analyze the conflict */
1615 	      SCIP_CALL( SCIPanalyzeConflict(scip, 0, NULL) );
1616 	   }
1617 	   else
1618 	   {
1619 	      /* initialize conflict analysis, and add all variables of infeasible constraint to conflict candidate queue */
1620 	      SCIP_CALL( SCIPinitConflictAnalysis(scip, SCIP_CONFTYPE_PROPAGATION, FALSE) );
1621 	
1622 	      /* add lower bound of the variable for which we tried to change the upper bound */
1623 	      SCIP_CALL( SCIPaddConflictLb(scip, infervar, NULL) );
1624 	
1625 	      /* add (correct) bound of the variable which let to the new upper bound */
1626 	      SCIP_CALL( resolvePropagation(scip, propdata, vbdvar, boundtype, NULL) );
1627 	
1628 	      /* analyze the conflict */
1629 	      SCIP_CALL( SCIPanalyzeConflict(scip, 0, NULL) );
1630 	   }
1631 	
1632 	   return SCIP_OKAY;
1633 	}
1634 	
1635 	/* tries to tighten the (global) lower bound of the given variable to the given new bound */
1636 	static
1637 	SCIP_RETCODE tightenVarLb(
1638 	   SCIP*                 scip,               /**< SCIP data structure */
1639 	   SCIP_PROP*            prop,               /**< vbounds propagator */
1640 	   SCIP_PROPDATA*        propdata,           /**< propagator data */
1641 	   SCIP_VAR*             var,                /**< variable whose lower bound should be tightened */
1642 	   SCIP_Real             newlb,              /**< new lower bound for the variable */
1643 	   SCIP_Bool             global,             /**< is the bound globally valid? */
1644 	   SCIP_VAR*             vbdvar,             /**< variable which is the reason for the lower bound change */
1645 	   SCIP_BOUNDTYPE        boundtype,          /**< bound which is the reason for the lower bound change */
1646 	   SCIP_Bool             force,              /**< should domain changes for continuous variables be forced */
1647 	   SCIP_Real             coef,               /**< coefficient in vbound constraint causing the propagation;
1648 	                                              *   or 0.0 if propagation is caused by clique or implication */
1649 	   SCIP_Real             constant,           /**< constant in vbound constraint causing the propagation;
1650 	                                              *   or 0.0 if propagation is caused by clique or implication */
1651 	   SCIP_Bool             canwide,            /**< can bound widening be used (for vbounds) or not (for inplications or cliques) */
1652 	   int*                  nchgbds,            /**< pointer to increase, if a bound was changed */
1653 	   SCIP_RESULT*          result              /**< pointer to store the result of the propagation */
1654 	   )
1655 	{
1656 	   INFERINFO inferinfo;
1657 	   SCIP_Real lb;
1658 	   SCIP_Bool tightened;
1659 	   SCIP_Bool infeasible;
1660 	
1661 	   assert(scip != NULL);
1662 	   assert(prop != NULL);
1663 	   assert(propdata != NULL);
1664 	   assert(var != NULL);
1665 	   assert(nchgbds != NULL);
1666 	   assert(result != NULL);
1667 	
1668 	   lb = SCIPvarGetLbLocal(var);
1669 	
1670 	   /* check that the new upper bound is better */
1671 	   if( (SCIPvarIsIntegral(var) && newlb - lb > 0.5) || (force && SCIPisGT(scip, newlb, lb)) )
1672 	      force = TRUE;
1673 	   else
1674 	      force = FALSE;
1675 	
1676 	   /* try to tighten the lower bound */
1677 	   if( global )
1678 	   {
1679 	      SCIP_CALL( SCIPtightenVarLbGlobal(scip, var, newlb, force, &infeasible, &tightened) );
1680 	   }
1681 	   else
1682 	   {
1683 	      inferinfo = getInferInfo(boundtype == SCIP_BOUNDTYPE_LOWER ? varGetLbIndex(propdata, vbdvar) : varGetUbIndex(propdata, vbdvar), boundtype);
1684 	
1685 	      SCIP_CALL( SCIPinferVarLbProp(scip, var, newlb, prop, inferInfoToInt(inferinfo), force, &infeasible, &tightened) );
1686 	   }
1687 	
1688 	   if( infeasible )
1689 	   {
1690 	      /* the infeasible results comes from the fact that the new lower bound lies above the current upper bound */
1691 	      assert(SCIPisGT(scip, newlb, SCIPvarGetUbLocal(var)));
1692 	      assert(!global || SCIPisGT(scip, newlb, SCIPvarGetUbGlobal(var)));
1693 	
1694 	      SCIPdebugMsg(scip, "tightening%s lower bound of variable <%s> to %g due the %s bound of variable <%s> led to infeasibility\n",
1695 	         (global ? " global" : ""), SCIPvarGetName(var), newlb, getBoundtypeString(boundtype), SCIPvarGetName(vbdvar));
1696 	
1697 	      if( global )
1698 	      {
1699 	         /* cutoff the root node */
1700 	         SCIP_CALL( SCIPcutoffNode(scip, SCIPgetRootNode(scip)) );
1701 	      }
1702 	      else
1703 	      {
1704 	         /* analyzes a infeasibility via conflict analysis */
1705 	         SCIP_CALL( analyzeConflictLowerbound(scip, propdata, var, newlb, vbdvar, boundtype, coef, constant, canwide) );
1706 	      }
1707 	      *result = SCIP_CUTOFF;
1708 	   }
1709 	   else if( tightened )
1710 	   {
1711 	      SCIPdebugMsg(scip, "tightened%s lower bound of variable <%s> to %g due the %s bound of variable <%s>\n",
1712 	         (global ? " global" : ""), SCIPvarGetName(var), newlb, getBoundtypeString(boundtype), SCIPvarGetName(vbdvar));
1713 	      (*nchgbds)++;
1714 	   }
1715 	
1716 	   return SCIP_OKAY;
1717 	}
1718 	
1719 	/* tries to tighten the (global) upper bound of the given variable to the given new bound */
1720 	static
1721 	SCIP_RETCODE tightenVarUb(
1722 	   SCIP*                 scip,               /**< SCIP data structure */
1723 	   SCIP_PROP*            prop,               /**< vbounds propagator */
1724 	   SCIP_PROPDATA*        propdata,           /**< propagator data */
1725 	   SCIP_VAR*             var,                /**< variable whose upper bound should be tightened */
1726 	   SCIP_Real             newub,              /**< new upper bound of the variable */
1727 	   SCIP_Bool             global,             /**< is the bound globally valid? */
1728 	   SCIP_VAR*             vbdvar,             /**< variable which is the reason for the upper bound change */
1729 	   SCIP_BOUNDTYPE        boundtype,          /**< bound which is the reason for the upper bound change */
1730 	   SCIP_Bool             force,              /**< should domain changes for continuous variables be forced */
1731 	   SCIP_Real             coef,               /**< coefficient in vbound constraint causing the propagation;
1732 	                                              *   or 0.0 if propagation is caused by clique or implication */
1733 	   SCIP_Real             constant,           /**< constant in vbound constraint causing the propagation;
1734 	                                              *   or 0.0 if propagation is caused by clique or implication */
1735 	   SCIP_Bool             canwide,            /**< can bound widening be used (for vbounds) or not (for inplications or cliques) */
1736 	   int*                  nchgbds,            /**< pointer to increase, if a bound was changed */
1737 	   SCIP_RESULT*          result              /**< pointer to store the result of the propagation */
1738 	   )
1739 	{
1740 	   INFERINFO inferinfo;
1741 	   SCIP_Real ub;
1742 	   SCIP_Bool tightened;
1743 	   SCIP_Bool infeasible;
1744 	
1745 	   assert(scip != NULL);
1746 	   assert(prop != NULL);
1747 	   assert(propdata != NULL);
1748 	   assert(var != NULL);
1749 	   assert(nchgbds != NULL);
1750 	   assert(result != NULL);
1751 	
1752 	   ub = SCIPvarGetUbLocal(var);
1753 	
1754 	   /* check that the new upper bound is better */
1755 	   if( (SCIPvarIsIntegral(var) && ub - newub > 0.5) || (force && SCIPisLT(scip, newub, ub)) )
1756 	      force = TRUE;
1757 	   else
1758 	      force = FALSE;
1759 	
1760 	   /* try to tighten the upper bound */
1761 	   if( global )
1762 	   {
1763 	      SCIP_CALL( SCIPtightenVarUbGlobal(scip, var, newub, force, &infeasible, &tightened) );
1764 	   }
1765 	   else
1766 	   {
1767 	      inferinfo = getInferInfo(boundtype == SCIP_BOUNDTYPE_LOWER ? varGetLbIndex(propdata, vbdvar) : varGetUbIndex(propdata, vbdvar), boundtype);
1768 	
1769 	      SCIP_CALL( SCIPinferVarUbProp(scip, var, newub, prop, inferInfoToInt(inferinfo), force, &infeasible, &tightened) );
1770 	   }
1771 	
1772 	   if( infeasible )
1773 	   {
1774 	      /* the infeasible results comes from the fact that the new upper bound lies below the current lower bound */
1775 	      assert(SCIPisLT(scip, newub, SCIPvarGetLbLocal(var)));
1776 	      assert(!global || SCIPisLT(scip, newub, SCIPvarGetLbGlobal(var)));
1777 	
1778 	      SCIPdebugMsg(scip, "tightening%s upper bound of variable <%s> to %g due the %s bound of variable <%s> led to infeasibility\n",
1779 	         (global ? " global" : ""), SCIPvarGetName(var), newub, getBoundtypeString(boundtype), SCIPvarGetName(vbdvar));
1780 	
1781 	      if( global )
1782 	      {
1783 	         /* cutoff the root node */
1784 	         SCIP_CALL( SCIPcutoffNode(scip, SCIPgetRootNode(scip)) );
1785 	      }
1786 	      else
1787 	      {
1788 	         /* analyzes a infeasibility via conflict analysis */
1789 	         SCIP_CALL( analyzeConflictUpperbound(scip, propdata, var, newub, vbdvar, boundtype, coef, constant, canwide) );
1790 	      }
1791 	      *result = SCIP_CUTOFF;
1792 	   }
1793 	   else if( tightened )
1794 	   {
1795 	      SCIPdebugMsg(scip, "tightened%s upper bound of variable <%s> to %g due the %s bound of variable <%s>\n",
1796 	         (global ? " global" : ""), SCIPvarGetName(var), newub, getBoundtypeString(boundtype), SCIPvarGetName(vbdvar));
1797 	      (*nchgbds)++;
1798 	   }
1799 	
1800 	   return SCIP_OKAY;
1801 	}
1802 	
1803 	/** performs propagation of variables lower and upper bounds, implications, and cliques */
1804 	static
1805 	SCIP_RETCODE propagateVbounds(
1806 	   SCIP*                 scip,               /**< SCIP data structure */
1807 	   SCIP_PROP*            prop,               /**< vbounds propagator */
1808 	   SCIP_Bool             force,              /**< should domain changes for continuous variables be forced */
1809 	   SCIP_RESULT*          result              /**< pointer to store the result of the propagation */
1810 	   )
1811 	{
1812 	   SCIP_PROPDATA* propdata;
1813 	   SCIP_VAR** vars;
1814 	   SCIP_VAR* startvar;
1815 	   SCIP_BOUNDTYPE starttype;
1816 	   SCIP_Real startbound;
1817 	   SCIP_Real globalbound;
1818 	   int* queuelist = NULL;
1819 	   int nqueuelist = 0;
1820 	   int startpos;
1821 	   int topopos;
1822 	   int v;
1823 	   int n;
1824 	   int nchgbds;
1825 	   int nbounds;
1826 	   SCIP_Bool lower;
1827 	   SCIP_Bool global;
1828 	
1829 	   assert(scip != NULL);
1830 	   assert(prop != NULL);
1831 	   assert(result != NULL);
1832 	
1833 	   (*result) = SCIP_DIDNOTRUN;
1834 	
1835 	   /* we do not run the propagator in presolving, because we want to avoid doing the expensive creation of the graph twice */
1836 	   if( SCIPgetStage(scip) == SCIP_STAGE_PRESOLVING )
1837 	      return SCIP_OKAY;
1838 	
1839 	   propdata = SCIPpropGetData(prop);
1840 	   assert(propdata != NULL);
1841 	
1842 	   /* initialize propagator data needed for propagation, if not done yet */
1843 	   if( !propdata->initialized )
1844 	   {
1845 	      SCIP_Bool infeasible;
1846 	
1847 	      SCIP_CALL( initData(scip, prop, &infeasible) );
1848 	
1849 	      if( infeasible )
1850 	      {
1851 	         *result = SCIP_CUTOFF;
1852 	         return SCIP_OKAY;
1853 	      }
1854 	   }
1855 	   assert(propdata->nbounds == 0 || propdata->propqueue != NULL);
1856 	
1857 	   vars = propdata->vars;
1858 	   nbounds = propdata->nbounds;
1859 	
1860 	   if( nbounds == 0 )
1861 	      return SCIP_OKAY;
1862 	
1863 	   /* propagate all variables if we are in repropagation */
1864 	   if( SCIPinRepropagation(scip) )
1865 	   {
1866 	      SCIP_VAR* var;
1867 	      int idx;
1868 	
1869 	      for( v = nbounds - 1; v >= 0; --v )
1870 	      {
1871 	         idx = propdata->topoorder[v];
1872 	         if( idx != -1 && !propdata->inqueue[v] )
1873 	         {
1874 	            var = vars[getVarIndex(idx)];
1875 	            lower = isIndexLowerbound(idx);
1876 	            if( !SCIPvarIsBinary(var) || (lower && SCIPvarGetLbLocal(var) > 0.5)
1877 	                  || (!lower && SCIPvarGetUbLocal(var) < 0.5) )
1878 	            {
1879 	               SCIP_CALL( SCIPpqueueInsert(propdata->propqueue, (void*)(size_t)(v + 1)) ); /*lint !e571 !e776*/
1880 	               propdata->inqueue[v] = TRUE;
1881 	            }
1882 	         }
1883 	      }
1884 	   }
1885 	
1886 	   /* return if no bound changes are in the priority queue (no changed bounds to handle since last propagation) */
1887 	   if( SCIPpqueueNElems(propdata->propqueue) == 0 )
1888 	      return SCIP_OKAY;
1889 	
1890 	   nchgbds = 0;
1891 	
1892 	   (*result) = SCIP_DIDNOTFIND;
1893 	
1894 	   /* allocate space for variables added to the queue - needed to clean up data */
1895 	   SCIP_CALL( SCIPallocBufferArray(scip, &queuelist, nbounds) );
1896 	
1897 	   SCIPdebugMsg(scip, "varbound propagator: %d elements in the propagation queue\n", SCIPpqueueNElems(propdata->propqueue));
1898 	
1899 	   /* get variable bound of highest priority from priority queue and try to deduce bound changes for other variables;
1900 	    * the priority queue is ordered w.r.t the topological sort of the varbound graph
1901 	    */
1902 	   while( SCIPpqueueNElems(propdata->propqueue) > 0 )
1903 	   {
1904 	      /* coverity[pointer_conversion_loses_bits] */
1905 	      topopos = ((int)(size_t)SCIPpqueueRemove(propdata->propqueue)) - 1;
1906 	      assert(propdata->inqueue[topopos]);
1907 	      startpos = propdata->topoorder[topopos];
1908 	      assert(startpos >= 0);
1909 	      queuelist[nqueuelist++] = topopos;
1910 	      assert( nqueuelist <= nbounds );
1911 	
1912 	      /* do not directly set propdata->inqueue[topopos] = FALSE: we allow only one propagation sweep through the
1913 	       * topologically ordered bounds; otherwise an infinite loop could occur */
1914 	
1915 	      startvar = vars[getVarIndex(startpos)];
1916 	      starttype = getBoundtype(startpos);
1917 	      lower = (starttype == SCIP_BOUNDTYPE_LOWER);
1918 	      startbound = ( lower ? SCIPvarGetLbLocal(startvar) : SCIPvarGetUbLocal(startvar) );
1919 	      globalbound = ( lower ? SCIPvarGetLbGlobal(startvar) : SCIPvarGetUbGlobal(startvar));
1920 	      global = SCIPisEQ(scip, startbound, globalbound);
1921 	
1922 	      SCIPdebugMsg(scip, "propagate new %s bound of %g of variable <%s>:\n",
1923 	         getBoundtypeString(starttype), startbound, SCIPvarGetName(startvar));
1924 	
1925 	      /* there should be neither implications nor cliques for non-binary variables */
1926 	      assert(SCIPvarIsBinary(startvar) || SCIPvarGetNImpls(startvar, lower) == 0);
1927 	      assert(SCIPvarIsBinary(startvar) || SCIPvarGetNCliques(startvar, lower) == 0);
1928 	
1929 	      if( SCIPvarIsBinary(startvar) )
1930 	      {
1931 	         /* we only propagate binary variables if the lower bound changed to 1.0 or the upper bound changed to 0.0 */
1932 	         if( lower != (startbound > 0.5) )
1933 	            continue;
1934 	
1935 	         /* propagate implications */
1936 	         if( propdata->useimplics )
1937 	         {
1938 	            int nimplvars;
1939 	
1940 	            /* if the lower bound of the startvar was changed, it was fixed to 1.0, otherwise it was fixed to 0.0;
1941 	             * get all implications for this varfixing
1942 	             */
1943 	            nimplvars = SCIPvarGetNImpls(startvar, lower);
1944 	
1945 	            /* if there are implications for the varfixing, propagate them */
1946 	            if( nimplvars > 0 )
1947 	            {
1948 	               SCIP_VAR** implvars;
1949 	               SCIP_BOUNDTYPE* impltypes;
1950 	               SCIP_Real* implbounds;
1951 	               int* implids;
1952 	
1953 	               implvars = SCIPvarGetImplVars(startvar, lower);
1954 	               impltypes = SCIPvarGetImplTypes(startvar, lower);
1955 	               implbounds = SCIPvarGetImplBounds(startvar, lower);
1956 	               implids = SCIPvarGetImplIds(startvar, lower);
1957 	
1958 	               for( n = 0; n < nimplvars; ++n )
1959 	               {
1960 	                  /* implication is just a shortcut, so we do not propagate it now,
1961 	                   * because we will propagate the longer way, anyway
1962 	                   */
1963 	                  if( implids[n] < 0 )
1964 	                     continue;
1965 	
1966 	                  /* it might happen that implications point to inactive variables (normally, those are removed when a
1967 	                   * variable becomes inactive, but in some cases, it cannot be done), we have to ignore these variables
1968 	                   */
1969 	                  if( !SCIPvarIsActive(implvars[n]) )
1970 	                     continue;
1971 	
1972 	                  if( impltypes[n] == SCIP_BOUNDTYPE_LOWER )
1973 	                  {
1974 	                     SCIP_CALL( tightenVarLb(scip, prop, propdata, implvars[n], implbounds[n], global, startvar,
1975 	                           starttype, force, 0.0, 0.0, FALSE, &nchgbds, result) );
1976 	                  }
1977 	                  else
1978 	                  {
1979 	                     SCIP_CALL( tightenVarUb(scip, prop, propdata, implvars[n], implbounds[n], global, startvar,
1980 	                           starttype, force, 0.0, 0.0, FALSE, &nchgbds, result) );
1981 	                  }
1982 	
1983 	                  if( *result == SCIP_CUTOFF )
1984 	                     break;
1985 	               }
1986 	               if( *result == SCIP_CUTOFF )
1987 	                  break;
1988 	            }
1989 	         }
1990 	
1991 	         /* propagate cliques */
1992 	         if( propdata->usecliques )
1993 	         {
1994 	            int ncliques;
1995 	
1996 	            /* if the lower bound of the startvar was changed, it was fixed to 1.0, otherwise it was fixed to 0.0;
1997 	             * get all cliques for this varfixing
1998 	             */
1999 	            ncliques = SCIPvarGetNCliques(startvar, lower);
2000 	
2001 	            /* if there are cliques for the varfixing, propagate them */
2002 	            if( ncliques > 0 )
2003 	            {
2004 	               SCIP_CLIQUE** cliques;
2005 	               int j;
2006 	
2007 	               cliques = SCIPvarGetCliques(startvar, lower);
2008 	
2009 	               for( j = 0; j < ncliques; ++j )
2010 	               {
2011 	                  SCIP_VAR** cliquevars;
2012 	                  SCIP_Bool* cliquevals;
2013 	                  int ncliquevars;
2014 	
2015 	                  cliquevars = SCIPcliqueGetVars(cliques[j]);
2016 	                  cliquevals = SCIPcliqueGetValues(cliques[j]);
2017 	                  ncliquevars = SCIPcliqueGetNVars(cliques[j]);
2018 	
2019 	                  /* fix all variables except for the startvar to the value which is not in the clique */
2020 	                  for( n = 0; n < ncliquevars; ++n )
2021 	                  {
2022 	                     if( cliquevars[n] == startvar )
2023 	                        continue;
2024 	
2025 	                     /* try to tighten the bound */
2026 	                     if( cliquevals[n] )
2027 	                     {
2028 	                        /* unnegated variable is in clique, so it has to be fixed to 0.0 */
2029 	                        SCIP_CALL( tightenVarUb(scip, prop, propdata, cliquevars[n], 0.0, global, startvar, starttype,
2030 	                              force, 0.0, 0.0, FALSE, &nchgbds, result) );
2031 	                     }
2032 	                     else
2033 	                     {
2034 	                        /* negated variable is in clique, so it has to be fixed to 1.0 */
2035 	                        SCIP_CALL( tightenVarLb(scip, prop, propdata, cliquevars[n], 1.0, global, startvar, starttype,
2036 	                              force, 0.0, 0.0, FALSE, &nchgbds, result) );
2037 	                     }
2038 	
2039 	                     if( *result == SCIP_CUTOFF )
2040 	                        break;
2041 	                  }
2042 	               }
2043 	               if( *result == SCIP_CUTOFF )
2044 	                  break;
2045 	            }
2046 	         }
2047 	      }
2048 	
2049 	      /* propagate vbounds */
2050 	      if( propdata->usevbounds && ! SCIPisInfinity(scip, REALABS(startbound)) )
2051 	      {
2052 	         SCIP_VAR* boundedvar;
2053 	         SCIP_Real newbound;
2054 	         SCIP_Real coef;
2055 	         SCIP_Real constant;
2056 	
2057 	         /* iterate over all vbounds for the given bound */
2058 	         for( n = 0; n < propdata->nvbounds[startpos]; ++n )
2059 	         {
2060 	            boundedvar = vars[getVarIndex(propdata->vboundboundedidx[startpos][n])];
2061 	            coef = propdata->vboundcoefs[startpos][n];
2062 	            constant = propdata->vboundconstants[startpos][n];
2063 	
2064 	            /* compute new bound */
2065 	            newbound = startbound * coef + constant;
2066 	
2067 	            /* try to tighten the bound */
2068 	            if( isIndexLowerbound(propdata->vboundboundedidx[startpos][n]) )
2069 	            {
2070 	               SCIP_CALL( tightenVarLb(scip, prop, propdata, boundedvar, newbound, global, startvar, starttype, force,
2071 	                     coef, constant, TRUE, &nchgbds, result) );
2072 	            }
2073 	            else
2074 	            {
2075 	               SCIP_CALL( tightenVarUb(scip, prop, propdata, boundedvar, newbound, global, startvar, starttype, force,
2076 	                     coef, constant, TRUE, &nchgbds, result) );
2077 	            }
2078 	
2079 	            if( *result == SCIP_CUTOFF )
2080 	               break;
2081 	         }
2082 	         if( *result == SCIP_CUTOFF )
2083 	            break;
2084 	      }
2085 	   }
2086 	
2087 	   /* clean up inqueue */
2088 	   for( v = 0; v < nqueuelist; ++v )
2089 	   {
2090 	      assert( 0 <= queuelist[v] && queuelist[v] < nbounds );
2091 	      propdata->inqueue[queuelist[v]] = FALSE;
2092 	      assert( SCIPpqueueFind(propdata->propqueue, (void*)(size_t) (queuelist[v] + 1)) == -1 ); /*lint !e571*//*lint !e776*/
2093 	   }
2094 	   SCIPfreeBufferArray(scip, &queuelist);
2095 	
2096 	#ifdef SCIP_DEBUG
2097 	   for( v = 0; v < nbounds; ++v)
2098 	   {
2099 	      if( propdata->inqueue[v] )
2100 	         assert( SCIPpqueueFind(propdata->propqueue, (void*)(size_t) (v + 1)) >= 0 );
2101 	      else
2102 	         assert( SCIPpqueueFind(propdata->propqueue, (void*)(size_t) (v + 1)) == -1 );
2103 	   }
2104 	#endif
2105 	
2106 	   SCIPdebugMsg(scip, "tightened %d variable bounds\n", nchgbds);
2107 	
2108 	   /* set the result depending on whether bound changes were found or not */
2109 	   if( *result != SCIP_CUTOFF && nchgbds > 0 )
2110 	      (*result) = SCIP_REDUCEDDOM;
2111 	
2112 	   return SCIP_OKAY;
2113 	}
2114 	
2115 	/**@name Callback methods of propagator
2116 	 *
2117 	 * @{
2118 	 */
2119 	
2120 	/** copy method for propagator plugins (called when SCIP copies plugins) */
2121 	static
2122 	SCIP_DECL_PROPCOPY(propCopyVbounds)
2123 	{  /*lint --e{715}*/
2124 	   assert(scip != NULL);
2125 	   assert(prop != NULL);
2126 	   assert(strcmp(SCIPpropGetName(prop), PROP_NAME) == 0);
2127 	
2128 	   /* call inclusion method of propagator */
2129 	   SCIP_CALL( SCIPincludePropVbounds(scip) );
2130 	
2131 	   return SCIP_OKAY;
2132 	}
2133 	
2134 	/** destructor of propagator to free user data (called when SCIP is exiting) */
2135 	static
2136 	SCIP_DECL_PROPFREE(propFreeVbounds)
2137 	{  /*lint --e{715}*/
2138 	   SCIP_PROPDATA* propdata;
2139 	
2140 	   /* free propagator data */
2141 	   propdata = SCIPpropGetData(prop);
2142 	
2143 	   SCIPfreeBlockMemory(scip, &propdata);
2144 	   SCIPpropSetData(prop, NULL);
2145 	
2146 	   return SCIP_OKAY;
2147 	}
2148 	
2149 	/** presolving initialization method of propagator (called when presolving is about to begin) */
2150 	static
2151 	SCIP_DECL_PROPINITPRE(propInitpreVbounds)
2152 	{  /*lint --e{715}*/
2153 	   SCIP_PROPDATA* propdata;
2154 	
2155 	   propdata = SCIPpropGetData(prop);
2156 	   assert(propdata != NULL);
2157 	
2158 	   propdata->lastpresolncliques = 0;
2159 	
2160 	   return SCIP_OKAY;
2161 	}
2162 	
2163 	/** solving process deinitialization method of propagator (called before branch and bound process data is freed) */
2164 	static
2165 	SCIP_DECL_PROPEXITSOL(propExitsolVbounds)
2166 	{  /*lint --e{715}*/
2167 	   SCIP_PROPDATA* propdata;
2168 	   int v;
2169 	
2170 	   propdata = SCIPpropGetData(prop);
2171 	   assert(propdata != NULL);
2172 	
2173 	   /* free data stored for propagation */
2174 	   if( propdata->initialized )
2175 	   {
2176 	      /* drop all variable events */
2177 	      SCIP_CALL( dropEvents(scip, propdata) );
2178 	
2179 	      /* release all variables */
2180 	      for( v = 0; v < propdata->nbounds; ++v )
2181 	      {
2182 	         /* free vbound data */
2183 	         if( propdata->vboundsize[v] > 0 )
2184 	         {
2185 	            SCIPfreeMemoryArray(scip, &propdata->vboundboundedidx[v]);
2186 	            SCIPfreeMemoryArray(scip, &propdata->vboundcoefs[v]);
2187 	            SCIPfreeMemoryArray(scip, &propdata->vboundconstants[v]);
2188 	         }
2189 	      }
2190 	
2191 	      /* free priority queue */
2192 	      SCIPpqueueFree(&propdata->propqueue);
2193 	
2194 	      /* free arrays */
2195 	      SCIPfreeBlockMemoryArray(scip, &propdata->vboundsize, propdata->nbounds);
2196 	      SCIPfreeBlockMemoryArray(scip, &propdata->nvbounds, propdata->nbounds);
2197 	      SCIPfreeBlockMemoryArray(scip, &propdata->vboundconstants, propdata->nbounds);
2198 	      SCIPfreeBlockMemoryArray(scip, &propdata->vboundcoefs, propdata->nbounds);
2199 	      SCIPfreeBlockMemoryArray(scip, &propdata->vboundboundedidx, propdata->nbounds);
2200 	      SCIPfreeBlockMemoryArray(scip, &propdata->inqueue, propdata->nbounds);
2201 	      SCIPfreeBlockMemoryArray(scip, &propdata->topoorder, propdata->nbounds);
2202 	
2203 	      /* free variable array and hashmap */
2204 	      SCIPhashmapFree(&propdata->varhashmap);
2205 	      SCIPfreeBlockMemoryArray(scip, &propdata->vars, propdata->nbounds / 2);
2206 	   }
2207 	
2208 	   /* reset propagation data */
2209 	   resetPropdata(propdata);
2210 	
2211 	   return SCIP_OKAY;
2212 	}
2213 	
2214 	/** performs Tarjan's algorithm for strongly connected components in the implicitly given directed implication graph
2215 	 *  from the given start index; each variable x is represented by two nodes lb(x) = 2*idx(x) and ub(x) = 2*idx(x)+1
2216 	 *  where lb(x) means that the lower bound of x should be changed, i.e., that x is fixed to 1, and vice versa.
2217 	 *
2218 	 *  The algorithm is an iterative version of Tarjans algorithm
2219 	 *  (see https://en.wikipedia.org/wiki/Tarjan%27s_strongly_connected_components_algorithm)
2220 	 *  with some additional tweaks.
2221 	 *  Each clique x_1 + ... + x_k <= 1 is represented by k(k-1) arcs (lb(x_i),ub(x_j)), j != i.
2222 	 *  This quadratic number can blow up the running time of Tarjan's algorithm, which is linear in the number of
2223 	 *  nodes and arcs of the graph. However, it suffices to consider only k of these arcs during the course of the algorithm.
2224 	 *  To this end, when we first come to a node lb(x_i) of the clique, traverse all arcs (lb(x_i),ub(x_j)) for this particular i,
2225 	 *  and store that we entered the clique via lb(x_i). Next time we come to any node lb(x_i') of the clique, we know
2226 	 *  that the only arc pointing to an unvisited node is (lb(x_i'),ub(x_i)), all other edges can be disregarded.
2227 	 *  After that, we can disregard the clique for the further search.
2228 	 *  Additionally, we try to identify infeasible fixings for binary variables. Those can be given by a path
2229 	 *  from x=1 to x=0 (or vice versa) or if x=0 (or 1) implies both y=0 and y=1.
2230 	 */
2231 	static
2232 	SCIP_RETCODE tarjan(
2233 	   SCIP*                 scip,               /**< SCIP data structure */
2234 	   int                   startnode,          /**< node to start the depth-first-search */
2235 	   int*                  startindex,         /**< next index to assign to a processed node */
2236 	   SCIP_Shortbool*       nodeonstack,        /**< array to store the whether a each node is on the stack */
2237 	   int*                  nodeindex,          /**< array to store the dfs index for each node */
2238 	   int*                  nodelowlink,        /**< array to store the lowlink for each node */
2239 	   SCIP_Shortbool*       nodeinfeasible,     /**< array to store whether the fixing of a node was detected to be infeasible */
2240 	   int*                  dfsstack,           /**< array of size number of nodes to store the stack */
2241 	   int*                  predstackidx,       /**< for each node on the stack: stack position of its predecessor in the Tarjan search */
2242 	   int*                  stacknextclique,    /**< array of size number of nodes to store the next clique to be regarded in
2243 	                                              *   the algorithm for all nodes on the stack */
2244 	   int*                  stacknextcliquevar, /**< array of size number of nodes to store the next variable in the next clique to be
2245 	                                              * regarded in the algorithm for all nodes on the stack */
2246 	   int*                  topoorder,          /**< array with reverse (almost) topological ordering of the nodes */
2247 	   int*                  nordered,           /**< number of ordered nodes (disconnected nodes are disregarded) */
2248 	   int*                  cliquefirstentry,   /**< node from which a clique was entered for the first time; needed because when
2249 	                                              *   entering the clique a second time, only the other bound corresponding to this node
2250 	                                              *   remains to be processed */
2251 	   int*                  cliquecurrentexit,  /**< for cliques which define an arc on the current path: target node of this arc */
2252 	   int*                  sccvars,            /**< array with all nontrivial strongly connected components in the graph */
2253 	   int*                  sccstarts,          /**< start indices of SCCs in sccvars array; one additional entry at the end
2254 	                                              *   to give length of used part of sccvars array */
2255 	   int*                  nsccs,              /**< pointer to store number of strongly connected components */
2256 	   int*                  infeasnodes,        /**< sparse array with node indices of infeasible nodes */
2257 	   int*                  ninfeasnodes,       /**< pointer to store the number of infeasible nodes */
2258 	   SCIP_Bool*            infeasible          /**< pointer to store whether an infeasibility was detected */
2259 	   )
2260 	{
2261 	   SCIP_VAR** vars;
2262 	   SCIP_VAR* startvar;
2263 	   SCIP_Bool lower;
2264 	   int label = *startindex;
2265 	   int stacksize;
2266 	   int currstackidx;
2267 	   int curridx;
2268 	   int idx;
2269 	
2270 	   assert(startnode >= 0);
2271 	   assert(startnode < 2 * (SCIPgetNVars(scip) - SCIPgetNContVars(scip)));
2272 	   assert(nodeindex != NULL);
2273 	   assert(nodeindex[startnode] == 0);
2274 	   assert(nodelowlink != NULL);
2275 	   assert(nodelowlink[startnode] == 0);
2276 	   assert(dfsstack != NULL);
2277 	   assert(stacknextclique != NULL);
2278 	   assert(infeasible != NULL);
2279 	
2280 	   *infeasible = FALSE;
2281 	
2282 	   vars = SCIPgetVars(scip);
2283 	
2284 	   /* put start node on the stack */
2285 	   dfsstack[0] = startnode;
2286 	   stacknextclique[0] = 0;
2287 	   stacknextcliquevar[0] = 0;
2288 	   predstackidx[0] = -1;
2289 	   stacksize = 1;
2290 	   idx = -1;
2291 	   currstackidx = 0;
2292 	#ifdef DEBUG_TARJAN
2293 	   SCIPdebugMsg(scip, "put %s(%s) on stack[%d]\n", indexGetBoundString(dfsstack[stacksize-1]),
2294 	      SCIPvarGetName(vars[getVarIndex(dfsstack[stacksize-1])]), stacksize-1);
2295 	#endif
2296 	
2297 	   /* we run until no more bounds indices are on the stack, i.e., no further nodes are connected to the startnode */
2298 	   while( stacksize > 0 )
2299 	   {
2300 	      SCIP_CLIQUE** cliques;
2301 	      int ncliques;
2302 	      SCIP_Bool found;
2303 	      int clqidx = -1;
2304 	      int j;
2305 	      int i;
2306 	
2307 	      /* get next node from stack */
2308 	      curridx = dfsstack[currstackidx];
2309 	      assert(nodelowlink[curridx] <= nodeindex[curridx]);
2310 	
2311 	      startvar = vars[getVarIndex(curridx)];
2312 	      lower = isIndexLowerbound(curridx);
2313 	
2314 	      /* mark current node as on stack, assign index and lowlink */
2315 	      if( nodeindex[curridx] == 0 )
2316 	      {
2317 	         assert(!nodeonstack[curridx]);
2318 	         assert(stacknextclique[currstackidx] == 0);
2319 	         assert(stacknextcliquevar[currstackidx] == 0);
2320 	         nodeonstack[curridx] = 1;
2321 	         nodeindex[curridx] = label;
2322 	         nodelowlink[curridx] = label;
2323 	         ++label;
2324 	
2325 	#ifdef DEBUG_TARJAN
2326 	         {
2327 	            ncliques = SCIPvarGetNCliques(startvar, lower);
2328 	            cliques = SCIPvarGetCliques(startvar, lower);
2329 	
2330 	            SCIPdebugMsg(scip, "variable %s(%s) has %d cliques\n", indexGetBoundString(curridx), SCIPvarGetName(startvar),
2331 	               ncliques);
2332 	            for( j = 0; j < ncliques; ++j )
2333 	            {
2334 	               SCIP_VAR** cliquevars;
2335 	               SCIP_Bool* cliquevals;
2336 	               int ncliquevars;
2337 	
2338 	               clqidx = SCIPcliqueGetIndex(cliques[j]);
2339 	               cliquevars = SCIPcliqueGetVars(cliques[j]);
2340 	               cliquevals = SCIPcliqueGetValues(cliques[j]);
2341 	               ncliquevars = SCIPcliqueGetNVars(cliques[j]);
2342 	
2343 	               SCIPdebugMsg(scip, "clique %d [%d vars, stacksize: %d]...\n", clqidx, ncliquevars, stacksize);
2344 	               for( int v = 0; v < ncliquevars; ++v )
2345 	                  SCIPdebugMsgPrint(scip, " %s<%s>", cliquevals[v] ? "" : "~", SCIPvarGetName(cliquevars[v]));
2346 	               SCIPdebugMsgPrint(scip,  "\n");
2347 	            }
2348 	         }
2349 	#endif
2350 	      }
2351 	      /* we just did a backtrack and still need to investigate some outgoing edges of the node;
2352 	       * however, we should have investigated some of the outgoing edges before
2353 	       */
2354 	      else
2355 	      {
2356 	         assert(stacknextclique[currstackidx] > 0 || stacknextcliquevar[currstackidx] > 0);
2357 	         assert(nodeindex[curridx] < label);
2358 	      }
2359 	      assert(stacknextclique[currstackidx] >= 0);
2360 	
2361 	      ncliques = SCIPvarGetNCliques(startvar, lower);
2362 	      cliques = SCIPvarGetCliques(startvar, lower);
2363 	      found = FALSE;
2364 	
2365 	      /* iterate over all not yet handled cliques and search for an unvisited node */
2366 	      for( j = stacknextclique[currstackidx]; j < ncliques; ++j )
2367 	      {
2368 	         SCIP_VAR** cliquevars;
2369 	         SCIP_Bool* cliquevals;
2370 	         int ncliquevars;
2371 	
2372 	         clqidx = SCIPcliqueGetIndex(cliques[j]);
2373 	         cliquevars = SCIPcliqueGetVars(cliques[j]);
2374 	         cliquevals = SCIPcliqueGetValues(cliques[j]);
2375 	         ncliquevars = SCIPcliqueGetNVars(cliques[j]);
2376 	
2377 	         /* we did not look at this clique before from the current node, i.e., we did not backtrack now from another
2378 	          * node which was reached via this clique
2379 	          */
2380 	         if( stacknextcliquevar[currstackidx] == 0 )
2381 	         {
2382 	#ifdef DEBUG_TARJAN
2383 	            SCIPdebugMsg(scip, "clique %d [%d vars, stacksize: %d]...\n", clqidx, ncliquevars, stacksize);
2384 	            for( int v = 0; v < ncliquevars; ++v )
2385 	               SCIPdebugMsgPrint(scip, " %s<%s>", cliquevals[v] ? "" : "~", SCIPvarGetName(cliquevars[v]));
2386 	            SCIPdebugMsgPrint(scip, "\n");
2387 	#endif
2388 	            /* the clique was not entered before, remember that we first entered it from curridx
2389 	             * (add 1 to distinguish it from 0 initialization)
2390 	             */
2391 	            if( cliquefirstentry[clqidx] == 0 )
2392 	            {
2393 	               cliquefirstentry[clqidx] = curridx + 1;
2394 	            }
2395 	            else
2396 	            {
2397 	               int cliquefirstentryidx = (cliquefirstentry[clqidx] > 0 ? cliquefirstentry[clqidx] : -cliquefirstentry[clqidx]) - 1;
2398 	               int infeasnode = -1;
2399 	               assert(cliquefirstentryidx != curridx);
2400 	
2401 	               /* The node by which we entered the clique the first time is still on the stack, so there is a
2402 	                * way from that node to the node by which we are entering the clique right now.
2403 	                * Since these two assignments together violate the clique and the second assignment is implied by the first,
2404 	                * the first one is infeasible
2405 	                */
2406 	               if( nodeonstack[cliquefirstentryidx] && !nodeinfeasible[cliquefirstentryidx] )
2407 	               {
2408 	                  SCIPdebugMsg(scip, "infeasible assignment (1): %s(%s)\n", indexGetBoundString(cliquefirstentryidx),
2409 	                     SCIPvarGetName(vars[getVarIndex(cliquefirstentryidx)]));
2410 	                  infeasnode = cliquefirstentryidx;
2411 	               }
2412 	               /* the first entry point of the clique was also implied by the current startnode, so this node implies
2413 	                * two variables in the clique and is therefore infeasible
2414 	                */
2415 	               else if( nodeindex[cliquefirstentryidx] >= *startindex && !nodeinfeasible[startnode] )
2416 	               {
2417 	                  SCIPdebugMsg(scip, "infeasible assignment (2): %s(%s)\n", indexGetBoundString(startnode),
2418 	                     SCIPvarGetName(vars[getVarIndex(startnode)]));
2419 	                  infeasnode = startnode;
2420 	               }
2421 	
2422 	               /* we identified an infeasibility */
2423 	               if( infeasnode >= 0 )
2424 	               {
2425 	                  /* both values are invalid for the variable, the whole problem is infeasible */
2426 	                  if( nodeinfeasible[getOtherBoundIndex(infeasnode)] )
2427 	                  {
2428 	                     *infeasible = TRUE;
2429 	                     return SCIP_OKAY;
2430 	                  }
2431 	                  infeasnodes[*ninfeasnodes] = infeasnode;
2432 	                  nodeinfeasible[infeasnode] = TRUE;
2433 	                  ++(*ninfeasnodes);
2434 	
2435 	                  /* the last node by which the clique was exited is not the negation of the current node and still on
2436 	                   * the stack: update the lowlink of the current node
2437 	                   */
2438 	                  if( cliquecurrentexit[clqidx] > 0
2439 	                     && curridx != getOtherBoundIndex(cliquecurrentexit[clqidx] - 1)
2440 	                     && nodeonstack[cliquecurrentexit[clqidx] - 1]
2441 	                     && nodeindex[cliquecurrentexit[clqidx] - 1] < nodelowlink[curridx] )
2442 	                  {
2443 	                     nodelowlink[curridx] = nodeindex[cliquecurrentexit[clqidx] - 1];
2444 	                  }
2445 	               }
2446 	               /* clique is entered for the second time; there is only one edge left to investigate, namely the edge to
2447 	                * the negation of the first entry point
2448 	                */
2449 	               else if( cliquefirstentry[clqidx] > 0 )
2450 	               {
2451 	#ifdef DEBUG_TARJAN
2452 	                  SCIPdebugMsg(scip, "entering clique %d a second time\n", clqidx);
2453 	#endif
2454 	                  idx = getOtherBoundIndex(cliquefirstentry[clqidx] - 1);
2455 	
2456 	                  /* node was not investigated yet, we found the next node to process */
2457 	                  if( nodeindex[idx] == 0 )
2458 	                     found = TRUE;
2459 	                  /* update lowlink if the node is on the stack */
2460 	                  else if( nodeonstack[idx] && nodeindex[idx] < nodelowlink[curridx] )
2461 	                     nodelowlink[curridx] = nodeindex[idx];
2462 	
2463 	                  /* cliquefirstentry[clqidx] < 0 means that we entered the clique at least two times already */
2464 	                  cliquefirstentry[clqidx] = -cliquefirstentry[clqidx];
2465 	               }
2466 	               else
2467 	               {
2468 	#ifdef DEBUG_TARJAN
2469 	                  SCIPdebugMsg(scip, "skip clique %d: visited more than twice already!\n", clqidx);
2470 	#endif
2471 	               }
2472 	               stacknextcliquevar[currstackidx] = ncliquevars;
2473 	            }
2474 	         }
2475 	
2476 	         /* iterate over variables in the clique; start where we stopped last time */
2477 	         for( i = stacknextcliquevar[currstackidx]; i < ncliquevars; ++i )
2478 	         {
2479 	            if( cliquevars[i] == startvar )
2480 	               continue;
2481 	
2482 	            if( !SCIPvarIsActive(cliquevars[i]) )
2483 	               continue;
2484 	
2485 	            if( cliquevals[i] )
2486 	               idx = getUbIndex(SCIPvarGetProbindex(cliquevars[i]));
2487 	            else
2488 	               idx = getLbIndex(SCIPvarGetProbindex(cliquevars[i]));
2489 	            assert(idx >= 0);
2490 	
2491 	            /* break when the first unvisited node is reached */
2492 	            if( nodeindex[idx] == 0 )
2493 	            {
2494 	               assert(!nodeonstack[idx]);
2495 	               stacknextcliquevar[currstackidx] = i + 1;
2496 	               found = TRUE;
2497 	               break;
2498 	            }
2499 	            else if( nodeonstack[idx] && nodeindex[idx] < nodelowlink[curridx] )
2500 	            {
2501 	               nodelowlink[curridx] = nodeindex[idx];
2502 	            }
2503 	         }
2504 	         if( found )
2505 	         {
2506 	            if( stacknextcliquevar[currstackidx] < ncliquevars )
2507 	               stacknextclique[currstackidx] = j;
2508 	            else
2509 	            {
2510 	               stacknextclique[currstackidx] = j + 1;
2511 	               stacknextcliquevar[currstackidx] = 0;
2512 	            }
2513 	            break;
2514 	         }
2515 	         else
2516 	         {
2517 	            assert(i == ncliquevars);
2518 	            stacknextclique[currstackidx] = j + 1;
2519 	            stacknextcliquevar[currstackidx] = 0;
2520 	         }
2521 	      }
2522 	      assert(found || j == ncliques);
2523 	      assert(found || stacknextclique[currstackidx] == ncliques);
2524 	
2525 	      /* we stopped because we found an unhandled node and not because we reached the end of the list */
2526 	      if( found )
2527 	      {
2528 	         int otheridx = getOtherBoundIndex(idx);
2529 	         int infeasnode = -1;
2530 	
2531 	         assert(idx >= 0);
2532 	         assert(!nodeonstack[idx]);
2533 	         assert(j < ncliques);
2534 	         assert(clqidx >= 0);
2535 	
2536 	         /* the negated node corresponding to the next node is already on the stack -> the negated assignment is
2537 	          * infeasible
2538 	          */
2539 	         if( nodeonstack[otheridx] && !nodeinfeasible[otheridx] )
2540 	         {
2541 	            SCIPdebugMsg(scip, "infeasible assignment (3): %s(%s)\n", indexGetBoundString(otheridx),
2542 	               SCIPvarGetName(vars[getVarIndex(otheridx)]));
2543 	            infeasnode = otheridx;
2544 	         }
2545 	         /* the negated node corresponding to the next node was reached from the same startnode -> the startnode is
2546 	          * infeasible
2547 	          */
2548 	         else if( nodeindex[otheridx] >= *startindex && !nodeinfeasible[startnode] )
2549 	         {
2550 	            SCIPdebugMsg(scip, "infeasible assignment (4): %s(%s)\n", indexGetBoundString(startnode),
2551 	               SCIPvarGetName(vars[getVarIndex(startnode)]));
2552 	            infeasnode = startnode;
2553 	         }
2554 	         /* treat infeasible case */
2555 	         if( infeasnode >= 0 )
2556 	         {
2557 	            if( nodeinfeasible[getOtherBoundIndex(infeasnode)] )
2558 	            {
2559 	               *infeasible = TRUE;
2560 	               return SCIP_OKAY;
2561 	            }
2562 	            infeasnodes[*ninfeasnodes] = infeasnode;
2563 	            nodeinfeasible[infeasnode] = TRUE;
2564 	            ++(*ninfeasnodes);
2565 	         }
2566 	
2567 	         SCIPdebugMsg(scip, "clique: %s(%s) -> %s(%s)\n", getBoundString(lower), SCIPvarGetName(startvar),
2568 	            indexGetBoundString(idx), SCIPvarGetName(vars[getVarIndex(idx)]));
2569 	
2570 	         /* put the adjacent node onto the stack */
2571 	         dfsstack[stacksize] = idx;
2572 	         stacknextclique[stacksize] = 0;
2573 	         stacknextcliquevar[stacksize] = 0;
2574 	         cliquecurrentexit[clqidx] = idx + 1;
2575 	         predstackidx[stacksize] = currstackidx;
2576 	         currstackidx = stacksize;
2577 	         stacksize++;
2578 	         assert(stacksize <= 2 * (SCIPgetNVars(scip) - SCIPgetNContVars(scip)));
2579 	
2580 	#ifdef DEBUG_TARJAN
2581 	         SCIPdebugMsg(scip, "put %s(%s) on stack[%d]\n", indexGetBoundString(dfsstack[stacksize-1]), SCIPvarGetName(vars[getVarIndex(dfsstack[stacksize-1])]), stacksize-1);
2582 	#endif
2583 	         /* restart while loop, get next index from stack */
2584 	         continue;
2585 	      }
2586 	      assert(stacknextclique[currstackidx] == ncliques);
2587 	
2588 	      /* no node with a smaller index can be reached from this node -> it is the root of a SCC,
2589 	       * consisting of all nodes above it on the stack, including the node itself
2590 	       */
2591 	      if( nodelowlink[curridx] == nodeindex[curridx] )
2592 	      {
2593 	         /* we are only interested in SCCs with more than one node */
2594 	         if( dfsstack[stacksize-1] != curridx )
2595 	         {
2596 	            int sccvarspos = sccstarts[*nsccs];
2597 	
2598 	            SCIPdebugMsg(scip, "SCC:");
2599 	
2600 	            /* store the SCC in sccvars */
2601 	            do{
2602 	               stacksize--;
2603 	               idx = dfsstack[stacksize];
2604 	               nodeonstack[idx] = 0;
2605 	               sccvars[sccvarspos] = idx;
2606 	               ++sccvarspos;
2607 	               SCIPdebugMsgPrint(scip, " %s(%s)", indexGetBoundString(idx), SCIPvarGetName(vars[getVarIndex(idx)]));
2608 	#ifdef DEBUG_TARJAN
2609 	               SCIPdebugMsg(scip, "remove %s(%s) from stack[%d]\n", indexGetBoundString(dfsstack[stacksize]), SCIPvarGetName(vars[getVarIndex(dfsstack[stacksize])]), stacksize);
2610 	#endif
2611 	            }
2612 	            while( idx != curridx );
2613 	            SCIPdebugMsgPrint(scip, "\n");
2614 	            ++(*nsccs);
2615 	            sccstarts[*nsccs] = sccvarspos;
2616 	         }
2617 	         /* trivial SCC: remove the single node from the stack, but don't store it as a SCC */
2618 	         else
2619 	         {
2620 	            stacksize--;
2621 	#ifdef DEBUG_TARJAN
2622 	            SCIPdebugMsg(scip, "remove %s(%s) from stack[%d]\n", indexGetBoundString(dfsstack[stacksize]), SCIPvarGetName(vars[getVarIndex(dfsstack[stacksize])]), stacksize);
2623 	#endif
2624 	            idx = dfsstack[stacksize];
2625 	            nodeonstack[idx] = 0;
2626 	            assert(nodeindex[idx] > 0);
2627 	         }
2628 	      }
2629 	      /* in a pure dfs, the node would now leave the stack, add it to the array of nodes in reverse topological order */
2630 	      if( topoorder != NULL && (stacksize > 0 || label > *startindex + 1) )
2631 	      {
2632 	         assert(nordered != NULL);
2633 	         topoorder[*nordered] = curridx;
2634 	         ++(*nordered);
2635 	      }
2636 	
2637 	      /* the current node was handled, backtrack */
2638 	      if( stacksize > 0 )
2639 	      {
2640 	         idx = dfsstack[predstackidx[currstackidx]];
2641 	         nodelowlink[idx] = MIN(nodelowlink[idx], nodelowlink[curridx]);
2642 	         currstackidx = predstackidx[currstackidx];
2643 	      }
2644 	   }
2645 	
2646 	   *startindex = label;
2647 	
2648 	   return SCIP_OKAY;
2649 	}
2650 	
2651 	
2652 	/** apply fixings and aggregations found by the clique graph analysis */
2653 	static
2654 	SCIP_RETCODE applyFixingsAndAggregations(
2655 	   SCIP*                 scip,               /**< SCIP data structure */
2656 	   SCIP_VAR**            vars,               /**< array of active variables */
2657 	   int*                  infeasnodes,        /**< sparse array with node indices of infeasible nodes */
2658 	   int                   ninfeasnodes,       /**< pointer to store the number of infeasible nodes */
2659 	   SCIP_Shortbool*       nodeinfeasible,     /**< array to store whether the fixing of a node was detected to be infeasible */
2660 	   int*                  sccvars,            /**< array with all nontrivial strongly connected components in the graph */
2661 	   int*                  sccstarts,          /**< start indices of SCCs in sccvars array; one additional entry at the end
2662 	                                              *   to give length of used part of sccvars array */
2663 	   int                   nsccs,              /**< pointer to store number of strongly connected components */
2664 	   SCIP_Bool*            infeasible,         /**< pointer to store whether an infeasibility was detected */
2665 	   int*                  nfixedvars,         /**< pointer to number of fixed variables, increment when fixing another one */
2666 	   int*                  naggrvars,          /**< pointer to number of aggregated variables, increment when aggregating another one */
2667 	   SCIP_RESULT*          result              /**< pointer to store result of the call */
2668 	   )
2669 	{
2670 	   int i = 0;
2671 	
2672 	   assert(scip != NULL);
2673 	   assert(vars != NULL);
2674 	   assert(infeasible != NULL);
2675 	
2676 	   /* for all infeasible node: fix variable to the other bound */
2677 	   if( !(*infeasible) && ninfeasnodes > 0 )
2678 	   {
2679 	      for( i = 0; i < ninfeasnodes; ++i )
2680 	      {
2681 	         SCIP_VAR* var = vars[getVarIndex(infeasnodes[i])];
2682 	         SCIP_Bool lower = isIndexLowerbound(infeasnodes[i]);
2683 	         SCIP_Bool fixed;
2684 	
2685 	         assert(nodeinfeasible[infeasnodes[i]]);
2686 	         nodeinfeasible[infeasnodes[i]] = FALSE;
2687 	
2688 	         SCIP_CALL( SCIPfixVar(scip, var, lower ? 0.0 : 1.0, infeasible, &fixed) );
2689 	
2690 	         SCIPdebugMsg(scip, "fix <%s>[%d] to %g: inf=%u, fixed=%u\n",
2691 	            SCIPvarGetName(var), infeasnodes[i], lower ? 0.0 : 1.0, *infeasible, fixed);
2692 	
2693 	         /* fixing was infeasible */
2694 	         if( *infeasible )
2695 	            break;
2696 	
2697 	         /* increase fixing counter and update result pointer */
2698 	         if( fixed )
2699 	         {
2700 	            *result = SCIP_SUCCESS;
2701 	            ++(*nfixedvars);
2702 	         }
2703 	      }
2704 	   }
2705 	   assert((*infeasible) || i == ninfeasnodes);
2706 	
2707 	   /* clear clean buffer array (if we did not enter the block above or stopped early due to an infeasibility) */
2708 	   for( ; i < ninfeasnodes; ++i )
2709 	   {
2710 	      assert(nodeinfeasible[infeasnodes[i]]);
2711 	      nodeinfeasible[infeasnodes[i]] = FALSE;
2712 	   }
2713 	
2714 	   if( !(*infeasible) && nsccs > 0 )
2715 	   {
2716 	      /* for each strongly connected component: aggregate all variables to the first one */
2717 	      for( i = 0; i < nsccs; ++i )
2718 	      {
2719 	         SCIP_VAR* startvar;
2720 	         SCIP_Bool lower;
2721 	         SCIP_Bool aggregated;
2722 	         SCIP_Bool redundant;
2723 	         int v;
2724 	
2725 	         assert(sccstarts[i] < sccstarts[i+1] - 1);
2726 	
2727 	         /* get variable and boundtype for first node of the SCC */
2728 	         startvar = vars[getVarIndex(sccvars[sccstarts[i]])];
2729 	         lower = isIndexLowerbound(sccvars[sccstarts[i]]);
2730 	
2731 	         for( v = sccstarts[i] + 1; v < sccstarts[i+1]; ++v )
2732 	         {
2733 	            /* aggregate variables: if both nodes represent the same bound, we have x=1 <=> y=1,
2734 	             * and thus aggregate x - y = 0; if both represent different bounds we have
2735 	             * x=1 <=> y=0, so we aggregate x + y = 1
2736 	             */
2737 	            SCIP_CALL( SCIPaggregateVars(scip, startvar, vars[getVarIndex(sccvars[v])], 1.0,
2738 	                  lower == isIndexLowerbound(sccvars[v]) ? -1.0 : 1.0,
2739 	                  lower == isIndexLowerbound(sccvars[v]) ? 0.0 : 1.0,
2740 	                  infeasible, &redundant, &aggregated) );
2741 	
2742 	            SCIPdebugMsg(scip, "aggregate <%s> + %g <%s> = %g: inf=%u, red=%u, aggr=%u\n",
2743 	               SCIPvarGetName(startvar), lower == isIndexLowerbound(sccvars[v]) ? -1.0 : 1.0,
2744 	               SCIPvarGetName(vars[getVarIndex(sccvars[v])]), lower == isIndexLowerbound(sccvars[v]) ? 0.0 : 1.0,
2745 	               *infeasible, redundant, aggregated);
2746 	
2747 	            /* aggregation was infeasible */
2748 	            if( *infeasible )
2749 	               break;
2750 	
2751 	            /* increase aggregation counter and update result pointer */
2752 	            if( aggregated )
2753 	            {
2754 	               ++(*naggrvars);
2755 	               *result = SCIP_SUCCESS;
2756 	            }
2757 	         }
2758 	      }
2759 	   }
2760 	
2761 	   return SCIP_OKAY;
2762 	}
2763 	
2764 	
2765 	
2766 	/** presolving method of propagator: search for strongly connected components in the implication graph and
2767 	 *  aggregate all variables within a component; additionally, identifies infeasible variable assignments
2768 	 *  as a side product if a path from x=1 to x=0 (or vice versa) is found or x=1 implies both y=0 and y=1
2769 	 *  The identification of such assignments depends on the order in which variable bounds are processed;
2770 	 *  therefore, we are doing a second run with the bounds processed in (almost) topological order.
2771 	 */
2772 	static
2773 	SCIP_DECL_PROPPRESOL(propPresolVbounds)
2774 	{  /*lint --e{715}*/
2775 	   SCIP_PROPDATA* propdata;
2776 	   SCIP_VAR** tmpvars;
2777 	   SCIP_VAR** vars;
2778 	   int* dfsstack;
2779 	   int* stacknextclique;
2780 	   int* stacknextcliquevar;
2781 	   int* nodeindex;
2782 	   int* nodelowlink;
2783 	   int* predstackidx;
2784 	   int* cliquefirstentry;
2785 	   int* cliquecurrentexit;
2786 	   int* topoorder;
2787 	   int* sccvars;
2788 	   int* sccstarts;
2789 	   int* infeasnodes;
2790 	   SCIP_Shortbool* nodeonstack;
2791 	   SCIP_Shortbool* nodeinfeasible;
2792 	   int ninfeasnodes;
2793 	   int nsccs;
2794 	   int nbounds;
2795 	   int nbinvars;
2796 	   int ncliques;
2797 	   int startindex = 1;
2798 	   int nordered = 0;
2799 	   int i;
2800 	   SCIP_Bool infeasible = FALSE;
2801 	
2802 	   assert(scip != NULL);
2803 	
2804 	   propdata = SCIPpropGetData(prop);
2805 	   assert(propdata != NULL);
2806 	
2807 	   ncliques = SCIPgetNCliques(scip);
2808 	
2809 	   *result = SCIP_DIDNOTRUN;
2810 	
2811 	   if( ncliques < 2 )
2812 	      return SCIP_OKAY;
2813 	
2814 	   /* too many cliques for medium presolving */
2815 	   if( presoltiming == SCIP_PRESOLTIMING_MEDIUM && ncliques > propdata->maxcliquesmedium * SCIPgetNBinVars(scip) )
2816 	      return SCIP_OKAY;
2817 	
2818 	   /* too many cliques for exhaustive presolving */
2819 	   if( ncliques > propdata->maxcliquesexhaustive * SCIPgetNBinVars(scip) )
2820 	      return SCIP_OKAY;
2821 	
2822 	   /* only run if enough new cliques were created since the last successful call */
2823 	   if( SCIPgetNCliquesCreated(scip) < (1.0 + propdata->minnewcliques) * propdata->lastpresolncliques )
2824 	      return SCIP_OKAY;
2825 	
2826 	   *result = SCIP_DIDNOTFIND;
2827 	
2828 	   nbinvars = SCIPgetNVars(scip) - SCIPgetNContVars(scip);
2829 	   nbounds = 2 * nbinvars;
2830 	
2831 	   /* cleanup cliques, stop if this proved infeasibility already */
2832 	   SCIP_CALL( SCIPcleanupCliques(scip, &infeasible) );
2833 	
2834 	   if( infeasible )
2835 	   {
2836 	      *result = SCIP_CUTOFF;
2837 	      return SCIP_OKAY;
2838 	   }
2839 	
2840 	   tmpvars = SCIPgetVars(scip);
2841 	
2842 	   /* duplicate variable array; needed to get the fixings right later */
2843 	   SCIP_CALL( SCIPduplicateBufferArray(scip, &vars, tmpvars, nbinvars) );
2844 	
2845 	   SCIP_CALL( SCIPallocBufferArray(scip, &dfsstack, nbounds) );
2846 	   SCIP_CALL( SCIPallocBufferArray(scip, &stacknextclique, nbounds) );
2847 	   SCIP_CALL( SCIPallocBufferArray(scip, &stacknextcliquevar, nbounds) );
2848 	   SCIP_CALL( SCIPallocBufferArray(scip, &predstackidx, nbounds) );
2849 	   SCIP_CALL( SCIPallocBufferArray(scip, &topoorder, nbounds) );
2850 	   SCIP_CALL( SCIPallocBufferArray(scip, &sccvars, nbounds) );
2851 	   SCIP_CALL( SCIPallocBufferArray(scip, &sccstarts, nbinvars + 1) );
2852 	   SCIP_CALL( SCIPallocBufferArray(scip, &infeasnodes, nbounds) );
2853 	   SCIP_CALL( SCIPallocClearBufferArray(scip, &nodeindex, nbounds) );
2854 	   SCIP_CALL( SCIPallocClearBufferArray(scip, &nodelowlink, nbounds) );
2855 	   SCIP_CALL( SCIPallocClearBufferArray(scip, &cliquefirstentry, ncliques) );
2856 	   SCIP_CALL( SCIPallocClearBufferArray(scip, &cliquecurrentexit, ncliques) );
2857 	   SCIP_CALL( SCIPallocClearBufferArray(scip, &nodeonstack, nbounds) );
2858 	   SCIP_CALL( SCIPallocCleanBufferArray(scip, &nodeinfeasible, nbounds) );
2859 	   sccstarts[0] = 0;
2860 	   nsccs = 0;
2861 	   ninfeasnodes = 0;
2862 	
2863 	   /* while there are unvisited nodes, run Tarjan's algorithm starting from one of these nodes */
2864 	   for( i = 0; i < nbounds && !infeasible; ++i )
2865 	   {
2866 	      if( nodeindex[i] == 0 )
2867 	      {
2868 	         SCIP_CALL( tarjan(scip, i, &startindex, nodeonstack, nodeindex, nodelowlink, nodeinfeasible,
2869 	               dfsstack, predstackidx, stacknextclique, stacknextcliquevar, topoorder, &nordered,
2870 	               cliquefirstentry, cliquecurrentexit, sccvars, sccstarts, &nsccs,
2871 	               infeasnodes, &ninfeasnodes, &infeasible) );
2872 	      }
2873 	   }
2874 	   assert(nordered <= nbounds);
2875 	
2876 	   /* aggregate all variables within a SCC and fix all variables for which one bounds was proven infeasible */
2877 	   if( ninfeasnodes > 0 || nsccs > 0 )
2878 	   {
2879 	      SCIP_CALL( applyFixingsAndAggregations(scip, vars, infeasnodes, ninfeasnodes, nodeinfeasible,
2880 	            sccvars, sccstarts, nsccs, &infeasible, nfixedvars, naggrvars, result) );
2881 	   }
2882 	
2883 	   /* second round, now with topological order! */
2884 	   if( !infeasible && nordered > 0 )
2885 	   {
2886 	      SCIP_VAR** vars2;
2887 	      int nbounds2;
2888 	
2889 	      assert(nordered > 1);
2890 	
2891 	      /* we already fixed or aggregated some variables in the first run, so we better clean up the cliques */
2892 	      if( *result == SCIP_SUCCESS )
2893 	      {
2894 	         SCIP_CALL( SCIPcleanupCliques(scip, &infeasible) );
2895 	
2896 	         if( infeasible )
2897 	            goto TERMINATE;
2898 	      }
2899 	
2900 	      nbounds2 = 2 * (SCIPgetNVars(scip) - SCIPgetNContVars(scip));
2901 	      ncliques = SCIPgetNCliques(scip);
2902 	
2903 	      SCIP_CALL( SCIPduplicateBufferArray(scip, &vars2, tmpvars, nbounds2/2) );
2904 	
2905 	      /* clear arrays that should be initialized to 0 */
2906 	      BMSclearMemoryArray(nodeonstack, nbounds2);
2907 	      BMSclearMemoryArray(nodeindex, nbounds2);
2908 	      BMSclearMemoryArray(nodelowlink, nbounds2);
2909 	      BMSclearMemoryArray(cliquefirstentry, ncliques);
2910 	      BMSclearMemoryArray(cliquecurrentexit, ncliques);
2911 	      sccstarts[0] = 0;
2912 	      nsccs = 0;
2913 	      ninfeasnodes = 0;
2914 	      startindex = 1;
2915 	
2916 	      /* while there are unvisited nodes, run Tarjan's algorithm starting from one of these nodes */
2917 	      for( i = nordered - 1; i >= 0  && !infeasible; --i )
2918 	      {
2919 	         int varindex;
2920 	         int startpos;
2921 	         assert(topoorder[i] < nbounds);
2922 	
2923 	         /* variable of next node in topological order */
2924 	         varindex = SCIPvarGetProbindex(vars[getVarIndex(topoorder[i])]);
2925 	
2926 	         /* variable was not fixed after the first run */
2927 	         if( varindex >= 0 )
2928 	         {
2929 	            startpos = isIndexLowerbound(topoorder[i]) ? getLbIndex(varindex) : getUbIndex(varindex);
2930 	            if( nodeindex[startpos] == 0 )
2931 	            {
2932 	               SCIP_CALL( tarjan(scip, startpos, &startindex, nodeonstack, nodeindex, nodelowlink, nodeinfeasible,
2933 	                     dfsstack, predstackidx, stacknextclique, stacknextcliquevar, NULL, NULL,
2934 	                     cliquefirstentry, cliquecurrentexit, sccvars, sccstarts, &nsccs,
2935 	                     infeasnodes, &ninfeasnodes, &infeasible) );
2936 	            }
2937 	         }
2938 	      }
2939 	
2940 	      /* aggregate all variables within a SCC and fix all variables for which one bounds was proven infeasible */
2941 	      if( ninfeasnodes > 0 || nsccs > 0 )
2942 	      {
2943 	         SCIP_CALL( applyFixingsAndAggregations(scip, vars2, infeasnodes, ninfeasnodes, nodeinfeasible,
2944 	               sccvars, sccstarts, nsccs, &infeasible, nfixedvars, naggrvars, result) );
2945 	      }
2946 	
2947 	      SCIPfreeBufferArray(scip, &vars2);
2948 	   }
2949 	
2950 	 TERMINATE:
2951 	   if( infeasible )
2952 	      *result = SCIP_CUTOFF;
2953 	#ifndef NDEBUG
2954 	   for( i = 0; i < nbounds; ++i )
2955 	   {
2956 	      assert(nodeinfeasible[i] == FALSE);
2957 	   }
2958 	#endif
2959 	   SCIPfreeCleanBufferArray(scip, &nodeinfeasible);
2960 	   SCIPfreeBufferArray(scip, &nodeonstack);
2961 	   SCIPfreeBufferArray(scip, &cliquecurrentexit);
2962 	   SCIPfreeBufferArray(scip, &cliquefirstentry);
2963 	   SCIPfreeBufferArray(scip, &nodelowlink);
2964 	   SCIPfreeBufferArray(scip, &nodeindex);
2965 	   SCIPfreeBufferArray(scip, &infeasnodes);
2966 	   SCIPfreeBufferArray(scip, &sccstarts);
2967 	   SCIPfreeBufferArray(scip, &sccvars);
2968 	   SCIPfreeBufferArray(scip, &topoorder);
2969 	   SCIPfreeBufferArray(scip, &predstackidx);
2970 	   SCIPfreeBufferArray(scip, &stacknextcliquevar);
2971 	   SCIPfreeBufferArray(scip, &stacknextclique);
2972 	   SCIPfreeBufferArray(scip, &dfsstack);
2973 	   SCIPfreeBufferArray(scip, &vars);
2974 	
2975 	   propdata->lastpresolncliques = SCIPgetNCliquesCreated(scip);
2976 	
2977 	   return SCIP_OKAY;
2978 	}
2979 	
2980 	
2981 	
2982 	/** execution method of propagator */
2983 	static
2984 	SCIP_DECL_PROPEXEC(propExecVbounds)
2985 	{  /*lint --e{715}*/
2986 	   *result = SCIP_DIDNOTRUN;
2987 	
2988 	   /* perform variable lower and upper bound propagation */
2989 	   SCIP_CALL( propagateVbounds(scip, prop, FALSE, result) );
2990 	
2991 	   assert((*result) == SCIP_CUTOFF || (*result) == SCIP_DIDNOTRUN
2992 	      || (*result) == SCIP_DIDNOTFIND || (*result) == SCIP_REDUCEDDOM);
2993 	
2994 	   return SCIP_OKAY;
2995 	}
2996 	
2997 	/** propagation conflict resolving method of propagator */
2998 	static
2999 	SCIP_DECL_PROPRESPROP(propRespropVbounds)
3000 	{  /*lint --e{715}*/
3001 	   SCIP_PROPDATA* propdata;
3002 	   SCIP_VAR** vars;
3003 	   SCIP_VAR* startvar;
3004 	   SCIP_BOUNDTYPE starttype;
3005 	   int pos;
3006 	
3007 	   propdata = SCIPpropGetData(prop);
3008 	   assert(propdata != NULL);
3009 	
3010 	   starttype = inferInfoGetBoundtype(intToInferInfo(inferinfo));
3011 	   pos = inferInfoGetPos(intToInferInfo(inferinfo));
3012 	   assert(pos >= 0);
3013 	   assert(pos < propdata->nbounds);
3014 	
3015 	   vars = propdata->vars;
3016 	   assert(vars != NULL);
3017 	   startvar = vars[getVarIndex(pos)];
3018 	   assert(startvar != NULL);
3019 	   assert(startvar != infervar);
3020 	
3021 	   SCIPdebugMsg(scip, "explain %s bound change of variable <%s>\n",
3022 	      getBoundtypeString(boundtype), SCIPvarGetName(infervar));
3023 	
3024 	   if( !SCIPvarIsBinary(startvar) && propdata->usebdwidening )
3025 	   {
3026 	      int* vboundboundedidx;
3027 	      SCIP_Real constant;
3028 	      SCIP_Real coef;
3029 	      int inferidx;
3030 	      int nvbounds;
3031 	      int b;
3032 	
3033 	      nvbounds = propdata->nvbounds[pos];
3034 	      vboundboundedidx = propdata->vboundboundedidx[pos];
3035 	
3036 	      inferidx = boundtype == SCIP_BOUNDTYPE_LOWER ? varGetLbIndex(propdata, infervar) : varGetUbIndex(propdata, infervar);
3037 	      assert(inferidx >= 0);
3038 	
3039 	      for( b = 0; b < nvbounds; ++b )
3040 	      {
3041 	         if( vboundboundedidx[b] == inferidx )
3042 	            break;
3043 	      }
3044 	      assert(b < nvbounds);
3045 	
3046 	      coef = propdata->vboundcoefs[pos][b];
3047 	      constant = propdata->vboundconstants[pos][b];
3048 	      assert(!SCIPisZero(scip, coef));
3049 	
3050 	      /* compute the relaxed bound which is sufficient to propagate the inference bound of given variable */
3051 	      if( boundtype == SCIP_BOUNDTYPE_LOWER )
3052 	         relaxedbd = computeRelaxedLowerbound(scip, infervar, relaxedbd, coef, constant);
3053 	      else
3054 	         relaxedbd = computeRelaxedUpperbound(scip, infervar, relaxedbd, coef, constant);
3055 	
3056 	      /* try to relax variable bound variable */
3057 	      SCIP_CALL( relaxVbdvar(scip, startvar, starttype, bdchgidx, relaxedbd) );
3058 	   }
3059 	   else
3060 	   {
3061 	      SCIP_CALL( resolvePropagation(scip, propdata, startvar, starttype, bdchgidx) );
3062 	   }
3063 	
3064 	   (*result) = SCIP_SUCCESS;
3065 	
3066 	   return SCIP_OKAY;
3067 	}
3068 	
3069 	/**@} */
3070 	
3071 	/**@name Callback methods of event handler
3072 	 *
3073 	 * @{
3074 	 */
3075 	
3076 	/** execution method of bound change event handler */
3077 	static
3078 	SCIP_DECL_EVENTEXEC(eventExecVbound)
3079 	{  /*lint --e{715}*/
3080 	   SCIP_PROPDATA* propdata;
3081 	   int idx;
3082 	
3083 	   assert(eventhdlr != NULL);
3084 	
3085 	   propdata = (SCIP_PROPDATA*)SCIPeventhdlrGetData(eventhdlr);
3086 	   assert(propdata != NULL);
3087 	
3088 	   /* coverity[pointer_conversion_loses_bits] */
3089 	   idx = (int) (size_t) eventdata;
3090 	   assert(idx >= 0);
3091 	
3092 	   SCIPdebugMsg(scip, "eventexec (type=%" SCIP_EVENTTYPE_FORMAT "): try to add sort index %d: %s(%s) to priority queue\n", SCIPeventGetType(event),
3093 	      idx, indexGetBoundString(propdata->topoorder[idx]),
3094 	      SCIPvarGetName(propdata->vars[getVarIndex(propdata->topoorder[idx])]));
3095 	
3096 	   if( SCIPeventGetType(event) == SCIP_EVENTTYPE_GUBCHANGED && SCIPvarIsBinary(SCIPeventGetVar(event))
3097 	      && SCIPeventGetNewbound(event) > 0.5 )
3098 	      return SCIP_OKAY;
3099 	
3100 	   if( SCIPeventGetType(event) == SCIP_EVENTTYPE_GLBCHANGED && SCIPvarIsBinary(SCIPeventGetVar(event))
3101 	      && SCIPeventGetNewbound(event) < 0.5 )
3102 	      return SCIP_OKAY;
3103 	
3104 	   assert(getVarIndex(propdata->topoorder[idx]) < SCIPgetNVars(scip));
3105 	   assert(SCIPvarGetType(propdata->vars[getVarIndex(propdata->topoorder[idx])]) != SCIP_VARTYPE_BINARY
3106 	      || (isIndexLowerbound(propdata->topoorder[idx]) == (SCIPeventGetNewbound(event) > 0.5)));
3107 	
3108 	   /* add the bound change to the propagation queue, if it is not already contained */
3109 	   if( !propdata->inqueue[idx] )
3110 	   {
3111 	      SCIP_CALL( SCIPpqueueInsert(propdata->propqueue, (void*)(size_t)(idx + 1)) ); /*lint !e571 !e776*/
3112 	      propdata->inqueue[idx] = TRUE;
3113 	      assert(SCIPpqueueNElems(propdata->propqueue) > 0);
3114 	   }
3115 	
3116 	   return SCIP_OKAY;
3117 	}
3118 	
3119 	/**@} */
3120 	
3121 	
3122 	/** creates the vbounds propagator and includes it in SCIP */
3123 	SCIP_RETCODE SCIPincludePropVbounds(
3124 	   SCIP*                 scip                /**< SCIP data structure */
3125 	   )
3126 	{
3127 	   SCIP_PROPDATA* propdata;
3128 	   SCIP_PROP* prop;
3129 	
3130 	   /* create vbounds propagator data */
3131 	   SCIP_CALL( SCIPallocBlockMemory(scip, &propdata) );
3132 	
3133 	   /* reset propagation data */
3134 	   resetPropdata(propdata);
3135 	
3136 	   /* include propagator */
3137 	   SCIP_CALL( SCIPincludePropBasic(scip, &prop, PROP_NAME, PROP_DESC, PROP_PRIORITY, PROP_FREQ, PROP_DELAY, PROP_TIMING,
3138 	         propExecVbounds, propdata) );
3139 	   assert(prop != NULL);
3140 	
3141 	   /* set optional callbacks via setter functions */
3142 	   SCIP_CALL( SCIPsetPropCopy(scip, prop, propCopyVbounds) );
3143 	   SCIP_CALL( SCIPsetPropFree(scip, prop, propFreeVbounds) );
3144 	   SCIP_CALL( SCIPsetPropInitpre(scip, prop, propInitpreVbounds) );
3145 	   SCIP_CALL( SCIPsetPropExitsol(scip, prop, propExitsolVbounds) );
3146 	   SCIP_CALL( SCIPsetPropResprop(scip, prop, propRespropVbounds) );
3147 	   SCIP_CALL( SCIPsetPropPresol(scip, prop, propPresolVbounds, PROP_PRESOL_PRIORITY, PROP_PRESOL_MAXROUNDS,
3148 	         PROP_PRESOLTIMING) );
3149 	
3150 	   /* include event handler for bound change events */
3151 	   SCIP_CALL( SCIPincludeEventhdlrBasic(scip, &propdata->eventhdlr, EVENTHDLR_NAME, EVENTHDLR_DESC,
3152 	         eventExecVbound, (SCIP_EVENTHDLRDATA*)propdata) );
3153 	
3154 	   SCIP_CALL( SCIPaddBoolParam(scip,
3155 	         "propagating/" PROP_NAME "/usebdwidening", "should bound widening be used to initialize conflict analysis?",
3156 	         &propdata->usebdwidening, FALSE, DEFAULT_USEBDWIDENING, NULL, NULL) );
3157 	   SCIP_CALL( SCIPaddBoolParam(scip,
3158 	         "propagating/" PROP_NAME "/useimplics", "should implications be propagated?",
3159 	         &propdata->useimplics, TRUE, DEFAULT_USEIMPLICS, NULL, NULL) );
3160 	   SCIP_CALL( SCIPaddBoolParam(scip,
3161 	         "propagating/" PROP_NAME "/usecliques", "should cliques be propagated?",
3162 	         &propdata->usecliques, TRUE, DEFAULT_USECLIQUES, NULL, NULL) );
3163 	   SCIP_CALL( SCIPaddBoolParam(scip,
3164 	         "propagating/" PROP_NAME "/usevbounds", "should vbounds be propagated?",
3165 	         &propdata->usevbounds, TRUE, DEFAULT_USEVBOUNDS, NULL, NULL) );
3166 	   SCIP_CALL( SCIPaddBoolParam(scip,
3167 	         "propagating/" PROP_NAME "/dotoposort", "should the bounds be topologically sorted in advance?",
3168 	         &propdata->dotoposort, FALSE, DEFAULT_DOTOPOSORT, NULL, NULL) );
3169 	   SCIP_CALL( SCIPaddBoolParam(scip,
3170 	         "propagating/" PROP_NAME "/sortcliques", "should cliques be regarded for the topological sort?",
3171 	         &propdata->sortcliques, TRUE, DEFAULT_SORTCLIQUES, NULL, NULL) );
3172 	   SCIP_CALL( SCIPaddBoolParam(scip,
3173 	         "propagating/" PROP_NAME "/detectcycles", "should cycles in the variable bound graph be identified?",
3174 	         &propdata->detectcycles, FALSE, DEFAULT_DETECTCYCLES, NULL, NULL) );
3175 	   SCIP_CALL( SCIPaddRealParam(scip,
3176 	         "propagating/" PROP_NAME "/minnewcliques", "minimum percentage of new cliques to trigger another clique table analysis",
3177 	         &propdata->minnewcliques, FALSE, DEFAULT_MINNEWCLIQUES, 0.0, 1.0, NULL, NULL) );
3178 	   SCIP_CALL( SCIPaddRealParam(scip, "propagating/" PROP_NAME "/maxcliquesmedium",
3179 	         "maximum number of cliques per variable to run clique table analysis in medium presolving",
3180 	         &propdata->maxcliquesmedium, FALSE, DEFAULT_MAXCLIQUESMEDIUM, 0.0, SCIP_REAL_MAX, NULL, NULL) );
3181 	   SCIP_CALL( SCIPaddRealParam(scip, "propagating/" PROP_NAME "/maxcliquesexhaustive",
3182 	         "maximum number of cliques per variable to run clique table analysis in exhaustive presolving",
3183 	         &propdata->maxcliquesexhaustive, FALSE, DEFAULT_MAXCLIQUESEXHAUSTIVE, 0.0, SCIP_REAL_MAX, NULL, NULL) );
3184 	
3185 	   return SCIP_OKAY;
3186 	}
3187 	
3188 	/** returns TRUE if the propagator has the status that all variable lower and upper bounds are propgated */
3189 	SCIP_Bool SCIPisPropagatedVbounds(
3190 	   SCIP*                 scip                /**< SCIP data structure */
3191 	   )
3192 	{
3193 	   SCIP_PROP* prop;
3194 	   SCIP_PROPDATA* propdata;
3195 	
3196 	   prop = SCIPfindProp(scip, PROP_NAME);
3197 	   assert(prop != NULL);
3198 	
3199 	   propdata = SCIPpropGetData(prop);
3200 	   assert(propdata != NULL);
3201 	
3202 	   return (SCIPpqueueNElems(propdata->propqueue) == 0);
3203 	}
3204 	
3205 	/** performs propagation of variables lower and upper bounds */
3206 	SCIP_RETCODE SCIPexecPropVbounds(
3207 	   SCIP*                 scip,               /**< SCIP data structure */
3208 	   SCIP_Bool             force,              /**< should domain changes for continuous variables be forced */
3209 	   SCIP_RESULT*          result              /**< pointer to store result */
3210 	   )
3211 	{
3212 	   SCIP_PROP* prop;
3213 	
3214 	   prop = SCIPfindProp(scip, PROP_NAME);
3215 	   assert(prop != NULL);
3216 	
3217 	   /* perform variable lower and upper bound propagation */
3218 	   SCIP_CALL( propagateVbounds(scip, prop, force, result) );
3219 	
3220 	   assert((*result) == SCIP_CUTOFF || (*result) == SCIP_DIDNOTRUN
3221 	      || (*result) == SCIP_DIDNOTFIND || (*result) == SCIP_REDUCEDDOM);
3222 	
3223 	   return SCIP_OKAY;
3224 	}
3225