1    	/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
2    	/*                                                                           */
3    	/*                  This file is part of the program and library             */
4    	/*         SCIP --- Solving Constraint Integer Programs                      */
5    	/*                                                                           */
6    	/*    Copyright (C) 2002-2022 Konrad-Zuse-Zentrum                            */
7    	/*                            fuer Informationstechnik Berlin                */
8    	/*                                                                           */
9    	/*  SCIP is distributed under the terms of the ZIB Academic License.         */
10   	/*                                                                           */
11   	/*  You should have received a copy of the ZIB Academic License              */
12   	/*  along with SCIP; see the file COPYING. If not visit scipopt.org.         */
13   	/*                                                                           */
14   	/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
15   	
16   	/**@file   conflict_graphanalysis.h
17   	 * @ingroup OTHER_CFILES
18   	 * @brief  methods and datastructures for conflict analysis
19   	 * @author Tobias Achterberg
20   	 * @author Timo Berthold
21   	 * @author Stefan Heinz
22   	 * @author Marc Pfetsch
23   	 * @author Michael Winkler
24   	 * @author Jakob Witzig
25   	 *
26   	 * This file implements a conflict analysis method like the one used in modern
27   	 * SAT solvers like zchaff. The algorithm works as follows:
28   	 *
29   	 * Given is a set of bound changes that are not allowed being applied simultaneously, because they
30   	 * render the current node infeasible (e.g. because a single constraint is infeasible in the these
31   	 * bounds, or because the LP relaxation is infeasible).  The goal is to deduce a clause on variables
32   	 * -- a conflict clause -- representing the "reason" for this conflict, i.e., the branching decisions
33   	 * or the deductions (applied e.g. in domain propagation) that lead to the conflict. This clause can
34   	 * then be added to the constraint set to help cutting off similar parts of the branch and bound
35   	 * tree, that would lead to the same conflict.  A conflict clause can also be generated, if the
36   	 * conflict was detected by a locally valid constraint. In this case, the resulting conflict clause
37   	 * is also locally valid in the same depth as the conflict detecting constraint. If all involved
38   	 * variables are binary, a linear (set covering) constraint can be generated, otherwise a bound
39   	 * disjunction constraint is generated. Details are given in
40   	 *
41   	 * Tobias Achterberg, Conflict Analysis in Mixed Integer Programming@n
42   	 * Discrete Optimization, 4, 4-20 (2007)
43   	 *
44   	 * See also @ref CONF. Here is an outline of the algorithm:
45   	 *
46   	 * -#  Put all the given bound changes to a priority queue, which is ordered,
47   	 *     such that the bound change that was applied last due to branching or deduction
48   	 *     is at the top of the queue. The variables in the queue are always active
49   	 *     problem variables. Because binary variables are preferred over general integer
50   	 *     variables, integer variables are put on the priority queue prior to the binary
51   	 *     variables. Create an empty conflict set.
52   	 * -#  Remove the top bound change b from the priority queue.
53   	 * -#  Perform the following case distinction:
54   	 *     -#  If the remaining queue is non-empty, and bound change b' (the one that is now
55   	 *         on the top of the queue) was applied at the same depth level as b, and if
56   	 *         b was a deduction with known inference reason, and if the inference constraint's
57   	 *         valid depth is smaller or equal to the conflict detecting constraint's valid
58   	 *         depth:
59   	 *          - Resolve bound change b by asking the constraint that inferred the
60   	 *            bound change to put all the bound changes on the priority queue, that
61   	 *            lead to the deduction of b.
62   	 *            Note that these bound changes have at most the same inference depth
63   	 *            level as b, and were deduced earlier than b.
64   	 *     -#  Otherwise, the bound change b was a branching decision or a deduction with
65   	 *         missing inference reason, or the inference constraint's validity is more local
66   	 *         than the one of the conflict detecting constraint.
67   	 *          - If a the bound changed corresponds to a binary variable, add it or its
68   	 *            negation to the conflict set, depending on which of them is currently fixed to
69   	 *            FALSE (i.e., the conflict set consists of literals that cannot be FALSE
70   	 *            altogether at the same time).
71   	 *          - Otherwise put the bound change into the conflict set.
72   	 *         Note that if the bound change was a branching, all deduced bound changes
73   	 *         remaining in the priority queue have smaller inference depth level than b,
74   	 *         since deductions are always applied after the branching decisions. However,
75   	 *         there is the possibility, that b was a deduction, where the inference
76   	 *         reason was not given or the inference constraint was too local.
77   	 *         With this lack of information, we must treat the deduced bound change like
78   	 *         a branching, and there may exist other deduced bound changes of the same
79   	 *         inference depth level in the priority queue.
80   	 * -#  If priority queue is non-empty, goto step 2.
81   	 * -#  The conflict set represents the conflict clause saying that at least one
82   	 *     of the conflict variables must take a different value. The conflict set is then passed
83   	 *     to the conflict handlers, that may create a corresponding constraint (e.g. a logicor
84   	 *     constraint or bound disjunction constraint) out of these conflict variables and
85   	 *     add it to the problem.
86   	 *
87   	 * If all deduced bound changes come with (global) inference information, depending on
88   	 * the conflict analyzing strategy, the resulting conflict set has the following property:
89   	 *  - 1-FirstUIP: In the depth level where the conflict was found, at most one variable
90   	 *    assigned at that level is member of the conflict set. This conflict variable is the
91   	 *    first unique implication point of its depth level (FUIP).
92   	 *  - All-FirstUIP: For each depth level, at most one variable assigned at that level is
93   	 *    member of the conflict set. This conflict variable is the first unique implication
94   	 *    point of its depth level (FUIP).
95   	 *
96   	 * The user has to do the following to get the conflict analysis running in its
97   	 * current implementation:
98   	 *  - A constraint handler or propagator supporting the conflict analysis must implement
99   	 *    the CONSRESPROP/PROPRESPROP call, that processes a bound change inference b and puts all
100  	 *    the reason bounds leading to the application of b with calls to
101  	 *    SCIPaddConflictBound() on the conflict queue (algorithm step 3.(a)).
102  	 *  - If the current bounds lead to a deduction of a bound change (e.g. in domain
103  	 *    propagation), a constraint handler should call SCIPinferVarLbCons() or
104  	 *    SCIPinferVarUbCons(), thus providing the constraint that inferred the bound change.
105  	 *    A propagator should call SCIPinferVarLbProp() or SCIPinferVarUbProp() instead,
106  	 *    thus providing a pointer to itself.
107  	 *  - If (in the current bounds) an infeasibility is detected, the constraint handler or
108  	 *    propagator should
109  	 *     1. call SCIPinitConflictAnalysis() to initialize the conflict queue,
110  	 *     2. call SCIPaddConflictBound() for each bound that lead to the conflict,
111  	 *     3. call SCIPanalyzeConflictCons() or SCIPanalyzeConflict() to analyze the conflict
112  	 *        and add an appropriate conflict constraint.
113  	 */
114  	
115  	/*---+----1----+----2----+----3----+----4----+----5----+----6----+----7----+----8----+----9----+----0----+----1----+----2*/
116  	
117  	#ifndef __SCIP_CONFLICT_GRAPHANALYSIS_H__
118  	#define __SCIP_CONFLICT_GRAPHANALYSIS_H__
119  	
120  	#include "scip/def.h"
121  	#include "scip/type_cuts.h"
122  	#include "scip/type_conflict.h"
123  	#include "scip/type_reopt.h"
124  	#include "scip/type_implics.h"
125  	#include "scip/type_set.h"
126  	#include "scip/type_stat.h"
127  	#include "scip/type_lp.h"
128  	#include "lpi/type_lpi.h"
129  	#include "scip/type_branch.h"
130  	#include "scip/type_mem.h"
131  	#include "scip/type_var.h"
132  	#include "scip/type_prob.h"
133  	#include "scip/type_event.h"
134  	#include <string.h>
135  	#if defined(_WIN32) || defined(_WIN64)
136  	#else
137  	#include <strings.h> /*lint --e{766}*/
138  	#endif
139  	
140  	#ifdef __cplusplus
141  	extern "C" {
142  	#endif
143  	
144  	/** creates an empty conflict set */
145  	SCIP_RETCODE SCIPconflictsetCreate(
146  	   SCIP_CONFLICTSET**    conflictset,        /**< pointer to store the conflict set */
147  	   BMS_BLKMEM*           blkmem              /**< block memory of transformed problem */
148  	   );
149  	
150  	/** frees a conflict set */
151  	void SCIPconflictsetFree(
152  	   SCIP_CONFLICTSET**    conflictset,        /**< pointer to the conflict set */
153  	   BMS_BLKMEM*           blkmem              /**< block memory of transformed problem */
154  	   );
155  	
156  	/** copies the given conflict handler to a new scip */
157  	SCIP_RETCODE SCIPconflicthdlrCopyInclude(
158  	   SCIP_CONFLICTHDLR*    conflicthdlr,       /**< conflict handler */
159  	   SCIP_SET*             set                 /**< SCIP_SET of SCIP to copy to */
160  	   );
161  	
162  	/** creates a conflict handler */
163  	SCIP_RETCODE SCIPconflicthdlrCreate(
164  	   SCIP_CONFLICTHDLR**   conflicthdlr,       /**< pointer to conflict handler data structure */
165  	   SCIP_SET*             set,                /**< global SCIP settings */
166  	   SCIP_MESSAGEHDLR*     messagehdlr,        /**< message handler */
167  	   BMS_BLKMEM*           blkmem,             /**< block memory for parameter settings */
168  	   const char*           name,               /**< name of conflict handler */
169  	   const char*           desc,               /**< description of conflict handler */
170  	   int                   priority,           /**< priority of the conflict handler */
171  	   SCIP_DECL_CONFLICTCOPY((*conflictcopy)),  /**< copy method of conflict handler or NULL if you don't want to copy your plugin into sub-SCIPs */
172  	   SCIP_DECL_CONFLICTFREE((*conflictfree)),  /**< destructor of conflict handler */
173  	   SCIP_DECL_CONFLICTINIT((*conflictinit)),  /**< initialize conflict handler */
174  	   SCIP_DECL_CONFLICTEXIT((*conflictexit)),  /**< deinitialize conflict handler */
175  	   SCIP_DECL_CONFLICTINITSOL((*conflictinitsol)),/**< solving process initialization method of conflict handler */
176  	   SCIP_DECL_CONFLICTEXITSOL((*conflictexitsol)),/**< solving process deinitialization method of conflict handler */
177  	   SCIP_DECL_CONFLICTEXEC((*conflictexec)),  /**< conflict processing method of conflict handler */
178  	   SCIP_CONFLICTHDLRDATA* conflicthdlrdata   /**< conflict handler data */
179  	   );
180  	
181  	/** calls destructor and frees memory of conflict handler */
182  	SCIP_RETCODE SCIPconflicthdlrFree(
183  	   SCIP_CONFLICTHDLR**   conflicthdlr,       /**< pointer to conflict handler data structure */
184  	   SCIP_SET*             set                 /**< global SCIP settings */
185  	   );
186  	
187  	/** calls init method of conflict handler */
188  	SCIP_RETCODE SCIPconflicthdlrInit(
189  	   SCIP_CONFLICTHDLR*    conflicthdlr,       /**< conflict handler */
190  	   SCIP_SET*             set                 /**< global SCIP settings */
191  	   );
192  	
193  	/** calls exit method of conflict handler */
194  	SCIP_RETCODE SCIPconflicthdlrExit(
195  	   SCIP_CONFLICTHDLR*    conflicthdlr,       /**< conflict handler */
196  	   SCIP_SET*             set                 /**< global SCIP settings */
197  	   );
198  	
199  	/** informs conflict handler that the branch and bound process is being started */
200  	SCIP_RETCODE SCIPconflicthdlrInitsol(
201  	   SCIP_CONFLICTHDLR*    conflicthdlr,       /**< conflict handler */
202  	   SCIP_SET*             set                 /**< global SCIP settings */
203  	   );
204  	
205  	/** informs conflict handler that the branch and bound process data is being freed */
206  	SCIP_RETCODE SCIPconflicthdlrExitsol(
207  	   SCIP_CONFLICTHDLR*    conflicthdlr,       /**< conflict handler */
208  	   SCIP_SET*             set                 /**< global SCIP settings */
209  	   );
210  	
211  	/** calls execution method of conflict handler */
212  	SCIP_RETCODE SCIPconflicthdlrExec(
213  	   SCIP_CONFLICTHDLR*    conflicthdlr,       /**< conflict handler */
214  	   SCIP_SET*             set,                /**< global SCIP settings */
215  	   SCIP_NODE*            node,               /**< node to add conflict constraint to */
216  	   SCIP_NODE*            validnode,          /**< node at which the constraint is valid */
217  	   SCIP_BDCHGINFO**      bdchginfos,         /**< bound change resembling the conflict set */
218  	   SCIP_Real*            relaxedbds,         /**< array with relaxed bounds which are efficient to create a valid conflict */
219  	   int                   nbdchginfos,        /**< number of bound changes in the conflict set */
220  	   SCIP_CONFTYPE         conftype,           /**< type of the conflict */
221  	   SCIP_Bool             usescutoffbound,    /**< depends the conflict on the cutoff bound? */
222  	   SCIP_Bool             resolved,           /**< was the conflict set already used to create a constraint? */
223  	   SCIP_RESULT*          result              /**< pointer to store the result of the callback method */
224  	   );
225  	
226  	/** sets priority of conflict handler */
227  	void SCIPconflicthdlrSetPriority(
228  	   SCIP_CONFLICTHDLR*    conflicthdlr,       /**< conflict handler */
229  	   SCIP_SET*             set,                /**< global SCIP settings */
230  	   int                   priority            /**< new priority of the conflict handler */
231  	   );
232  	
233  	/** set copy method of conflict handler */
234  	void SCIPconflicthdlrSetCopy(
235  	   SCIP_CONFLICTHDLR*    conflicthdlr,       /**< conflict handler */
236  	   SCIP_DECL_CONFLICTCOPY((*conflictcopy))   /**< copy method of the conflict handler */
237  	   );
238  	
239  	/** set destructor of conflict handler */
240  	void SCIPconflicthdlrSetFree(
241  	   SCIP_CONFLICTHDLR*    conflicthdlr,       /**< conflict handler */
242  	   SCIP_DECL_CONFLICTFREE((*conflictfree))   /**< destructor of conflict handler */
243  	   );
244  	
245  	/** set initialization method of conflict handler */
246  	void SCIPconflicthdlrSetInit(
247  	   SCIP_CONFLICTHDLR*    conflicthdlr,       /**< conflict handler */
248  	   SCIP_DECL_CONFLICTINIT((*conflictinit))   /**< initialization method conflict handler */
249  	   );
250  	
251  	/** set deinitialization method of conflict handler */
252  	void SCIPconflicthdlrSetExit(
253  	   SCIP_CONFLICTHDLR*    conflicthdlr,       /**< conflict handler */
254  	   SCIP_DECL_CONFLICTEXIT((*conflictexit))   /**< deinitialization method conflict handler */
255  	   );
256  	
257  	/** set solving process initialization method of conflict handler */
258  	void SCIPconflicthdlrSetInitsol(
259  	   SCIP_CONFLICTHDLR*    conflicthdlr,       /**< conflict handler */
260  	   SCIP_DECL_CONFLICTINITSOL((*conflictinitsol))/**< solving process initialization method of conflict handler */
261  	   );
262  	
263  	/** set solving process deinitialization method of conflict handler */
264  	void SCIPconflicthdlrSetExitsol(
265  	   SCIP_CONFLICTHDLR*    conflicthdlr,       /**< conflict handler */
266  	   SCIP_DECL_CONFLICTEXITSOL((*conflictexitsol))/**< solving process deinitialization method of conflict handler */
267  	   );
268  	
269  	/** enables or disables all clocks of \p conflicthdlr, depending on the value of the flag */
270  	void SCIPconflicthdlrEnableOrDisableClocks(
271  	   SCIP_CONFLICTHDLR*    conflicthdlr,       /**< the conflict handler for which all clocks should be enabled or disabled */
272  	   SCIP_Bool             enable              /**< should the clocks of the conflict handler be enabled? */
273  	   );
274  	
275  	/** return TRUE if conflict analysis is applicable; In case the function return FALSE there is no need to initialize the
276  	 *  conflict analysis since it will not be applied
277  	 */
278  	SCIP_Bool SCIPconflictApplicable(
279  	   SCIP_SET*             set                 /**< global SCIP settings */
280  	   );
281  	
282  	/** creates a temporary bound change information object that is destroyed after the conflict sets are flushed */
283  	SCIP_RETCODE conflictCreateTmpBdchginfo(
284  	   SCIP_CONFLICT*        conflict,           /**< conflict analysis data */
285  	   BMS_BLKMEM*           blkmem,             /**< block memory */
286  	   SCIP_SET*             set,                /**< global SCIP settings */
287  	   SCIP_VAR*             var,                /**< active variable that changed the bounds */
288  	   SCIP_BOUNDTYPE        boundtype,          /**< type of bound for var: lower or upper bound */
289  	   SCIP_Real             oldbound,           /**< old value for bound */
290  	   SCIP_Real             newbound,           /**< new value for bound */
291  	   SCIP_BDCHGINFO**      bdchginfo           /**< pointer to store bound change information */
292  	   );
293  	
294  	
295  	/*
296  	 * Conflict LP Bound Changes
297  	 */
298  	
299  	
300  	/** calculates the maximal size of conflict sets to be used */
301  	int conflictCalcMaxsize(
302  	   SCIP_SET*             set,                /**< global SCIP settings */
303  	   SCIP_PROB*            prob                /**< problem data */
304  	   );
305  	
306  	/** undoes bound changes on variables, still leaving the given infeasibility proof valid */
307  	SCIP_RETCODE SCIPundoBdchgsProof(
308  	   SCIP_SET*             set,                /**< global SCIP settings */
309  	   SCIP_PROB*            prob,               /**< problem data */
310  	   int                   currentdepth,       /**< current depth in the tree */
311  	   SCIP_Real*            proofcoefs,         /**< coefficients in infeasibility proof */
312  	   SCIP_Real             prooflhs,           /**< left hand side of proof */
313  	   SCIP_Real*            proofact,           /**< current activity of proof */
314  	   SCIP_Real*            curvarlbs,          /**< current lower bounds of active problem variables */
315  	   SCIP_Real*            curvarubs,          /**< current upper bounds of active problem variables */
316  	   int*                  lbchginfoposs,      /**< positions of currently active lower bound change information in variables' arrays */
317  	   int*                  ubchginfoposs,      /**< positions of currently active upper bound change information in variables' arrays */
318  	   SCIP_LPBDCHGS*        oldlpbdchgs,        /**< old LP bound changes used for reset the LP bound change, or NULL */
319  	   SCIP_LPBDCHGS*        relaxedlpbdchgs,    /**< relaxed LP bound changes used for reset the LP bound change, or NULL */
320  	   SCIP_Bool*            resolve,            /**< pointer to store whether the changed LP should be resolved again, or NULL */
321  	   SCIP_LPI*             lpi                 /**< pointer to LPi to access infinity of LP solver; necessary to set correct values */
322  	   );
323  	
324  	/** applies conflict analysis starting with given bound changes, that could not be undone during previous
325  	 *  infeasibility analysis
326  	 */
327  	SCIP_RETCODE SCIPconflictAnalyzeRemainingBdchgs(
328  	   SCIP_CONFLICT*        conflict,           /**< conflict analysis data */
329  	   BMS_BLKMEM*           blkmem,             /**< block memory of transformed problem */
330  	   SCIP_SET*             set,                /**< global SCIP settings */
331  	   SCIP_STAT*            stat,               /**< problem statistics */
332  	   SCIP_PROB*            prob,               /**< problem data */
333  	   SCIP_TREE*            tree,               /**< branch and bound tree */
334  	   SCIP_Bool             diving,             /**< are we in strong branching or diving mode? */
335  	   int*                  lbchginfoposs,      /**< positions of currently active lower bound change information in variables' arrays */
336  	   int*                  ubchginfoposs,      /**< positions of currently active upper bound change information in variables' arrays */
337  	   int*                  nconss,             /**< pointer to store the number of generated conflict constraints */
338  	   int*                  nliterals,          /**< pointer to store the number of literals in generated conflict constraints */
339  	   int*                  nreconvconss,       /**< pointer to store the number of generated reconvergence constraints */
340  	   int*                  nreconvliterals     /**< pointer to store the number of literals generated reconvergence constraints */
341  	   );
342  	
343  	/** initializes the propagation conflict analysis by clearing the conflict candidate queue */
344  	SCIP_RETCODE SCIPconflictInit(
345  	   SCIP_CONFLICT*        conflict,           /**< conflict analysis data */
346  	   SCIP_SET*             set,                /**< global SCIP settings */
347  	   SCIP_STAT*            stat,               /**< problem statistics */
348  	   SCIP_PROB*            prob,               /**< problem data */
349  	   SCIP_CONFTYPE         conftype,           /**< type of the conflict */
350  	   SCIP_Bool             usescutoffbound     /**< depends the conflict on a cutoff bound? */
351  	   );
352  	
353  	/** adds variable's bound to conflict candidate queue */
354  	SCIP_RETCODE SCIPconflictAddBound(
355  	   SCIP_CONFLICT*        conflict,           /**< conflict analysis data */
356  	   BMS_BLKMEM*           blkmem,             /**< block memory */
357  	   SCIP_SET*             set,                /**< global SCIP settings */
358  	   SCIP_STAT*            stat,               /**< dynamic problem statistics */
359  	   SCIP_VAR*             var,                /**< problem variable */
360  	   SCIP_BOUNDTYPE        boundtype,          /**< type of bound that was changed: lower or upper bound */
361  	   SCIP_BDCHGIDX*        bdchgidx            /**< bound change index (time stamp of bound change), or NULL for current time */
362  	   );
363  	
364  	/** adds variable's bound to conflict candidate queue with the additional information of a relaxed bound */
365  	SCIP_RETCODE SCIPconflictAddRelaxedBound(
366  	   SCIP_CONFLICT*        conflict,           /**< conflict analysis data */
367  	   BMS_BLKMEM*           blkmem,             /**< block memory */
368  	   SCIP_SET*             set,                /**< global SCIP settings */
369  	   SCIP_STAT*            stat,               /**< dynamic problem statistics */
370  	   SCIP_VAR*             var,                /**< problem variable */
371  	   SCIP_BOUNDTYPE        boundtype,          /**< type of bound that was changed: lower or upper bound */
372  	   SCIP_BDCHGIDX*        bdchgidx,           /**< bound change index (time stamp of bound change), or NULL for current time */
373  	   SCIP_Real             relaxedbd           /**< the relaxed bound */
374  	   );
375  	
376  	/** checks if the given variable is already part of the current conflict set or queued for resolving with the same or
377  	 *  even stronger bound
378  	 */
379  	SCIP_RETCODE SCIPconflictIsVarUsed(
380  	   SCIP_CONFLICT*        conflict,           /**< conflict analysis data */
381  	   SCIP_VAR*             var,                /**< problem variable */
382  	   SCIP_SET*             set,                /**< global SCIP settings */
383  	   SCIP_BOUNDTYPE        boundtype,          /**< type of bound for which the score should be increased */
384  	   SCIP_BDCHGIDX*        bdchgidx,           /**< bound change index (time stamp of bound change), or NULL for current time */
385  	   SCIP_Bool*            used                /**< pointer to store if the variable is already used */
386  	   );
387  	
388  	/** returns the conflict lower bound if the variable is present in the current conflict set; otherwise the global lower
389  	 *  bound
390  	 */
391  	SCIP_Real SCIPconflictGetVarLb(
392  	   SCIP_CONFLICT*        conflict,           /**< conflict analysis data */
393  	   SCIP_VAR*             var                 /**< problem variable */
394  	   );
395  	
396  	/** returns the conflict upper bound if the variable is present in the current conflict set; otherwise the global upper
397  	 *  bound
398  	 */
399  	SCIP_Real SCIPconflictGetVarUb(
400  	   SCIP_CONFLICT*        conflict,           /**< conflict analysis data */
401  	   SCIP_VAR*             var                 /**< problem variable */
402  	   );
403  	
404  	/** try to find a subset of changed bounds leading to an infeasible LP
405  	 *
406  	 *  1. call undoBdchgsDualfarkas() or undoBdchgsDualsol()
407  	 *     -> update lb/ubchginfoposs arrays
408  	 *     -> store additional changes in bdchg and curvarlbs/ubs arrays
409  	 *     -> apply additional changes to the LPI
410  	 *  2. (optional) if additional bound changes were undone:
411  	 *     -> resolve LP
412  	 *     -> goto 1.
413  	 *  3. redo all bound changes in the LPI to restore the LPI to its original state
414  	 *  4. analyze conflict
415  	 *     -> put remaining changed bounds (see lb/ubchginfoposs arrays) into starting conflict set
416  	 */
417  	SCIP_RETCODE SCIPrunBoundHeuristic(
418  	   SCIP_CONFLICT*        conflict,           /**< conflict data */
419  	   SCIP_SET*             set,                /**< global SCIP settings */
420  	   SCIP_STAT*            stat,               /**< problem statistics */
421  	   SCIP_PROB*            origprob,           /**< original problem */
422  	   SCIP_PROB*            transprob,          /**< transformed problem */
423  	   SCIP_TREE*            tree,               /**< branch and bound tree */
424  	   SCIP_REOPT*           reopt,              /**< reoptimization data */
425  	   SCIP_LP*              lp,                 /**< LP data */
426  	   SCIP_LPI*             lpi,                /**< LPI data */
427  	   BMS_BLKMEM*           blkmem,             /**< block memory */
428  	   SCIP_Real*            proofcoefs,         /**< coefficients in the proof constraint */
429  	   SCIP_Real*            prooflhs,           /**< lhs of the proof constraint */
430  	   SCIP_Real*            proofactivity,      /**< maximal activity of the proof constraint */
431  	   SCIP_Real*            curvarlbs,          /**< current lower bounds of active problem variables */
432  	   SCIP_Real*            curvarubs,          /**< current upper bounds of active problem variables */
433  	   int*                  lbchginfoposs,      /**< positions of currently active lower bound change information in variables' arrays */
434  	   int*                  ubchginfoposs,      /**< positions of currently active upper bound change information in variables' arrays */
435  	   int*                  iterations,         /**< pointer to store the total number of LP iterations used */
436  	   SCIP_Bool             marklpunsolved,     /**< whether LP should be marked unsolved after analysis (needed for strong branching) */
437  	   SCIP_Bool*            dualproofsuccess,   /**< pointer to store success result of dual proof analysis */
438  	   SCIP_Bool*            valid               /**< pointer to store whether the result is still a valid proof */
439  	   );
440  	
441  	#ifdef __cplusplus
442  	}
443  	#endif
444  	
445  	#endif
446