1    	/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
2    	/*                                                                           */
3    	/*                  This file is part of the program and library             */
4    	/*         SCIP --- Solving Constraint Integer Programs                      */
5    	/*                                                                           */
6    	/*  Copyright 2002-2022 Zuse Institute Berlin                                */
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   conflict_general.c
26   	 * @ingroup OTHER_CFILES
27   	 * @brief  methods and datastructures for conflict analysis
28   	 * @author Tobias Achterberg
29   	 * @author Timo Berthold
30   	 * @author Stefan Heinz
31   	 * @author Marc Pfetsch
32   	 * @author Michael Winkler
33   	 * @author Jakob Witzig
34   	 *
35   	 * SCIP contains two kinds of conflict analysis:
36   	 *    - In graph based conflict analysis, the graph consisting of derived
37   	 *      is analysed. Code and documentation is available in conflict_graphanalysis.h
38   	 *    - In dual proof analysis, an infeasible LP relaxation is analysed.
39   	 *      Using the dual solution, a valid constraint is derived that is violated
40   	 *      by all values in the domain. This constraint is added to the problem
41   	 *      and can then be used for domain propagation.
42   	 *      Code is available in conflict_dualproofanalysis.h
43   	 * This file contains the methods that are shared by both kinds of conflict analysis.
44   	 */
45   	
46   	/*---+----1----+----2----+----3----+----4----+----5----+----6----+----7----+----8----+----9----+----0----+----1----+----2*/
47   	
48   	#include "lpi/lpi.h"
49   	#include "scip/clock.h"
50   	#include "scip/conflict.h"
51   	#include "scip/conflictstore.h"
52   	#include "scip/cons.h"
53   	#include "scip/cons_linear.h"
54   	#include "scip/cuts.h"
55   	#include "scip/history.h"
56   	#include "scip/lp.h"
57   	#include "scip/presolve.h"
58   	#include "scip/prob.h"
59   	#include "scip/prop.h"
60   	#include "scip/pub_conflict.h"
61   	#include "scip/pub_cons.h"
62   	#include "scip/pub_lp.h"
63   	#include "scip/pub_message.h"
64   	#include "scip/pub_misc.h"
65   	#include "scip/pub_misc_sort.h"
66   	#include "scip/pub_paramset.h"
67   	#include "scip/pub_prop.h"
68   	#include "scip/pub_tree.h"
69   	#include "scip/pub_var.h"
70   	#include "scip/scip_conflict.h"
71   	#include "scip/scip_cons.h"
72   	#include "scip/scip_mem.h"
73   	#include "scip/scip_sol.h"
74   	#include "scip/scip_var.h"
75   	#include "scip/set.h"
76   	#include "scip/sol.h"
77   	#include "scip/struct_conflict.h"
78   	#include "scip/struct_lp.h"
79   	#include "scip/struct_prob.h"
80   	#include "scip/struct_set.h"
81   	#include "scip/struct_stat.h"
82   	#include "scip/struct_tree.h"
83   	#include "scip/struct_var.h"
84   	#include "scip/tree.h"
85   	#include "scip/var.h"
86   	#include "scip/visual.h"
87   	#include <string.h>
88   	#if defined(_WIN32) || defined(_WIN64)
89   	#else
90   	#include <strings.h> /*lint --e{766}*/
91   	#endif
92   	
93   	/* because calculations might cancel out some values, we stop the infeasibility analysis if a value is bigger than
94   	 * 2^53 = 9007199254740992
95   	 */
96   	#define NUMSTOP 9007199254740992.0
97   	
98   	/** returns the current number of conflict sets in the conflict set storage */
99   	int SCIPconflictGetNConflicts(
100  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
101  	   )
102  	{
103  	   assert(conflict != NULL);
104  	
105  	   return conflict->nconflictsets;
106  	}
107  	
108  	/** returns the total number of conflict constraints that were added to the problem */
109  	SCIP_Longint SCIPconflictGetNAppliedConss(
110  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
111  	   )
112  	{
113  	   assert(conflict != NULL);
114  	
115  	   return conflict->nappliedglbconss + conflict->nappliedlocconss;
116  	}
117  	
118  	/** returns the total number of literals in conflict constraints that were added to the problem */
119  	SCIP_Longint SCIPconflictGetNAppliedLiterals(
120  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
121  	   )
122  	{
123  	   assert(conflict != NULL);
124  	
125  	   return conflict->nappliedglbliterals + conflict->nappliedlocliterals;
126  	}
127  	
128  	/** returns the total number of global bound changes applied by the conflict analysis */
129  	SCIP_Longint SCIPconflictGetNGlobalChgBds(
130  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
131  	   )
132  	{
133  	   assert(conflict != NULL);
134  	
135  	   return conflict->nglbchgbds;
136  	}
137  	
138  	/** returns the total number of conflict constraints that were added globally to the problem */
139  	SCIP_Longint SCIPconflictGetNAppliedGlobalConss(
140  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
141  	   )
142  	{
143  	   assert(conflict != NULL);
144  	
145  	   return conflict->nappliedglbconss;
146  	}
147  	
148  	/** returns the total number of literals in conflict constraints that were added globally to the problem */
149  	SCIP_Longint SCIPconflictGetNAppliedGlobalLiterals(
150  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
151  	   )
152  	{
153  	   assert(conflict != NULL);
154  	
155  	   return conflict->nappliedglbliterals;
156  	}
157  	
158  	/** returns the total number of local bound changes applied by the conflict analysis */
159  	SCIP_Longint SCIPconflictGetNLocalChgBds(
160  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
161  	   )
162  	{
163  	   assert(conflict != NULL);
164  	
165  	   return conflict->nlocchgbds;
166  	}
167  	
168  	/** returns the total number of conflict constraints that were added locally to the problem */
169  	SCIP_Longint SCIPconflictGetNAppliedLocalConss(
170  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
171  	   )
172  	{
173  	   assert(conflict != NULL);
174  	
175  	   return conflict->nappliedlocconss;
176  	}
177  	
178  	/** returns the total number of literals in conflict constraints that were added locally to the problem */
179  	SCIP_Longint SCIPconflictGetNAppliedLocalLiterals(
180  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
181  	   )
182  	{
183  	   assert(conflict != NULL);
184  	
185  	   return conflict->nappliedlocliterals;
186  	}
187  	
188  	/** compares two conflict set entries, such that bound changes inferred later are
189  	 *  ordered prior to ones that were inferred earlier
190  	 */
191  	static
192  	SCIP_DECL_SORTPTRCOMP(conflictBdchginfoComp)
193  	{  /*lint --e{715}*/
194  	   SCIP_BDCHGINFO* bdchginfo1;
195  	   SCIP_BDCHGINFO* bdchginfo2;
196  	
197  	   bdchginfo1 = (SCIP_BDCHGINFO*)elem1;
198  	   bdchginfo2 = (SCIP_BDCHGINFO*)elem2;
199  	   assert(bdchginfo1 != NULL);
200  	   assert(bdchginfo2 != NULL);
201  	   assert(!SCIPbdchginfoIsRedundant(bdchginfo1));
202  	   assert(!SCIPbdchginfoIsRedundant(bdchginfo2));
203  	
204  	   if( bdchginfo1 == bdchginfo2 )
205  	      return 0;
206  	
207  	   if( !SCIPbdchgidxIsEarlierNonNull(SCIPbdchginfoGetIdx(bdchginfo1), SCIPbdchginfoGetIdx(bdchginfo2)) )
208  	      return -1;
209  	   else
210  	      return +1;
211  	}
212  	
213  	/** enables or disables all clocks of \p conflict, depending on the value of the flag */
214  	void SCIPconflictEnableOrDisableClocks(
215  	   SCIP_CONFLICT*        conflict,           /**< the conflict analysis data for which all clocks should be enabled or disabled */
216  	   SCIP_Bool             enable              /**< should the clocks of the conflict analysis data be enabled? */
217  	   )
218  	{
219  	   assert(conflict != NULL);
220  	
221  	   SCIPclockEnableOrDisable(conflict->boundlpanalyzetime, enable);
222  	   SCIPclockEnableOrDisable(conflict->dIBclock, enable);
223  	   SCIPclockEnableOrDisable(conflict->inflpanalyzetime, enable);
224  	   SCIPclockEnableOrDisable(conflict->propanalyzetime, enable);
225  	   SCIPclockEnableOrDisable(conflict->pseudoanalyzetime, enable);
226  	   SCIPclockEnableOrDisable(conflict->sbanalyzetime, enable);
227  	}
228  	
229  	/** creates conflict analysis data for propagation conflicts */
230  	SCIP_RETCODE SCIPconflictCreate(
231  	   SCIP_CONFLICT**       conflict,           /**< pointer to conflict analysis data */
232  	   BMS_BLKMEM*           blkmem,             /**< block memory of transformed problem */
233  	   SCIP_SET*             set                 /**< global SCIP settings */
234  	   )
235  	{
236  	   assert(conflict != NULL);
237  	
238  	   SCIP_ALLOC( BMSallocMemory(conflict) );
239  	
240  	   SCIP_CALL( SCIPclockCreate(&(*conflict)->dIBclock, SCIP_CLOCKTYPE_DEFAULT) );
241  	   SCIP_CALL( SCIPclockCreate(&(*conflict)->propanalyzetime, SCIP_CLOCKTYPE_DEFAULT) );
242  	   SCIP_CALL( SCIPclockCreate(&(*conflict)->inflpanalyzetime, SCIP_CLOCKTYPE_DEFAULT) );
243  	   SCIP_CALL( SCIPclockCreate(&(*conflict)->boundlpanalyzetime, SCIP_CLOCKTYPE_DEFAULT) );
244  	   SCIP_CALL( SCIPclockCreate(&(*conflict)->sbanalyzetime, SCIP_CLOCKTYPE_DEFAULT) );
245  	   SCIP_CALL( SCIPclockCreate(&(*conflict)->pseudoanalyzetime, SCIP_CLOCKTYPE_DEFAULT) );
246  	
247  	   /* enable or disable timing depending on the parameter statistic timing */
248  	   SCIPconflictEnableOrDisableClocks((*conflict), set->time_statistictiming);
249  	
250  	   SCIP_CALL( SCIPpqueueCreate(&(*conflict)->bdchgqueue, set->mem_arraygrowinit, set->mem_arraygrowfac,
251  	         conflictBdchginfoComp, NULL) );
252  	   SCIP_CALL( SCIPpqueueCreate(&(*conflict)->forcedbdchgqueue, set->mem_arraygrowinit, set->mem_arraygrowfac,
253  	         conflictBdchginfoComp, NULL) );
254  	   SCIP_CALL( SCIPconflictsetCreate(&(*conflict)->conflictset, blkmem) );
255  	   (*conflict)->conflictsets = NULL;
256  	   (*conflict)->conflictsetscores = NULL;
257  	   (*conflict)->tmpbdchginfos = NULL;
258  	   (*conflict)->conflictsetssize = 0;
259  	   (*conflict)->nconflictsets = 0;
260  	   (*conflict)->proofsets = NULL;
261  	   (*conflict)->proofsetssize = 0;
262  	   (*conflict)->nproofsets = 0;
263  	   (*conflict)->tmpbdchginfossize = 0;
264  	   (*conflict)->ntmpbdchginfos = 0;
265  	   (*conflict)->count = 0;
266  	   (*conflict)->nglbchgbds = 0;
267  	   (*conflict)->nappliedglbconss = 0;
268  	   (*conflict)->nappliedglbliterals = 0;
269  	   (*conflict)->nlocchgbds = 0;
270  	   (*conflict)->nappliedlocconss = 0;
271  	   (*conflict)->nappliedlocliterals = 0;
272  	   (*conflict)->npropcalls = 0;
273  	   (*conflict)->npropsuccess = 0;
274  	   (*conflict)->npropconfconss = 0;
275  	   (*conflict)->npropconfliterals = 0;
276  	   (*conflict)->npropreconvconss = 0;
277  	   (*conflict)->npropreconvliterals = 0;
278  	   (*conflict)->ninflpcalls = 0;
279  	   (*conflict)->ninflpsuccess = 0;
280  	   (*conflict)->ninflpconfconss = 0;
281  	   (*conflict)->ninflpconfliterals = 0;
282  	   (*conflict)->ninflpreconvconss = 0;
283  	   (*conflict)->ninflpreconvliterals = 0;
284  	   (*conflict)->ninflpiterations = 0;
285  	   (*conflict)->nboundlpcalls = 0;
286  	   (*conflict)->nboundlpsuccess = 0;
287  	   (*conflict)->nboundlpconfconss = 0;
288  	   (*conflict)->nboundlpconfliterals = 0;
289  	   (*conflict)->nboundlpreconvconss = 0;
290  	   (*conflict)->nboundlpreconvliterals = 0;
291  	   (*conflict)->nboundlpiterations = 0;
292  	   (*conflict)->nsbcalls = 0;
293  	   (*conflict)->nsbsuccess = 0;
294  	   (*conflict)->nsbconfconss = 0;
295  	   (*conflict)->nsbconfliterals = 0;
296  	   (*conflict)->nsbreconvconss = 0;
297  	   (*conflict)->nsbreconvliterals = 0;
298  	   (*conflict)->nsbiterations = 0;
299  	   (*conflict)->npseudocalls = 0;
300  	   (*conflict)->npseudosuccess = 0;
301  	   (*conflict)->npseudoconfconss = 0;
302  	   (*conflict)->npseudoconfliterals = 0;
303  	   (*conflict)->npseudoreconvconss = 0;
304  	   (*conflict)->npseudoreconvliterals = 0;
305  	   (*conflict)->ndualproofsinfglobal = 0;
306  	   (*conflict)->ndualproofsinflocal = 0;
307  	   (*conflict)->ndualproofsinfsuccess = 0;
308  	   (*conflict)->dualproofsinfnnonzeros = 0;
309  	   (*conflict)->ndualproofsbndglobal = 0;
310  	   (*conflict)->ndualproofsbndlocal = 0;
311  	   (*conflict)->ndualproofsbndsuccess = 0;
312  	   (*conflict)->dualproofsbndnnonzeros = 0;
313  	
314  	   SCIP_CALL( SCIPconflictInitProofset((*conflict), blkmem) );
315  	
316  	   return SCIP_OKAY;
317  	}
318  	
319  	/** frees conflict analysis data for propagation conflicts */
320  	SCIP_RETCODE SCIPconflictFree(
321  	   SCIP_CONFLICT**       conflict,           /**< pointer to conflict analysis data */
322  	   BMS_BLKMEM*           blkmem              /**< block memory of transformed problem */
323  	   )
324  	{
325  	   assert(conflict != NULL);
326  	   assert(*conflict != NULL);
327  	   assert((*conflict)->nconflictsets == 0);
328  	   assert((*conflict)->ntmpbdchginfos == 0);
329  	
330  	#if defined(SCIP_CONFGRAPH) || defined(SCIP_CONFGRAPH_DOT)
331  	   confgraphFree();
332  	#endif
333  	
334  	   SCIPclockFree(&(*conflict)->dIBclock);
335  	   SCIPclockFree(&(*conflict)->propanalyzetime);
336  	   SCIPclockFree(&(*conflict)->inflpanalyzetime);
337  	   SCIPclockFree(&(*conflict)->boundlpanalyzetime);
338  	   SCIPclockFree(&(*conflict)->sbanalyzetime);
339  	   SCIPclockFree(&(*conflict)->pseudoanalyzetime);
340  	   SCIPpqueueFree(&(*conflict)->bdchgqueue);
341  	   SCIPpqueueFree(&(*conflict)->forcedbdchgqueue);
342  	   SCIPconflictsetFree(&(*conflict)->conflictset, blkmem);
343  	   SCIPproofsetFree(&(*conflict)->proofset, blkmem);
344  	
345  	   BMSfreeMemoryArrayNull(&(*conflict)->conflictsets);
346  	   BMSfreeMemoryArrayNull(&(*conflict)->conflictsetscores);
347  	   BMSfreeMemoryArrayNull(&(*conflict)->proofsets);
348  	   BMSfreeMemoryArrayNull(&(*conflict)->tmpbdchginfos);
349  	   BMSfreeMemory(conflict);
350  	
351  	   return SCIP_OKAY;
352  	}
353  	
354  	/** returns the conflict lower bound if the variable is present in the current conflict set; otherwise the global lower
355  	 *  bound
356  	 */
357  	SCIP_Real SCIPconflictGetVarLb(
358  	   SCIP_CONFLICT*        conflict,           /**< conflict analysis data */
359  	   SCIP_VAR*             var                 /**< problem variable */
360  	   )
361  	{
362  	   if( var->conflictlbcount == conflict->count )
363  	   {
364  	      assert(EPSGE(var->conflictlb, var->conflictrelaxedlb, 1e-09));
365  	      return var->conflictrelaxedlb;
366  	   }
367  	
368  	   return SCIPvarGetLbGlobal(var);
369  	}
370  	
371  	/** returns the conflict upper bound if the variable is present in the current conflict set; otherwise the global upper
372  	 *  bound
373  	 */
374  	SCIP_Real SCIPconflictGetVarUb(
375  	   SCIP_CONFLICT*        conflict,           /**< conflict analysis data */
376  	   SCIP_VAR*             var                 /**< problem variable */
377  	   )
378  	{
379  	   if( var->conflictubcount == conflict->count )
380  	   {
381  	      assert(EPSLE(var->conflictub, var->conflictrelaxedub, 1e-09));
382  	      return var->conflictrelaxedub;
383  	   }
384  	
385  	   return SCIPvarGetUbGlobal(var);
386  	}
387  	
388  	/** gets time in seconds used for preprocessing global conflict constraint before appliance */
389  	SCIP_Real SCIPconflictGetGlobalApplTime(
390  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
391  	   )
392  	{
393  	   assert(conflict != NULL);
394  	
395  	   return SCIPclockGetTime(conflict->dIBclock);
396  	}
397  	
398  	/** gets time in seconds used for analyzing propagation conflicts */
399  	SCIP_Real SCIPconflictGetPropTime(
400  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
401  	   )
402  	{
403  	   assert(conflict != NULL);
404  	
405  	   return SCIPclockGetTime(conflict->propanalyzetime);
406  	}
407  	
408  	/** gets number of calls to propagation conflict analysis */
409  	SCIP_Longint SCIPconflictGetNPropCalls(
410  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
411  	   )
412  	{
413  	   assert(conflict != NULL);
414  	
415  	   return conflict->npropcalls;
416  	}
417  	
418  	/** gets number of calls to propagation conflict analysis that yield at least one conflict constraint */
419  	SCIP_Longint SCIPconflictGetNPropSuccess(
420  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
421  	   )
422  	{
423  	   assert(conflict != NULL);
424  	
425  	   return conflict->npropsuccess;
426  	}
427  	
428  	/** gets number of conflict constraints detected in propagation conflict analysis */
429  	SCIP_Longint SCIPconflictGetNPropConflictConss(
430  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
431  	   )
432  	{
433  	   assert(conflict != NULL);
434  	
435  	   return conflict->npropconfconss;
436  	}
437  	
438  	/** gets total number of literals in conflict constraints created in propagation conflict analysis */
439  	SCIP_Longint SCIPconflictGetNPropConflictLiterals(
440  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
441  	   )
442  	{
443  	   assert(conflict != NULL);
444  	
445  	   return conflict->npropconfliterals;
446  	}
447  	
448  	/** gets number of reconvergence constraints detected in propagation conflict analysis */
449  	SCIP_Longint SCIPconflictGetNPropReconvergenceConss(
450  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
451  	   )
452  	{
453  	   assert(conflict != NULL);
454  	
455  	   return conflict->npropreconvconss;
456  	}
457  	
458  	/** gets total number of literals in reconvergence constraints created in propagation conflict analysis */
459  	SCIP_Longint SCIPconflictGetNPropReconvergenceLiterals(
460  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
461  	   )
462  	{
463  	   assert(conflict != NULL);
464  	
465  	   return conflict->npropreconvliterals;
466  	}
467  	
468  	/** gets time in seconds used for analyzing infeasible LP conflicts */
469  	SCIP_Real SCIPconflictGetInfeasibleLPTime(
470  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
471  	   )
472  	{
473  	   assert(conflict != NULL);
474  	
475  	   return SCIPclockGetTime(conflict->inflpanalyzetime);
476  	}
477  	
478  	/** gets number of calls to infeasible LP conflict analysis */
479  	SCIP_Longint SCIPconflictGetNInfeasibleLPCalls(
480  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
481  	   )
482  	{
483  	   assert(conflict != NULL);
484  	
485  	   return conflict->ninflpcalls;
486  	}
487  	
488  	/** gets number of calls to infeasible LP conflict analysis that yield at least one conflict constraint */
489  	SCIP_Longint SCIPconflictGetNInfeasibleLPSuccess(
490  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
491  	   )
492  	{
493  	   assert(conflict != NULL);
494  	
495  	   return conflict->ninflpsuccess;
496  	}
497  	
498  	/** gets number of conflict constraints detected in infeasible LP conflict analysis */
499  	SCIP_Longint SCIPconflictGetNInfeasibleLPConflictConss(
500  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
501  	   )
502  	{
503  	   assert(conflict != NULL);
504  	
505  	   return conflict->ninflpconfconss;
506  	}
507  	
508  	/** gets total number of literals in conflict constraints created in infeasible LP conflict analysis */
509  	SCIP_Longint SCIPconflictGetNInfeasibleLPConflictLiterals(
510  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
511  	   )
512  	{
513  	   assert(conflict != NULL);
514  	
515  	   return conflict->ninflpconfliterals;
516  	}
517  	
518  	/** gets number of reconvergence constraints detected in infeasible LP conflict analysis */
519  	SCIP_Longint SCIPconflictGetNInfeasibleLPReconvergenceConss(
520  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
521  	   )
522  	{
523  	   assert(conflict != NULL);
524  	
525  	   return conflict->ninflpreconvconss;
526  	}
527  	
528  	/** gets total number of literals in reconvergence constraints created in infeasible LP conflict analysis */
529  	SCIP_Longint SCIPconflictGetNInfeasibleLPReconvergenceLiterals(
530  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
531  	   )
532  	{
533  	   assert(conflict != NULL);
534  	
535  	   return conflict->ninflpreconvliterals;
536  	}
537  	
538  	/** gets number of LP iterations in infeasible LP conflict analysis */
539  	SCIP_Longint SCIPconflictGetNInfeasibleLPIterations(
540  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
541  	   )
542  	{
543  	   assert(conflict != NULL);
544  	
545  	   return conflict->ninflpiterations;
546  	}
547  	
548  	/** gets time in seconds used for analyzing bound exceeding LP conflicts */
549  	SCIP_Real SCIPconflictGetBoundexceedingLPTime(
550  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
551  	   )
552  	{
553  	   assert(conflict != NULL);
554  	
555  	   return SCIPclockGetTime(conflict->boundlpanalyzetime);
556  	}
557  	
558  	/** gets number of calls to bound exceeding LP conflict analysis */
559  	SCIP_Longint SCIPconflictGetNBoundexceedingLPCalls(
560  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
561  	   )
562  	{
563  	   assert(conflict != NULL);
564  	
565  	   return conflict->nboundlpcalls;
566  	}
567  	
568  	/** gets number of calls to bound exceeding LP conflict analysis that yield at least one conflict constraint */
569  	SCIP_Longint SCIPconflictGetNBoundexceedingLPSuccess(
570  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
571  	   )
572  	{
573  	   assert(conflict != NULL);
574  	
575  	   return conflict->nboundlpsuccess;
576  	}
577  	
578  	/** gets number of conflict constraints detected in bound exceeding LP conflict analysis */
579  	SCIP_Longint SCIPconflictGetNBoundexceedingLPConflictConss(
580  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
581  	   )
582  	{
583  	   assert(conflict != NULL);
584  	
585  	   return conflict->nboundlpconfconss;
586  	}
587  	
588  	/** gets total number of literals in conflict constraints created in bound exceeding LP conflict analysis */
589  	SCIP_Longint SCIPconflictGetNBoundexceedingLPConflictLiterals(
590  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
591  	   )
592  	{
593  	   assert(conflict != NULL);
594  	
595  	   return conflict->nboundlpconfliterals;
596  	}
597  	
598  	/** gets number of reconvergence constraints detected in bound exceeding LP conflict analysis */
599  	SCIP_Longint SCIPconflictGetNBoundexceedingLPReconvergenceConss(
600  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
601  	   )
602  	{
603  	   assert(conflict != NULL);
604  	
605  	   return conflict->nboundlpreconvconss;
606  	}
607  	
608  	/** gets total number of literals in reconvergence constraints created in bound exceeding LP conflict analysis */
609  	SCIP_Longint SCIPconflictGetNBoundexceedingLPReconvergenceLiterals(
610  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
611  	   )
612  	{
613  	   assert(conflict != NULL);
614  	
615  	   return conflict->nboundlpreconvliterals;
616  	}
617  	
618  	/** gets number of LP iterations in bound exceeding LP conflict analysis */
619  	SCIP_Longint SCIPconflictGetNBoundexceedingLPIterations(
620  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
621  	   )
622  	{
623  	   assert(conflict != NULL);
624  	
625  	   return conflict->nboundlpiterations;
626  	}
627  	
628  	/** gets time in seconds used for analyzing infeasible strong branching conflicts */
629  	SCIP_Real SCIPconflictGetStrongbranchTime(
630  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
631  	   )
632  	{
633  	   assert(conflict != NULL);
634  	
635  	   return SCIPclockGetTime(conflict->sbanalyzetime);
636  	}
637  	
638  	/** gets number of successful calls to dual proof analysis derived from infeasible LPs */
639  	SCIP_Longint SCIPconflictGetNDualproofsInfSuccess(
640  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
641  	   )
642  	{
643  	   assert(conflict != NULL);
644  	
645  	   return conflict->ndualproofsinfsuccess;
646  	}
647  	
648  	/** gets number of globally valid dual proof constraints derived from infeasible LPs */
649  	SCIP_Longint SCIPconflictGetNDualproofsInfGlobal(
650  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
651  	   )
652  	{
653  	   assert(conflict != NULL);
654  	
655  	   return conflict->ndualproofsinfglobal;
656  	}
657  	
658  	/** gets number of locally valid dual proof constraints derived from infeasible LPs */
659  	SCIP_Longint SCIPconflictGetNDualproofsInfLocal(
660  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
661  	   )
662  	{
663  	   assert(conflict != NULL);
664  	
665  	   return conflict->ndualproofsinflocal;
666  	}
667  	
668  	/** gets average length of dual proof constraints derived from infeasible LPs */
669  	SCIP_Longint SCIPconflictGetNDualproofsInfNonzeros(
670  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
671  	   )
672  	{
673  	   assert(conflict != NULL);
674  	
675  	   return conflict->dualproofsinfnnonzeros;
676  	}
677  	
678  	/** gets number of successfully analyzed dual proofs derived from bound exceeding LPs */
679  	SCIP_Longint SCIPconflictGetNDualproofsBndSuccess(
680  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
681  	   )
682  	{
683  	   assert(conflict != NULL);
684  	
685  	   return conflict->ndualproofsbndsuccess;
686  	}
687  	
688  	/** gets number of globally applied dual proofs derived from bound exceeding LPs */
689  	SCIP_Longint SCIPconflictGetNDualproofsBndGlobal(
690  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
691  	   )
692  	{
693  	   assert(conflict != NULL);
694  	
695  	   return conflict->ndualproofsbndglobal;
696  	}
697  	
698  	/** gets number of locally applied dual proofs derived from bound exceeding LPs */
699  	SCIP_Longint SCIPconflictGetNDualproofsBndLocal(
700  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
701  	   )
702  	{
703  	   assert(conflict != NULL);
704  	
705  	   return conflict->ndualproofsbndlocal;
706  	}
707  	
708  	/** gets average length of dual proofs derived from bound exceeding LPs */
709  	SCIP_Longint SCIPconflictGetNDualproofsBndNonzeros(
710  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
711  	   )
712  	{
713  	   assert(conflict != NULL);
714  	
715  	   return conflict->dualproofsbndnnonzeros;
716  	}
717  	
718  	/** gets number of calls to infeasible strong branching conflict analysis */
719  	SCIP_Longint SCIPconflictGetNStrongbranchCalls(
720  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
721  	   )
722  	{
723  	   assert(conflict != NULL);
724  	
725  	   return conflict->nsbcalls;
726  	}
727  	
728  	/** gets number of calls to infeasible strong branching conflict analysis that yield at least one conflict constraint */
729  	SCIP_Longint SCIPconflictGetNStrongbranchSuccess(
730  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
731  	   )
732  	{
733  	   assert(conflict != NULL);
734  	
735  	   return conflict->nsbsuccess;
736  	}
737  	
738  	/** gets number of conflict constraints detected in infeasible strong branching conflict analysis */
739  	SCIP_Longint SCIPconflictGetNStrongbranchConflictConss(
740  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
741  	   )
742  	{
743  	   assert(conflict != NULL);
744  	
745  	   return conflict->nsbconfconss;
746  	}
747  	
748  	/** gets total number of literals in conflict constraints created in infeasible strong branching conflict analysis */
749  	SCIP_Longint SCIPconflictGetNStrongbranchConflictLiterals(
750  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
751  	   )
752  	{
753  	   assert(conflict != NULL);
754  	
755  	   return conflict->nsbconfliterals;
756  	}
757  	
758  	/** gets number of reconvergence constraints detected in infeasible strong branching conflict analysis */
759  	SCIP_Longint SCIPconflictGetNStrongbranchReconvergenceConss(
760  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
761  	   )
762  	{
763  	   assert(conflict != NULL);
764  	
765  	   return conflict->nsbreconvconss;
766  	}
767  	
768  	/** gets total number of literals in reconvergence constraints created in infeasible strong branching conflict analysis */
769  	SCIP_Longint SCIPconflictGetNStrongbranchReconvergenceLiterals(
770  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
771  	   )
772  	{
773  	   assert(conflict != NULL);
774  	
775  	   return conflict->nsbreconvliterals;
776  	}
777  	
778  	/** gets number of LP iterations in infeasible strong branching conflict analysis */
779  	SCIP_Longint SCIPconflictGetNStrongbranchIterations(
780  	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
781  	   )
782  	{
783  	   assert(conflict != NULL);
784  	
785  	   return conflict->nsbiterations;
786  	}
787  	
788  	/** adds a weighted LP row to an aggregation row */
789  	static
790  	SCIP_RETCODE addRowToAggrRow(
791  	   SCIP_SET*             set,                /**< global SCIP settings */
792  	   SCIP_ROW*             row,                /**< LP row */
793  	   SCIP_Real             weight,             /**< weight for scaling */
794  	   SCIP_AGGRROW*         aggrrow             /**< aggregation row */
795  	   )
796  	{
797  	   assert(set != NULL);
798  	   assert(row != NULL);
799  	   assert(weight != 0.0);
800  	
801  	   /* add minimal value to dual row's left hand side: y_i < 0 -> lhs, y_i > 0 -> rhs */
802  	   if( weight < 0.0 )
803  	   {
804  	      assert(!SCIPsetIsInfinity(set, -row->lhs));
805  	      SCIP_CALL( SCIPaggrRowAddRow(set->scip, aggrrow, row, weight, -1) );
806  	   }
807  	   else
808  	   {
809  	      assert(!SCIPsetIsInfinity(set, row->rhs));
810  	      SCIP_CALL( SCIPaggrRowAddRow(set->scip, aggrrow, row, weight, +1) );
811  	   }
812  	   SCIPsetDebugMsg(set, " -> add %s row <%s>[%g,%g](lp depth: %d): dual=%g -> dualrhs=%g\n",
813  	      row->local ? "local" : "global",
814  	      SCIProwGetName(row), row->lhs - row->constant, row->rhs - row->constant,
815  	      row->lpdepth, weight, SCIPaggrRowGetRhs(aggrrow));
816  	
817  	   return SCIP_OKAY;
818  	}
819  	
820  	/** checks validity of an LP row and a corresponding weight */
821  	static
822  	SCIP_Bool checkDualFeasibility(
823  	   SCIP_SET*             set,                /**< global SCIP settings */
824  	   SCIP_ROW*             row,                /**< LP row */
825  	   SCIP_Real             weight,             /**< weight for scaling */
826  	   SCIP_Bool*            zerocontribution    /**< pointer to store whether every row entry is zero within tolerances */
827  	   )
828  	{
829  	   SCIP_Bool valid = TRUE;
830  	
831  	   *zerocontribution = TRUE;
832  	
833  	   /* dual solution values of 0.0 are always valid */
834  	   if( REALABS(weight) > QUAD_EPSILON )
835  	   {
836  	      *zerocontribution = FALSE;
837  	
838  	      /* check dual feasibility */
839  	      if( (SCIPsetIsInfinity(set, -row->lhs) && weight > 0.0) || (SCIPsetIsInfinity(set, row->rhs) && weight < 0.0) )
840  	      {
841  	         int i;
842  	
843  	         /* ignore slight numerical violations if the contribution of every component of the row is close to zero */
844  	         if( weight > 0.0 )
845  	            *zerocontribution = SCIPsetIsDualfeasZero(set, row->rhs * weight);
846  	         else
847  	            *zerocontribution = SCIPsetIsDualfeasZero(set, row->lhs * weight);
848  	
849  	         for( i = 0; i < row->len && *zerocontribution; i++ )
850  	         {
851  	            if( !SCIPsetIsDualfeasZero(set, weight * row->vals[i]) )
852  	               *zerocontribution = FALSE;
853  	         }
854  	
855  	         if( !(*zerocontribution) )
856  	         {
857  	            SCIPsetDebugMsg(set, " -> invalid dual solution value %g for row <%s>: lhs=%g, rhs=%g\n",
858  	               weight, SCIProwGetName(row), row->lhs, row->rhs);
859  	
860  	            valid = FALSE;
861  	         }
862  	      }
863  	   }
864  	
865  	   return valid;
866  	}
867  	
868  	/** calculates the minimal activity of a given aggregation row */
869  	SCIP_Real SCIPaggrRowGetMinActivity(
870  	   SCIP_SET*             set,                /**< global SCIP settings */
871  	   SCIP_PROB*            transprob,          /**< transformed problem data */
872  	   SCIP_AGGRROW*         aggrrow,            /**< aggregation row */
873  	   SCIP_Real*            curvarlbs,          /**< current lower bounds of active problem variables (or NULL for global bounds) */
874  	   SCIP_Real*            curvarubs,          /**< current upper bounds of active problem variables (or NULL for global bounds) */
875  	   SCIP_Bool*            infdelta            /**< pointer to store whether at least one variable contributes with an infinite value */
876  	   )
877  	{
878  	   SCIP_VAR** vars;
879  	   SCIP_Real QUAD(minact);
880  	   int* inds;
881  	   int nnz;
882  	   int i;
883  	
884  	   vars = SCIPprobGetVars(transprob);
885  	   assert(vars != NULL);
886  	
887  	   nnz = SCIPaggrRowGetNNz(aggrrow);
888  	   inds = SCIPaggrRowGetInds(aggrrow);
889  	
890  	   QUAD_ASSIGN(minact, 0.0);
891  	
892  	   if( infdelta != NULL )
893  	      *infdelta = FALSE;
894  	
895  	   for( i = 0; i < nnz; i++ )
896  	   {
897  	      SCIP_Real val;
898  	      SCIP_Real QUAD(delta);
899  	      int v = inds[i];
900  	
901  	      assert(SCIPvarGetProbindex(vars[v]) == v);
902  	
903  	      val = SCIPaggrRowGetProbvarValue(aggrrow, v);
904  	
905  	      if( val > 0.0 )
906  	      {
907  	         SCIP_Real bnd = (curvarlbs == NULL ? SCIPvarGetLbGlobal(vars[v]) : curvarlbs[v]);
908  	
909  	         if( SCIPsetIsInfinity(set, -bnd) )
910  	         {
911  	            if( infdelta != NULL )
912  	               *infdelta = TRUE;
913  	
914  	            return -SCIPsetInfinity(set);
915  	         }
916  	
917  	         SCIPquadprecProdDD(delta, val, bnd);
918  	      }
919  	      else
920  	      {
921  	         SCIP_Real bnd = (curvarubs == NULL ? SCIPvarGetUbGlobal(vars[v]) : curvarubs[v]);
922  	
923  	         if( SCIPsetIsInfinity(set, bnd) )
924  	         {
925  	            if( infdelta != NULL )
926  	               *infdelta = TRUE;
927  	
928  	            return -SCIPsetInfinity(set);
929  	         }
930  	
931  	         SCIPquadprecProdDD(delta, val, bnd);
932  	      }
933  	
934  	      /* update minimal activity */
935  	      SCIPquadprecSumQQ(minact, minact, delta);
936  	   }
937  	
938  	   /* check whether the minimal activity is infinite */
939  	   if( SCIPsetIsInfinity(set, QUAD_TO_DBL(minact)) )
940  	      return SCIPsetInfinity(set);
941  	   if( SCIPsetIsInfinity(set, -QUAD_TO_DBL(minact)) )
942  	      return -SCIPsetInfinity(set);
943  	
944  	   return QUAD_TO_DBL(minact);
945  	}
946  	
947  	/** sort local rows by increasing depth and number of nonzeros as tie-breaker */
948  	static
949  	SCIP_RETCODE sortLocalRows(
950  	   SCIP_SET*             set,                /**< global SCIP settings */
951  	   SCIP_AGGRROW*         aggrrow,            /**< aggregation row */
952  	   SCIP_ROW**            rows,               /**< array of local rows */
953  	   int*                  rowinds,            /**< array of row indices */
954  	   int*                  rowdepth,           /**< array of LP depths */
955  	   int                   nrows               /**< number of local rows */
956  	   )
957  	{
958  	   int* rownnz;
959  	   int i;
960  	
961  	   assert(aggrrow != NULL);
962  	   assert(rows != NULL);
963  	   assert(nrows > 0);
964  	   assert(rowinds != NULL);
965  	   assert(rowdepth != NULL);
966  	
967  	   /* sort row indices by increasing depth */
968  	   SCIPsortIntInt(rowdepth, rowinds, nrows);
969  	   assert(rowdepth[0] <= rowdepth[nrows-1]);
970  	
971  	   SCIP_CALL( SCIPsetAllocBufferArray(set, &rownnz, nrows) );
972  	
973  	   /* get number of nonzero entries for every row */
974  	   for( i = 0; i < nrows; i++ )
975  	   {
976  	      SCIP_ROW* row = rows[rowinds[i]];
977  	      assert(row != NULL);
978  	
979  	      rownnz[i] = row->len;
980  	   }
981  	
982  	   /* since SCIP has no stable sorting function we sort each bucket separately */
983  	   for( i = 0; i < nrows; i++ )
984  	   {
985  	      int j = i;
986  	      int d = rowdepth[i];
987  	
988  	      /* search for the next row with a greater depth */
989  	      while( j+1 < nrows && rowdepth[j+1] == d )
990  	         j++;
991  	
992  	      /* the bucket has size one */
993  	      if( j == i )
994  	         continue;
995  	
996  	      assert(j-i+1 <= nrows);
997  	
998  	      /* sort row indices by increasing number of nonzero elements */
999  	      SCIPsortIntIntInt(&rownnz[i], &rowdepth[i], &rowinds[i], j-i+1);
1000 	      assert(rownnz[i] <= rownnz[j]);
1001 	
1002 	      i = j;
1003 	   } /*lint --e{850} i is modified in the body of the for loop */
1004 	
1005 	#ifndef NDEBUG
1006 	   for( i = 0; i < nrows-1; i++ )
1007 	      assert(rowdepth[i] < rowdepth[i+1] || (rowdepth[i] == rowdepth[i+1] && rownnz[i] <= rownnz[i+1]));
1008 	#endif
1009 	
1010 	   SCIPsetFreeBufferArray(set, &rownnz);
1011 	
1012 	   return SCIP_OKAY;
1013 	}
1014 	
1015 	/** adds locally valid rows to the proof constraint */
1016 	static
1017 	SCIP_RETCODE addLocalRows(
1018 	   SCIP_SET*             set,                /**< global SCIP settings */
1019 	   SCIP_PROB*            transprob,          /**< transformed problem */
1020 	   SCIP_LP*              lp,                 /**< LP data */
1021 	   SCIP_AGGRROW*         proofrow,           /**< aggregated row representing the proof */
1022 	   SCIP_ROW**            rows,               /**< array if locally valid rows */
1023 	   SCIP_Real*            dualsols,           /**< dual solution vector */
1024 	   int*                  localrowinds,       /**< array of row indecies */
1025 	   int*                  localrowdepth,      /**< array of row depths */
1026 	   int                   nlocalrows,         /**< number of local rows stored in rows array */
1027 	   SCIP_Real*            proofact,           /**< pointer to store the activity of the proof constraint */
1028 	   int*                  validdepth,         /**< pointer to store the depth where the proof constraint is valid */
1029 	   SCIP_Real*            curvarlbs,          /**< current lower bounds of active problem variables */
1030 	   SCIP_Real*            curvarubs,          /**< current upper bounds of active problem variables */
1031 	   SCIP_Bool*            valid               /**< pointer store whether the proof constraint is valid */
1032 	   )
1033 	{
1034 	   SCIP_Bool infdelta;
1035 	   int i;
1036 	
1037 	   assert(set != NULL);
1038 	   assert(lp != NULL);
1039 	
1040 	   *validdepth = 0;
1041 	
1042 	   if( !set->conf_uselocalrows )
1043 	      return SCIP_OKAY;
1044 	
1045 	   SCIPsetDebugMsg(set, "add local rows to dual proof:\n");
1046 	
1047 	   /* check whether the proof is already valid, e.g., violated within the local bounds */
1048 	   *proofact = SCIPaggrRowGetMinActivity(set, transprob, proofrow, curvarlbs, curvarubs, &infdelta);
1049 	
1050 	   /* we stop if the minimal activity is infinite but all variables have a finite activity delta (bad numerics) */
1051 	   if( !infdelta && SCIPsetIsInfinity(set, REALABS(*proofact)) )
1052 	   {
1053 	      *valid = FALSE;
1054 	      return SCIP_OKAY;
1055 	   }
1056 	
1057 	   /* break if the proof is valid w.r.t local bounds
1058 	    * note: it can happen that the proof contains a variable with an infinite activity delta.
1059 	    *       here, we don't break immediately because we might be able to fix it by adding local rows
1060 	    */
1061 	   if( !infdelta && SCIPsetIsGT(set, *proofact, SCIPaggrRowGetRhs(proofrow)) )
1062 	   {
1063 	      *valid = TRUE;
1064 	      return SCIP_OKAY;
1065 	   }
1066 	
1067 	   /* sort local rows by depth */
1068 	   SCIP_CALL( sortLocalRows(set, proofrow, rows, localrowinds, localrowdepth, nlocalrows) );
1069 	
1070 	   /* add successively local rows */
1071 	   for( i = 0; i < nlocalrows; ++i )
1072 	   {
1073 	      SCIP_ROW* row;
1074 	      int r;
1075 	
1076 	      r = localrowinds[i];
1077 	      row = rows[r];
1078 	
1079 	      assert(row != NULL);
1080 	      assert(row->len == 0 || row->cols != NULL);
1081 	      assert(row->len == 0 || row->vals != NULL);
1082 	      assert(row == lp->lpirows[r]);
1083 	      assert(row->local);
1084 	      assert(row->lpdepth == localrowdepth[i]);
1085 	
1086 	      /* ignore dual solution values of 0.0 (in this case: y_i == 0) */
1087 	      if( REALABS(dualsols[r]) > 0.0 )
1088 	      {
1089 	#ifndef NDEBUG
1090 	         SCIP_Bool zerocontribution;
1091 	
1092 	         /* check dual feasibility */
1093 	         *valid = checkDualFeasibility(set, row, dualsols[r], &zerocontribution);
1094 	         assert(*valid);
1095 	         assert(!zerocontribution);
1096 	#endif
1097 	
1098 	         if( SCIPsetIsDualfeasZero(set, dualsols[r]) )
1099 	            continue;
1100 	
1101 	         /* add row to dual proof */
1102 	         SCIP_CALL( addRowToAggrRow(set, row, -dualsols[r], proofrow) );
1103 	
1104 	         /* update depth where the proof is valid */
1105 	         if( *validdepth < localrowdepth[i] )
1106 	            *validdepth = localrowdepth[i];
1107 	
1108 	         /* get the new minimal activity */
1109 	         *proofact = SCIPaggrRowGetMinActivity(set, transprob, proofrow, curvarlbs, curvarubs, &infdelta);
1110 	
1111 	         /* we stop if the minimal activity is infinite but all variables have a finite activity delta (bad numerics) */
1112 	         if( !infdelta && SCIPsetIsInfinity(set, REALABS(*proofact)) )
1113 	         {
1114 	            *valid = FALSE;
1115 	            goto TERMINATE;
1116 	         }
1117 	
1118 	         /* break if the proof is valid w.r.t local bounds */
1119 	         if( !infdelta && SCIPsetIsGT(set, *proofact, SCIPaggrRowGetRhs(proofrow)) )
1120 	         {
1121 	            *valid = TRUE;
1122 	            break;
1123 	         }
1124 	      }
1125 	   }
1126 	
1127 	   /* remove all nearly zero coefficients */
1128 	   SCIPaggrRowRemoveZeros(set->scip, proofrow, TRUE, valid);
1129 	
1130 	  TERMINATE:
1131 	   if( !(*valid) )
1132 	   {
1133 	      SCIPsetDebugMsg(set, " -> proof is not valid: %g <= %g\n", *proofact, SCIPaggrRowGetRhs(proofrow));
1134 	      SCIPsetDebugMsg(set, " -> stop due to numerical troubles\n");
1135 	   }
1136 	   else
1137 	   {
1138 	      *proofact = SCIPaggrRowGetMinActivity(set, transprob, proofrow, curvarlbs, curvarubs, &infdelta);
1139 	
1140 	      /* we stop if the minimal activity is infinite but all variables have a finite activity delta (bad numerics) */
1141 	      if( !infdelta && SCIPsetIsInfinity(set, REALABS(*proofact)) )
1142 	      {
1143 	         *valid = FALSE;
1144 	         SCIPsetDebugMsg(set, " -> proof is not valid: %g <= %g [infdelta: %u]\n", *proofact, SCIPaggrRowGetRhs(proofrow), infdelta);
1145 	      }
1146 	      else if( infdelta || SCIPsetIsLE(set, *proofact, SCIPaggrRowGetRhs(proofrow)) )
1147 	      {
1148 	         *valid = FALSE;
1149 	         SCIPsetDebugMsg(set, " -> proof is not valid: %g <= %g [infdelta: %u]\n", *proofact, SCIPaggrRowGetRhs(proofrow), infdelta);
1150 	      }
1151 	   }
1152 	
1153 	   return SCIP_OKAY;
1154 	}
1155 	
1156 	/** calculates a Farkas proof from the current dual LP solution */
1157 	SCIP_RETCODE SCIPgetFarkasProof(
1158 	   SCIP_SET*             set,                /**< global SCIP settings */
1159 	   SCIP_PROB*            prob,               /**< transformed problem */
1160 	   SCIP_LP*              lp,                 /**< LP data */
1161 	   SCIP_LPI*             lpi,                /**< LPI data */
1162 	   SCIP_TREE*            tree,               /**< tree data */
1163 	   SCIP_AGGRROW*         farkasrow,          /**< aggregated row representing the proof */
1164 	   SCIP_Real*            farkasact,          /**< maximal activity of the proof constraint */
1165 	   int*                  validdepth,         /**< pointer to store the valid depth of the proof constraint */
1166 	   SCIP_Real*            curvarlbs,          /**< current lower bounds of active problem variables */
1167 	   SCIP_Real*            curvarubs,          /**< current upper bounds of active problem variables */
1168 	   SCIP_Bool*            valid               /**< pointer store whether the proof constraint is valid */
1169 	   )
1170 	{
1171 	   SCIP_ROW** rows;
1172 	   SCIP_Real* dualfarkas;
1173 	   SCIP_ROW* row;
1174 	   int* localrowinds;
1175 	   int* localrowdepth;
1176 	   SCIP_Bool infdelta;
1177 	   int nlocalrows;
1178 	   int nrows;
1179 	   int r;
1180 	
1181 	   assert(set != NULL);
1182 	   assert(prob != NULL);
1183 	   assert(lp != NULL);
1184 	   assert(lp->flushed);
1185 	   assert(lp->solved);
1186 	   assert(curvarlbs != NULL);
1187 	   assert(curvarubs != NULL);
1188 	   assert(valid != NULL);
1189 	
1190 	   assert(SCIPlpiIsPrimalInfeasible(lpi) || SCIPlpiIsObjlimExc(lpi) || SCIPlpiIsDualFeasible(lpi));
1191 	   assert(SCIPlpiIsPrimalInfeasible(lpi) || !SCIPlpDivingObjChanged(lp));
1192 	
1193 	   /* get LP rows and problem variables */
1194 	   rows = SCIPlpGetRows(lp);
1195 	   nrows = SCIPlpGetNRows(lp);
1196 	   assert(nrows == 0 || rows != NULL);
1197 	   assert(nrows == lp->nlpirows);
1198 	
1199 	   /* it can happen that infeasibility is detetected within LP presolve. in that case, the LP solver may not be able to
1200 	    * to return the dual ray.
1201 	    */
1202 	   if( !SCIPlpiHasDualRay(lpi) )
1203 	   {
1204 	      *valid = FALSE;
1205 	      return SCIP_OKAY;
1206 	   }
1207 	
1208 	   assert(farkasrow != NULL);
1209 	
1210 	   /* allocate temporary memory */
1211 	   SCIP_CALL( SCIPsetAllocBufferArray(set, &dualfarkas, nrows) );
1212 	   BMSclearMemoryArray(dualfarkas, nrows);
1213 	
1214 	   /* get dual Farkas values of rows */
1215 	   SCIP_CALL( SCIPlpiGetDualfarkas(lpi, dualfarkas) );
1216 	
1217 	   localrowinds = NULL;
1218 	   localrowdepth = NULL;
1219 	   nlocalrows = 0;
1220 	
1221 	   /* calculate the Farkas row */
1222 	   (*valid) = TRUE;
1223 	   (*validdepth) = 0;
1224 	
1225 	   for( r = 0; r < nrows; ++r )
1226 	   {
1227 	      row = rows[r];
1228 	      assert(row != NULL);
1229 	      assert(row->len == 0 || row->cols != NULL);
1230 	      assert(row->len == 0 || row->vals != NULL);
1231 	      assert(row == lp->lpirows[r]);
1232 	
1233 	      /* ignore dual ray values of 0.0 (in this case: y_i == z_i == 0) */
1234 	      if( REALABS(dualfarkas[r]) > 0.0 )
1235 	      {
1236 	         SCIP_Bool zerocontribution;
1237 	
1238 	         /* check dual feasibility */
1239 	         *valid = checkDualFeasibility(set, row, dualfarkas[r], &zerocontribution);
1240 	
1241 	         if( !(*valid) )
1242 	            goto TERMINATE;
1243 	
1244 	         if( zerocontribution )
1245 	            continue;
1246 	
1247 	         if( SCIPsetIsDualfeasZero(set, dualfarkas[r]) )
1248 	            continue;
1249 	
1250 	         if( !row->local )
1251 	         {
1252 	            SCIP_CALL( addRowToAggrRow(set, row, -dualfarkas[r], farkasrow) );
1253 	
1254 	            /* due to numerical reasons we want to stop */
1255 	            if( REALABS(SCIPaggrRowGetRhs(farkasrow)) > NUMSTOP )
1256 	            {
1257 	               (*valid) = FALSE;
1258 	               goto TERMINATE;
1259 	            }
1260 	         }
1261 	         else
1262 	         {
1263 	            int lpdepth = SCIProwGetLPDepth(row);
1264 	
1265 	            if( nlocalrows == 0 && lpdepth < SCIPtreeGetFocusDepth(tree) )
1266 	            {
1267 	               SCIP_CALL( SCIPsetAllocBufferArray(set, &localrowinds, nrows-r) );
1268 	               SCIP_CALL( SCIPsetAllocBufferArray(set, &localrowdepth, nrows-r) );
1269 	            }
1270 	
1271 	            if( lpdepth < SCIPtreeGetFocusDepth(tree) )
1272 	            {
1273 	               assert(localrowinds != NULL);
1274 	               assert(localrowdepth != NULL);
1275 	
1276 	               localrowinds[nlocalrows] = r;
1277 	               localrowdepth[nlocalrows++] = lpdepth;
1278 	            }
1279 	         }
1280 	      }
1281 	   }
1282 	
1283 	   /* remove all coefficients that are too close to zero */
1284 	   SCIPaggrRowRemoveZeros(set->scip, farkasrow, TRUE, valid);
1285 	
1286 	   if( !(*valid) )
1287 	      goto TERMINATE;
1288 	
1289 	   infdelta = FALSE;
1290 	
1291 	   /* calculate the current Farkas activity, always using the best bound w.r.t. the Farkas coefficient */
1292 	   *farkasact = SCIPaggrRowGetMinActivity(set, prob, farkasrow, curvarlbs, curvarubs, &infdelta);
1293 	
1294 	   SCIPsetDebugMsg(set, " -> farkasact=%g farkasrhs=%g [infdelta: %u], \n",
1295 	      (*farkasact), SCIPaggrRowGetRhs(farkasrow), infdelta);
1296 	
1297 	   /* The constructed proof is not valid, this can happen due to numerical reasons,
1298 	    * e.g., we only consider rows r with !SCIPsetIsZero(set, dualfarkas[r]),
1299 	    * or because of local rows were ignored so far.
1300 	    * Due to the latter case, it might happen at least one variable contributes
1301 	    * with an infinite value to the activity (see: https://git.zib.de/integer/scip/issues/2743)
1302 	    */
1303 	   if( infdelta || SCIPsetIsFeasLE(set, *farkasact, SCIPaggrRowGetRhs(farkasrow)))
1304 	   {
1305 	      /* add contribution of local rows */
1306 	      if( nlocalrows > 0 && set->conf_uselocalrows > 0 )
1307 	      {
1308 	         SCIP_CALL( addLocalRows(set, prob, lp, farkasrow, rows, dualfarkas, localrowinds, localrowdepth,
1309 	               nlocalrows, farkasact, validdepth, curvarlbs, curvarubs, valid) );
1310 	      }
1311 	      else
1312 	      {
1313 	         (*valid) = FALSE;
1314 	         SCIPsetDebugMsg(set, " -> proof is not valid to due infinite activity delta\n");
1315 	      }
1316 	   }
1317 	
1318 	  TERMINATE:
1319 	
1320 	   SCIPfreeBufferArrayNull(set->scip, &localrowdepth);
1321 	   SCIPfreeBufferArrayNull(set->scip, &localrowinds);
1322 	   SCIPsetFreeBufferArray(set, &dualfarkas);
1323 	
1324 	   return SCIP_OKAY;
1325 	}
1326 	
1327 	/** calculates a dual proof from the current dual LP solution */
1328 	SCIP_RETCODE SCIPgetDualProof(
1329 	   SCIP_SET*             set,                /**< global SCIP settings */
1330 	   SCIP_PROB*            transprob,          /**< transformed problem */
1331 	   SCIP_LP*              lp,                 /**< LP data */
1332 	   SCIP_LPI*             lpi,                /**< LPI data */
1333 	   SCIP_TREE*            tree,               /**< tree data */
1334 	   SCIP_AGGRROW*         farkasrow,          /**< aggregated row representing the proof */
1335 	   SCIP_Real*            farkasact,          /**< maximal activity of the proof constraint */
1336 	   int*                  validdepth,         /**< pointer to store the valid depth of the proof constraint */
1337 	   SCIP_Real*            curvarlbs,          /**< current lower bounds of active problem variables */
1338 	   SCIP_Real*            curvarubs,          /**< current upper bounds of active problem variables */
1339 	   SCIP_Bool*            valid               /**< pointer store whether the proof constraint is valid */
1340 	   )
1341 	{
1342 	   SCIP_RETCODE retcode;
1343 	   SCIP_ROW** rows;
1344 	   SCIP_ROW* row;
1345 	   SCIP_Real* primsols;
1346 	   SCIP_Real* dualsols;
1347 	   SCIP_Real* redcosts;
1348 	   int* localrowinds;
1349 	   int* localrowdepth;
1350 	   SCIP_Real maxabsdualsol;
1351 	   SCIP_Bool infdelta;
1352 	   int nlocalrows;
1353 	   int nrows;
1354 	   int ncols;
1355 	   int r;
1356 	
1357 	   assert(set != NULL);
1358 	   assert(transprob != NULL);
1359 	   assert(lp != NULL);
1360 	   assert(lp->flushed);
1361 	   assert(lp->solved);
1362 	   assert(curvarlbs != NULL);
1363 	   assert(curvarubs != NULL);
1364 	   assert(valid != NULL);
1365 	
1366 	   *validdepth = 0;
1367 	   *valid = TRUE;
1368 	
1369 	   localrowinds = NULL;
1370 	   localrowdepth = NULL;
1371 	   nlocalrows = 0;
1372 	
1373 	   /* get LP rows and problem variables */
1374 	   rows = SCIPlpGetRows(lp);
1375 	   nrows = SCIPlpGetNRows(lp);
1376 	   ncols = SCIPlpGetNCols(lp);
1377 	   assert(nrows == 0 || rows != NULL);
1378 	   assert(nrows == lp->nlpirows);
1379 	
1380 	   /* get temporary memory */
1381 	   SCIP_CALL( SCIPsetAllocBufferArray(set, &primsols, ncols) );
1382 	   SCIP_CALL( SCIPsetAllocBufferArray(set, &dualsols, nrows) );
1383 	   SCIP_CALL( SCIPsetAllocBufferArray(set, &redcosts, ncols) );
1384 	
1385 	   /* get solution from LPI */
1386 	   retcode = SCIPlpiGetSol(lpi, NULL, primsols, dualsols, NULL, redcosts);
1387 	   if( retcode == SCIP_LPERROR ) /* on an error in the LP solver, just abort the conflict analysis */
1388 	   {
1389 	      (*valid) = FALSE;
1390 	      goto TERMINATE;
1391 	   }
1392 	   SCIP_CALL( retcode );
1393 	#ifdef SCIP_DEBUG
1394 	   {
1395 	      SCIP_Real objval;
1396 	      SCIP_CALL( SCIPlpiGetObjval(lpi, &objval) );
1397 	      SCIPsetDebugMsg(set, " -> LP objval: %g\n", objval);
1398 	   }
1399 	#endif
1400 	
1401 	   /* check whether the dual solution is numerically stable */
1402 	   maxabsdualsol = 0;
1403 	   for( r = 0; r < nrows; r++ )
1404 	   {
1405 	      SCIP_Real absdualsol = REALABS(dualsols[r]);
1406 	
1407 	      if( absdualsol > maxabsdualsol )
1408 	         maxabsdualsol = absdualsol;
1409 	   }
1410 	
1411 	   /* don't consider dual solution with maxabsdualsol > 1e+07, this would almost cancel out the objective constraint */
1412 	   if( maxabsdualsol > 1e+07 )
1413 	   {
1414 	      (*valid) = FALSE;
1415 	      goto TERMINATE;
1416 	   }
1417 	
1418 	   /* clear the proof */
1419 	   SCIPaggrRowClear(farkasrow);
1420 	
1421 	   /* Let y be the dual solution and r be the reduced cost vector. Let z be defined as
1422 	    *    z_i := y_i if i is a global row,
1423 	    *    z_i := 0   if i is a local row.
1424 	    * Define the set X := {x | lhs <= Ax <= rhs, lb <= x <= ub, c^Tx <= c*}, with c* being the current primal bound.
1425 	    * Then the following inequalities are valid for all x \in X:
1426 	    *                                 - c* <= -c^Tx
1427 	    *   <=>                     z^TAx - c* <= (z^TA - c^T) x
1428 	    *   <=>                     z^TAx - c* <= (y^TA - c^T - (y-z)^TA) x
1429 	    *   <=>                     z^TAx - c* <= (-r^T - (y-z)^TA) x         (dual feasibility of (y,r): y^TA + r^T == c^T)
1430 	    * Because lhs <= Ax <= rhs and lb <= x <= ub, the inequality can be relaxed to give
1431 	    *     min{z^Tq | lhs <= q <= rhs} - c* <= max{(-r^T - (y-z)^TA) x | lb <= x <= ub}, or X = {}.
1432 	    *
1433 	    * The resulting dual row is:  z^T{lhs,rhs} - c* <= (-r^T - (y-z)^TA){lb,ub},
1434 	    * where lhs, rhs, lb, and ub are selected in order to maximize the feasibility of the row.
1435 	    */
1436 	
1437 	   /* add the objective function to the aggregation row with respect to the current cutoff bound
1438 	    *
1439 	    * for an integral objective the right-hand side is reduced by the cutoff bound delta to cut off up to the next
1440 	    * possible objective value below the cutoff bound
1441 	    */
1442 	   SCIP_CALL( SCIPaggrRowAddObjectiveFunction(set->scip, farkasrow, lp->cutoffbound - (SCIPprobIsObjIntegral(transprob) ? SCIPsetCutoffbounddelta(set) : 0.0), 1.0) );
1443 	
1444 	   /* dual row: z^T{lhs,rhs} - c* <= (-r^T - (y-z)^TA){lb,ub}
1445 	    * process rows: add z^T{lhs,rhs} to the dual row's left hand side, and -(y-z)^TA to the dual row's coefficients
1446 	    */
1447 	   for( r = 0; r < nrows; ++r )
1448 	   {
1449 	      row = rows[r];
1450 	      assert(row != NULL);
1451 	      assert(row->len == 0 || row->cols != NULL);
1452 	      assert(row->len == 0 || row->vals != NULL);
1453 	      assert(row == lp->lpirows[r]);
1454 	
1455 	      /* ignore dual solution values of 0.0 (in this case: y_i == z_i == 0) */
1456 	      if( REALABS(dualsols[r]) > 0.0 )
1457 	      {
1458 	         SCIP_Bool zerocontribution;
1459 	
1460 	         /* check dual feasibility */
1461 	         *valid = checkDualFeasibility(set, row, dualsols[r], &zerocontribution);
1462 	
1463 	         if( !(*valid) )
1464 	            goto TERMINATE;
1465 	
1466 	         if( zerocontribution )
1467 	            continue;
1468 	
1469 	         if( SCIPsetIsDualfeasZero(set, dualsols[r]) )
1470 	            continue;
1471 	
1472 	         /* skip local row */
1473 	         if( !row->local )
1474 	         {
1475 	            SCIP_CALL( addRowToAggrRow(set, row, -dualsols[r], farkasrow) );
1476 	
1477 	            /* due to numerical reasons we want to stop */
1478 	            if( REALABS(SCIPaggrRowGetRhs(farkasrow)) > NUMSTOP )
1479 	            {
1480 	               (*valid) = FALSE;
1481 	               goto TERMINATE;
1482 	            }
1483 	         }
1484 	         else
1485 	         {
1486 	            int lpdepth = SCIProwGetLPDepth(row);
1487 	
1488 	            if( nlocalrows == 0 && lpdepth < SCIPtreeGetFocusDepth(tree) )
1489 	            {
1490 	               SCIP_CALL( SCIPsetAllocBufferArray(set, &localrowinds, nrows-r) );
1491 	               SCIP_CALL( SCIPsetAllocBufferArray(set, &localrowdepth, nrows-r) );
1492 	            }
1493 	
1494 	            if( lpdepth < SCIPtreeGetFocusDepth(tree) )
1495 	            {
1496 	               assert(localrowinds != NULL);
1497 	               assert(localrowdepth != NULL);
1498 	
1499 	               localrowinds[nlocalrows] = r;
1500 	               localrowdepth[nlocalrows++] = lpdepth;
1501 	            }
1502 	         }
1503 	      }
1504 	   }
1505 	
1506 	   /* remove all nearly zero coefficients */
1507 	   SCIPaggrRowRemoveZeros(set->scip, farkasrow, TRUE, valid);
1508 	
1509 	   if( !(*valid) )
1510 	      goto TERMINATE;
1511 	
1512 	   infdelta = FALSE;
1513 	
1514 	   /* check validity of the proof */
1515 	   *farkasact = SCIPaggrRowGetMinActivity(set, transprob, farkasrow, curvarlbs, curvarubs, &infdelta);
1516 	
1517 	   SCIPsetDebugMsg(set, " -> farkasact=%g farkasrhs=%g [infdelta: %u], \n",
1518 	      (*farkasact), SCIPaggrRowGetRhs(farkasrow), infdelta);
1519 	
1520 	   /* The constructed proof is not valid, this can happen due to numerical reasons,
1521 	    * e.g., we only consider rows r with !SCIPsetIsZero(set, dualsol[r]),
1522 	    * or because of local rows were ignored so far.
1523 	    * Due to the latter case, it might happen at least one variable contributes
1524 	    * with an infinite value to the activity (see: https://git.zib.de/integer/scip/issues/2743)
1525 	    */
1526 	   if( infdelta || SCIPsetIsFeasLE(set, *farkasact, SCIPaggrRowGetRhs(farkasrow)))
1527 	   {
1528 	      /* add contribution of local rows */
1529 	      if( nlocalrows > 0 && set->conf_uselocalrows > 0 )
1530 	      {
1531 	         SCIP_CALL( addLocalRows(set, transprob, lp, farkasrow, rows, dualsols, localrowinds, localrowdepth,
1532 	               nlocalrows, farkasact, validdepth, curvarlbs, curvarubs, valid) );
1533 	      }
1534 	      else
1535 	      {
1536 	         (*valid) = FALSE;
1537 	         SCIPsetDebugMsg(set, " -> proof is not valid to due infinite activity delta\n");
1538 	      }
1539 	   }
1540 	
1541 	  TERMINATE:
1542 	
1543 	   SCIPfreeBufferArrayNull(set->scip, &localrowdepth);
1544 	   SCIPfreeBufferArrayNull(set->scip, &localrowinds);
1545 	   SCIPsetFreeBufferArray(set, &redcosts);
1546 	   SCIPsetFreeBufferArray(set, &dualsols);
1547 	   SCIPsetFreeBufferArray(set, &primsols);
1548 	
1549 	   return SCIP_OKAY;
1550 	}
1551 	
1552 	
1553 	/*
1554 	 * pseudo solution conflict analysis
1555 	 */
1556 	
1557 	/** analyzes a pseudo solution with objective value exceeding the current cutoff to find out the bound changes on
1558 	 *  variables that were responsible for the objective value degradation;
1559 	 *  on success, calls standard conflict analysis with the responsible variables as starting conflict set, thus creating
1560 	 *  a conflict constraint out of the resulting conflict set;
1561 	 *  updates statistics for pseudo solution conflict analysis
1562 	 */
1563 	SCIP_RETCODE SCIPconflictAnalyzePseudo(
1564 	   SCIP_CONFLICT*        conflict,           /**< conflict analysis data */
1565 	   BMS_BLKMEM*           blkmem,             /**< block memory of transformed problem */
1566 	   SCIP_SET*             set,                /**< global SCIP settings */
1567 	   SCIP_STAT*            stat,               /**< problem statistics */
1568 	   SCIP_PROB*            transprob,          /**< transformed problem */
1569 	   SCIP_PROB*            origprob,           /**< original problem */
1570 	   SCIP_TREE*            tree,               /**< branch and bound tree */
1571 	   SCIP_REOPT*           reopt,              /**< reoptimization data structure */
1572 	   SCIP_LP*              lp,                 /**< LP data */
1573 	   SCIP_BRANCHCAND*      branchcand,         /**< branching candidate storage */
1574 	   SCIP_EVENTQUEUE*      eventqueue,         /**< event queue */
1575 	   SCIP_CLIQUETABLE*     cliquetable,        /**< clique table data structure */
1576 	   SCIP_Bool*            success             /**< pointer to store whether a conflict constraint was created, or NULL */
1577 	   )
1578 	{
1579 	   SCIP_VAR** vars;
1580 	   SCIP_VAR* var;
1581 	   SCIP_Real* curvarlbs;
1582 	   SCIP_Real* curvarubs;
1583 	   int* lbchginfoposs;
1584 	   int* ubchginfoposs;
1585 	   SCIP_Real* pseudocoefs;
1586 	   SCIP_Real pseudolhs;
1587 	   SCIP_Real pseudoact;
1588 	   int nvars;
1589 	   int v;
1590 	
1591 	   assert(conflict != NULL);
1592 	   assert(conflict->nconflictsets == 0);
1593 	   assert(set != NULL);
1594 	   assert(stat != NULL);
1595 	   assert(transprob != NULL);
1596 	   assert(lp != NULL);
1597 	   assert(!SCIPsetIsInfinity(set, -SCIPlpGetPseudoObjval(lp, set, transprob)));
1598 	   assert(!SCIPsetIsInfinity(set, lp->cutoffbound));
1599 	
1600 	   if( success != NULL )
1601 	      *success = FALSE;
1602 	
1603 	   /* check, if pseudo solution conflict analysis is enabled */
1604 	   if( !set->conf_enable || !set->conf_usepseudo )
1605 	      return SCIP_OKAY;
1606 	
1607 	   /* check, if there are any conflict handlers to use a conflict set */
1608 	   if( set->nconflicthdlrs == 0 )
1609 	      return SCIP_OKAY;
1610 	
1611 	   SCIPsetDebugMsg(set, "analyzing pseudo solution (obj: %g) that exceeds objective limit (%g)\n",
1612 	      SCIPlpGetPseudoObjval(lp, set, transprob), lp->cutoffbound);
1613 	
1614 	   conflict->conflictset->conflicttype = SCIP_CONFTYPE_BNDEXCEEDING;
1615 	   conflict->conflictset->usescutoffbound = TRUE;
1616 	
1617 	   /* start timing */
1618 	   SCIPclockStart(conflict->pseudoanalyzetime, set);
1619 	   conflict->npseudocalls++;
1620 	
1621 	   vars = transprob->vars;
1622 	   nvars = transprob->nvars;
1623 	   assert(nvars == 0 || vars != NULL);
1624 	
1625 	   /* The current primal bound c* gives an upper bound for the current pseudo objective value:
1626 	    *   min{c^T x | lb <= x <= ub} <= c*.
1627 	    * We have to transform this row into a >= inequality in order to use methods above:
1628 	    *                          -c* <= max{-c^T x | lb <= x <= ub}.
1629 	    * In the local subproblem, this row is violated. We want to undo bound changes while still keeping the
1630 	    * row violated.
1631 	    */
1632 	
1633 	   /* get temporary memory for remembering variables' current bounds and corresponding bound change information
1634 	    * positions in variable's bound change information arrays
1635 	    */
1636 	   SCIP_CALL( SCIPsetAllocBufferArray(set, &curvarlbs, nvars) );
1637 	   SCIP_CALL( SCIPsetAllocBufferArray(set, &curvarubs, nvars) );
1638 	   SCIP_CALL( SCIPsetAllocBufferArray(set, &lbchginfoposs, nvars) );
1639 	   SCIP_CALL( SCIPsetAllocBufferArray(set, &ubchginfoposs, nvars) );
1640 	
1641 	   /* get temporary memory for infeasibility proof coefficients */
1642 	   SCIP_CALL( SCIPsetAllocBufferArray(set, &pseudocoefs, nvars) );
1643 	
1644 	   /* for an integral objective use the cutoff bound reduced by the cutoff bound delta to cut off up to the next better
1645 	    * objective value
1646 	    */
1647 	   pseudolhs = -(lp->cutoffbound - (SCIPprobIsObjIntegral(transprob) ? SCIPsetCutoffbounddelta(set) : 0.0));
1648 	
1649 	   /* store the objective values as infeasibility proof coefficients, and recalculate the pseudo activity */
1650 	   pseudoact = 0.0;
1651 	   for( v = 0; v < nvars; ++v )
1652 	   {
1653 	      var = vars[v];
1654 	      pseudocoefs[v] = -SCIPvarGetObj(var);
1655 	      curvarlbs[v] = SCIPvarGetLbLocal(var);
1656 	      curvarubs[v] = SCIPvarGetUbLocal(var);
1657 	      lbchginfoposs[v] = var->nlbchginfos-1;
1658 	      ubchginfoposs[v] = var->nubchginfos-1;
1659 	
1660 	      if( SCIPsetIsZero(set, pseudocoefs[v]) )
1661 	      {
1662 	         pseudocoefs[v] = 0.0;
1663 	         continue;
1664 	      }
1665 	
1666 	      if( pseudocoefs[v] > 0.0 )
1667 	         pseudoact += pseudocoefs[v] * curvarubs[v];
1668 	      else
1669 	         pseudoact += pseudocoefs[v] * curvarlbs[v];
1670 	   }
1671 	   assert(SCIPsetIsFeasEQ(set, pseudoact, -SCIPlpGetPseudoObjval(lp, set, transprob)));
1672 	   SCIPsetDebugMsg(set, "  -> recalculated pseudo infeasibility proof:  %g <= %g\n", pseudolhs, pseudoact);
1673 	
1674 	   /* check, if the pseudo row is still violated (after recalculation of pseudo activity) */
1675 	   if( SCIPsetIsFeasGT(set, pseudolhs, pseudoact) )
1676 	   {
1677 	      int nconss;
1678 	      int nliterals;
1679 	      int nreconvconss;
1680 	      int nreconvliterals;
1681 	
1682 	      /* undo bound changes without destroying the infeasibility proof */
1683 	      SCIP_CALL( SCIPundoBdchgsProof(set, transprob, SCIPtreeGetCurrentDepth(tree), pseudocoefs, pseudolhs, &pseudoact,
1684 	            curvarlbs, curvarubs, lbchginfoposs, ubchginfoposs, NULL, NULL, NULL, lp->lpi) );
1685 	
1686 	      /* analyze conflict on remaining bound changes */
1687 	      SCIP_CALL( SCIPconflictAnalyzeRemainingBdchgs(conflict, blkmem, set, stat, transprob, tree, FALSE, \
1688 	            lbchginfoposs, ubchginfoposs, &nconss, &nliterals, &nreconvconss, &nreconvliterals) );
1689 	      conflict->npseudosuccess += (nconss > 0 ? 1 : 0);
1690 	      conflict->npseudoconfconss += nconss;
1691 	      conflict->npseudoconfliterals += nliterals;
1692 	      conflict->npseudoreconvconss += nreconvconss;
1693 	      conflict->npseudoreconvliterals += nreconvliterals;
1694 	      if( success != NULL )
1695 	         *success = (nconss > 0);
1696 	   }
1697 	
1698 	   /* free temporary memory */
1699 	   SCIPsetFreeBufferArray(set, &pseudocoefs);
1700 	   SCIPsetFreeBufferArray(set, &ubchginfoposs);
1701 	   SCIPsetFreeBufferArray(set, &lbchginfoposs);
1702 	   SCIPsetFreeBufferArray(set, &curvarubs);
1703 	   SCIPsetFreeBufferArray(set, &curvarlbs);
1704 	
1705 	   /* flush conflict set storage */
1706 	   SCIP_CALL( SCIPconflictFlushConss(conflict, blkmem, set, stat, transprob, origprob, tree, reopt, lp, branchcand, eventqueue, cliquetable) );
1707 	
1708 	   /* stop timing */
1709 	   SCIPclockStop(conflict->pseudoanalyzetime, set);
1710 	
1711 	   return SCIP_OKAY;
1712 	}
1713 	
1714 	/** gets time in seconds used for analyzing pseudo solution conflicts */
1715 	SCIP_Real SCIPconflictGetPseudoTime(
1716 	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
1717 	   )
1718 	{
1719 	   assert(conflict != NULL);
1720 	
1721 	   return SCIPclockGetTime(conflict->pseudoanalyzetime);
1722 	}
1723 	
1724 	/** gets number of calls to pseudo solution conflict analysis */
1725 	SCIP_Longint SCIPconflictGetNPseudoCalls(
1726 	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
1727 	   )
1728 	{
1729 	   assert(conflict != NULL);
1730 	
1731 	   return conflict->npseudocalls;
1732 	}
1733 	
1734 	/** gets number of calls to pseudo solution conflict analysis that yield at least one conflict constraint */
1735 	SCIP_Longint SCIPconflictGetNPseudoSuccess(
1736 	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
1737 	   )
1738 	{
1739 	   assert(conflict != NULL);
1740 	
1741 	   return conflict->npseudosuccess;
1742 	}
1743 	
1744 	/** gets number of conflict constraints detected in pseudo solution conflict analysis */
1745 	SCIP_Longint SCIPconflictGetNPseudoConflictConss(
1746 	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
1747 	   )
1748 	{
1749 	   assert(conflict != NULL);
1750 	
1751 	   return conflict->npseudoconfconss;
1752 	}
1753 	
1754 	/** gets total number of literals in conflict constraints created in pseudo solution conflict analysis */
1755 	SCIP_Longint SCIPconflictGetNPseudoConflictLiterals(
1756 	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
1757 	   )
1758 	{
1759 	   assert(conflict != NULL);
1760 	
1761 	   return conflict->npseudoconfliterals;
1762 	}
1763 	
1764 	/** gets number of reconvergence constraints detected in pseudo solution conflict analysis */
1765 	SCIP_Longint SCIPconflictGetNPseudoReconvergenceConss(
1766 	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
1767 	   )
1768 	{
1769 	   assert(conflict != NULL);
1770 	
1771 	   return conflict->npseudoreconvconss;
1772 	}
1773 	
1774 	/** gets total number of literals in reconvergence constraints created in pseudo solution conflict analysis */
1775 	SCIP_Longint SCIPconflictGetNPseudoReconvergenceLiterals(
1776 	   SCIP_CONFLICT*        conflict            /**< conflict analysis data */
1777 	   )
1778 	{
1779 	   assert(conflict != NULL);
1780 	
1781 	   return conflict->npseudoreconvliterals;
1782 	}
1783 	
1784 	/** actually performs analysis of infeasible LP */
1785 	static
1786 	SCIP_RETCODE conflictAnalyzeLP(
1787 	   SCIP_CONFLICT*        conflict,           /**< conflict analysis data */
1788 	   SCIP_CONFLICTSTORE*   conflictstore,      /**< conflict store */
1789 	   BMS_BLKMEM*           blkmem,             /**< block memory of transformed problem */
1790 	   SCIP_SET*             set,                /**< global SCIP settings */
1791 	   SCIP_STAT*            stat,               /**< problem statistics */
1792 	   SCIP_PROB*            transprob,          /**< transformed problem */
1793 	   SCIP_PROB*            origprob,           /**< original problem */
1794 	   SCIP_TREE*            tree,               /**< branch and bound tree */
1795 	   SCIP_REOPT*           reopt,              /**< reoptimization data structure */
1796 	   SCIP_LP*              lp,                 /**< LP data */
1797 	   SCIP_BRANCHCAND*      branchcand,         /**< branching candidate storage */
1798 	   SCIP_EVENTQUEUE*      eventqueue,         /**< event queue */
1799 	   SCIP_CLIQUETABLE*     cliquetable,        /**< clique table data structure */
1800 	   SCIP_Bool             diving,             /**< are we in strong branching or diving mode? */
1801 	   SCIP_Bool*            dualproofsuccess,   /**< pointer to store success result of dual proof analysis */
1802 	   int*                  iterations,         /**< pointer to store the total number of LP iterations used */
1803 	   int*                  nconss,             /**< pointer to store the number of generated conflict constraints */
1804 	   int*                  nliterals,          /**< pointer to store the number of literals in generated conflict constraints */
1805 	   int*                  nreconvconss,       /**< pointer to store the number of generated reconvergence constraints */
1806 	   int*                  nreconvliterals,    /**< pointer to store the number of literals generated reconvergence constraints */
1807 	   SCIP_Bool             marklpunsolved      /**< whether LP should be marked unsolved after analysis (needed for strong branching) */
1808 	   )
1809 	{
1810 	   SCIP_VAR** vars;
1811 	   SCIP_AGGRROW* farkasrow;
1812 	   SCIP_LPI* lpi;
1813 	   SCIP_Bool valid;
1814 	   SCIP_Bool globalinfeasible;
1815 	   int* lbchginfoposs;
1816 	   int* ubchginfoposs;
1817 	   int validdepth;
1818 	   int nvars;
1819 	   int v;
1820 	   SCIP_Real* curvarlbs;
1821 	   SCIP_Real* curvarubs;
1822 	   SCIP_Real farkasactivity;
1823 	
1824 	   assert(conflict != NULL);
1825 	   assert(conflict->nconflictsets == 0);
1826 	   assert(set != NULL);
1827 	   assert(SCIPprobAllColsInLP(transprob, set, lp)); /* LP conflict analysis is only valid, if all variables are known */
1828 	   assert(stat != NULL);
1829 	   assert(transprob != NULL);
1830 	   assert(lp != NULL);
1831 	   assert(lp->flushed);
1832 	   assert(lp->solved);
1833 	   assert(iterations != NULL);
1834 	   assert(nconss != NULL);
1835 	   assert(nliterals != NULL);
1836 	   assert(nreconvconss != NULL);
1837 	   assert(nreconvliterals != NULL);
1838 	
1839 	   *iterations = 0;
1840 	   *nconss = 0;
1841 	   *nliterals = 0;
1842 	   *nreconvconss = 0;
1843 	   *nreconvliterals = 0;
1844 	
1845 	   vars = transprob->vars;
1846 	   nvars = transprob->nvars;
1847 	
1848 	   valid = TRUE;
1849 	   validdepth = 0;
1850 	
1851 	   /* get LP solver interface */
1852 	   lpi = SCIPlpGetLPI(lp);
1853 	   assert(SCIPlpiIsPrimalInfeasible(lpi) || SCIPlpiIsObjlimExc(lpi) || SCIPlpiIsDualFeasible(lpi));
1854 	   assert(SCIPlpiIsPrimalInfeasible(lpi) || !SCIPlpDivingObjChanged(lp));
1855 	
1856 	   if( !SCIPlpiIsPrimalInfeasible(lpi) )
1857 	   {
1858 	      SCIP_Real objval;
1859 	
1860 	      assert(!SCIPlpDivingObjChanged(lp));
1861 	
1862 	      /* make sure, a dual feasible solution exists, that exceeds the objective limit;
1863 	       * With FASTMIP setting, CPLEX does not apply the final pivot to reach the dual solution exceeding the objective
1864 	       * limit. Therefore, we have to either turn off FASTMIP and resolve the problem or continue solving it without
1865 	       * objective limit for at least one iteration. It seems that the strategy to continue with FASTMIP for one
1866 	       * additional simplex iteration yields better results.
1867 	       */
1868 	      SCIP_CALL( SCIPlpiGetObjval(lpi, &objval) );
1869 	      if( objval < lp->lpiobjlim )
1870 	      {
1871 	         SCIP_RETCODE retcode;
1872 	
1873 	         /* temporarily disable objective limit and install an iteration limit */
1874 	         SCIP_CALL( SCIPlpiSetRealpar(lpi, SCIP_LPPAR_OBJLIM, SCIPlpiInfinity(lpi)) );
1875 	         SCIP_CALL( SCIPlpiSetIntpar(lpi, SCIP_LPPAR_LPITLIM, 1) );
1876 	
1877 	         /* start LP timer */
1878 	         SCIPclockStart(stat->conflictlptime, set);
1879 	
1880 	         /* resolve LP */
1881 	         retcode = SCIPlpiSolveDual(lpi);
1882 	
1883 	         /* stop LP timer */
1884 	         SCIPclockStop(stat->conflictlptime, set);
1885 	
1886 	         /* check return code of LP solving call */
1887 	         valid = (retcode != SCIP_LPERROR);
1888 	         if( valid )
1889 	         {
1890 	            int iter;
1891 	
1892 	            SCIP_CALL( retcode );
1893 	
1894 	            /* count number of LP iterations */
1895 	            SCIP_CALL( SCIPlpiGetIterations(lpi, &iter) );
1896 	            (*iterations) += iter;
1897 	            stat->nconflictlps++;
1898 	            stat->nconflictlpiterations += iter;
1899 	            SCIPsetDebugMsg(set, " -> resolved objlim exceeding LP in %d iterations (total: %" SCIP_LONGINT_FORMAT ") (infeasible:%u, objlim: %u, optimal:%u)\n",
1900 	               iter, stat->nconflictlpiterations, SCIPlpiIsPrimalInfeasible(lpi), SCIPlpiIsObjlimExc(lpi), SCIPlpiIsOptimal(lpi));
1901 	            valid = (SCIPlpiIsObjlimExc(lpi) || SCIPlpiIsPrimalInfeasible(lpi) || SCIPlpiIsDualFeasible(lpi));
1902 	         }
1903 	
1904 	         /* reinstall old objective and iteration limits in LP solver */
1905 	         SCIP_CALL( SCIPlpiSetRealpar(lpi, SCIP_LPPAR_OBJLIM, lp->lpiobjlim) );
1906 	         SCIP_CALL( SCIPlpiSetIntpar(lpi, SCIP_LPPAR_LPITLIM, lp->lpiitlim) );
1907 	
1908 	         /* abort, if the LP produced an error */
1909 	         if( !valid )
1910 	            return SCIP_OKAY;
1911 	      }
1912 	   }
1913 	   assert(SCIPlpiIsPrimalInfeasible(lpi) || SCIPlpiIsObjlimExc(lpi) || SCIPlpiIsDualFeasible(lpi));
1914 	
1915 	   if( !SCIPlpiIsPrimalInfeasible(lpi) )
1916 	   {
1917 	      SCIP_Real objval;
1918 	
1919 	      assert(!SCIPlpDivingObjChanged(lp));
1920 	
1921 	      SCIP_CALL( SCIPlpiGetObjval(lpi, &objval) );
1922 	      if( objval < lp->lpiobjlim )
1923 	      {
1924 	         SCIPsetDebugMsg(set, " -> LP does not exceed the cutoff bound: obj=%g, cutoff=%g\n", objval, lp->lpiobjlim);
1925 	         return SCIP_OKAY;
1926 	      }
1927 	      else
1928 	      {
1929 	         SCIPsetDebugMsg(set, " -> LP exceeds the cutoff bound: obj=%g, cutoff=%g\n", objval, lp->lpiobjlim);
1930 	      }
1931 	   }
1932 	
1933 	   assert(valid);
1934 	
1935 	   SCIP_CALL( SCIPaggrRowCreate(set->scip, &farkasrow) );
1936 	   SCIP_CALL( SCIPsetAllocBufferArray(set, &lbchginfoposs, transprob->nvars) );
1937 	   SCIP_CALL( SCIPsetAllocBufferArray(set, &ubchginfoposs, transprob->nvars) );
1938 	
1939 	   farkasactivity = 0.0;
1940 	
1941 	   /* get temporary memory for remembering variables' current bounds and corresponding bound change information
1942 	    * positions in variable's bound change information arrays
1943 	    */
1944 	   SCIP_CALL( SCIPsetAllocBufferArray(set, &curvarlbs, nvars) );
1945 	   SCIP_CALL( SCIPsetAllocBufferArray(set, &curvarubs, nvars) );
1946 	
1947 	   /* get current bounds and current positions in lb/ubchginfos arrays of variables */
1948 	   valid = TRUE;
1949 	   for( v = 0; v < nvars && valid; ++v )
1950 	   {
1951 	      SCIP_VAR* var;
1952 	
1953 	      var = vars[v];
1954 	
1955 	      curvarlbs[v] = SCIPvarGetLbLP(var, set);
1956 	      curvarubs[v] = SCIPvarGetUbLP(var, set);
1957 	      lbchginfoposs[v] = var->nlbchginfos-1;
1958 	      ubchginfoposs[v] = var->nubchginfos-1;
1959 	      assert(diving || SCIPsetIsEQ(set, curvarlbs[v], SCIPvarGetLbLocal(var)));
1960 	      assert(diving || SCIPsetIsEQ(set, curvarubs[v], SCIPvarGetUbLocal(var)));
1961 	
1962 	      /* check, if last bound changes were due to strong branching or diving */
1963 	      if( diving )
1964 	      {
1965 	         SCIP_Real lb;
1966 	         SCIP_Real ub;
1967 	
1968 	         lb = SCIPvarGetLbLocal(var);
1969 	         ub = SCIPvarGetUbLocal(var);
1970 	         if( SCIPsetIsGT(set, curvarlbs[v], lb) )
1971 	            lbchginfoposs[v] = var->nlbchginfos;
1972 	         else if( SCIPsetIsLT(set, curvarlbs[v], lb) )
1973 	         {
1974 	            /* the bound in the diving LP was relaxed -> the LP is not a subproblem of the current node -> abort! */
1975 	            /**@todo we could still analyze such a conflict, but we would have to take care with our data structures */
1976 	            valid = FALSE;
1977 	         }
1978 	         if( SCIPsetIsLT(set, curvarubs[v], ub) )
1979 	            ubchginfoposs[v] = var->nubchginfos;
1980 	         else if( SCIPsetIsGT(set, curvarubs[v], ub) )
1981 	         {
1982 	            /* the bound in the diving LP was relaxed -> the LP is not a subproblem of the current node -> abort! */
1983 	            /**@todo we could still analyze such a conflict, but we would have to take care with our data structures */
1984 	            valid = FALSE;
1985 	         }
1986 	      }
1987 	   }
1988 	
1989 	   if( !valid )
1990 	      goto TERMINATE;
1991 	
1992 	   /* the LP is prooven to be infeasible */
1993 	   if( SCIPlpiIsPrimalInfeasible(lpi) )
1994 	   {
1995 	      SCIP_CALL( SCIPgetFarkasProof(set, transprob, lp, lpi, tree, farkasrow, &farkasactivity, &validdepth,
1996 	         curvarlbs, curvarubs, &valid) );
1997 	   }
1998 	   /* the LP is dual feasible and/or exceeds the current incumbant solution */
1999 	   else
2000 	   {
2001 	      assert(SCIPlpiIsDualFeasible(lpi) || SCIPlpiIsObjlimExc(lpi));
2002 	      SCIP_CALL( SCIPgetDualProof(set, transprob, lp, lpi, tree, farkasrow, &farkasactivity, &validdepth,
2003 	         curvarlbs, curvarubs, &valid) );
2004 	   }
2005 	
2006 	   if( !valid || validdepth >= SCIPtreeGetCurrentDepth(tree) )
2007 	      goto TERMINATE;
2008 	
2009 	   globalinfeasible = FALSE;
2010 	
2011 	   /* start dual proof analysis */
2012 	   if( ((set->conf_useinflp == 'b' || set->conf_useinflp == 'd') && conflict->conflictset->conflicttype == SCIP_CONFTYPE_INFEASLP)
2013 	      || ((set->conf_useboundlp == 'b' || set->conf_useboundlp == 'd') && conflict->conflictset->conflicttype == SCIP_CONFTYPE_BNDEXCEEDING) )
2014 	   {
2015 	      /* start dual proof analysis */
2016 	      SCIP_CALL( SCIPconflictAnalyzeDualProof(conflict, set, stat, blkmem, origprob, transprob, tree, reopt, lp, farkasrow, \
2017 	         validdepth, curvarlbs, curvarubs, TRUE, &globalinfeasible, dualproofsuccess) );
2018 	   }
2019 	
2020 	   assert(valid);
2021 	
2022 	   /* todo: in theory, we could apply conflict graph analysis for locally valid proofs, too, but this needs to be implemented */
2023 	   if( !globalinfeasible && validdepth <= SCIPtreeGetEffectiveRootDepth(tree)
2024 	      && (((set->conf_useinflp == 'b' || set->conf_useinflp == 'c') && conflict->conflictset->conflicttype == SCIP_CONFTYPE_INFEASLP)
2025 	      || ((set->conf_useboundlp == 'b' || set->conf_useboundlp == 'c') && conflict->conflictset->conflicttype == SCIP_CONFTYPE_BNDEXCEEDING)) )
2026 	   {
2027 	      SCIP_Real* farkascoefs;
2028 	      SCIP_Real farkaslhs;
2029 	      int* inds;
2030 	      int nnz;
2031 	
2032 	#ifdef SCIP_DEBUG
2033 	      {
2034 	         SCIP_Real objlim;
2035 	         SCIPsetDebugMsg(set, "analyzing conflict on infeasible LP (infeasible: %u, objlimexc: %u, optimal:%u) in depth %d (diving: %u)\n",
2036 	               SCIPlpiIsPrimalInfeasible(lpi), SCIPlpiIsObjlimExc(lpi), SCIPlpiIsOptimal(lpi), SCIPtreeGetCurrentDepth(tree), diving);
2037 	
2038 	         SCIP_CALL( SCIPlpiGetRealpar(lpi, SCIP_LPPAR_OBJLIM, &objlim) );
2039 	         SCIPsetDebugMsg(set, " -> objective limit in LP solver: %g (in LP: %g)\n", objlim, lp->lpiobjlim);
2040 	      }
2041 	#endif
2042 	
2043 	      SCIP_CALL( SCIPsetAllocBufferArray(set, &farkascoefs, SCIPprobGetNVars(transprob)) );
2044 	      BMSclearMemoryArray(farkascoefs, SCIPprobGetNVars(transprob));
2045 	
2046 	      farkaslhs = -SCIPaggrRowGetRhs(farkasrow);
2047 	      farkasactivity = -farkasactivity;
2048 	
2049 	      inds = SCIPaggrRowGetInds(farkasrow);
2050 	      nnz = SCIPaggrRowGetNNz(farkasrow);
2051 	
2052 	      for( v = 0; v < nnz; v++ )
2053 	      {
2054 	         int i = inds[v];
2055 	
2056 	         assert(SCIPvarGetProbindex(vars[i]) == inds[v]);
2057 	
2058 	         farkascoefs[i] = -SCIPaggrRowGetProbvarValue(farkasrow, i);
2059 	      }
2060 	
2061 	      SCIP_CALL( SCIPrunBoundHeuristic(conflict, set, stat, origprob, transprob, tree, reopt, lp, lpi, blkmem, farkascoefs,
2062 	            &farkaslhs, &farkasactivity, curvarlbs, curvarubs, lbchginfoposs, ubchginfoposs, iterations, marklpunsolved,
2063 	            dualproofsuccess, &valid) );
2064 	
2065 	      SCIPsetFreeBufferArray(set, &farkascoefs);
2066 	
2067 	      if( !valid )
2068 	         goto FLUSHPROOFSETS;
2069 	
2070 	      /* analyze the conflict starting with remaining bound changes */
2071 	      SCIP_CALL( SCIPconflictAnalyzeRemainingBdchgs(conflict, blkmem, set, stat, transprob, tree, diving, \
2072 	            lbchginfoposs, ubchginfoposs, nconss, nliterals, nreconvconss, nreconvliterals) );
2073 	
2074 	      /* flush conflict set storage */
2075 	      SCIP_CALL( SCIPconflictFlushConss(conflict, blkmem, set, stat, transprob, origprob, tree, reopt, lp, branchcand, \
2076 	            eventqueue, cliquetable) );
2077 	   }
2078 	
2079 	  FLUSHPROOFSETS:
2080 	   /* flush proof set */
2081 	   if( SCIPproofsetGetNVars(conflict->proofset) > 0 || conflict->nproofsets > 0 )
2082 	   {
2083 	      SCIP_CALL( SCIPconflictFlushProofset(conflict, conflictstore, blkmem, set, stat, transprob, origprob, tree, reopt, lp, \
2084 	            branchcand, eventqueue, cliquetable) );
2085 	   }
2086 	
2087 	  TERMINATE:
2088 	   SCIPsetFreeBufferArray(set, &curvarubs);
2089 	   SCIPsetFreeBufferArray(set, &curvarlbs);
2090 	   SCIPsetFreeBufferArray(set, &ubchginfoposs);
2091 	   SCIPsetFreeBufferArray(set, &lbchginfoposs);
2092 	   SCIPaggrRowFree(set->scip, &farkasrow);
2093 	
2094 	   return SCIP_OKAY;
2095 	}
2096 	
2097 	
2098 	/*
2099 	 * infeasible strong branching conflict analysis
2100 	 */
2101 	
2102 	/** analyses infeasible strong branching sub problems for conflicts */
2103 	SCIP_RETCODE SCIPconflictAnalyzeStrongbranch(
2104 	   SCIP_CONFLICT*        conflict,           /**< conflict analysis data */
2105 	   SCIP_CONFLICTSTORE*   conflictstore,      /**< conflict store */
2106 	   BMS_BLKMEM*           blkmem,             /**< block memory buffers */
2107 	   SCIP_SET*             set,                /**< global SCIP settings */
2108 	   SCIP_STAT*            stat,               /**< dynamic problem statistics */
2109 	   SCIP_PROB*            transprob,          /**< transformed problem */
2110 	   SCIP_PROB*            origprob,           /**< original problem */
2111 	   SCIP_TREE*            tree,               /**< branch and bound tree */
2112 	   SCIP_REOPT*           reopt,              /**< reoptimization data structure */
2113 	   SCIP_LP*              lp,                 /**< LP data */
2114 	   SCIP_BRANCHCAND*      branchcand,         /**< branching candidate storage */
2115 	   SCIP_EVENTQUEUE*      eventqueue,         /**< event queue */
2116 	   SCIP_CLIQUETABLE*     cliquetable,        /**< clique table data structure */
2117 	   SCIP_COL*             col,                /**< LP column with at least one infeasible strong branching subproblem */
2118 	   SCIP_Bool*            downconflict,       /**< pointer to store whether a conflict constraint was created for an
2119 	                                              *   infeasible downwards branch, or NULL */
2120 	   SCIP_Bool*            upconflict          /**< pointer to store whether a conflict constraint was created for an
2121 	                                              *   infeasible upwards branch, or NULL */
2122 	   )
2123 	{
2124 	   int* cstat;
2125 	   int* rstat;
2126 	   SCIP_RETCODE retcode;
2127 	   SCIP_Bool resolve;
2128 	   SCIP_Real oldlb;
2129 	   SCIP_Real oldub;
2130 	   SCIP_Real newlb;
2131 	   SCIP_Real newub;
2132 	   SCIP_Bool dualraysuccess;
2133 	   int iter;
2134 	   int nconss;
2135 	   int nliterals;
2136 	   int nreconvconss;
2137 	   int nreconvliterals;
2138 	
2139 	   assert(stat != NULL);
2140 	   assert(lp != NULL);
2141 	   assert(lp->flushed);
2142 	   assert(lp->solved);
2143 	   assert(SCIPprobAllColsInLP(transprob, set, lp)); /* LP conflict analysis is only valid, if all variables are known */
2144 	   assert(col != NULL);
2145 	   assert((col->sbdownvalid && SCIPsetIsGE(set, col->sbdown, lp->cutoffbound)
2146 	         && SCIPsetFeasCeil(set, col->primsol-1.0) >= col->lb - 0.5)
2147 	      || (col->sbupvalid && SCIPsetIsGE(set, col->sbup, lp->cutoffbound)
2148 	         && SCIPsetFeasFloor(set, col->primsol+1.0) <= col->ub + 0.5));
2149 	   assert(SCIPtreeGetCurrentDepth(tree) > 0);
2150 	
2151 	   if( downconflict != NULL )
2152 	      *downconflict = FALSE;
2153 	   if( upconflict != NULL )
2154 	      *upconflict = FALSE;
2155 	
2156 	   /* check, if infeasible LP conflict analysis is enabled */
2157 	   if( !set->conf_enable || !set->conf_usesb )
2158 	      return SCIP_OKAY;
2159 	
2160 	   /* check, if there are any conflict handlers to use a conflict set */
2161 	   if( set->nconflicthdlrs == 0 )
2162 	      return SCIP_OKAY;
2163 	
2164 	   /* inform the LPI that strong branch is (temporarily) finished */
2165 	   SCIP_CALL( SCIPlpiEndStrongbranch(lp->lpi) );
2166 	
2167 	   /* start timing */
2168 	   SCIPclockStart(conflict->sbanalyzetime, set);
2169 	
2170 	   /* get temporary memory for storing current LP basis */
2171 	   SCIP_CALL( SCIPsetAllocBufferArray(set, &cstat, lp->nlpicols) );
2172 	   SCIP_CALL( SCIPsetAllocBufferArray(set, &rstat, lp->nlpirows) );
2173 	
2174 	   /* get current LP basis */
2175 	   SCIP_CALL( SCIPlpiGetBase(lp->lpi, cstat, rstat) );
2176 	
2177 	   /* remember old bounds */
2178 	   oldlb = col->lb;
2179 	   oldub = col->ub;
2180 	
2181 	   resolve = FALSE;
2182 	
2183 	   /* is down branch infeasible? */
2184 	   if( col->sbdownvalid && SCIPsetIsGE(set, col->sbdown, lp->cutoffbound) )
2185 	   {
2186 	      newub = SCIPsetFeasCeil(set, col->primsol-1.0);
2187 	      if( newub >= col->lb - 0.5 )
2188 	      {
2189 	         SCIPsetDebugMsg(set, "analyzing conflict on infeasible downwards strongbranch for variable <%s>[%g,%g] in depth %d\n",
2190 	            SCIPvarGetName(SCIPcolGetVar(col)), SCIPvarGetLbLocal(SCIPcolGetVar(col)), SCIPvarGetUbLocal(SCIPcolGetVar(col)),
2191 	            SCIPtreeGetCurrentDepth(tree));
2192 	
2193 	         conflict->conflictset->conflicttype = SCIP_CONFTYPE_INFEASLP;
2194 	         conflict->nsbcalls++;
2195 	
2196 	         /* change the upper bound */
2197 	         col->ub = newub;
2198 	         SCIP_CALL( SCIPlpiChgBounds(lp->lpi, 1, &col->lpipos, &col->lb, &col->ub) );
2199 	
2200 	         /* start LP timer */
2201 	         SCIPclockStart(stat->conflictlptime, set);
2202 	
2203 	         /* resolve the LP */
2204 	         retcode = SCIPlpiSolveDual(lp->lpi);
2205 	
2206 	         /* stop LP timer */
2207 	         SCIPclockStop(stat->conflictlptime, set);
2208 	
2209 	         /* check return code of LP solving call */
2210 	         if( retcode != SCIP_LPERROR )
2211 	         {
2212 	            SCIP_CALL( retcode );
2213 	
2214 	            /* count number of LP iterations */
2215 	            SCIP_CALL( SCIPlpiGetIterations(lp->lpi, &iter) );
2216 	            stat->nconflictlps++;
2217 	            stat->nconflictlpiterations += iter;
2218 	            conflict->nsbiterations += iter;
2219 	            SCIPsetDebugMsg(set, " -> resolved downwards strong branching LP in %d iterations\n", iter);
2220 	
2221 	            /* perform conflict analysis on infeasible LP; last parameter guarantees status 'solved' on return */
2222 	            SCIP_CALL( conflictAnalyzeLP(conflict, conflictstore, blkmem, set, stat, transprob, origprob, tree, reopt, \
2223 	                  lp, branchcand, eventqueue, cliquetable, TRUE, &dualraysuccess, &iter, &nconss, &nliterals, \
2224 	                  &nreconvconss, &nreconvliterals, FALSE) );
2225 	            conflict->nsbsuccess += ((nconss > 0 || dualraysuccess) ? 1 : 0);
2226 	            conflict->nsbiterations += iter;
2227 	            conflict->nsbconfconss += nconss;
2228 	            conflict->nsbconfliterals += nliterals;
2229 	            conflict->nsbreconvconss += nreconvconss;
2230 	            conflict->nsbreconvliterals += nreconvliterals;
2231 	            if( downconflict != NULL )
2232 	               *downconflict = (nconss > 0);
2233 	         }
2234 	
2235 	         /* reset the upper bound */
2236 	         col->ub = oldub;
2237 	         SCIP_CALL( SCIPlpiChgBounds(lp->lpi, 1, &col->lpipos, &col->lb, &col->ub) );
2238 	
2239 	         /* reset LP basis */
2240 	         SCIP_CALL( SCIPlpiSetBase(lp->lpi, cstat, rstat) );
2241 	
2242 	         /* mark the LP to be resolved at the end */
2243 	         resolve = TRUE;
2244 	      }
2245 	   }
2246 	
2247 	   /* is up branch infeasible? */
2248 	   if( col->sbupvalid && SCIPsetIsGE(set, col->sbup, lp->cutoffbound) )
2249 	   {
2250 	      newlb = SCIPsetFeasFloor(set, col->primsol+1.0);
2251 	      if( newlb <= col->ub + 0.5 )
2252 	      {
2253 	         SCIPsetDebugMsg(set, "analyzing conflict on infeasible upwards strongbranch for variable <%s>[%g,%g] in depth %d\n",
2254 	            SCIPvarGetName(SCIPcolGetVar(col)), SCIPvarGetLbLocal(SCIPcolGetVar(col)), SCIPvarGetUbLocal(SCIPcolGetVar(col)),
2255 	            SCIPtreeGetCurrentDepth(tree));
2256 	
2257 	         conflict->conflictset->conflicttype = SCIP_CONFTYPE_INFEASLP;
2258 	         conflict->nsbcalls++;
2259 	
2260 	         /* change the lower bound */
2261 	         col->lb = newlb;
2262 	         SCIP_CALL( SCIPlpiChgBounds(lp->lpi, 1, &col->lpipos, &col->lb, &col->ub) );
2263 	
2264 	         /* start LP timer */
2265 	         SCIPclockStart(stat->conflictlptime, set);
2266 	
2267 	         /* resolve the LP */
2268 	         retcode = SCIPlpiSolveDual(lp->lpi);
2269 	
2270 	         /* stop LP timer */
2271 	         SCIPclockStop(stat->conflictlptime, set);
2272 	
2273 	         /* check return code of LP solving call */
2274 	         if( retcode != SCIP_LPERROR )
2275 	         {
2276 	            SCIP_CALL( retcode );
2277 	
2278 	            /* count number of LP iterations */
2279 	            SCIP_CALL( SCIPlpiGetIterations(lp->lpi, &iter) );
2280 	            stat->nconflictlps++;
2281 	            stat->nconflictlpiterations += iter;
2282 	            conflict->nsbiterations += iter;
2283 	            SCIPsetDebugMsg(set, " -> resolved upwards strong branching LP in %d iterations\n", iter);
2284 	
2285 	            /* perform conflict analysis on infeasible LP; last parameter guarantees status 'solved' on return */
2286 	            SCIP_CALL( conflictAnalyzeLP(conflict, conflictstore, blkmem, set, stat, transprob, origprob, tree, reopt, \
2287 	                  lp, branchcand, eventqueue, cliquetable, TRUE, &dualraysuccess, &iter, &nconss, &nliterals, \
2288 	                  &nreconvconss, &nreconvliterals, FALSE) );
2289 	            conflict->nsbsuccess += ((nconss > 0 || dualraysuccess) ? 1 : 0);
2290 	            conflict->nsbiterations += iter;
2291 	            conflict->nsbconfconss += nconss;
2292 	            conflict->nsbconfliterals += nliterals;
2293 	            conflict->nsbreconvconss += nreconvconss;
2294 	            conflict->nsbreconvliterals += nreconvliterals;
2295 	            if( upconflict != NULL )
2296 	               *upconflict = (nconss > 0);
2297 	         }
2298 	
2299 	         /* reset the lower bound */
2300 	         col->lb = oldlb;
2301 	         SCIP_CALL( SCIPlpiChgBounds(lp->lpi, 1, &col->lpipos, &col->lb, &col->ub) );
2302 	
2303 	         /* reset LP basis */
2304 	         SCIP_CALL( SCIPlpiSetBase(lp->lpi, cstat, rstat) );
2305 	
2306 	         /* mark the LP to be resolved at the end */
2307 	         resolve = TRUE;
2308 	      }
2309 	   }
2310 	
2311 	   /* free temporary memory for storing current LP basis */
2312 	   SCIPsetFreeBufferArray(set, &rstat);
2313 	   SCIPsetFreeBufferArray(set, &cstat);
2314 	
2315 	   assert(lp->flushed);
2316 	
2317 	   /* resolve LP if something has changed in order to synchronize LPI and LP */
2318 	   if ( resolve )
2319 	   {
2320 	      /* start LP timer */
2321 	      SCIPclockStart(stat->conflictlptime, set);
2322 	
2323 	      /* resolve the LP */
2324 	      SCIP_CALL( SCIPlpiSolveDual(lp->lpi) );
2325 	
2326 	      /* stop LP timer */
2327 	      SCIPclockStop(stat->conflictlptime, set);
2328 	   }
2329 	
2330 	   /* stop timing */
2331 	   SCIPclockStop(conflict->sbanalyzetime, set);
2332 	
2333 	   /* inform the LPI that strong branch starts (again) */
2334 	   SCIP_CALL( SCIPlpiStartStrongbranch(lp->lpi) );
2335 	
2336 	   return SCIP_OKAY;
2337 	}
2338 	
2339 	/** analyzes an infeasible LP to find out the bound changes on variables that were responsible for the infeasibility;
2340 	 *  on success, calls standard conflict analysis with the responsible variables as starting conflict set, thus creating
2341 	 *  a conflict constraint out of the resulting conflict set;
2342 	 *  updates statistics for infeasible LP conflict analysis
2343 	 */
2344 	static
2345 	SCIP_RETCODE conflictAnalyzeInfeasibleLP(
2346 	   SCIP_CONFLICT*        conflict,           /**< conflict analysis data */
2347 	   SCIP_CONFLICTSTORE*   conflictstore,      /**< conflict store */
2348 	   BMS_BLKMEM*           blkmem,             /**< block memory of transformed problem */
2349 	   SCIP_SET*             set,                /**< global SCIP settings */
2350 	   SCIP_STAT*            stat,               /**< problem statistics */
2351 	   SCIP_PROB*            transprob,          /**< transformed problem */
2352 	   SCIP_PROB*            origprob,           /**< original problem */
2353 	   SCIP_TREE*            tree,               /**< branch and bound tree */
2354 	   SCIP_REOPT*           reopt,              /**< reoptimization data structure */
2355 	   SCIP_LP*              lp,                 /**< LP data */
2356 	   SCIP_BRANCHCAND*      branchcand,         /**< branching candidate storage */
2357 	   SCIP_EVENTQUEUE*      eventqueue,         /**< event queue */
2358 	   SCIP_CLIQUETABLE*     cliquetable,        /**< clique table data structure */
2359 	   SCIP_Bool*            success             /**< pointer to store whether a conflict constraint was created, or NULL */
2360 	   )
2361 	{
2362 	   SCIP_Bool dualraysuccess = FALSE;
2363 	   SCIP_Longint olddualproofsuccess;
2364 	   int iterations;
2365 	   int nconss;
2366 	   int nliterals;
2367 	   int nreconvconss;
2368 	   int nreconvliterals;
2369 	
2370 	   assert(conflict != NULL);
2371 	   assert(set != NULL);
2372 	   assert(lp != NULL);
2373 	   assert(SCIPprobAllColsInLP(transprob, set, lp)); /* LP conflict analysis is only valid, if all variables are known */
2374 	
2375 	   assert(success == NULL || *success == FALSE);
2376 	
2377 	   /* check, if infeasible LP conflict analysis is enabled */
2378 	   if( !set->conf_enable || set->conf_useinflp == 'o' )
2379 	      return SCIP_OKAY;
2380 	
2381 	   /* check, if there are any conflict handlers to use a conflict set */
2382 	   if( set->nconflicthdlrs == 0 )
2383 	      return SCIP_OKAY;
2384 	
2385 	   SCIPsetDebugMsg(set, "analyzing conflict on infeasible LP in depth %d (solstat: %d, objchanged: %u)\n",
2386 	      SCIPtreeGetCurrentDepth(tree), SCIPlpGetSolstat(lp), SCIPlpDivingObjChanged(lp));
2387 	
2388 	   /* start timing */
2389 	   SCIPclockStart(conflict->inflpanalyzetime, set);
2390 	   conflict->ninflpcalls++;
2391 	
2392 	   conflict->conflictset->conflicttype = SCIP_CONFTYPE_INFEASLP;
2393 	
2394 	   olddualproofsuccess = conflict->ndualproofsinfsuccess;
2395 	
2396 	   /* perform conflict analysis */
2397 	   SCIP_CALL( conflictAnalyzeLP(conflict, conflictstore, blkmem, set, stat, transprob, origprob, tree, reopt, lp, branchcand, eventqueue, \
2398 	         cliquetable, SCIPlpDiving(lp), &dualraysuccess, &iterations, &nconss, &nliterals, &nreconvconss, &nreconvliterals, TRUE) );
2399 	   conflict->ninflpsuccess += ((nconss > 0 || conflict->ndualproofsinfsuccess > olddualproofsuccess) ? 1 : 0);
2400 	   conflict->ninflpiterations += iterations;
2401 	   conflict->ninflpconfconss += nconss;
2402 	   conflict->ninflpconfliterals += nliterals;
2403 	   conflict->ninflpreconvconss += nreconvconss;
2404 	   conflict->ninflpreconvliterals += nreconvliterals;
2405 	   if( success != NULL )
2406 	      *success = (nconss > 0 || conflict->ndualproofsinfsuccess > olddualproofsuccess);
2407 	
2408 	   /* stop timing */
2409 	   SCIPclockStop(conflict->inflpanalyzetime, set);
2410 	
2411 	   return SCIP_OKAY;
2412 	}
2413 	
2414 	/** analyzes a bound exceeding LP to find out the bound changes on variables that were responsible for exceeding the
2415 	 *  primal bound;
2416 	 *  on success, calls standard conflict analysis with the responsible variables as starting conflict set, thus creating
2417 	 *  a conflict constraint out of the resulting conflict set;
2418 	 *  updates statistics for bound exceeding LP conflict analysis
2419 	 */
2420 	static
2421 	SCIP_RETCODE conflictAnalyzeBoundexceedingLP(
2422 	   SCIP_CONFLICT*        conflict,           /**< conflict analysis data */
2423 	   SCIP_CONFLICTSTORE*   conflictstore,      /**< conflict store */
2424 	   BMS_BLKMEM*           blkmem,             /**< block memory of transformed problem */
2425 	   SCIP_SET*             set,                /**< global SCIP settings */
2426 	   SCIP_STAT*            stat,               /**< problem statistics */
2427 	   SCIP_PROB*            transprob,          /**< transformed problem */
2428 	   SCIP_PROB*            origprob,           /**< original problem */
2429 	   SCIP_TREE*            tree,               /**< branch and bound tree */
2430 	   SCIP_REOPT*           reopt,              /**< reoptimization data structure */
2431 	   SCIP_LP*              lp,                 /**< LP data */
2432 	   SCIP_BRANCHCAND*      branchcand,         /**< branching candidate storage */
2433 	   SCIP_EVENTQUEUE*      eventqueue,         /**< event queue */
2434 	   SCIP_CLIQUETABLE*     cliquetable,        /**< clique table data structure */
2435 	   SCIP_Bool*            success             /**< pointer to store whether a conflict constraint was created, or NULL */
2436 	   )
2437 	{
2438 	   SCIP_Bool dualraysuccess;
2439 	   SCIP_Longint oldnsuccess;
2440 	   int iterations;
2441 	   int nconss;
2442 	   int nliterals;
2443 	   int nreconvconss;
2444 	   int nreconvliterals;
2445 	
2446 	   assert(conflict != NULL);
2447 	   assert(set != NULL);
2448 	   assert(lp != NULL);
2449 	   assert(!SCIPlpDivingObjChanged(lp));
2450 	   assert(SCIPprobAllColsInLP(transprob, set, lp)); /* LP conflict analysis is only valid, if all variables are known */
2451 	
2452 	   assert(success == NULL || *success == FALSE);
2453 	
2454 	   /* check, if bound exceeding LP conflict analysis is enabled */
2455 	   if( !set->conf_enable || set->conf_useboundlp == 'o')
2456 	      return SCIP_OKAY;
2457 	
2458 	   /* check, if there are any conflict handlers to use a conflict set */
2459 	   if( set->nconflicthdlrs == 0 )
2460 	      return SCIP_OKAY;
2461 	
2462 	   SCIPsetDebugMsg(set, "analyzing conflict on bound exceeding LP in depth %d (solstat: %d)\n",
2463 	      SCIPtreeGetCurrentDepth(tree), SCIPlpGetSolstat(lp));
2464 	
2465 	   /* start timing */
2466 	   SCIPclockStart(conflict->boundlpanalyzetime, set);
2467 	   conflict->nboundlpcalls++;
2468 	
2469 	   /* mark the conflict to depend on the cutoff bound */
2470 	   conflict->conflictset->conflicttype = SCIP_CONFTYPE_BNDEXCEEDING;
2471 	   conflict->conflictset->usescutoffbound = TRUE;
2472 	
2473 	   oldnsuccess = conflict->ndualproofsbndsuccess + conflict->ndualproofsinfsuccess;
2474 	
2475 	   /* perform conflict analysis */
2476 	   SCIP_CALL( conflictAnalyzeLP(conflict, conflictstore, blkmem, set, stat, transprob, origprob, tree, reopt, lp, branchcand, eventqueue, \
2477 	         cliquetable, SCIPlpDiving(lp), &dualraysuccess, &iterations, &nconss, &nliterals, &nreconvconss, &nreconvliterals, TRUE) );
2478 	   conflict->nboundlpsuccess += ((nconss > 0 || conflict->ndualproofsbndsuccess + conflict->ndualproofsinfsuccess > oldnsuccess) ? 1 : 0);
2479 	   conflict->nboundlpiterations += iterations;
2480 	   conflict->nboundlpconfconss += nconss;
2481 	   conflict->nboundlpconfliterals += nliterals;
2482 	   conflict->nboundlpreconvconss += nreconvconss;
2483 	   conflict->nboundlpreconvliterals += nreconvliterals;
2484 	   if( success != NULL )
2485 	      *success = (nconss > 0 || conflict->ndualproofsbndsuccess + conflict->ndualproofsinfsuccess > oldnsuccess);
2486 	
2487 	   /* stop timing */
2488 	   SCIPclockStop(conflict->boundlpanalyzetime, set);
2489 	
2490 	   return SCIP_OKAY;
2491 	}
2492 	
2493 	/** analyzes an infeasible or bound exceeding LP to find out the bound changes on variables that were responsible for the
2494 	 *  infeasibility or for exceeding the primal bound;
2495 	 *  on success, calls standard conflict analysis with the responsible variables as starting conflict set, thus creating
2496 	 *  a conflict constraint out of the resulting conflict set;
2497 	 *  updates statistics for infeasible or bound exceeding LP conflict analysis;
2498 	 *  may only be called if SCIPprobAllColsInLP()
2499 	 */
2500 	SCIP_RETCODE SCIPconflictAnalyzeLP(
2501 	   SCIP_CONFLICT*        conflict,           /**< conflict analysis data */
2502 	   SCIP_CONFLICTSTORE*   conflictstore,      /**< conflict store */
2503 	   BMS_BLKMEM*           blkmem,             /**< block memory of transformed problem */
2504 	   SCIP_SET*             set,                /**< global SCIP settings */
2505 	   SCIP_STAT*            stat,               /**< problem statistics */
2506 	   SCIP_PROB*            transprob,          /**< transformed problem */
2507 	   SCIP_PROB*            origprob,           /**< original problem */
2508 	   SCIP_TREE*            tree,               /**< branch and bound tree */
2509 	   SCIP_REOPT*           reopt,              /**< reoptimization data structure */
2510 	   SCIP_LP*              lp,                 /**< LP data */
2511 	   SCIP_BRANCHCAND*      branchcand,         /**< branching candidate storage */
2512 	   SCIP_EVENTQUEUE*      eventqueue,         /**< event queue */
2513 	   SCIP_CLIQUETABLE*     cliquetable,        /**< clique table data structure */
2514 	   SCIP_Bool*            success             /**< pointer to store whether a conflict constraint was created, or NULL */
2515 	   )
2516 	{
2517 	   SCIP_LPSOLVALS storedsolvals;
2518 	   SCIP_COLSOLVALS* storedcolsolvals;
2519 	   SCIP_ROWSOLVALS* storedrowsolvals;
2520 	   int c;
2521 	   int r;
2522 	
2523 	   if( success != NULL )
2524 	      *success = FALSE;
2525 	
2526 	   /* check if the conflict analysis is applicable */
2527 	   if( !set->conf_enable || (set->conf_useinflp == 'o' && set->conf_useboundlp == 'o') )
2528 	      return SCIP_OKAY;
2529 	
2530 	   /* in rare cases, it might happen that the solution stati of the LP and the LPI are out of sync; in particular this
2531 	    * happens when a new incumbent which cuts off the current node is found during the LP solving loop; in this case the
2532 	    * LP has status objlimit, but if diving has been used, the LPI only has the basis information, but is not solved
2533 	    *
2534 	    * @todo: alternatively, solve the LPI
2535 	    */
2536 	   if( !SCIPlpiWasSolved(SCIPlpGetLPI(lp)) )
2537 	      return SCIP_OKAY;
2538 	
2539 	   /* LP conflict analysis is only valid, if all variables are known */
2540 	   assert( SCIPprobAllColsInLP(transprob, set, lp) );
2541 	   assert( SCIPlpGetSolstat(lp) == SCIP_LPSOLSTAT_INFEASIBLE || SCIPlpGetSolstat(lp) == SCIP_LPSOLSTAT_OBJLIMIT
2542 	      || (SCIPlpGetSolstat(lp) == SCIP_LPSOLSTAT_OPTIMAL && set->lp_disablecutoff == 1) );
2543 	
2544 	   /* save status */
2545 	   storedsolvals.lpsolstat = lp->lpsolstat;
2546 	   storedsolvals.lpobjval = lp->lpobjval;
2547 	   storedsolvals.primalfeasible = lp->primalfeasible;
2548 	   storedsolvals.primalchecked = lp->primalchecked;
2549 	   storedsolvals.dualfeasible = lp->dualfeasible;
2550 	   storedsolvals.dualchecked = lp->dualchecked;
2551 	   storedsolvals.solisbasic = lp->solisbasic;
2552 	   storedsolvals.lpissolved = lp->solved;
2553 	
2554 	   /* store solution values */
2555 	   SCIP_CALL( SCIPsetAllocBufferArray(set, &storedcolsolvals, lp->ncols) );
2556 	   SCIP_CALL( SCIPsetAllocBufferArray(set, &storedrowsolvals, lp->nrows) );
2557 	   for (c = 0; c < lp->ncols; ++c)
2558 	   {
2559 	      SCIP_COL* col;
2560 	
2561 	      col = lp->cols[c];
2562 	      assert( col != NULL );
2563 	
2564 	      storedcolsolvals[c].primsol = col->primsol;
2565 	      storedcolsolvals[c].redcost = col->redcost;
2566 	      storedcolsolvals[c].basisstatus = col->basisstatus; /*lint !e641 !e732*/
2567 	   }
2568 	   for (r = 0; r < lp->nrows; ++r)
2569 	   {
2570 	      SCIP_ROW* row;
2571 	
2572 	      row = lp->rows[r];
2573 	      assert( row != NULL );
2574 	
2575 	      if ( lp->lpsolstat == SCIP_LPSOLSTAT_INFEASIBLE )
2576 	         storedrowsolvals[r].dualsol = row->dualfarkas;
2577 	      else
2578 	      {
2579 	         assert( lp->lpsolstat == SCIP_LPSOLSTAT_OBJLIMIT ||
2580 	            (SCIPlpGetSolstat(lp) == SCIP_LPSOLSTAT_OPTIMAL && set->lp_disablecutoff == 1) );
2581 	         storedrowsolvals[r].dualsol = row->dualsol;
2582 	      }
2583 	      storedrowsolvals[r].activity = row->activity;
2584 	      storedrowsolvals[r].basisstatus = row->basisstatus; /*lint !e641 !e732*/
2585 	   }
2586 	
2587 	   /* check, if the LP was infeasible or bound exceeding */
2588 	   if( SCIPlpiIsPrimalInfeasible(SCIPlpGetLPI(lp)) )
2589 	   {
2590 	      SCIP_CALL( conflictAnalyzeInfeasibleLP(conflict, conflictstore, blkmem, set, stat, transprob, origprob, tree, \
2591 	            reopt, lp, branchcand, eventqueue, cliquetable, success) );
2592 	   }
2593 	   else
2594 	   {
2595 	      SCIP_CALL( conflictAnalyzeBoundexceedingLP(conflict, conflictstore, blkmem, set, stat, transprob, origprob, tree, \
2596 	            reopt, lp, branchcand, eventqueue, cliquetable, success) );
2597 	   }
2598 	
2599 	   /* possibly restore solution values */
2600 	   if( lp->flushed && SCIPlpGetSolstat(lp) == SCIP_LPSOLSTAT_NOTSOLVED )
2601 	   {
2602 	      /* restore status */
2603 	      lp->lpsolstat = storedsolvals.lpsolstat;
2604 	      lp->lpobjval = storedsolvals.lpobjval;
2605 	      lp->primalfeasible = storedsolvals.primalfeasible;
2606 	      lp->primalchecked = storedsolvals.primalchecked;
2607 	      lp->dualfeasible = storedsolvals.dualfeasible;
2608 	      lp->dualchecked = storedsolvals.dualchecked;
2609 	      lp->solisbasic = storedsolvals.solisbasic;
2610 	      lp->solved = storedsolvals.lpissolved;
2611 	
2612 	      for (c = 0; c < lp->ncols; ++c)
2613 	      {
2614 	         SCIP_COL* col;
2615 	
2616 	         col = lp->cols[c];
2617 	         assert( col != NULL );
2618 	         col->primsol = storedcolsolvals[c].primsol;
2619 	         col->redcost = storedcolsolvals[c].redcost;
2620 	         col->basisstatus = storedcolsolvals[c].basisstatus; /*lint !e641 !e732*/
2621 	      }
2622 	      for (r = 0; r < lp->nrows; ++r)
2623 	      {
2624 	         SCIP_ROW* row;
2625 	
2626 	         row = lp->rows[r];
2627 	         assert( row != NULL );
2628 	
2629 	         if ( lp->lpsolstat == SCIP_LPSOLSTAT_INFEASIBLE )
2630 	            row->dualfarkas = storedrowsolvals[r].dualsol;
2631 	         else
2632 	         {
2633 	            assert( lp->lpsolstat == SCIP_LPSOLSTAT_OBJLIMIT );
2634 	            row->dualsol = storedrowsolvals[r].dualsol;
2635 	         }
2636 	         row->activity = storedrowsolvals[r].activity;
2637 	         row->basisstatus = storedrowsolvals[r].basisstatus; /*lint !e641 !e732*/
2638 	      }
2639 	   }
2640 	   SCIPsetFreeBufferArray(set, &storedrowsolvals);
2641 	   SCIPsetFreeBufferArray(set, &storedcolsolvals);
2642 	
2643 	   return SCIP_OKAY;
2644 	}
2645