SCIP Doxygen Documentation
 
Loading...
Searching...
No Matches
conflict_dualproofanalysis.h
Go to the documentation of this file.
1/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
2/* */
3/* This file is part of the program and library */
4/* SCIP --- Solving Constraint Integer Programs */
5/* */
6/* Copyright (c) 2002-2024 Zuse Institute Berlin (ZIB) */
7/* */
8/* Licensed under the Apache License, Version 2.0 (the "License"); */
9/* you may not use this file except in compliance with the License. */
10/* You may obtain a copy of the License at */
11/* */
12/* http://www.apache.org/licenses/LICENSE-2.0 */
13/* */
14/* Unless required by applicable law or agreed to in writing, software */
15/* distributed under the License is distributed on an "AS IS" BASIS, */
16/* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. */
17/* See the License for the specific language governing permissions and */
18/* limitations under the License. */
19/* */
20/* You should have received a copy of the Apache-2.0 license */
21/* along with SCIP; see the file LICENSE. If not visit scipopt.org. */
22/* */
23/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
24
25/**@file 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
46#include "scip/def.h"
47#include "scip/type_branch.h"
48#include "scip/type_conflict.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
63extern "C" {
64#endif
65/*
66 * Proof Sets
67 */
68
69/** frees a proofset */
71 SCIP_PROOFSET** proofset, /**< proof set */
72 BMS_BLKMEM* blkmem /**< block memory */
73 );
74
75/** returns the number of variables in the proofset */
77 SCIP_PROOFSET* proofset /**< proof set */
78 );
79/** returns the number of variables in the proofset */
80
81
82/** creates and clears the proofset */
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 */
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 */
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
void SCIPproofsetFree(SCIP_PROOFSET **proofset, BMS_BLKMEM *blkmem)
SCIP_RETCODE SCIPconflictInitProofset(SCIP_CONFLICT *conflict, BMS_BLKMEM *blkmem)
SCIP_RETCODE SCIPconflictAnalyzeDualProof(SCIP_CONFLICT *conflict, SCIP_SET *set, SCIP_STAT *stat, BMS_BLKMEM *blkmem, SCIP_PROB *origprob, SCIP_PROB *transprob, SCIP_TREE *tree, SCIP_REOPT *reopt, SCIP_LP *lp, SCIP_AGGRROW *proofrow, int validdepth, SCIP_Real *curvarlbs, SCIP_Real *curvarubs, SCIP_Bool initialproof, SCIP_Bool *globalinfeasible, SCIP_Bool *success)
SCIP_RETCODE SCIPconflictFlushProofset(SCIP_CONFLICT *conflict, SCIP_CONFLICTSTORE *conflictstore, BMS_BLKMEM *blkmem, SCIP_SET *set, SCIP_STAT *stat, SCIP_PROB *transprob, SCIP_PROB *origprob, SCIP_TREE *tree, SCIP_REOPT *reopt, SCIP_LP *lp, SCIP_BRANCHCAND *branchcand, SCIP_EVENTQUEUE *eventqueue, SCIP_CLIQUETABLE *cliquetable)
int SCIPproofsetGetNVars(SCIP_PROOFSET *proofset)
common defines and data types used in all packages of SCIP
#define SCIP_Bool
Definition def.h:91
#define SCIP_Real
Definition def.h:172
memory allocation routines
struct BMS_BlkMem BMS_BLKMEM
Definition memory.h:437
type definitions for branching rules
struct SCIP_BranchCand SCIP_BRANCHCAND
Definition type_branch.h:55
type definitions for conflict analysis
struct SCIP_Conflict SCIP_CONFLICT
struct SCIP_ProofSet SCIP_PROOFSET
type definitions for conflict store
struct SCIP_ConflictStore SCIP_CONFLICTSTORE
type definitions for cuts
struct SCIP_AggrRow SCIP_AGGRROW
Definition type_cuts.h:37
type definitions for managing events
struct SCIP_EventQueue SCIP_EVENTQUEUE
Definition type_event.h:175
type definitions for implications, variable bounds, and cliques
struct SCIP_CliqueTable SCIP_CLIQUETABLE
type definitions for LP management
struct SCIP_Lp SCIP_LP
Definition type_lp.h:110
type definitions for storing and manipulating the main problem
struct SCIP_Prob SCIP_PROB
Definition type_prob.h:52
type definitions for collecting reoptimization information
struct SCIP_Reopt SCIP_REOPT
Definition type_reopt.h:39
type definitions for return codes for SCIP methods
enum SCIP_Retcode SCIP_RETCODE
type definitions for global SCIP settings
struct SCIP_Set SCIP_SET
Definition type_set.h:71
type definitions for problem statistics
struct SCIP_Stat SCIP_STAT
Definition type_stat.h:69
type definitions for branch and bound tree
struct SCIP_Tree SCIP_TREE
Definition type_tree.h:65
type definitions for problem variables