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_dualproofanalysis.h 26 * @ingroup OTHER_CFILES 27 * @brief internal methods for dual proof conflict analysis 28 * @author Timo Berthold 29 * @author Jakob Witzig 30 * 31 * In dual proof analysis, an infeasible LP relaxation is analysed. 32 * Using the dual solution, a valid constraint is derived that is violated 33 * by all values in the domain. This constraint is added to the problem 34 * and can then be used for domain propagation. More details can be found in [1] 35 * 36 * [1] J. Witzig, T. Berthold, en S. Heinz, ‘Computational aspects of infeasibility analysis in mixed integer programming’, 37 * Math. Prog. Comp., mrt. 2021, doi: 10.1007/s12532-021-00202-0. 38 */ 39 40 /*---+----1----+----2----+----3----+----4----+----5----+----6----+----7----+----8----+----9----+----0----+----1----+----2*/ 41 42 #ifndef __SCIP_CONFLICT_DUALPROOFANALYSIS_H__ 43 #define __SCIP_CONFLICT_DUALPROOFANALYSIS_H__ 44 45 #include "blockmemshell/memory.h" 46 #include "scip/def.h" 47 #include "scip/type_branch.h" 48 #include "scip/type_conflict.h" 49 #include "scip/type_conflictstore.h" 50 #include "scip/type_event.h" 51 #include "scip/type_implics.h" 52 #include "scip/type_lp.h" 53 #include "scip/type_prob.h" 54 #include "scip/type_reopt.h" 55 #include "scip/type_retcode.h" 56 #include "scip/type_set.h" 57 #include "scip/type_stat.h" 58 #include "scip/type_tree.h" 59 #include "scip/type_var.h" 60 #include "scip/type_cuts.h" 61 62 #ifdef __cplusplus 63 extern "C" { 64 #endif 65 /* 66 * Proof Sets 67 */ 68 69 /** frees a proofset */ 70 void SCIPproofsetFree( 71 SCIP_PROOFSET** proofset, /**< proof set */ 72 BMS_BLKMEM* blkmem /**< block memory */ 73 ); 74 75 /** returns the number of variables in the proofset */ 76 int SCIPproofsetGetNVars( 77 SCIP_PROOFSET* proofset /**< proof set */ 78 ); 79 /** returns the number of variables in the proofset */ 80 81 82 /** creates and clears the proofset */ 83 SCIP_RETCODE SCIPconflictInitProofset( 84 SCIP_CONFLICT* conflict, /**< conflict analysis data */ 85 BMS_BLKMEM* blkmem /**< block memory of transformed problem */ 86 ); 87 88 89 /* create proof constraints out of proof sets */ 90 SCIP_RETCODE SCIPconflictFlushProofset( 91 SCIP_CONFLICT* conflict, /**< conflict analysis data */ 92 SCIP_CONFLICTSTORE* conflictstore, /**< conflict store */ 93 BMS_BLKMEM* blkmem, /**< block memory */ 94 SCIP_SET* set, /**< global SCIP settings */ 95 SCIP_STAT* stat, /**< dynamic problem statistics */ 96 SCIP_PROB* transprob, /**< transformed problem after presolve */ 97 SCIP_PROB* origprob, /**< original problem */ 98 SCIP_TREE* tree, /**< branch and bound tree */ 99 SCIP_REOPT* reopt, /**< reoptimization data structure */ 100 SCIP_LP* lp, /**< current LP data */ 101 SCIP_BRANCHCAND* branchcand, /**< branching candidate storage */ 102 SCIP_EVENTQUEUE* eventqueue, /**< event queue */ 103 SCIP_CLIQUETABLE* cliquetable /**< clique table data structure */ 104 ); 105 106 /** perform conflict analysis based on a dual unbounded ray 107 * 108 * given an aggregation of rows lhs <= a^Tx such that lhs > maxactivity. if the constraint has size one we add a 109 * bound change instead of the constraint. 110 */ 111 SCIP_RETCODE SCIPconflictAnalyzeDualProof( 112 SCIP_CONFLICT* conflict, /**< conflict analysis data */ 113 SCIP_SET* set, /**< global SCIP settings */ 114 SCIP_STAT* stat, /**< dynamic SCIP statistics */ 115 BMS_BLKMEM* blkmem, /**< block memory */ 116 SCIP_PROB* origprob, /**< original problem */ 117 SCIP_PROB* transprob, /**< transformed problem */ 118 SCIP_TREE* tree, /**< tree data */ 119 SCIP_REOPT* reopt, /**< reoptimization data */ 120 SCIP_LP* lp, /**< LP data */ 121 SCIP_AGGRROW* proofrow, /**< aggregated row representing the proof */ 122 int validdepth, /**< valid depth of the dual proof */ 123 SCIP_Real* curvarlbs, /**< current lower bounds of active problem variables */ 124 SCIP_Real* curvarubs, /**< current upper bounds of active problem variables */ 125 SCIP_Bool initialproof, /**< do we analyze the initial reason of infeasibility? */ 126 SCIP_Bool* globalinfeasible, /**< pointer to store whether global infeasibility could be proven */ 127 SCIP_Bool* success /**< pointer to store success result */ 128 ); 129 130 #ifdef __cplusplus 131 } 132 #endif 133 134 #endif 135