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   presolve.c
26   	 * @ingroup OTHER_CFILES
27   	 * @brief  methods for presolving
28   	 * @author Michael Winkler
29   	 */
30   	
31   	/* all general presolving methods (not working on any specific kind of data(, e.g. consdata) should be implemented here */
32   	
33   	/*---+----1----+----2----+----3----+----4----+----5----+----6----+----7----+----8----+----9----+----0----+----1----+----2*/
34   	
35   	#include "blockmemshell/memory.h"
36   	#include "scip/presolve.h"
37   	#include "scip/prob.h"
38   	#include "scip/pub_implics.h"
39   	#include "scip/pub_message.h"
40   	#include "scip/pub_var.h"
41   	#include "scip/scip_mem.h"
42   	#include "scip/scip_message.h"
43   	#include "scip/scip_numerics.h"
44   	#include "scip/scip_tree.h"
45   	#include "scip/struct_mem.h"
46   	#include "scip/struct_scip.h"
47   	#include "scip/tree.h"
48   	
49   	/*
50   	 * Local methods
51   	 */
52   	
53   	/** collect variable bound information for a variable set reduction and global implication; only variable which have the
54   	 *  vartype != SCIP_VARTYPE_BINARY have variable bounds
55   	 */
56   	static
57   	void collectNonBinaryVBoundData(
58   	   SCIP*                 scip,               /**< SCIP data structure */
59   	   SCIP_VAR*             var,                /**< set variable */
60   	   int                   varidx,             /**< for lower bound set variable index, for upper bound set variable index
61   	                                              *   + number of variables
62   	                                              */
63   	   int                   pos,                /**< variables's position in bdchinfos */
64   	   int                   nredvars,           /**< number of reduced variables so far */
65   	   SCIP_Real*            bounds,             /**< array of bounds where one of them must be fullfilled */
66   	   SCIP_Bool*            boundtypes,         /**< array of bound types */
67   	   SCIP_Real*            newbounds,          /**< array of implied bounds(, size is two times number of variables, first
68   	                                              *   half for implied lower bounds, second for implied upper bounds)
69   	                                              */
70   	   int*                  counts,             /**< array of number of implication on a bound (, size is two times number
71   	                                              *   of variables, first half for implied lower bounds, second for implied
72   	                                              *   upper bounds)
73   	                                              */
74   	   int*                  countnonzeros,      /**< array to store the indices of non-zero entries in the counts array */
75   	   int*                  ncountnonzeros,     /**< pointer to store the number of non-zero entries in the counts array */
76   	   int*                  issetvar,           /**< array containing for set variables the position in the current set, or
77   	                                              *   0 if it is not a set variable or -1, if it is a redundant(i.e. implies
78   	                                              *   another set variable) set variables(, size is two times number of
79   	                                              *   variables, first half for implied lower bounds, second for implied
80   	                                              *   upper bounds) */
81   	   int                   nvars,              /**< number of problem variables */
82   	   int*                  foundbin,           /**< pointer to store the lowest index of a binary implication variable
83   	                                              *   when found
84   	                                              */
85   	   int*                  foundnonbin,        /**< pointer to store the lowest index of a non-binary implication variable
86   	                                              *   when found
87   	                                              */
88   	   int*                  implidx,            /**< array to store the variable indices (for upper bound 'nvars' is added
89   	                                              *   to the index) which are implied
90   	                                              */
91   	   int*                  nimplidx,           /**< pointer to store the number of implied variables */
92   	   SCIP_Real*            lastbounds          /**< array to remember last implied bounds before taken the current
93   	                                              *   variable into account, first nvars for lower bound, second nvars for
94   	                                              *   upper bound
95   	                                              *
96   	                                              *   this array is used when a set variable got redundant, because it
97   	                                              *   implies another set variable, and we need to correct the counts array
98   	                                              */
99   	   )
100  	{
101  	   SCIP_VAR** implvars;
102  	   SCIP_Real* implcoefs;
103  	   SCIP_Real* implconsts;
104  	   int nimpls;
105  	   int idx;
106  	   int w;
107  	
108  	   assert(scip != NULL);
109  	   assert(var != NULL);
110  	   assert(SCIPvarGetType(var) != SCIP_VARTYPE_BINARY);
111  	   assert(varidx >= 0);
112  	   assert(pos >= 0);
113  	   assert(bounds != NULL);
114  	   assert(boundtypes != NULL);
115  	   assert(newbounds != NULL);
116  	   assert(counts != NULL);
117  	   assert(issetvar != NULL);
118  	   assert(2 * nvars > varidx);
119  	   assert(foundbin != NULL);
120  	   assert(foundnonbin != NULL);
121  	   assert(implidx != NULL);
122  	   assert(nimplidx != NULL);
123  	   assert(lastbounds != NULL);
124  	
125  	   /* 1. case: lower bound in set */
126  	   if( !boundtypes[pos] )
127  	   {
128  	      assert(counts[varidx] <= pos - nredvars + 1);
129  	
130  	      /* update implication counter of set variable */
131  	      if( counts[varidx] == pos - nredvars )
132  	      {
133  	         ++counts[varidx];
134  	
135  	         if( counts[varidx] == 1 )
136  	         {
137  	            assert(*ncountnonzeros < 2*nvars);
138  	            countnonzeros[*ncountnonzeros] = varidx;
139  	            ++(*ncountnonzeros);
140  	            newbounds[varidx] = bounds[pos];
141  	            lastbounds[*nimplidx] = SCIP_INVALID;
142  	         }
143  	         else if( newbounds[varidx] > bounds[pos] )
144  	         {
145  	            lastbounds[*nimplidx] = newbounds[varidx];
146  	            newbounds[varidx] = bounds[pos];
147  	         }
148  	         else
149  	         {
150  	            lastbounds[*nimplidx] = SCIP_INVALID;
151  	         }
152  	
153  	         *foundnonbin = MIN(*foundnonbin, varidx);
154  	
155  	         implidx[*nimplidx] = varidx;
156  	         ++(*nimplidx);
157  	      }
158  	
159  	      nimpls = SCIPvarGetNVubs(var);
160  	      implvars = SCIPvarGetVubVars(var);
161  	      implcoefs = SCIPvarGetVubCoefs(var);
162  	      implconsts = SCIPvarGetVubConstants(var);
163  	
164  	      for( w = nimpls - 1; w >= 0; --w )
165  	      {
166  	         assert(!SCIPisZero(scip, implcoefs[w]));
167  	         idx = SCIPvarGetProbindex(implvars[w]);
168  	
169  	         /* do not use inactive variables */
170  	         /* @todo if implvars[x] is aggregated, we could transform the variable into the active representation */
171  	         if( idx < 0 || SCIPisFeasEQ(scip, SCIPvarGetLbGlobal(implvars[w]), SCIPvarGetUbGlobal(implvars[w])) )
172  	            continue;
173  	
174  	         /* the upper bound of implvars[w] is bounding upper bound of var */
175  	         if( implcoefs[w] < 0.0 )
176  	         {
177  	            /* update the counters and implied bounds */
178  	            idx += nvars;
179  	
180  	            if( counts[idx] == pos - nredvars )
181  	            {
182  	               if( SCIPvarIsBinary(implvars[w]) )
183  	               {
184  	                  /* do not look at fixed variables */
185  	                  if( SCIPvarGetLbGlobal(implvars[w]) > 0.5 || SCIPvarGetUbGlobal(implvars[w]) < 0.5 )
186  	                     continue;
187  	
188  	                  /* (implvars[w] = 1 ===> var <= implcoefs[w] + implconsts[w] and if implcoefs[w] +
189  	                   *  implconsts[w] < bounds[pos]) ===> (because var => bounds[v] ===> implvars[w] = 0)
190  	                   */
191  	                  if( SCIPisFeasLT(scip, implcoefs[w] + implconsts[w], bounds[pos]) )
192  	                  {
193  	                     /* set variable 'var' with bound implies other set variable 'implvars[w]' with corresponding bound
194  	                      * so we can remove the set variable 'var'
195  	                      */
196  	                     if( issetvar[idx] > 0 )
197  	                     {
198  	                        SCIPdebugMsg(scip, "set variable <%s> %s %g implies other set variable <%s> %s %g\n",
199  	                           SCIPvarGetName(var), ">=", bounds[pos], SCIPvarGetName(implvars[w]), "<=", 0.0);
200  	
201  	                        issetvar[varidx] = -1;
202  	                        break;
203  	                     }
204  	
205  	                     ++counts[idx];
206  	                     *foundbin = MIN(*foundbin, idx);
207  	
208  	                     if( counts[idx] == 1 )
209  	                     {
210  	                        assert(*ncountnonzeros < 2*nvars);
211  	                        countnonzeros[*ncountnonzeros] = idx;
212  	                        ++(*ncountnonzeros);
213  	                     }
214  	
215  	                     implidx[*nimplidx] = idx;
216  	                     ++(*nimplidx);
217  	                  }
218  	               }
219  	               /* if (implvars[w] = ub(implvars[w]) ==> var <= implcoefs[w]*SCIPvarGetUbGlobal(implvars[w]) +
220  	                * implconsts[w]) but (var >= bounds[pos] with bounds[pos] >
221  	                * implcoefs[w]*SCIPvarGetUbGlobal(implvars[w]) + implconsts[w]) it follows (new_ub(var) <
222  	                * ub(var))
223  	                */
224  	               else if( SCIPisFeasLT(scip, implcoefs[w] * SCIPvarGetUbGlobal(implvars[w]) + implconsts[w], bounds[pos]) )
225  	               {
226  	                  SCIP_Real newub;
227  	
228  	                  newub = (bounds[pos] - implconsts[w]) / implcoefs[w];
229  	
230  	                  /* set variable 'var' with bound implies other set variable 'implvars[w]' with corresponding bound so
231  	                   * we can remove the set variable 'var'
232  	                   */
233  	                  if( issetvar[idx] > 0 && newub <= bounds[issetvar[idx] - 1] )
234  	                  {
235  	                     SCIPdebugMsg(scip, "set variable <%s> %s %g implies other set variable <%s> %s %g (%g)\n",
236  	                        SCIPvarGetName(var), ">=", bounds[pos], SCIPvarGetName(implvars[w]), "<=", newub, bounds[issetvar[idx] - 1] );
237  	
238  	                     issetvar[varidx] = -1;
239  	                     break;
240  	                  }
241  	
242  	                  ++counts[idx];
243  	
244  	                  if( counts[idx] == 1 )
245  	                  {
246  	                     assert(*ncountnonzeros < 2*nvars);
247  	                     countnonzeros[*ncountnonzeros] = idx;
248  	                     ++(*ncountnonzeros);
249  	                     newbounds[idx] = newub;
250  	                     lastbounds[*nimplidx] = SCIP_INVALID;
251  	                  }
252  	                  else if( newbounds[idx] < newub )
253  	                  {
254  	                     lastbounds[*nimplidx] = newbounds[idx];
255  	                     newbounds[idx] = newub;
256  	                  }
257  	                  else
258  	                     lastbounds[*nimplidx] = SCIP_INVALID;
259  	
260  	                  *foundnonbin = MIN(*foundnonbin, idx);
261  	
262  	                  implidx[*nimplidx] = idx;
263  	                  ++(*nimplidx);
264  	               }
265  	            }
266  	         }
267  	         else
268  	         {
269  	            assert(counts[varidx] <= pos - nredvars + 1);
270  	
271  	            /* update the counters and implied bounds */
272  	            if( counts[idx] == pos - nredvars )
273  	            {
274  	               if( SCIPvarIsBinary(implvars[w]) )
275  	               {
276  	                  /* do not look at fixed variables */
277  	                  if( SCIPvarGetLbGlobal(implvars[w]) > 0.5 || SCIPvarGetUbGlobal(implvars[w]) < 0.5 )
278  	                     continue;
279  	
280  	                  /* (implvars[w] = 0 ===> var <= implconsts[w] and if implconsts[w] < bounds[pos]) ===> (because
281  	                   *  var >= bounds[pos] ===> implvars[w] = 1)
282  	                   */
283  	                  if( SCIPisFeasLT(scip, implconsts[w], bounds[pos]) )
284  	                  {
285  	                     /* set variable 'var' with bound implies other set variable 'implvars[w]' with corresponding bound
286  	                      * so we can remove the set variable 'var'
287  	                      */
288  	                     if( issetvar[idx] > 0 )
289  	                     {
290  	                        SCIPdebugMsg(scip, "set variable <%s> %s %g implies other set variable <%s> %s %g\n",
291  	                           SCIPvarGetName(var), ">=", bounds[pos], SCIPvarGetName(implvars[w]), ">=", 1.0);
292  	
293  	                        issetvar[varidx] = -1;
294  	                        break;
295  	                     }
296  	
297  	                     ++counts[idx];
298  	                     *foundbin = MIN(*foundbin, idx);
299  	
300  	                     if( counts[idx] == 1 )
301  	                     {
302  	                        assert(*ncountnonzeros < 2*nvars);
303  	                        countnonzeros[*ncountnonzeros] = idx;
304  	                        ++(*ncountnonzeros);
305  	                     }
306  	
307  	                     implidx[*nimplidx] = idx;
308  	                     ++(*nimplidx);
309  	                  }
310  	               }
311  	               /* if (implvars[w] = lb(implvars[w]) => var <= implcoefs[w]*SCIPvarGetLbGlobal(implvars[w]) +
312  	                * implconsts[w]) but (var >= bounds[pos] with bounds[pos] >
313  	                * implcoefs[w]*SCIPvarGetLbGlobal(implvars[w]) + implconsts[w]) it follows (new_lb(var) >
314  	                * lb(var))
315  	                */
316  	               else if( SCIPisFeasLT(scip, implcoefs[w]*SCIPvarGetLbGlobal(implvars[w]) + implconsts[w], bounds[pos]) )
317  	               {
318  	                  SCIP_Real newlb;
319  	
320  	                  newlb = (bounds[pos] - implconsts[w]) / implcoefs[w];
321  	
322  	                  /* set variable 'var' with bound implies other set variable 'implvars[w]' with corresponding bound so
323  	                   * we can remove the set variable 'var'
324  	                   */
325  	                  if( issetvar[idx] > 0 && newlb >= bounds[issetvar[idx] - 1] )
326  	                  {
327  	                     SCIPdebugMsg(scip, "set variable <%s> %s %g implies other set variable <%s> %s %g (%g)\n",
328  	                        SCIPvarGetName(var), ">=", bounds[pos], SCIPvarGetName(implvars[w]), ">=", newlb, bounds[issetvar[idx] - 1] );
329  	
330  	                     issetvar[varidx] = -1;
331  	                     break;
332  	                  }
333  	
334  	                  ++counts[idx];
335  	
336  	                  if( counts[idx] == 1 )
337  	                  {
338  	                     assert(*ncountnonzeros < 2*nvars);
339  	                     countnonzeros[*ncountnonzeros] = idx;
340  	                     ++(*ncountnonzeros);
341  	                     lastbounds[*nimplidx] = SCIP_INVALID;
342  	                     newbounds[idx] = newlb;
343  	                  }
344  	                  else if( newbounds[idx] > newlb )
345  	                  {
346  	                     lastbounds[*nimplidx] = newbounds[idx];
347  	                     newbounds[idx] = newlb;
348  	                  }
349  	                  else
350  	                     lastbounds[*nimplidx] = SCIP_INVALID;
351  	
352  	                  *foundnonbin = MIN(*foundnonbin, idx);
353  	
354  	                  implidx[*nimplidx] = idx;
355  	                  ++(*nimplidx);
356  	               }
357  	            }
358  	         }
359  	      }
360  	   }
361  	   /* 2.case: upper bound in set */
362  	   else
363  	   {
364  	      assert(boundtypes[pos]);
365  	      assert(counts[varidx] <= pos - nredvars + 1);
366  	
367  	      /* update implication counter of set variable */
368  	      if( counts[varidx] == pos - nredvars )
369  	      {
370  	         ++counts[varidx];
371  	
372  	         if( counts[varidx] == 1 )
373  	         {
374  	            assert(*ncountnonzeros < 2*nvars);
375  	            countnonzeros[*ncountnonzeros] = varidx;
376  	            ++(*ncountnonzeros);
377  	            newbounds[varidx] = bounds[pos];
378  	            lastbounds[*nimplidx] = SCIP_INVALID;
379  	         }
380  	         else if( newbounds[varidx] < bounds[pos] )
381  	         {
382  	            lastbounds[*nimplidx] = newbounds[varidx];
383  	            newbounds[varidx] = bounds[pos];
384  	         }
385  	         else
386  	         {
387  	            lastbounds[*nimplidx] = SCIP_INVALID;
388  	         }
389  	
390  	         *foundnonbin = MIN(*foundnonbin, varidx);
391  	
392  	         implidx[*nimplidx] = varidx;
393  	         ++(*nimplidx);
394  	      }
395  	
396  	      nimpls = SCIPvarGetNVlbs(var);
397  	      implvars = SCIPvarGetVlbVars(var);
398  	      implcoefs = SCIPvarGetVlbCoefs(var);
399  	      implconsts = SCIPvarGetVlbConstants(var);
400  	
401  	      for( w = nimpls - 1; w >= 0; --w )
402  	      {
403  	         assert(!SCIPisZero(scip, implcoefs[w]));
404  	         idx = SCIPvarGetProbindex(implvars[w]);
405  	
406  	         /* do not use inactive variables */
407  	         /* @todo if implvars[x] is aggregated, we could transform the variable into the active representation */
408  	         if( idx < 0 || SCIPisFeasEQ(scip, SCIPvarGetLbGlobal(implvars[w]), SCIPvarGetUbGlobal(implvars[w])) )
409  	            continue;
410  	
411  	         /* the lower bound of implvars[w] is bounding lower bound of var */
412  	         if( implcoefs[w] < 0.0 )
413  	         {
414  	            assert(counts[idx] <= pos - nredvars + 1);
415  	
416  	            /* update the counters and implied bounds */
417  	            if( counts[idx] == pos - nredvars )
418  	            {
419  	               if( SCIPvarIsBinary(implvars[w]) )
420  	               {
421  	                  /* do not look at fixed variables */
422  	                  if( SCIPvarGetLbGlobal(implvars[w]) > 0.5 || SCIPvarGetUbGlobal(implvars[w]) < 0.5 )
423  	                     continue;
424  	
425  	                  /* (implvars[w] = 0 ===> var >= implconsts[w] and if implconsts[w] > bounds[pos]) ===> (because
426  	                   *  var <= bounds[pos] ===> implvars[w] = 1)
427  	                   */
428  	                  if( SCIPisFeasGT(scip, implconsts[w], bounds[pos]) )
429  	                  {
430  	                     if( issetvar[idx] > 0 )
431  	                     {
432  	                        SCIPdebugMsg(scip, "set variable <%s> %s %g implies other set variable <%s> %s %g\n",
433  	                           SCIPvarGetName(var), "<=", bounds[pos], SCIPvarGetName(implvars[w]), ">=", 1.0);
434  	
435  	                        issetvar[varidx] = -1;
436  	                        break;
437  	                     }
438  	
439  	                     ++counts[idx];
440  	                     *foundbin = MIN(*foundbin, idx);
441  	
442  	                     if( counts[idx] == 1 )
443  	                     {
444  	                        assert(*ncountnonzeros < 2*nvars);
445  	                        countnonzeros[*ncountnonzeros] = idx;
446  	                        ++(*ncountnonzeros);
447  	                     }
448  	
449  	                     implidx[*nimplidx] = idx;
450  	                     ++(*nimplidx);
451  	                  }
452  	               }
453  	               /* if (implvars[w] = lb(implvars[w]) ==> var <= implcoefs[w]*SCIPvarGetLbGlobal(implvars[w]) +
454  	                * implconsts[w]) but (var <= bounds[pos] with bounds[pos] <
455  	                * implcoefs[w]*SCIPvarGetLbGlobal(implvars[w]) + implconsts[w]) it follows (new_lb(var) >
456  	                * ub(var))
457  	                */
458  	               else if( SCIPisFeasGT(scip, implcoefs[w]*SCIPvarGetLbGlobal(implvars[w]) + implconsts[w], bounds[pos]) )
459  	               {
460  	                  SCIP_Real newlb;
461  	
462  	                  newlb = (bounds[pos] - implconsts[w]) / implcoefs[w];
463  	
464  	                  if( issetvar[idx] > 0 && newlb >= bounds[issetvar[idx] - 1] )
465  	                  {
466  	                     SCIPdebugMsg(scip, "set variable <%s> %s %g implies other set variable <%s> %s %g (%g)\n",
467  	                        SCIPvarGetName(var), "<=", bounds[pos], SCIPvarGetName(implvars[w]), ">=",  newlb, bounds[issetvar[idx] - 1]);
468  	
469  	                     issetvar[varidx] = -1;
470  	                     break;
471  	                  }
472  	
473  	                  ++counts[idx];
474  	
475  	                  if( counts[idx] == 1 )
476  	                  {
477  	                     assert(*ncountnonzeros < 2*nvars);
478  	                     countnonzeros[*ncountnonzeros] = idx;
479  	                     ++(*ncountnonzeros);
480  	                     lastbounds[*nimplidx] = SCIP_INVALID;
481  	                     newbounds[idx] = newlb;
482  	                  }
483  	                  else if( newbounds[idx] > newlb )
484  	                  {
485  	                     lastbounds[*nimplidx] = newbounds[idx];
486  	                     newbounds[idx] = newlb;
487  	                  }
488  	                  else
489  	                     lastbounds[*nimplidx] = SCIP_INVALID;
490  	
491  	                  *foundnonbin = MIN(*foundnonbin, idx);
492  	
493  	                  implidx[*nimplidx] = idx;
494  	                  ++(*nimplidx);
495  	               }
496  	            }
497  	         }
498  	         else
499  	         {
500  	            /* update the counters and implied bounds */
501  	            idx += nvars;
502  	
503  	            assert(counts[idx] <= pos - nredvars + 1);
504  	
505  	            if( counts[idx] == pos - nredvars )
506  	            {
507  	               if( SCIPvarIsBinary(implvars[w]) )
508  	               {
509  	                  /* do not look at fixed variables */
510  	                  if( SCIPvarGetLbGlobal(implvars[w]) > 0.5 || SCIPvarGetUbGlobal(implvars[w]) < 0.5 )
511  	                     continue;
512  	
513  	                  /* (implvars[w] = 1 ===> var >= implcoefs[w] + implconsts[w] and if implcoefs[w] +
514  	                   *  implconsts[w] > bounds[pos]) ===> (because var <= bounds[pos] ===> implvars[w] = 0)
515  	                   */
516  	                  if( SCIPisFeasGT(scip, implcoefs[w] + implconsts[w], bounds[pos]) )
517  	                  {
518  	                     if( issetvar[idx] > 0 )
519  	                     {
520  	                        SCIPdebugMsg(scip, "set variable <%s> %s %g implies other set variable <%s> %s %g\n",
521  	                           SCIPvarGetName(var), "<=", bounds[pos], SCIPvarGetName(implvars[w]), "<=", 0.0);
522  	
523  	                        issetvar[varidx] = -1;
524  	                        break;
525  	                     }
526  	
527  	                     ++counts[idx];
528  	                     *foundbin = MIN(*foundbin, idx);
529  	
530  	                     if( counts[idx] == 1 )
531  	                     {
532  	                        assert(*ncountnonzeros < 2*nvars);
533  	                        countnonzeros[*ncountnonzeros] = idx;
534  	                        ++(*ncountnonzeros);
535  	                     }
536  	
537  	                     implidx[*nimplidx] = idx;
538  	                     ++(*nimplidx);
539  	                  }
540  	               }
541  	               /* if (implvars[w] = ub(implvars[w]) => var <= implcoefs[w]*SCIPvarGetUbGlobal(implvars[w]) +
542  	                * implconsts[w]) but (var <= bounds[pos] with bounds[pos] <
543  	                * implcoefs[w]*SCIPvarGetUbGlobal(implvars[w]) + implconsts[w]) it follows (new_ub(var) <
544  	                * ub(var))
545  	                */
546  	               else if( SCIPisFeasGT(scip, implcoefs[w]*SCIPvarGetUbGlobal(implvars[w]) + implconsts[w], bounds[pos]) )
547  	               {
548  	                  SCIP_Real newub;
549  	
550  	                  newub = (bounds[pos] - implconsts[w]) / implcoefs[w];
551  	
552  	                  if( issetvar[idx] > 0 && newub <= bounds[issetvar[idx] - 1] )
553  	                  {
554  	                     SCIPdebugMsg(scip, "set variable <%s> %s %g implies other set variable <%s> %s %g (%g)\n",
555  	                        SCIPvarGetName(var), "<=", bounds[pos], SCIPvarGetName(implvars[w]), "<=",  newub, bounds[issetvar[idx] - 1]);
556  	
557  	                     issetvar[varidx] = -1;
558  	                     break;
559  	                  }
560  	
561  	                  ++counts[idx];
562  	
563  	                  if( counts[idx] == 1 )
564  	                  {
565  	                     assert(*ncountnonzeros < 2*nvars);
566  	                     countnonzeros[*ncountnonzeros] = idx;
567  	                     ++(*ncountnonzeros);
568  	                     lastbounds[*nimplidx] = SCIP_INVALID;
569  	                     newbounds[idx] = newub;
570  	                  }
571  	                  else if( newbounds[idx] < newub )
572  	                  {
573  	                     lastbounds[*nimplidx] = newbounds[idx];
574  	                     newbounds[idx] = newub;
575  	                  }
576  	                  else
577  	                     lastbounds[*nimplidx] = SCIP_INVALID;
578  	
579  	                  *foundnonbin = MIN(*foundnonbin, idx);
580  	
581  	                  implidx[*nimplidx] = idx;
582  	                  ++(*nimplidx);
583  	               }
584  	            }
585  	         }
586  	      }
587  	   }
588  	}
589  	
590  	
591  	/** collect non-binary implication data for variable set reduction and global bound implications; only variable which
592  	 *  have the vartype SCIP_VARTYPE_BINARY have implications, otherwise the implications are saved as variable bounds
593  	 */
594  	static
595  	void collectNonBinaryImplicationData(
596  	   SCIP*                 scip,               /**< SCIP data structure */
597  	   SCIP_VAR*             var,                /**< set variable */
598  	   int                   varidx,             /**< for lower bound set variable index, for upper bound set
599  	                                              *   variable index + number of variables
600  	                                              */
601  	   int                   pos,                /**< variables's position in bdchinfos */
602  	   int                   nredvars,           /**< number of reduced variables so far */
603  	   SCIP_Bool             value,              /**< value used for clique and implication info */
604  	   SCIP_Real*            bounds,             /**< array of bounds where one of them must be fullfilled */
605  	   SCIP_Bool*            boundtypes,         /**< array of bound types */
606  	   SCIP_Real*            newbounds,          /**< array of implied bounds(, size is two times number of variables, first
607  	                                              *   half for implied lower bounds, second for implied upper bounds)
608  	                                              */
609  	   int*                  counts,             /**< array of number of implication on a bound (, size is two times number
610  	                                              *   of variables, first half for implied lower bounds, second for implied
611  	                                              *   upper bounds)
612  	                                              */
613  	   int*                  countnonzeros,      /**< array to store the indices of non-zero entries in the counts array */
614  	   int*                  ncountnonzeros,     /**< pointer to store the number of non-zero entries in the counts array */
615  	   int*                  issetvar,           /**< array containing for set variables the position in the current set, or
616  	                                              *   0 if it is not a set variable or -1, if it is a redundant(i.e. implies
617  	                                              *   another set variable) set variables(, size is two times number of
618  	                                              *   variables, first half for implied lower bounds, second for implied
619  	                                              *   upper bounds) */
620  	   int                   nvars,              /**< number of problem variables */
621  	   int*                  foundbin,           /**< pointer to store the lowest index of a binary implication variable
622  	                                              *   when found
623  	                                              */
624  	   int*                  foundnonbin,        /**< pointer to store the lowest index of a non-binary implication variable
625  	                                              *   when found
626  	                                              */
627  	   int*                  implidx,            /**< array to store the variable indices (for upper bound 'nvars' is added
628  	                                              *   to the index) which are implied
629  	                                              */
630  	   int*                  nimplidx,           /**< pointer to store the number of implied variables */
631  	   SCIP_Real*            lastbounds          /**< array to remember last implied bounds before taken the current
632  	                                              *   variable into account, first nvars for lower bound, second nvars for
633  	                                              *   upper bound
634  	                                              *
635  	                                              *   this array is used when a set variable got redundant, because it
636  	                                              *   implies another set variable, and we need to correct the counts array
637  	                                              */
638  	   )
639  	{
640  	   assert(scip != NULL);
641  	   assert(var != NULL);
642  	   assert(SCIPvarGetType(var) == SCIP_VARTYPE_BINARY);
643  	   assert(varidx >= 0);
644  	   assert(pos >= 0);
645  	   assert(bounds != NULL);
646  	   assert(boundtypes != NULL);
647  	   assert(newbounds != NULL);
648  	   assert(counts != NULL);
649  	   assert(issetvar != NULL);
650  	   assert(2 * nvars > varidx);
651  	   assert(foundbin != NULL);
652  	   assert(foundnonbin != NULL);
653  	   assert(implidx != NULL);
654  	   assert(nimplidx != NULL);
655  	   assert(lastbounds != NULL);
656  	
657  	   if( issetvar[varidx] > 0 )
658  	   {
659  	      SCIP_VAR** implvars;
660  	      SCIP_Real* implbounds;
661  	      SCIP_BOUNDTYPE* implboundtypes;
662  	      int idx;
663  	      int w;
664  	
665  	      /* get implication information */
666  	      implvars = SCIPvarGetImplVars(var, value);
667  	      implboundtypes = SCIPvarGetImplTypes(var, value);
668  	      implbounds = SCIPvarGetImplBounds(var, value);
669  	
670  	      for( w = SCIPvarGetNImpls(var, value) - 1; w >= 0; --w )
671  	      {
672  	         assert(implvars != NULL);
673  	         assert(implboundtypes != NULL);
674  	
675  	         /* no self implication should exist in the implication data structure */
676  	         assert(implvars[w] != var);
677  	
678  	         idx = SCIPvarGetProbindex(implvars[w]);
679  	
680  	         /* do not use inactive variables */
681  	         /* @todo if implvars[x] is aggregated, we could transform the variable into the active representation */
682  	         if( idx < 0 || SCIPisFeasEQ(scip, SCIPvarGetLbGlobal(implvars[w]), SCIPvarGetUbGlobal(implvars[w])) )
683  	            continue;
684  	
685  	         if( implboundtypes[w] == SCIP_BOUNDTYPE_UPPER )
686  	         {
687  	            SCIP_Bool redundant;
688  	
689  	            idx += nvars;
690  	
691  	            assert(counts[idx] <= pos - nredvars + 1);
692  	
693  	            /* set variable 'var' with bound implies other set variable 'implvars[w]' with a non-worse bound than the
694  	             * bound so we can remove the set variable 'var'
695  	             */
696  	            if( issetvar[idx] > 0 && bounds[issetvar[idx] - 1] >= implbounds[w] )
697  	            {
698  	               SCIPdebugMsg(scip, "set variable <%s> %s %g implies other set variable <%s> %s %g (%g)\n",
699  	                  SCIPvarGetName(var), boundtypes[pos] ? "<=" : ">=", bounds[pos], SCIPvarGetName(implvars[w]),
700  	                  "<=", implbounds[w], bounds[issetvar[idx] - 1]);
701  	
702  	               issetvar[varidx] = -1;
703  	               break;
704  	            }
705  	
706  	            /* ignore implications that are redundant with respect to the current global bounds (see #2888) */
707  	            redundant = SCIPisLE(scip, SCIPvarGetUbGlobal(implvars[w]), implbounds[w]);
708  	
709  	            /* update implication counter and implied upper bound */
710  	            if( counts[idx] == pos - nredvars && !redundant )
711  	            {
712  	               ++counts[idx];
713  	
714  	               if( SCIPvarIsBinary(implvars[w]) )
715  	               {
716  	                  /* the implied upper bound on a binary variable should not be trivial, otherwise we might globally fix
717  	                   * this variable to a wrong value
718  	                   *
719  	                   * @note it is possible that the implied bound is lower than zero, when the implied variable has
720  	                   * become binary during the search
721  	                   */
722  	                  assert(SCIPisFeasLE(scip, implbounds[w], 0.0));
723  	                  *foundbin = MIN(*foundbin, idx);
724  	
725  	                  if( counts[idx] == 1 )
726  	                  {
727  	                     assert(*ncountnonzeros < 2*nvars);
728  	                     countnonzeros[*ncountnonzeros] = idx;
729  	                     ++(*ncountnonzeros);
730  	                  }
731  	               }
732  	               else
733  	               {
734  	                  *foundnonbin = MIN(*foundnonbin, idx);
735  	
736  	                  if( counts[idx] == 1 )
737  	                  {
738  	                     assert(*ncountnonzeros < 2*nvars);
739  	                     countnonzeros[*ncountnonzeros] = idx;
740  	                     ++(*ncountnonzeros);
741  	                     newbounds[idx] = implbounds[w];
742  	                     lastbounds[*nimplidx] = SCIP_INVALID;
743  	                  }
744  	                  else if( newbounds[idx] < implbounds[w] )
745  	                  {
746  	                     lastbounds[*nimplidx] = newbounds[idx];
747  	                     newbounds[idx] = implbounds[w];
748  	                  }
749  	                  else
750  	                     lastbounds[*nimplidx] = SCIP_INVALID;
751  	               }
752  	
753  	               implidx[*nimplidx] = idx;
754  	               ++(*nimplidx);
755  	            }
756  	         }
757  	         else
758  	         {
759  	            SCIP_Bool redundant;
760  	
761  	            assert(counts[idx] <= pos - nredvars + 1);
762  	
763  	            /* set variable 'var' with bound implies other set variable 'implvars[w]' with a non-worse bound than the
764  	             * bound so we can remove the set variable 'var'
765  	             */
766  	            if( issetvar[idx] > 0 && bounds[issetvar[idx] - 1] <= implbounds[w] )
767  	            {
768  	               SCIPdebugMsg(scip, "set variable <%s> %s %g implies other set variable <%s> %s %g (%g)\n",
769  	                  SCIPvarGetName(var), boundtypes[pos] ? "<=" : ">=", bounds[pos], SCIPvarGetName(implvars[w]),
770  	                  ">=", implbounds[w], bounds[issetvar[idx] - 1]);
771  	
772  	               issetvar[varidx] = -1;
773  	               break;
774  	            }
775  	
776  	            /* ignore implications that are redundant with respect to the current global bounds (see #2888) */
777  	            redundant = SCIPisGE(scip, SCIPvarGetLbGlobal(implvars[w]), implbounds[w]);
778  	
779  	            /* update implication counter */
780  	            if( counts[idx] == pos - nredvars && !redundant )
781  	            {
782  	               ++counts[idx];
783  	
784  	               if( SCIPvarIsBinary(implvars[w]) )
785  	               {
786  	                  /* the implied lower bound on a binary variable should not be trivial, otherwise we might globally fix
787  	                   * this variable to a wrong value
788  	                   *
789  	                   * @note is is possible that the implied bound is greater than one, when the implied variable has
790  	                   * become binary during the search
791  	                   */
792  	                  assert(SCIPisFeasGE(scip, implbounds[w], 1.0));
793  	                  *foundbin = MIN(*foundbin, idx);
794  	
795  	                  if( counts[idx] == 1 )
796  	                  {
797  	                     assert(*ncountnonzeros < 2*nvars);
798  	                     countnonzeros[*ncountnonzeros] = idx;
799  	                     ++(*ncountnonzeros);
800  	                  }
801  	               }
802  	               else
803  	               {
804  	                  *foundnonbin = MIN(*foundnonbin, idx);
805  	
806  	                  if( counts[idx] == 1 )
807  	                  {
808  	                     assert(*ncountnonzeros < 2*nvars);
809  	                     countnonzeros[*ncountnonzeros] = idx;
810  	                     ++(*ncountnonzeros);
811  	                     newbounds[idx] = implbounds[w];
812  	                     lastbounds[*nimplidx] = SCIP_INVALID;
813  	                  }
814  	                  else if( newbounds[idx] > implbounds[w] )
815  	                  {
816  	                     lastbounds[*nimplidx] = newbounds[idx];
817  	                     newbounds[idx] = implbounds[w];
818  	                  }
819  	                  else
820  	                     lastbounds[*nimplidx] = SCIP_INVALID;
821  	               }
822  	
823  	               implidx[*nimplidx] = idx;
824  	               ++(*nimplidx);
825  	            }
826  	         }
827  	      }
828  	   }
829  	}
830  	
831  	/** collect clique data on binary variables for variable set reduction and global bound implications */
832  	static
833  	void collectBinaryCliqueData(
834  	   SCIP_VAR*             var,                /**< set variable */
835  	   int                   varidx,             /**< for lower bound set variable index, for upper bound set variable index
836  	                                              *   + number of variables
837  	                                              */
838  	   int                   pos,                /**< variables's position in bdchinfos */
839  	   int                   nredvars,           /**< number of reduced variables so far */
840  	   SCIP_Bool             value,              /**< value used for clique and implication info */
841  	   SCIP_Real*            bounds,             /**< array of bounds where one of them must be fullfilled */
842  	   SCIP_Bool*            boundtypes,         /**< array of bound types */
843  	   SCIP_Real*            newbounds,          /**< array of implied bounds(, size is two times number of variables, first
844  	                                              *   half for implied lower bounds, second for implied upper bounds)
845  	                                              */
846  	   int*                  counts,             /**< array of number of implication on a bound (, size is two times number of
847  	                                              *   variables, first half for implied lower bounds, second for implied upper
848  	                                              *   bounds)
849  	                                              */
850  	   int*                  countnonzeros,      /**< array to store the indices of non-zero entries in the counts array */
851  	   int*                  ncountnonzeros,     /**< pointer to store the number of non-zero entries in the counts array */
852  	   int*                  issetvar,           /**< array containing for set variables the position in the current set, or
853  	                                              *   0 if it is not a set variable, or -1, if it is a redundant (i.e. implies
854  	                                              *   another set variable) set variable
855  	                                              *   (the size of the array is two times the number of variables, first half
856  	                                              *   for implied lower bounds, second for implied upper bounds)
857  	                                              */
858  	   int                   nvars,              /**< number of problem variables */
859  	   int*                  foundbin,           /**< pointer to store the lowest index of a binary implication variable when found */
860  	   int*                  implidx,            /**< array to store the variable indices (for upper bound 'nvars' is added
861  	                                              *   to the index) which are implied
862  	                                              */
863  	   int*                  nimplidx            /**< pointer to store the number of implied variables */
864  	   )
865  	{
866  	   SCIP_CLIQUE** cliques;
867  	   SCIP_VAR** clqvars;
868  	   SCIP_Bool* clqvalues;
869  	   int idx;
870  	   int c;
871  	   int w;
872  	
873  	   assert(var != NULL);
874  	   assert(SCIPvarIsBinary(var));
875  	   assert(varidx >= 0);
876  	   assert(pos >= 0);
877  	   assert(bounds != NULL);
878  	   assert(boundtypes != NULL);
879  	   assert(newbounds != NULL);
880  	   assert(counts != NULL);
881  	   assert(issetvar != NULL);
882  	   assert(2 * nvars > varidx);
883  	   assert(foundbin != NULL);
884  	   assert(implidx != NULL);
885  	   assert(nimplidx != NULL);
886  	
887  	   /* implication counter cannot exceed number implication variables */
888  	   assert(counts[varidx] <= pos - nredvars);
889  	
890  	   /* if the set variable is not yet redundant we might increase the self implication counter */
891  	   if( issetvar[varidx] > 0 )
892  	   {
893  	      /* update implication counter for set variables */
894  	      if( counts[varidx] == pos - nredvars )
895  	      {
896  	         ++counts[varidx];
897  	         *foundbin = MIN(*foundbin, varidx);
898  	
899  	         if( counts[varidx] == 1 )
900  	         {
901  	            assert(*ncountnonzeros < 2*nvars);
902  	            countnonzeros[*ncountnonzeros] = varidx;
903  	            ++(*ncountnonzeros);
904  	         }
905  	
906  	         implidx[*nimplidx] = varidx;
907  	         ++(*nimplidx);
908  	      }
909  	   }
910  	
911  	   cliques = SCIPvarGetCliques(var, value);
912  	
913  	   /* update implication counter on all by cliques implied variables */
914  	   for( c = SCIPvarGetNCliques(var, value) - 1; c >= 0; --c )
915  	   {
916  	      clqvars = SCIPcliqueGetVars(cliques[c]);
917  	      clqvalues = SCIPcliqueGetValues(cliques[c]);
918  	
919  	      for( w = SCIPcliqueGetNVars(cliques[c]) - 1; w >= 0; --w )
920  	      {
921  	         /* already handle self-implication and do not look at fixed variables */
922  	         if( clqvars[w] == var || SCIPvarGetLbGlobal(clqvars[w]) > 0.5 || SCIPvarGetUbGlobal(clqvars[w]) < 0.5 )
923  	            continue;
924  	
925  	         idx = SCIPvarGetProbindex(clqvars[w]);
926  	         assert(idx >= 0);
927  	
928  	         if( clqvalues[w] )
929  	            idx += nvars;
930  	
931  	         assert(counts[idx] <= pos - nredvars + 1);
932  	
933  	         /* set variable 'var' with bound implies other set variable 'clqvars[w]' with corresponding set bound so we can
934  	          * remove the set variable 'var'
935  	          */
936  	         if( issetvar[idx] > 0 )
937  	         {
938  	            SCIPdebugMessage("set variable <%s> %s %g implies other set variable <%s> %s %g\n",
939  	               SCIPvarGetName(var), boundtypes[pos] ? "<=" : ">=", bounds[pos], SCIPvarGetName(clqvars[w]),
940  	               clqvalues[w] ? "<=" : ">=", clqvalues[w] ? 0.0 : 1.0);
941  	
942  	            issetvar[varidx] = -1;
943  	            break;
944  	         }
945  	
946  	         /* update implication counter */
947  	         if( counts[idx] == pos - nredvars )
948  	         {
949  	            ++counts[idx];
950  	            *foundbin = MIN(*foundbin, idx);
951  	
952  	            if( counts[idx] == 1 )
953  	            {
954  	               assert(*ncountnonzeros < 2*nvars);
955  	               countnonzeros[*ncountnonzeros] = idx;
956  	               ++(*ncountnonzeros);
957  	            }
958  	
959  	            implidx[*nimplidx] = idx;
960  	            ++(*nimplidx);
961  	         }
962  	      }
963  	   }
964  	}
965  	
966  	
967  	
968  	/*
969  	 * presolving methods
970  	 */
971  	
972  	#define CLEARRATIO 0.8
973  	
974  	/** try to reduce the necessary variable in a set of variables with corresponding bounds and boundtypes for which one
975  	 *  must be fulfilled
976  	 *
977  	 *  e.g. a set of logicor or bounddisjunctive constraint variables would be such a set
978  	 *
979  	 *  consider the following set:
980  	 *
981  	 *  x1 >= 1, x2 >= 3, x3 >= 1, x4 <= 0
982  	 *
983  	 *  by (global) implication data (cliques, implications, and variable bounds) we have also the following implications
984  	 *  given:
985  	 *
986  	 *  x1 >= 1 => x3 >= 1
987  	 *  x2 >= 2 => x3 >= 1
988  	 *  x4 <= 0 => x1 >= 1
989  	 *
990  	 *  Because of the last implication x4 is redundant, because x1 >= 1 would also be fulfilled in the variable set, so we
991  	 *  can reduce the set by x4.
992  	 *  Also, the both other implications and x3 >= 1 (in the given variable set) all imply exactly x3 >= 1, so we tighten
993  	 *  the global lower bound of x3 to 1 and the set of variables gets redundant.
994  	 */
995  	SCIP_RETCODE SCIPshrinkDisjunctiveVarSet(
996  	   SCIP*                 scip,               /**< SCIP data structure */
997  	   SCIP_VAR**            vars,               /**< variables array for which at least one must be fulfilled in the
998  	                                              *   following bounds and boundtypes */
999  	   SCIP_Real*            bounds,             /**< bounds array for which at least one must be fulfilled */
1000 	   SCIP_Bool*            boundtypes,         /**< boundtypes array (TRUE == SCIP_BOUNDTYPE_UPPER, FALSE == SCIP_BOUNDTYPE_LOWER)
1001 	                                              *   for which at least one must be fulfilled */
1002 	   SCIP_Bool*            redundants,         /**< array which be filled and then indicate if a variable in the set is redundant */
1003 	   int                   nvars,              /**< number of variables */
1004 	   int*                  nredvars,           /**< pointer to store how many variables can be removed */
1005 	   int*                  nglobalred,         /**< pointer to store number of global reductions on variable bounds found
1006 	                                              *   through this set of variables */
1007 	   SCIP_Bool*            setredundant,       /**< pointer to store if we found a global reduction on a variable which was part
1008 	                                              *   of the given set of variables, this makes this disjunction redundant */
1009 	   SCIP_Bool*            glbinfeas,          /**< pointer to store if global infeasibility was detected */
1010 	   SCIP_Bool             fullshortening      /**< do we want to try the shortening procedure over the whole set (which might be expensive) */
1011 	   )
1012 	{
1013 	   SCIP_Real* newbounds; /* array saving all overall implied global bounds, first nprobvars for lower bound, second
1014 	                          * nprobvars for upper bound
1015 	                          */
1016 	   SCIP_Real* lastbounds;/* temporary array to remember last implied bounds before taken the current variable into
1017 	                          * account, first nprobvars for lower bound, second nprobvars for upper bound
1018 	                          *
1019 	                          * this array is used when a set variable got redundant, because it implies another set
1020 	                          * variable, and we need to correct the counts array
1021 	                          */
1022 	   int* issetvar;        /* array for mapping from a problem variable to the position in the variable set (,pos + 1 in
1023 	                          * the variable set, 0 for no set variable, and -1 if this variable was removed from the set),
1024 	                          * first nprobvars for lower bound, second nprobvars for upper bound
1025 	                          */
1026 	   int* counts;          /* array saving number of implication by set variables, first nprobvars for lower bound, second
1027 	                          * nprobvars for upper bound
1028 	                          */
1029 	   int* implidx;         /* temporary array to remember all indices of implied variables by the current set variable
1030 	                          * looked at, first nprobvars for lower bound, second nprobvars for upper bound
1031 	                          *
1032 	                          * this array is used when a set variable got redundant, because it implies another set
1033 	                          * variable, and we need to correct the counts array
1034 	                          */
1035 	   int* countnonzeros;
1036 	
1037 	   SCIP_VAR* var;
1038 	   SCIP_Bool usebin = TRUE;
1039 	   SCIP_Bool usenonbin = TRUE;
1040 	   SCIP_Bool globalred = TRUE;
1041 	   SCIP_Bool reducedset;
1042 	   SCIP_Bool value;
1043 	   SCIP_Bool implbinvarsexist;
1044 	   int start = INT_MAX;
1045 	   int nimplidx;
1046 	   int foundbin;
1047 	   int foundnonbin;
1048 	   int varidx;
1049 	   int nprobvars;
1050 	   int ncountnonzeros;
1051 	   int maxcountnonzeros;
1052 	   int w;
1053 	   int v;
1054 	
1055 	   if( nvars == 0 )
1056 	      return SCIP_OKAY;
1057 	
1058 	   assert(scip != NULL);
1059 	   assert(vars != NULL);
1060 	   assert(bounds != NULL);
1061 	   assert(boundtypes != NULL);
1062 	   assert(redundants != NULL);
1063 	   assert(nredvars != NULL);
1064 	   assert(nglobalred != NULL);
1065 	   assert(setredundant != NULL);
1066 	   assert(glbinfeas != NULL);
1067 	   assert(scip->transprob != NULL);
1068 	   nprobvars = SCIPprobGetNVars(scip->transprob);
1069 	
1070 	   /* allocate temporary memory */
1071 	   SCIP_CALL( SCIPallocCleanBufferArray(scip, &issetvar, 2*nprobvars) ); /*lint !e647*/
1072 	   SCIP_CALL( SCIPallocCleanBufferArray(scip, &counts, 2*nprobvars) ); /*lint !e647*/
1073 	   SCIP_CALL( SCIPallocBufferArray(scip, &newbounds, 2*nprobvars) );
1074 	   SCIP_CALL( SCIPallocBufferArray(scip, &lastbounds, 2*nprobvars) );
1075 	   SCIP_CALL( SCIPallocBufferArray(scip, &implidx, 2*nprobvars) );
1076 	   SCIP_CALL( SCIPallocBufferArray(scip, &countnonzeros, 2*nprobvars) );
1077 	
1078 	   *nredvars = 0;
1079 	   *glbinfeas = FALSE;
1080 	   ncountnonzeros = 0;
1081 	
1082 	   maxcountnonzeros = (int)(2*nprobvars*CLEARRATIO); /*lint !e790*/
1083 	
1084 	   /* initialize variable indices data */
1085 	   for( v = 0; v < nvars; ++v )
1086 	   {
1087 	      varidx = SCIPvarGetProbindex(vars[v]);
1088 	      assert(varidx >= 0);
1089 	
1090 	      if( boundtypes[v] )
1091 	         varidx += nprobvars;
1092 	
1093 	      /* initialize issetvar array */
1094 	      issetvar[varidx] = v+1;
1095 	   }
1096 	
1097 	   /* check if implicit binary variables exist, because for these variables the implications can be stored in the
1098 	    * variable bounds instead of the 'normal' implications
1099 	    */
1100 	   implbinvarsexist = (SCIPprobGetNImplBinVars(scip->transprob) > 0);
1101 	
1102 	#if 0
1103 	   /* @todo do the cleanup here rather than before calling SCIPshrinkDisjunctiveVarSet()? */
1104 	   if( usebin )
1105 	   {
1106 	      SCIP_Bool infeasible;
1107 	
1108 	      SCIP_CALL( SCIPcleanupCliques(scip, &infeasible) );
1109 	   }
1110 	#endif
1111 	
1112 	   /* check for same implicit binary variables */
1113 	   for( v = 0; v < nvars; ++v )
1114 	   {
1115 	      var =  vars[v];
1116 	
1117 	      foundbin = INT_MAX;
1118 	      foundnonbin = INT_MAX;
1119 	      reducedset = FALSE;
1120 	      nimplidx = 0;
1121 	
1122 	      value = (!boundtypes[v]);
1123 	
1124 	      varidx = SCIPvarGetProbindex(var);
1125 	      assert(varidx >= 0);
1126 	
1127 	      if( !value )
1128 	         varidx += nprobvars;
1129 	
1130 	      if( usebin )
1131 	      {
1132 	         /* collect clique data on binary variables */
1133 	         if( SCIPvarIsBinary(var) )
1134 	         {
1135 	            collectBinaryCliqueData(var, varidx, v, *nredvars, value, bounds, boundtypes, newbounds, counts, countnonzeros,
1136 	               &ncountnonzeros, issetvar, nprobvars, &foundbin, implidx, &nimplidx);
1137 	         }
1138 	      }
1139 	
1140 	      /* only variable which have the vartype SCIP_VARTYPE_BINARY have implications, otherwise the implications are
1141 	       * saved as variable bounds
1142 	       *
1143 	       * we only check binary to non-binary implications if we can detect further implications which either lead to
1144 	       * global reductions or to redundant set variables
1145 	       */
1146 	      if( SCIPvarGetType(var) == SCIP_VARTYPE_BINARY && ((usebin && implbinvarsexist) || usenonbin) )
1147 	      {
1148 	         collectNonBinaryImplicationData(scip, var, varidx, v, *nredvars, value, bounds, boundtypes, newbounds, counts,
1149 	            countnonzeros, &ncountnonzeros, issetvar, nprobvars, &foundbin, &foundnonbin, implidx, &nimplidx, lastbounds);
1150 	      }
1151 	      /* only variable which have the vartype != SCIP_VARTYPE_BINARY have variable bounds
1152 	       *
1153 	       * we only check the variable bounds if we can detect further implications which either lead to global reductions
1154 	       * or to redundant set variables
1155 	       */
1156 	      else if( SCIPvarGetType(var) != SCIP_VARTYPE_BINARY && ((usebin && implbinvarsexist) || usenonbin) )
1157 	      {
1158 	         collectNonBinaryVBoundData(scip, var, varidx, v, *nredvars, bounds, boundtypes, newbounds, counts, countnonzeros,
1159 	            &ncountnonzeros, issetvar, nprobvars, &foundbin, &foundnonbin, implidx, &nimplidx, lastbounds);
1160 	      }
1161 	
1162 	      /* reduce implication counters on all variables which are implied by a variable now marked as redundant */
1163 	      if( issetvar[varidx] < 0 )
1164 	      {
1165 	         SCIP_VAR** probvars;
1166 	         int probidx;
1167 	
1168 	         SCIPdebugMsg(scip, "marked variable <%s> as redundant variable in variable set\n", SCIPvarGetName(var));
1169 	
1170 	         probvars = SCIPprobGetVars(scip->transprob);
1171 	         assert(probvars != NULL);
1172 	
1173 	         /* correct implication counters and bounds, if the redundant variable implies other variables we need to reduce
1174 	          * the counter and get the last bounds before this implication
1175 	          */
1176 	         for( w = nimplidx - 1; w >= 0; --w )
1177 	         {
1178 	            assert(implidx[w] < 2 * nprobvars);
1179 	            assert(counts[implidx[w]] == v - (*nredvars) + 1);
1180 	
1181 	            --counts[implidx[w]];
1182 	
1183 	            if( implidx[w] == countnonzeros[ncountnonzeros-1] && counts[implidx[w]] == 0 )
1184 	               --ncountnonzeros;
1185 	
1186 	            probidx = implidx[w] < nprobvars ? implidx[w] : implidx[w] - nprobvars;
1187 	            /* only for non-binary variables we need to correct the bounds */
1188 	            if( !SCIPvarIsBinary(probvars[probidx]) && lastbounds[w] != SCIP_INVALID )/*lint !e777*/
1189 	               newbounds[implidx[w]] = lastbounds[w];
1190 	         }
1191 	
1192 	         reducedset = TRUE;
1193 	         ++(*nredvars);
1194 	      }
1195 	
1196 	      /* check if we want to shorten the whole set of variables, or terminate early if we did not find any further
1197 	       * implication
1198 	       */
1199 	      if( !fullshortening )
1200 	      {
1201 	         /* check if it makes sense to look for further binary implications */
1202 	         if( foundbin < INT_MAX && !reducedset )
1203 	            usebin = FALSE;
1204 	         /* check if it makes sense to look for further non-binary implications */
1205 	         if( foundnonbin < INT_MAX && !reducedset )
1206 	            usenonbin = FALSE;
1207 	      }
1208 	
1209 	      /* are global reductions still possible */
1210 	      globalred = globalred && (foundbin < INT_MAX || foundnonbin < INT_MAX);
1211 	
1212 	      /* remember the first possible position for a global bound change */
1213 	      if( globalred )
1214 	      {
1215 	         /* get correct variable index(, we added nprobvars for the upper bound implication) */
1216 	         if( foundbin < INT_MAX && foundbin >= nprobvars )
1217 	            foundbin -= nprobvars;
1218 	
1219 	         /* get correct variable index(, we added nprobvars for the upper bound implication) */
1220 	         if( foundnonbin < INT_MAX && foundnonbin >= nprobvars )
1221 	            foundnonbin -= nprobvars;
1222 	
1223 	         if( start > foundbin )
1224 	            start = foundbin;
1225 	
1226 	         if( start > foundnonbin )
1227 	            start = foundnonbin;
1228 	      }
1229 	      else
1230 	         start = INT_MAX;
1231 	
1232 	      /* check if it can find any global implications anymore */
1233 	      if( !usebin && !usenonbin )
1234 	         break;
1235 	   }
1236 	
1237 	   /* remove redundant set variables */
1238 	   if( *nredvars > 0 )
1239 	   {
1240 	#ifndef NDEBUG
1241 	      int nreds = 0;
1242 	#endif
1243 	
1244 	      for( v = nvars - 1; v >= 0; --v )
1245 	      {
1246 	         var = vars[v];
1247 	
1248 	         varidx = SCIPvarGetProbindex(var);
1249 	         assert(varidx >= 0);
1250 	
1251 	         if( boundtypes[v] )
1252 	            varidx += nprobvars;
1253 	
1254 	         /* if set variable was marked to be redundant remove it */
1255 	         if( issetvar[varidx] < 0 )
1256 	         {
1257 	            SCIPdebugMsg(scip, "mark redundant variable <%s> to be removed from variable set\n", SCIPvarGetName(var));
1258 	
1259 	            redundants[v] = TRUE;
1260 	#ifndef NDEBUG
1261 	            ++nreds;
1262 	#endif
1263 	         }
1264 	      }
1265 	      assert((*nredvars) == nreds);
1266 	   }
1267 	
1268 	   /* if we found some global boundchanges, we perform then now */
1269 	   if( globalred )
1270 	   {
1271 	      SCIP_VAR** probvars;
1272 	      SCIP_VAR* probvar;
1273 	
1274 	      SCIPdebugMsg(scip, "variable set led to global reductions (in %s)\n", SCIPprobGetName(scip->transprob));
1275 	
1276 	      probvars = SCIPprobGetVars(scip->transprob);
1277 	      assert(probvars != NULL);
1278 	
1279 	      assert(start < nprobvars);
1280 	
1281 	      /* check for same implicit binary variables */
1282 	      for( v = start; v < nprobvars; ++v )
1283 	      {
1284 	         probvar = probvars[v];
1285 	         assert(probvar != NULL);
1286 	
1287 	         assert(counts[v] <= nvars);
1288 	         assert(counts[nprobvars + v] <= nvars);
1289 	
1290 	         if( counts[v] + (*nredvars) == nvars )
1291 	         {
1292 	            if( SCIPvarIsBinary(probvar) )
1293 	            {
1294 	               SCIPdebugMsg(scip, "can fix variable %s [%g, %g] to 1.0\n", SCIPvarGetName(probvar),
1295 	                  SCIPvarGetLbGlobal(probvar), SCIPvarGetUbGlobal(probvar));
1296 	
1297 	               if( SCIPvarGetLbGlobal(probvar) < 0.5 )
1298 	               {
1299 	                  SCIP_CALL( SCIPnodeAddBoundchg(scip->tree->root, scip->mem->probmem, scip->set, scip->stat,
1300 	                        scip->transprob, scip->origprob, scip->tree, scip->reopt, scip->lp, scip->branchcand,
1301 	                        scip->eventqueue, scip->cliquetable, probvar, 1.0, SCIP_BOUNDTYPE_LOWER, FALSE) );
1302 	
1303 	                  assert(SCIPvarGetLbGlobal(probvar) > 0.5 || scip->tree->npendingbdchgs > 0);
1304 	
1305 	                  ++(*nglobalred);
1306 	
1307 	                  if( issetvar[v] > 0 )
1308 	                     *setredundant = TRUE;
1309 	               }
1310 	            }
1311 	            else
1312 	            {
1313 	               SCIPdebugMsg(scip, "can tighten lower bound variable %s [%g, %g] to %g\n", SCIPvarGetName(probvar),
1314 	                  SCIPvarGetLbGlobal(probvar), SCIPvarGetUbGlobal(probvar), newbounds[v]);
1315 	
1316 	               /* the new lower bound is greater than the global upper bound => the problem is global infeasible */
1317 	               if( SCIPisLT(scip, SCIPvarGetUbGlobal(probvar), newbounds[v]) )
1318 	               {
1319 	                  SCIPdebugMsg(scip, "-> global infeasibility proven.\n");
1320 	
1321 	                  *glbinfeas = TRUE;
1322 	                  break;
1323 	               }
1324 	
1325 	               if( SCIPisLT(scip, SCIPvarGetLbGlobal(probvar), newbounds[v]) )
1326 	               {
1327 	                  SCIP_CALL( SCIPnodeAddBoundchg(scip->tree->root, scip->mem->probmem, scip->set, scip->stat,
1328 	                        scip->transprob, scip->origprob, scip->tree, scip->reopt, scip->lp, scip->branchcand,
1329 	                        scip->eventqueue, scip->cliquetable, probvar, newbounds[v], SCIP_BOUNDTYPE_LOWER, FALSE) );
1330 	
1331 	                  ++(*nglobalred);
1332 	
1333 	                  if( issetvar[v] > 0 && newbounds[v] >= bounds[issetvar[v] - 1] )
1334 	                     *setredundant = TRUE;
1335 	               }
1336 	            }
1337 	         }
1338 	         else if( counts[nprobvars + v] + (*nredvars) == nvars )
1339 	         {
1340 	            if( SCIPvarIsBinary(probvar) )
1341 	            {
1342 	               SCIPdebugMsg(scip, "can fix variable %s [%g, %g] to 0.0\n", SCIPvarGetName(probvar),
1343 	                  SCIPvarGetLbGlobal(probvar), SCIPvarGetUbGlobal(probvar));
1344 	
1345 	               if( SCIPvarGetUbGlobal(probvar) > 0.5 )
1346 	               {
1347 	                  SCIP_CALL( SCIPnodeAddBoundchg(scip->tree->root, scip->mem->probmem, scip->set, scip->stat,
1348 	                        scip->transprob, scip->origprob, scip->tree, scip->reopt, scip->lp, scip->branchcand, scip->eventqueue,
1349 	                        scip->cliquetable, probvar, 0.0, SCIP_BOUNDTYPE_UPPER, FALSE) );
1350 	
1351 	                  assert(SCIPvarGetUbGlobal(probvar) < 0.5 || scip->tree->npendingbdchgs > 0);
1352 	
1353 	                  ++(*nglobalred);
1354 	
1355 	                  if( issetvar[nprobvars + v] > 0 )
1356 	                     *setredundant = TRUE;
1357 	               }
1358 	            }
1359 	            else
1360 	            {
1361 	               int idx = nprobvars + v;
1362 	
1363 	               SCIPdebugMsg(scip, "can tighten upper bound variable %s [%g, %g] to %g\n", SCIPvarGetName(probvar),
1364 	                  SCIPvarGetLbGlobal(probvar), SCIPvarGetUbGlobal(probvar), newbounds[idx]);
1365 	
1366 	               /* the new upper bound is small than the global upper bound => the problem is global infeasible */
1367 	               if( SCIPisGT(scip, SCIPvarGetLbGlobal(probvar), newbounds[idx]) )
1368 	               {
1369 	                  SCIPdebugMsg(scip, "-> global infeasibility proven.\n");
1370 	
1371 	                  *glbinfeas = TRUE;
1372 	                  break;
1373 	               }
1374 	
1375 	               if( SCIPisGT(scip, SCIPvarGetUbGlobal(probvar), newbounds[idx]) )
1376 	               {
1377 	                  SCIP_CALL( SCIPnodeAddBoundchg(scip->tree->root, scip->mem->probmem, scip->set, scip->stat,
1378 	                        scip->transprob, scip->origprob, scip->tree, scip->reopt, scip->lp, scip->branchcand, scip->eventqueue,
1379 	                        scip->cliquetable, probvar, newbounds[idx], SCIP_BOUNDTYPE_UPPER, FALSE) );
1380 	
1381 	                  ++(*nglobalred);
1382 	
1383 	                  if( issetvar[idx] > 0 && newbounds[idx] <= bounds[issetvar[idx] - 1] )
1384 	                     *setredundant = TRUE;
1385 	               }
1386 	            }
1387 	         }
1388 	      }
1389 	   }
1390 	
1391 	   /* reset issetvar array to 0 */
1392 	   for( v = 0; v < nvars; ++v )
1393 	   {
1394 	      varidx = SCIPvarGetProbindex(vars[v]);
1395 	      assert(varidx >= 0);
1396 	
1397 	      if( boundtypes[v] )
1398 	         varidx += nprobvars;
1399 	
1400 	      issetvar[varidx] = 0;
1401 	   }
1402 	
1403 	   if( ncountnonzeros >= maxcountnonzeros )
1404 	   {
1405 	      BMSclearMemoryArray(counts, 2*nprobvars);
1406 	   }
1407 	   else
1408 	   {
1409 	      while( --ncountnonzeros >= 0 )
1410 	         counts[countnonzeros[ncountnonzeros]] = 0;
1411 	   }
1412 	
1413 	   SCIPfreeBufferArray(scip, &countnonzeros);
1414 	   SCIPfreeBufferArray(scip, &implidx);
1415 	   SCIPfreeBufferArray(scip, &lastbounds);
1416 	   SCIPfreeBufferArray(scip, &newbounds);
1417 	   SCIPfreeCleanBufferArray(scip, &counts);
1418 	   SCIPfreeCleanBufferArray(scip, &issetvar);
1419 	
1420 	   return SCIP_OKAY;
1421 	}
1422