Scippy

    SCIP

    Solving Constraint Integer Programs

    Detailed Description

    internal methods for dual proof conflict analysis

    Author
    Timo Berthold
    Jakob Witzig
    Sander Borst

    In dual proof analysis, an infeasible LP relaxation is analysed. Using the dual solution, a valid constraint is derived that is violated by all values in the domain. This constraint is added to the problem and can then be used for domain propagation. More details can be found in [1]

    [1] J. Witzig, T. Berthold, en S. Heinz, ‘Computational aspects of infeasibility analysis in mixed integer programming’, Math. Prog. Comp., mrt. 2021, doi: 10.1007/s12532-021-00202-0.

    Definition in file conflict_dualproofanalysis.c.

    #include "lpi/lpi.h"
    #include "scip/certificate.h"
    #include "scip/clock.h"
    #include "scip/conflict_general.h"
    #include "scip/conflict_dualproofanalysis.h"
    #include "scip/conflictstore.h"
    #include "scip/cons.h"
    #include "scip/cons_linear.h"
    #include "scip/cons_exactlinear.h"
    #include "scip/cuts.h"
    #include "scip/history.h"
    #include "scip/lp.h"
    #include "scip/presolve.h"
    #include "scip/prob.h"
    #include "scip/prop.h"
    #include "scip/pub_conflict.h"
    #include "scip/pub_cons.h"
    #include "scip/pub_lp.h"
    #include "scip/pub_message.h"
    #include "scip/pub_misc.h"
    #include "scip/pub_misc_sort.h"
    #include "scip/pub_paramset.h"
    #include "scip/pub_prop.h"
    #include "scip/pub_tree.h"
    #include "scip/pub_var.h"
    #include "scip/scip_certificate.h"
    #include "scip/scip_conflict.h"
    #include "scip/scip_cons.h"
    #include "scip/scip_exact.h"
    #include "scip/scip_mem.h"
    #include "scip/scip_sol.h"
    #include "scip/scip_var.h"
    #include "scip/set.h"
    #include "scip/sol.h"
    #include "scip/struct_conflict.h"
    #include "scip/struct_lp.h"
    #include "scip/struct_prob.h"
    #include "scip/struct_set.h"
    #include "scip/struct_stat.h"
    #include "scip/struct_tree.h"
    #include "scip/struct_var.h"
    #include "scip/struct_certificate.h"
    #include "scip/tree.h"
    #include "scip/var.h"
    #include "scip/visual.h"

    Go to the source code of this file.

    Macros

    #define BOUNDSWITCH   0.51
     
    #define POSTPROCESS   FALSE
     
    #define VARTYPEUSEVBDS   0
     
    #define ALLOWLOCAL   FALSE
     
    #define MINFRAC   0.05
     
    #define MAXFRAC   0.999
     
    #define debugPrintViolationInfo(...)
     

    Functions

    static char varGetChar (SCIP_VAR *var)
     
    static void proofsetClear (SCIP_PROOFSET *proofset)
     
    static SCIP_RETCODE proofsetCreate (SCIP_PROOFSET **proofset, BMS_BLKMEM *blkmem)
     
    void SCIPproofsetFree (SCIP_PROOFSET **proofset, BMS_BLKMEM *blkmem)
     
    static int * proofsetGetInds (SCIP_PROOFSET *proofset)
     
    static SCIP_RealproofsetGetVals (SCIP_PROOFSET *proofset)
     
    static SCIP_Real proofsetGetRhs (SCIP_PROOFSET *proofset)
     
    int SCIPproofsetGetNVars (SCIP_PROOFSET *proofset)
     
    static SCIP_CONFTYPE proofsetGetConftype (SCIP_PROOFSET *proofset)
     
    static SCIP_RETCODE proofsetAddSparseData (SCIP_PROOFSET *proofset, BMS_BLKMEM *blkmem, SCIP_Real *vals, int *inds, int nnz, SCIP_Real rhs)
     
    static SCIP_RETCODE proofsetAddAggrrow (SCIP_PROOFSET *proofset, SCIP_SET *set, BMS_BLKMEM *blkmem, SCIP_AGGRROW *aggrrow)
     
    static void proofsetCancelVarWithBound (SCIP_PROOFSET *proofset, SCIP_SET *set, SCIP_VAR *var, int pos, SCIP_Bool *valid)
     
    SCIP_RETCODE SCIPconflictInitProofset (SCIP_CONFLICT *conflict, BMS_BLKMEM *blkmem)
     
    static SCIP_RETCODE conflictEnsureProofsetsMem (SCIP_CONFLICT *conflict, SCIP_SET *set, int num)
     
    static SCIP_RETCODE conflictInsertProofset (SCIP_CONFLICT *conflict, SCIP_SET *set, SCIP_PROOFSET *proofset)
     
    static SCIP_RETCODE tightenSingleVar (SCIP_CONFLICT *conflict, SCIP_SET *set, SCIP_STAT *stat, SCIP_TREE *tree, BMS_BLKMEM *blkmem, SCIP_PROB *origprob, SCIP_PROB *transprob, SCIP_REOPT *reopt, SCIP_LP *lp, SCIP_BRANCHCAND *branchcand, SCIP_EVENTQUEUE *eventqueue, SCIP_EVENTFILTER *eventfilter, SCIP_CLIQUETABLE *cliquetable, SCIP_VAR *var, SCIP_Real val, SCIP_Real rhs, SCIP_CONFTYPE prooftype, int validdepth)
     
    static SCIP_Real getMinActivity (SCIP_SET *set, SCIP_PROB *transprob, SCIP_Real *coefs, int *inds, int nnz, SCIP_Real *curvarlbs, SCIP_Real *curvarubs)
     
    static SCIP_Real getMaxActivity (SCIP_SET *set, SCIP_PROB *transprob, SCIP_Real *coefs, int *inds, int nnz, SCIP_Real *curvarlbs, SCIP_Real *curvarubs)
     
    static SCIP_RETCODE propagateLongProof (SCIP_CONFLICT *conflict, SCIP_SET *set, SCIP_STAT *stat, SCIP_REOPT *reopt, SCIP_TREE *tree, BMS_BLKMEM *blkmem, SCIP_PROB *origprob, SCIP_PROB *transprob, SCIP_LP *lp, SCIP_BRANCHCAND *branchcand, SCIP_EVENTQUEUE *eventqueue, SCIP_EVENTFILTER *eventfilter, SCIP_CLIQUETABLE *cliquetable, SCIP_Real *coefs, int *inds, int nnz, SCIP_Real rhs, SCIP_CONFTYPE conflicttype, int validdepth)
     
    static SCIP_RETCODE createAndAddProofcons (SCIP_CONFLICT *conflict, SCIP_CONFLICTSTORE *conflictstore, SCIP_PROOFSET *proofset, SCIP_SET *set, SCIP_STAT *stat, SCIP_PROB *origprob, SCIP_PROB *transprob, SCIP_TREE *tree, SCIP_REOPT *reopt, SCIP_LP *lp, SCIP_BRANCHCAND *branchcand, SCIP_EVENTQUEUE *eventqueue, SCIP_EVENTFILTER *eventfilter, SCIP_CLIQUETABLE *cliquetable, BMS_BLKMEM *blkmem)
     
    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_EVENTFILTER *eventfilter, SCIP_CLIQUETABLE *cliquetable)
     
    static void tightenCoefficients (SCIP_SET *set, SCIP_PROOFSET *proofset, int *nchgcoefs, SCIP_Bool *redundant)
     
    static SCIP_RETCODE separateAlternativeProofs (SCIP_CONFLICT *conflict, SCIP_SET *set, SCIP_STAT *stat, SCIP_PROB *transprob, SCIP_TREE *tree, BMS_BLKMEM *blkmem, SCIP_AGGRROW *proofrow, SCIP_Real *curvarlbs, SCIP_Real *curvarubs, SCIP_CONFTYPE conflicttype)
     
    static SCIP_RETCODE tightenDualproof (SCIP_CONFLICT *conflict, SCIP_SET *set, SCIP_STAT *stat, BMS_BLKMEM *blkmem, SCIP_PROB *transprob, SCIP_TREE *tree, SCIP_AGGRROW *proofrow, int validdepth, SCIP_Real *curvarlbs, SCIP_Real *curvarubs, SCIP_Bool initialproof)
     
    SCIP_RETCODE SCIPconflictAnalyzeDualProof (SCIP_CONFLICT *conflict, SCIP_SET *set, SCIP_STAT *stat, SCIP_EVENTFILTER *eventfilter, 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)
     

    Macro Definition Documentation

    ◆ BOUNDSWITCH

    #define BOUNDSWITCH   0.51

    threshold for bound switching - see cuts.c

    Definition at line 89 of file conflict_dualproofanalysis.c.

    ◆ POSTPROCESS

    #define POSTPROCESS   FALSE

    apply postprocessing to the cut - see cuts.c

    Definition at line 90 of file conflict_dualproofanalysis.c.

    ◆ VARTYPEUSEVBDS

    #define VARTYPEUSEVBDS   0

    We do not allow variable bound substitution - see cuts.c for more information.

    Definition at line 91 of file conflict_dualproofanalysis.c.

    ◆ ALLOWLOCAL

    #define ALLOWLOCAL   FALSE

    allow to generate local cuts - see cuts.

    Definition at line 92 of file conflict_dualproofanalysis.c.

    ◆ MINFRAC

    #define MINFRAC   0.05

    minimal fractionality of floor(rhs) - see cuts.c

    Definition at line 93 of file conflict_dualproofanalysis.c.

    ◆ MAXFRAC

    #define MAXFRAC   0.999

    maximal fractionality of floor(rhs) - see cuts.c

    Definition at line 94 of file conflict_dualproofanalysis.c.

    ◆ debugPrintViolationInfo

    #define debugPrintViolationInfo (   ...)

    Definition at line 1308 of file conflict_dualproofanalysis.c.

    Function Documentation

    ◆ varGetChar()

    static char varGetChar ( SCIP_VAR var)
    static

    return the char associated with the type of the variable

    Parameters
    varvariable

    Definition at line 103 of file conflict_dualproofanalysis.c.

    References SCIP_VARTYPE_BINARY, SCIP_VARTYPE_INTEGER, SCIPvarGetType(), and SCIPvarIsIntegral().

    Referenced by tightenSingleVar().

    ◆ proofsetClear()

    static void proofsetClear ( SCIP_PROOFSET proofset)
    static

    ◆ proofsetCreate()

    static SCIP_RETCODE proofsetCreate ( SCIP_PROOFSET **  proofset,
    BMS_BLKMEM blkmem 
    )
    static

    creates a proofset

    Parameters
    proofsetproof set
    blkmemblock memory of transformed problem

    Definition at line 131 of file conflict_dualproofanalysis.c.

    References BMSallocBlockMemory, NULL, SCIP_ALLOC, SCIP_CONFTYPE_UNKNOWN, SCIP_LONGINT_MAX, and SCIP_OKAY.

    Referenced by SCIPconflictInitProofset(), separateAlternativeProofs(), and tightenDualproof().

    ◆ SCIPproofsetFree()

    void SCIPproofsetFree ( SCIP_PROOFSET **  proofset,
    BMS_BLKMEM blkmem 
    )

    frees a proofset

    Parameters
    proofsetproof set
    blkmemblock memory

    Definition at line 152 of file conflict_dualproofanalysis.c.

    References BMSfreeBlockMemory, BMSfreeBlockMemoryArrayNull, and NULL.

    Referenced by SCIPconflictFlushProofset(), SCIPconflictFree(), separateAlternativeProofs(), and tightenDualproof().

    ◆ proofsetGetInds()

    static int * proofsetGetInds ( SCIP_PROOFSET proofset)
    static

    return the indices of variables in the proofset

    Parameters
    proofsetproof set

    Definition at line 169 of file conflict_dualproofanalysis.c.

    References SCIP_ProofSet::inds, and NULL.

    Referenced by createAndAddProofcons(), SCIPconflictFlushProofset(), and tightenDualproof().

    ◆ proofsetGetVals()

    static SCIP_Real * proofsetGetVals ( SCIP_PROOFSET proofset)
    static

    return coefficient of variable in the proofset with given probindex

    Parameters
    proofsetproof set

    Definition at line 180 of file conflict_dualproofanalysis.c.

    References NULL, and SCIP_ProofSet::vals.

    Referenced by createAndAddProofcons(), SCIPconflictFlushProofset(), and tightenDualproof().

    ◆ proofsetGetRhs()

    static SCIP_Real proofsetGetRhs ( SCIP_PROOFSET proofset)
    static

    return the right-hand side if a proofset

    Parameters
    proofsetproof set

    Definition at line 191 of file conflict_dualproofanalysis.c.

    References NULL, and SCIP_ProofSet::rhs.

    Referenced by createAndAddProofcons(), SCIPconflictFlushProofset(), and tightenCoefficients().

    ◆ SCIPproofsetGetNVars()

    int SCIPproofsetGetNVars ( SCIP_PROOFSET proofset)

    returns the number of variables in the proofset

    Parameters
    proofsetproof set

    Definition at line 201 of file conflict_dualproofanalysis.c.

    References SCIP_ProofSet::nnz, and NULL.

    Referenced by conflictAnalyzeLP(), createAndAddProofcons(), SCIPconflictFlushProofset(), tightenCoefficients(), and tightenDualproof().

    ◆ proofsetGetConftype()

    static SCIP_CONFTYPE proofsetGetConftype ( SCIP_PROOFSET proofset)
    static

    returns the number of variables in the proofset

    Parameters
    proofsetproof set

    Definition at line 212 of file conflict_dualproofanalysis.c.

    References SCIP_ProofSet::conflicttype, and NULL.

    Referenced by createAndAddProofcons(), and SCIPconflictFlushProofset().

    ◆ proofsetAddSparseData()

    static SCIP_RETCODE proofsetAddSparseData ( SCIP_PROOFSET proofset,
    BMS_BLKMEM blkmem,
    SCIP_Real vals,
    int *  inds,
    int  nnz,
    SCIP_Real  rhs 
    )
    static

    adds given data as aggregation row to the proofset

    Parameters
    proofsetproof set
    blkmemblock memory
    valsvariable coefficients
    indsvariable array
    nnzsize of variable and coefficient array
    rhsright-hand side of the aggregation row

    Definition at line 223 of file conflict_dualproofanalysis.c.

    References BMSduplicateBlockMemoryArray, BMSreallocBlockMemoryArray, SCIP_ProofSet::inds, SCIP_ProofSet::nnz, NULL, SCIP_ProofSet::rhs, SCIP_ALLOC, SCIP_OKAY, SCIP_ProofSet::size, and SCIP_ProofSet::vals.

    Referenced by proofsetAddAggrrow(), and separateAlternativeProofs().

    ◆ proofsetAddAggrrow()

    static SCIP_RETCODE proofsetAddAggrrow ( SCIP_PROOFSET proofset,
    SCIP_SET set,
    BMS_BLKMEM blkmem,
    SCIP_AGGRROW aggrrow 
    )
    static

    adds an aggregation row to the proofset

    Parameters
    proofsetproof set
    setglobal SCIP settings
    blkmemblock memory
    aggrrowaggregation row to add

    Definition at line 274 of file conflict_dualproofanalysis.c.

    References SCIP_ProofSet::certificateline, SCIP_AggrRow::certificateline, NULL, proofsetAddSparseData(), SCIP_CALL, SCIP_Longint, SCIP_LONGINT_MAX, SCIP_OKAY, SCIP_Real, SCIPaggrRowGetInds(), SCIPaggrRowGetNNz(), SCIPaggrRowGetProbvarValue(), SCIPaggrRowGetRhs(), SCIPisCertified(), SCIPsetAllocBufferArray, SCIPsetFreeBufferArray, and SCIP_AggrRow::vals.

    Referenced by tightenDualproof().

    ◆ proofsetCancelVarWithBound()

    static void proofsetCancelVarWithBound ( SCIP_PROOFSET proofset,
    SCIP_SET set,
    SCIP_VAR var,
    int  pos,
    SCIP_Bool valid 
    )
    static

    Removes a given variable var from position pos from the proofset and updates the right-hand side according to sign of the coefficient, i.e., rhs -= coef * bound, where bound = lb if coef >= 0 and bound = ub, otherwise.

    Note
    : The list of non-zero indices and coefficients will be updated by swapping the last non-zero index to pos.

    Definition at line 325 of file conflict_dualproofanalysis.c.

    References FALSE, SCIP_ProofSet::inds, SCIP_ProofSet::nnz, NULL, SCIP_ProofSet::rhs, SCIPsetIsInfinity(), SCIPvarGetLbGlobal(), SCIPvarGetUbGlobal(), TRUE, and SCIP_ProofSet::vals.

    Referenced by tightenDualproof().

    ◆ SCIPconflictInitProofset()

    SCIP_RETCODE SCIPconflictInitProofset ( SCIP_CONFLICT conflict,
    BMS_BLKMEM blkmem 
    )

    creates and clears the proofset

    Parameters
    conflictconflict analysis data
    blkmemblock memory of transformed problem

    Definition at line 364 of file conflict_dualproofanalysis.c.

    References NULL, SCIP_Conflict::proofset, proofsetCreate(), SCIP_CALL, and SCIP_OKAY.

    Referenced by SCIPconflictCreate().

    ◆ conflictEnsureProofsetsMem()

    static SCIP_RETCODE conflictEnsureProofsetsMem ( SCIP_CONFLICT conflict,
    SCIP_SET set,
    int  num 
    )
    static

    resizes proofsets array to be able to store at least num entries

    Parameters
    conflictconflict analysis data
    setglobal SCIP settings
    numminimal number of slots in array

    Definition at line 379 of file conflict_dualproofanalysis.c.

    References BMSreallocMemoryArray, NULL, SCIP_Conflict::proofsets, SCIP_Conflict::proofsetssize, SCIP_ALLOC, SCIP_OKAY, and SCIPsetCalcMemGrowSize().

    Referenced by conflictInsertProofset().

    ◆ conflictInsertProofset()

    static SCIP_RETCODE conflictInsertProofset ( SCIP_CONFLICT conflict,
    SCIP_SET set,
    SCIP_PROOFSET proofset 
    )
    static

    add a proofset to the list of all proofsets

    Parameters
    conflictconflict analysis data
    setglobal SCIP settings
    proofsetproof set to add

    Definition at line 403 of file conflict_dualproofanalysis.c.

    References conflictEnsureProofsetsMem(), SCIP_Conflict::nproofsets, NULL, SCIP_Conflict::proofsets, SCIP_CALL, and SCIP_OKAY.

    Referenced by separateAlternativeProofs(), and tightenDualproof().

    ◆ tightenSingleVar()

    static SCIP_RETCODE tightenSingleVar ( SCIP_CONFLICT conflict,
    SCIP_SET set,
    SCIP_STAT stat,
    SCIP_TREE tree,
    BMS_BLKMEM blkmem,
    SCIP_PROB origprob,
    SCIP_PROB transprob,
    SCIP_REOPT reopt,
    SCIP_LP lp,
    SCIP_BRANCHCAND branchcand,
    SCIP_EVENTQUEUE eventqueue,
    SCIP_EVENTFILTER eventfilter,
    SCIP_CLIQUETABLE cliquetable,
    SCIP_VAR var,
    SCIP_Real  val,
    SCIP_Real  rhs,
    SCIP_CONFTYPE  prooftype,
    int  validdepth 
    )
    static

    tighten the bound of a singleton variable in a constraint

    if the bound is contradicting with a global bound we cannot tighten the bound directly. in this case we need to create and add a constraint of size one such that propagating this constraint will enforce the infeasibility.

    Parameters
    conflictconflict analysis data
    setglobal SCIP settings
    statdynamic SCIP statistics
    treetree data
    blkmemblock memory
    origproboriginal problem
    transprobtransformed problem
    reoptreoptimization data
    lpLP data
    branchcandbranching candidates
    eventqueueevent queue
    eventfilterglobal event filter
    cliquetableclique table
    varproblem variable
    valcoefficient of the variable
    rhsrhs of the constraint
    prooftypetype of the proof
    validdepthdepth where the bound change is valid

    Definition at line 428 of file conflict_dualproofanalysis.c.

    References SCIP_Conflict::dualproofsbndnnonzeros, SCIP_Conflict::dualproofsinfnnonzeros, FALSE, SCIP_Conflict::nboundlpsuccess, SCIP_Conflict::ndualproofsbndglobal, SCIP_Conflict::ndualproofsbndlocal, SCIP_Conflict::ndualproofsbndsuccess, SCIP_Conflict::ndualproofsinfglobal, SCIP_Conflict::ndualproofsinflocal, SCIP_Conflict::ndualproofsinfsuccess, SCIP_Conflict::nglbchgbds, SCIP_Conflict::ninflpsuccess, SCIP_Conflict::nlocchgbds, NULL, SCIP_Tree::path, SCIP_Bool, SCIP_BOUNDTYPE_LOWER, SCIP_BOUNDTYPE_UPPER, SCIP_CALL, SCIP_CONFTYPE_ALTINFPROOF, SCIP_CONFTYPE_INFEASLP, SCIP_MAXSTRLEN, SCIP_OKAY, SCIP_Real, SCIPaddCoefLinear(), SCIPconsRelease(), SCIPcreateConsLinear(), SCIPnodeAddBoundchg(), SCIPnodeAddCons(), SCIPnodeCutoff(), SCIPnodeGetNumber(), SCIPnodePropagateAgain(), SCIPprobAddCons(), SCIPsetDebugMsg, SCIPsetFeasFloor(), SCIPsetInfinity(), SCIPsetIsGE(), SCIPsetIsGT(), SCIPsetIsIntegral(), SCIPsetIsLE(), SCIPsetIsLT(), SCIPsnprintf(), SCIPtreeGetEffectiveRootDepth(), SCIPvarAdjustBd(), SCIPvarGetLbGlobal(), SCIPvarGetLbLocal(), SCIPvarGetName(), SCIPvarGetUbGlobal(), SCIPvarGetUbLocal(), SCIPvarIsIntegral(), SCIP_Lp::strongbranching, TRUE, and varGetChar().

    Referenced by propagateLongProof(), and SCIPconflictFlushProofset().

    ◆ getMinActivity()

    static SCIP_Real getMinActivity ( SCIP_SET set,
    SCIP_PROB transprob,
    SCIP_Real coefs,
    int *  inds,
    int  nnz,
    SCIP_Real curvarlbs,
    SCIP_Real curvarubs 
    )
    static

    calculates the minimal activity of a given set of bounds and coefficients

    Parameters
    setglobal SCIP settings
    transprobtransformed problem data
    coefscoefficients in sparse representation
    indsnon-zero indices
    nnznumber of non-zero indices
    curvarlbscurrent lower bounds of active problem variables (or NULL for global bounds)
    curvarubscurrent upper bounds of active problem variables (or NULL for global bounds)

    Definition at line 579 of file conflict_dualproofanalysis.c.

    References NULL, QUAD, QUAD_ASSIGN, QUAD_TO_DBL, SCIP_Real, SCIPprobGetVars(), SCIPquadprecProdDD, SCIPquadprecSumQQ, SCIPsetInfinity(), SCIPsetIsInfinity(), SCIPvarGetLbGlobal(), SCIPvarGetProbindex(), and SCIPvarGetUbGlobal().

    Referenced by createAndAddProofcons(), and propagateLongProof().

    ◆ getMaxActivity()

    static SCIP_Real getMaxActivity ( SCIP_SET set,
    SCIP_PROB transprob,
    SCIP_Real coefs,
    int *  inds,
    int  nnz,
    SCIP_Real curvarlbs,
    SCIP_Real curvarubs 
    )
    static

    calculates the minimal activity of a given set of bounds and coefficients

    Parameters
    setglobal SCIP settings
    transprobtransformed problem data
    coefscoefficients in sparse representation
    indsnon-zero indices
    nnznumber of non-zero indices
    curvarlbscurrent lower bounds of active problem variables (or NULL for global bounds)
    curvarubscurrent upper bounds of active problem variables (or NULL for global bounds)

    Definition at line 653 of file conflict_dualproofanalysis.c.

    References NULL, QUAD, QUAD_ASSIGN, QUAD_TO_DBL, SCIP_Real, SCIPprobGetVars(), SCIPquadprecProdDD, SCIPquadprecSumQQ, SCIPsetInfinity(), SCIPsetIsInfinity(), SCIPvarGetLbGlobal(), SCIPvarGetProbindex(), and SCIPvarGetUbGlobal().

    Referenced by createAndAddProofcons(), and tightenDualproof().

    ◆ propagateLongProof()

    static SCIP_RETCODE propagateLongProof ( SCIP_CONFLICT conflict,
    SCIP_SET set,
    SCIP_STAT stat,
    SCIP_REOPT reopt,
    SCIP_TREE tree,
    BMS_BLKMEM blkmem,
    SCIP_PROB origprob,
    SCIP_PROB transprob,
    SCIP_LP lp,
    SCIP_BRANCHCAND branchcand,
    SCIP_EVENTQUEUE eventqueue,
    SCIP_EVENTFILTER eventfilter,
    SCIP_CLIQUETABLE cliquetable,
    SCIP_Real coefs,
    int *  inds,
    int  nnz,
    SCIP_Real  rhs,
    SCIP_CONFTYPE  conflicttype,
    int  validdepth 
    )
    static

    propagate a long proof

    Parameters
    conflictconflict analysis data
    setglobal SCIP settings
    statdynamic SCIP statistics
    reoptreoptimization data
    treetree data
    blkmemblock memory
    origproboriginal problem
    transprobtransformed problem
    lpLP data
    branchcandbranching candidate storage
    eventqueueevent queue
    eventfilterglobal event filter
    cliquetableclique table data structure
    coefscoefficients in sparse representation
    indsnon-zero indices
    nnznumber of non-zero indices
    rhsright-hand side
    conflicttypetype of the conflict
    validdepthdepth where the proof is valid

    Definition at line 727 of file conflict_dualproofanalysis.c.

    References getMinActivity(), NULL, SCIP_CALL, SCIP_OKAY, SCIP_Real, SCIPprobGetVars(), SCIPsetIsEQ(), SCIPsetIsGE(), SCIPsetIsInfinity(), SCIPsetIsLE(), SCIPsetIsZero(), SCIPvarGetLbGlobal(), SCIPvarGetUbGlobal(), and tightenSingleVar().

    Referenced by createAndAddProofcons().

    ◆ createAndAddProofcons()

    static SCIP_RETCODE createAndAddProofcons ( SCIP_CONFLICT conflict,
    SCIP_CONFLICTSTORE conflictstore,
    SCIP_PROOFSET proofset,
    SCIP_SET set,
    SCIP_STAT stat,
    SCIP_PROB origprob,
    SCIP_PROB transprob,
    SCIP_TREE tree,
    SCIP_REOPT reopt,
    SCIP_LP lp,
    SCIP_BRANCHCAND branchcand,
    SCIP_EVENTQUEUE eventqueue,
    SCIP_EVENTFILTER eventfilter,
    SCIP_CLIQUETABLE cliquetable,
    BMS_BLKMEM blkmem 
    )
    static

    creates a proof constraint and tries to add it to the storage

    Parameters
    conflictconflict analysis data
    conflictstoreconflict pool data
    proofsetproof set
    setglobal SCIP settings
    statdynamic SCIP statistics
    origproboriginal problem
    transprobtransformed problem
    treetree data
    reoptreoptimization data
    lpLP data
    branchcandbranching candidate storage
    eventqueueevent queue
    eventfilterglobal event filter
    cliquetableclique table data structure
    blkmemblock memory

    Definition at line 831 of file conflict_dualproofanalysis.c.

    References SCIP_Stat::avgnnz, SCIP_ProofSet::certificateline, SCIP_Conflict::dualproofsbndnnonzeros, SCIP_Conflict::dualproofsinfnnonzeros, FALSE, getMaxActivity(), getMinActivity(), MIN, SCIP_Conflict::ndualproofsbndglobal, SCIP_Conflict::ndualproofsbndlocal, SCIP_Conflict::ndualproofsbndsuccess, SCIP_Conflict::ndualproofsinfglobal, SCIP_Conflict::ndualproofsinflocal, SCIP_Conflict::ndualproofsinfsuccess, NULL, SCIP_Prob::nvars, SCIP_Tree::path, proofsetGetConftype(), proofsetGetInds(), proofsetGetRhs(), proofsetGetVals(), propagateLongProof(), SCIP_Certificate::rowdatahash, SCIP_Bool, SCIP_CALL, SCIP_CONFTYPE_ALTBNDPROOF, SCIP_CONFTYPE_ALTINFPROOF, SCIP_CONFTYPE_BNDEXCEEDING, SCIP_CONFTYPE_INFEASLP, SCIP_INVALIDCALL, SCIP_LONGINT_FORMAT, SCIP_MAXSTRLEN, SCIP_OKAY, SCIP_R_ROUND_NEAREST, SCIP_Real, SCIPaddCoefLinear(), SCIPallocBufferArray, SCIPbuffer(), SCIPconflictstoreAddDualraycons(), SCIPconflictstoreAddDualsolcons(), SCIPconflictstoreGetAvgNnzDualBndProofs(), SCIPconflictstoreGetAvgNnzDualInfProofs(), SCIPconflictstoreGetNDualBndProofs(), SCIPconflictstoreGetNDualInfProofs(), SCIPconsGetHdlr(), SCIPconshdlrGetName(), SCIPconsMarkConflict(), SCIPcreateConsExactLinear(), SCIPcreateConsLinear(), SCIPdebugMessage, SCIPfreeBufferArray, SCIPgetCertificate(), SCIPgetLhsExactLinear(), SCIPgetLhsLinear(), SCIPgetRhsExactLinear(), SCIPgetRhsLinear(), SCIPhashmapInsertLong(), SCIPisCertified(), SCIPnodeAddCons(), SCIPnodeCutoff(), SCIPnodeGetNumber(), SCIPprobAddCons(), SCIPprobGetVars(), SCIPproofsetGetNVars(), SCIPrationalCreateBuffer(), SCIPrationalCreateBufferArray(), SCIPrationalFreeBuffer(), SCIPrationalFreeBufferArray(), SCIPrationalIsAbsInfinity(), SCIPrationalRoundReal(), SCIPrationalSetNegInfinity(), SCIPrationalSetReal(), SCIPreleaseCons(), SCIPsetDebugMsg, SCIPsetInfinity(), SCIPsetIsGT(), SCIPsetIsInfinity(), SCIPsetIsLE(), SCIPsetIsNegative(), SCIPsetIsPositive(), SCIPsetIsZero(), SCIPsnprintf(), SCIPtreeGetEffectiveRootDepth(), SCIPtreeGetFocusDepth(), SCIPupgradeConsLinear(), SCIPvarIsIntegral(), SCIPvarIsRelaxationOnly(), SCIP_Prob::startnconss, TRUE, and SCIP_ProofSet::validdepth.

    Referenced by SCIPconflictFlushProofset().

    ◆ SCIPconflictFlushProofset()

    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_EVENTFILTER eventfilter,
    SCIP_CLIQUETABLE cliquetable 
    )

    create proof constraints out of proof sets

    Parameters
    conflictconflict analysis data
    conflictstoreconflict store
    blkmemblock memory
    setglobal SCIP settings
    statdynamic problem statistics
    transprobtransformed problem after presolve
    origproboriginal problem
    treebranch and bound tree
    reoptreoptimization data structure
    lpcurrent LP data
    branchcandbranching candidate storage
    eventqueueevent queue
    eventfilterglobal event filter
    cliquetableclique table data structure

    Definition at line 1173 of file conflict_dualproofanalysis.c.

    References SCIP_ProofSet::conflicttype, createAndAddProofcons(), FALSE, SCIP_Conflict::nproofsets, NULL, SCIP_Conflict::proofset, proofsetClear(), proofsetGetConftype(), proofsetGetInds(), proofsetGetRhs(), proofsetGetVals(), SCIP_Conflict::proofsets, SCIP_Bool, SCIP_CALL, SCIP_CONFTYPE_BNDEXCEEDING, SCIP_CONFTYPE_INFEASLP, SCIP_CONFTYPE_UNKNOWN, SCIP_OKAY, SCIP_Real, SCIPprobGetVars(), SCIPproofsetFree(), SCIPproofsetGetNVars(), tightenSingleVar(), TRUE, and SCIP_ProofSet::validdepth.

    Referenced by conflictAnalyzeLP().

    ◆ tightenCoefficients()

    static void tightenCoefficients ( SCIP_SET set,
    SCIP_PROOFSET proofset,
    int *  nchgcoefs,
    SCIP_Bool redundant 
    )
    static

    apply coefficient tightening

    Parameters
    setglobal SCIP settings
    proofsetproof set
    nchgcoefspointer to store number of changed coefficients
    redundantpointer to store whether the proof set is redundant

    Definition at line 1316 of file conflict_dualproofanalysis.c.

    References FALSE, SCIP_ProofSet::inds, MAX, MIN, SCIP_ProofSet::nnz, proofsetGetRhs(), REALABS, SCIP_ProofSet::rhs, SCIP_Real, SCIPcutsTightenCoefficients(), SCIPproofsetGetNVars(), SCIPsetDebugMsg, SCIPsetInfinity(), and SCIP_ProofSet::vals.

    Referenced by separateAlternativeProofs(), and tightenDualproof().

    ◆ separateAlternativeProofs()

    static SCIP_RETCODE separateAlternativeProofs ( SCIP_CONFLICT conflict,
    SCIP_SET set,
    SCIP_STAT stat,
    SCIP_PROB transprob,
    SCIP_TREE tree,
    BMS_BLKMEM blkmem,
    SCIP_AGGRROW proofrow,
    SCIP_Real curvarlbs,
    SCIP_Real curvarubs,
    SCIP_CONFTYPE  conflicttype 
    )
    static

    try to generate alternative proofs by applying subadditive functions

    Parameters
    conflictconflict analysis data
    setglobal SCIP settings
    statdynamic SCIP statistics
    transprobtransformed problem
    treetree data
    blkmemblock memory
    proofrowproof rows data
    curvarlbscurrent lower bounds of active problem variables
    curvarubscurrent upper bounds of active problem variables
    conflicttypetype of the conflict

    Definition at line 1358 of file conflict_dualproofanalysis.c.

    References ALLOWLOCAL, BOUNDSWITCH, conflictInsertProofset(), SCIP_ProofSet::conflicttype, MAX, MAXFRAC, MINFRAC, NULL, POSTPROCESS, proofsetAddSparseData(), proofsetCreate(), SCIP_Bool, SCIP_CALL, SCIP_CONFTYPE_ALTBNDPROOF, SCIP_CONFTYPE_ALTINFPROOF, SCIP_CONFTYPE_INFEASLP, SCIP_OKAY, SCIP_Real, SCIPaggrRowCalcEfficacyNorm(), SCIPaggrRowGetInds(), SCIPaggrRowGetMinActivity(), SCIPaggrRowGetNNz(), SCIPaggrRowGetProbvarValue(), SCIPaggrRowGetRhs(), SCIPcalcFlowCover(), SCIPcreateSol(), SCIPcutGenerationHeuristicCMIR(), SCIPfreeSol(), SCIPprobGetNVars(), SCIPprobGetVars(), SCIPproofsetFree(), SCIPsetAllocBufferArray, SCIPsetFreeBufferArray, SCIPsetInfinity(), SCIPsetIsPositive(), SCIPsolSetVal(), SCIPvarGetAvgSol(), tightenCoefficients(), and VARTYPEUSEVBDS.

    Referenced by tightenDualproof().

    ◆ tightenDualproof()

    static SCIP_RETCODE tightenDualproof ( SCIP_CONFLICT conflict,
    SCIP_SET set,
    SCIP_STAT stat,
    BMS_BLKMEM blkmem,
    SCIP_PROB transprob,
    SCIP_TREE tree,
    SCIP_AGGRROW proofrow,
    int  validdepth,
    SCIP_Real curvarlbs,
    SCIP_Real curvarubs,
    SCIP_Bool  initialproof 
    )
    static

    tighten a given infeasibility proof a^Tx <= b with minact > b w.r.t. local bounds

    1) Apply cut generating functions

    • c-MIR
    • Flow-cover
    • TODO: implement other subadditive functions 2) Remove continuous variables contributing with its global bound
    • TODO: implement a variant of non-zero-cancellation
    Parameters
    conflictconflict analysis data
    setglobal SCIP settings
    statdynamic SCIP statistics
    blkmemblock memory
    transprobtransformed problem
    treetree data
    proofrowaggregated row representing the proof
    validdepthdepth where the proof is valid
    curvarlbscurrent lower bounds of active problem variables
    curvarubscurrent upper bounds of active problem variables
    initialproofdo we analyze the initial reason of infeasibility?

    Definition at line 1489 of file conflict_dualproofanalysis.c.

    References conflictInsertProofset(), SCIP_Conflict::conflictset, SCIP_ConflictSet::conflicttype, SCIP_ProofSet::conflicttype, debugPrintViolationInfo, eps, FALSE, getMaxActivity(), SCIP_ProofSet::inds, MIN, SCIP_ProofSet::nnz, NULL, SCIP_Conflict::proofset, proofsetAddAggrrow(), proofsetCancelVarWithBound(), proofsetClear(), proofsetCreate(), proofsetGetInds(), proofsetGetVals(), SCIP_ProofSet::rhs, SCIP_Bool, SCIP_CALL, SCIP_CONFTYPE_ALTBNDPROOF, SCIP_CONFTYPE_ALTINFPROOF, SCIP_CONFTYPE_BNDEXCEEDING, SCIP_CONFTYPE_INFEASLP, SCIP_OKAY, SCIP_Real, SCIPaggrRowGetInds(), SCIPaggrRowGetMinActivity(), SCIPaggrRowGetNNz(), SCIPaggrRowGetRhs(), SCIPprobGetVars(), SCIPproofsetFree(), SCIPproofsetGetNVars(), SCIPsetDebugMsg, SCIPsetIsEQ(), SCIPsetIsInfinity(), SCIPsetIsZero(), SCIPvarGetLbGlobal(), SCIPvarGetName(), SCIPvarGetProbindex(), SCIPvarGetUbGlobal(), SCIPvarIsBinary(), SCIPvarIsIntegral(), SCIPvarIsNonimpliedIntegral(), separateAlternativeProofs(), tightenCoefficients(), SCIP_ProofSet::validdepth, and SCIP_ProofSet::vals.

    Referenced by SCIPconflictAnalyzeDualProof().

    ◆ SCIPconflictAnalyzeDualProof()

    SCIP_RETCODE SCIPconflictAnalyzeDualProof ( SCIP_CONFLICT conflict,
    SCIP_SET set,
    SCIP_STAT stat,
    SCIP_EVENTFILTER eventfilter,
    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 
    )

    perform conflict analysis based on a dual unbounded ray

    given an aggregation of rows lhs <= a^Tx such that lhs > maxactivity. if the constraint has size one we add a bound change instead of the constraint.

    Parameters
    conflictconflict analysis data
    setglobal SCIP settings
    statdynamic SCIP statistics
    eventfilterglobal event filter
    blkmemblock memory
    origproboriginal problem
    transprobtransformed problem
    treetree data
    reoptreoptimization data
    lpLP data
    proofrowaggregated row representing the proof
    validdepthvalid depth of the dual proof
    curvarlbscurrent lower bounds of active problem variables
    curvarubscurrent upper bounds of active problem variables
    initialproofdo we analyze the initial reason of infeasibility?
    globalinfeasiblepointer to store whether global infeasibility could be proven
    successpointer to store success result

    Definition at line 1682 of file conflict_dualproofanalysis.c.

    References FALSE, SCIP_Conflict::ndualproofsinfsuccess, NULL, SCIP_Tree::path, SCIP_Bool, SCIP_CALL, SCIP_OKAY, SCIP_Real, SCIPaggrRowGetMinActivity(), SCIPaggrRowGetNNz(), SCIPaggrRowGetRhs(), SCIPnodeCutoff(), SCIPsetDebugMsg, SCIPsetIsFeasLE(), SCIPtreeGetFocusDepth(), tightenDualproof(), and TRUE.

    Referenced by conflictAnalyzeLP(), and SCIPrunBoundHeuristic().