cons_pseudoboolean.c

Go to the documentation of this file.

/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
/*                                                                           */
/*                  This file is part of the program and library             */
/*         SCIP --- Solving Constraint Integer Programs                      */
/*                                                                           */
/*    Copyright (C) 2002-2022 Konrad-Zuse-Zentrum                            */
/*                            fuer Informationstechnik Berlin                */
/*                                                                           */
/*  SCIP is distributed under the terms of the ZIB Academic License.         */
/*                                                                           */
/*  You should have received a copy of the ZIB Academic License              */
/*  along with SCIP; see the file COPYING. If not visit scipopt.org.         */
/*                                                                           */
/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */

/**@file   cons_pseudoboolean.c
 * @ingroup DEFPLUGINS_CONS
 * @brief  constraint handler for pseudo Boolean constraints
 * @author Gerald Gamrath
 * @author Stefan Heinz
 * @author Michael Winkler
 *
 *
 * The constraint handler deals with pseudo Boolean constraints. These are constraints of the form
 * \f[
 * \mbox{lhs} \leq \sum_{k=0}^m c_k \cdot x_k  +  \sum_{i=0}^n c_i \cdot \prod_{j \in I_i} x_j \leq \mbox{rhs}
 * \f]
 * where all x are binary and all c are integer
 *
 * @todo Add eventhandling.
 */

/*---+----1----+----2----+----3----+----4----+----5----+----6----+----7----+----8----+----9----+----0----+----1----+----2*/

#include "blockmemshell/memory.h"
#include "scip/cons_and.h"
#include "scip/cons_indicator.h"
#include "scip/cons_knapsack.h"
#include "scip/cons_linear.h"
#include "scip/cons_logicor.h"
#include "scip/cons_pseudoboolean.h"
#include "scip/cons_setppc.h"
#include "scip/cons_xor.h"
#include "scip/debug.h"
#include "scip/pub_cons.h"
#include "scip/pub_message.h"
#include "scip/pub_misc.h"
#include "scip/pub_misc_sort.h"
#include "scip/pub_var.h"
#include "scip/scip_cons.h"
#include "scip/scip_copy.h"
#include "scip/scip_general.h"
#include "scip/scip_mem.h"
#include "scip/scip_message.h"
#include "scip/scip_numerics.h"
#include "scip/scip_param.h"
#include "scip/scip_prob.h"
#include "scip/scip_sol.h"
#include "scip/scip_var.h"
#include <string.h>

#ifdef WITHEQKNAPSACK
#include "scip/cons_eqknapsack.h"
#endif

/* constraint handler properties */
#define CONSHDLR_NAME          "pseudoboolean"
#define CONSHDLR_DESC          "constraint handler dealing with pseudo Boolean constraints"
#define CONSHDLR_ENFOPRIORITY  -1000000 /**< priority of the constraint handler for constraint enforcing */
#define CONSHDLR_CHECKPRIORITY -5000000 /**< priority of the constraint handler for checking feasibility */
#define CONSHDLR_EAGERFREQ          100 /**< frequency for using all instead of only the useful constraints in separation,
                                              *   propagation and enforcement, -1 for no eager evaluations, 0 for first only */
#define CONSHDLR_MAXPREROUNDS        -1 /**< maximal number of presolving rounds the constraint handler participates in (-1: no limit) */
#define CONSHDLR_NEEDSCONS         TRUE /**< should the constraint handler be skipped, if no constraints are available? */

#define CONSHDLR_PRESOLTIMING            SCIP_PRESOLTIMING_MEDIUM /**< presolving timing of the constraint handler (fast, medium, or exhaustive) */

#define DEFAULT_DECOMPOSENORMALPBCONS FALSE /**< decompose all normal pseudo boolean constraint into a "linear" constraint and "and" constraints */
#define DEFAULT_DECOMPOSEINDICATORPBCONS TRUE /**< decompose all indicator pseudo boolean constraint into a "linear" constraint and "and" constraints */

#define DEFAULT_SEPARATENONLINEAR  TRUE /**< if decomposed, should the nonlinear constraints be separated during LP processing */
#define DEFAULT_PROPAGATENONLINEAR TRUE /**< if decomposed, should the nonlinear constraints be propagated during node processing */
#define DEFAULT_REMOVABLENONLINEAR TRUE /**< if decomposed, should the nonlinear constraints be removable */
#define USEINDICATOR               TRUE
#define NONLINCONSUPGD_PRIORITY   60000 /**< priority of upgrading nonlinear constraints */

/* remove this line to compile the upgrade from nonlinear to pseudoboolean constraints */
#undef NONLINCONSUPGD_PRIORITY  /*lint !e750*/

/*
 * Data structures
 */
#define HASHSIZE_PSEUDOBOOLEANNONLINEARTERMS 500 /**< minimal size of hash table in and constraint tables */


/* - create special linear(knapsack, setppc, logicor, (eqknapsack)) and and-constraints with check flags FALSE, to
 *   get smaller amount of locks on the term variables, do all presolving ...?! in these constraint handlers
 *
 * - do the checking here, lock and-resultants in both directions and all and-variables according to their
 *   coefficients and sides of the constraint,
 *   @note this only works if the and-resultant has no objective cofficient, otherwise we need to lock variables also in both directions
 *
 * - need to keep and constraint pointer for special propagations like if two ands are due to their variables in
 *   one clique, add this cliques of and-resultants
 *
 * - do special presolving like on instance :
 * check/IP/PseudoBoolean/normalized-PB07/OPT-SMALLINT-NLC/submittedPB07/manquinho/bsg/normalized-bsg_1000_25_1.opb.gz
 *
 *  there exist constraint like:        1 x1 x2 + 1 x1 x3 + 1 x1 x4 + 1 x1 x5 <= 1 ;
 *  which "equals" a linear constraint: 3 x1 + x2 + x3 + x4 + x5 <= 4 ;
 *
 *  in more general terms:                     1 x1 x2 x3 x4 + 1 x1 x2 x5 x6 x7 + 1 x1 x2 x8 x9 <= 1 ;
 *  which "equals" a pseudoboolean constraint: 2 x1 + 2 x2 + 1 x3 x4 + 1 x5 x6 x7 + 1 x8 x9 <= 5 ;
 *
 *  in an even more general terms:             5 x1 x2 x3 x4 + 1 x1 x2 x5 x6 x7 + 1 x1 x2 x8 x9 <= 6 ;
 *            equals(should the knapsack do)   1 x1 x2 x3 x4 + 1 x1 x2 x5 x6 x7 + 1 x1 x2 x8 x9 <= 2 ;
 *  which "equals" a pseudoboolean constraint: 2 x1 + 2 x2 + 1 x3 x4 + 1 x5 x6 x7 + 1 x8 x9 <= 6 ;
 *  (         without knapsack                 7 x1 + 7 x2 + 5 x3 x4 + 1 x5 x6 x7 + 1 x8 x9 <= 20 ; )
 *
 *  another special case :                     1 x1 x2 x3 + 1 x1 x2 x4 + 1 x5 x6 <= 1 ;
 *  which "equals" a pseudoboolean constraint: 2 x1 + 2 x2 + 1 x3 + 1 x4 + 1 x5 x6 <= 5 ;
 *  which "equals" a pseudoboolean constraint: 4 x1 + 4 x2 + 2 x3 + 2 x4 + 1 x5 + 1 x6 <= 10 ;
 *
 *  another special case :                     1 x1 x2 + 1 x1 x3 + 2 x4 x5 <= 3 ;
 *  which "equals" a pseudoboolean constraint: 2 x1 + 1 x2 + 1 x3 + 2 x4 x5 <= 5 ;
 *  which "equals" a pseudoboolean constraint: 2 x1 + 1 x2 + 1 x3 + 1 x4 + 1 x5 <= 5 ;
 */
/* @todo - in and-constraint better count nfixed zeros in both directions and maybe nfixedones for better propagation
 *
 *       - do better conflict analysis by choosing the earliest fixed variable which led to a conflict instead of maybe
 *         best coefficient or create more conflicts by using all to zero fixed variables one by one
 *
 *       - how to make sure that we aggregate in a right way, when aggregating a resultant and a "normal" variable,
 *         maybe add in SCIPaggregateVars a check for original variables, to prefer them if the variable type is the
 *         same; probably it would be better too if we would aggregate two resultants that the one with less variables
 *         inside the and-constraint will stay active
 *
 * @note since product resultants are artificial, we do not care for their solution value, but this can lead to fixation
 *       of the resultant not representing the product, in 'optimization mode' we do not care, but this might make
 *       solution debugging complicated
 */

/** and-constraint data object */
struct ConsAndData
{
   SCIP_CONS*            cons;                /**< pointer to the and-constraint of this 'term' of variables */
   SCIP_CONS*            origcons;            /**< pointer to the original and-constraint of this 'term' of variables
                                               *   only after problem was transformed, NULL otherwise */
   SCIP_VAR**            vars;                /**< all and-constraint variables */
   int                   nvars;               /**< number of all and-constraint variables */
   int                   svars;               /**< size for all and-constraint variables */
   SCIP_VAR**            newvars;             /**< new variables in this presolving round */
   int                   nnewvars;            /**< number of new variables in this presolving round */
   int                   snewvars;            /**< size of new variables in this presolving round */
   int                   noriguses;           /**< how often is this data in used by original constraints */
   int                   nuses;               /**< how often is this data in used by transformed constraints */
   unsigned int          istransformed:1;     /**< is transformed data active */
   unsigned int          isoriginal:1;        /**< is original data active */
};
typedef struct ConsAndData CONSANDDATA;

/** constraint data for pseudoboolean constraints */
struct SCIP_ConsData
{
   SCIP_Real             lhs;                /**< left hand side of constraint */
   SCIP_Real             rhs;                /**< right hand side of constraint */

   SCIP_CONS*            lincons;            /**< linear constraint which represents this pseudoboolean constraint */
   SCIP_LINEARCONSTYPE   linconstype;        /**< type of linear constraint which represents this pseudoboolean constraint */
   int                   nlinvars;           /**< number of linear variables (without and-resultants) */

   CONSANDDATA**         consanddatas;       /**< array of and-constraints-data-objects sorted after index of
                                              *   and-resultant of corresponding and-constraint */
   SCIP_Real*            andcoefs;           /**< array of coefficients for and-constraints of
                                              *   and-constraints-data-objects
                                              *   (changes during presolving, needs to be updated in every presolving
                                              *   round) */
   SCIP_Bool*            andnegs;            /**< array of negation status for and-constraints of
                                              *   and-constraints-data-objects
                                              *   (changes during presolving, needs to be updated in every presolving
                                              *   round) */
   int                   nconsanddatas;      /**< number of and-constraints-data-objects */
   int                   sconsanddatas;      /**< size of and-constraints-data-objects array */

   SCIP_VAR*             intvar;             /**< a artificial variable which was added only for the objective function,
                                              *   if this variable is not NULL this constraint (without this integer
                                              *   variable) describes the objective function */

   SCIP_VAR*             indvar;             /**< indicator variable if it's a soft constraint, or NULL */
   SCIP_Real             weight;             /**< weight of the soft constraint, if it is one */

   unsigned int          issoftcons:1;       /**< is this a soft constraint */
   unsigned int          changed:1;          /**< was constraint changed? */
   unsigned int          propagated:1;       /**< is constraint already propagated? */
   unsigned int          presolved:1;        /**< is constraint already presolved? */
   unsigned int          cliquesadded:1;     /**< were the cliques of the constraint already extracted? */
   unsigned int          upgradetried:1;     /**< was constraint upgrading already tried */
};

/** constraint handler data */
struct SCIP_ConshdlrData
{
   CONSANDDATA**         allconsanddatas;    /**< array of all and-constraint data objects inside the whole problem,
                                              *   created via this constraint handler */
   int                   nallconsanddatas;   /**< number of all and-constraint data objects inside the whole problem,
                                              *   created via this constraint handler */
   int                   sallconsanddatas;   /**< size of all and-constraint data objects inside the whole problem,
                                              *   created via this constraint handler */
   SCIP_HASHTABLE*       hashtable;          /**< hash table for all and-constraint data objects */
   int                   hashtablesize;      /**< size for hash table for all and-constraint data objects */

   SCIP_HASHMAP*         hashmap;            /**< hash map for mapping all resultant to and-constraint */
   int                   hashmapsize;        /**< size for hash map for mapping all resultant to and-constraint */

   SCIP_Bool             decomposenormalpbcons;/**< decompose the pseudo boolean constraint into a "linear" constraint and "and" constraints */
   SCIP_Bool             decomposeindicatorpbcons;/**< decompose the indicator pseudo boolean constraint into a "linear" constraint and "and" constraints */
   SCIP_Bool             inithashmapandtable;/**< flag to store if the hashmap and -table is initialized */
   int                   nlinconss;          /**< for counting number of created linear constraints */
   int                   noriguses;          /**< how many consanddata objects are used by original constraints */
};

/*
 * Local methods
 */


/** comparison method for sorting consanddatas according to the index of their corresponding resultant variables, if a
 *  consanddata object is delete it is handled like it has an inactive resultant, so this will be put in front while
 *  sorting
 */
static
SCIP_DECL_SORTPTRCOMP(resvarCompWithInactive)
{
   CONSANDDATA* consanddata1;
   CONSANDDATA* consanddata2;

   consanddata1 = (CONSANDDATA*)elem1;
   consanddata2 = (CONSANDDATA*)elem2;

   /* check if and constraint data object is still valid */
   if( !consanddata1->istransformed )
   {
      if( !consanddata2->istransformed )
      {
         return 0;
      }
      else
         return -1;
   }
   else if( !consanddata2->istransformed )
      return +1;

   assert(consanddata1->cons != NULL);
   assert(consanddata2->cons != NULL);

   /* check if and constraint is still active */
   if( SCIPconsIsDeleted(consanddata1->cons) )
   {
      if( SCIPconsIsDeleted(consanddata2->cons) )
      {
         return 0;
      }
      else
         return -1;
   }
   else if( SCIPconsIsDeleted(consanddata2->cons) )
      return +1;
   else
   {
      SCIP_VAR* var1;
      SCIP_VAR* var2;

      /* hack with setting the first pointer to NULL */
      var1 = SCIPgetResultantAnd(NULL, consanddata1->cons);
      var2 = SCIPgetResultantAnd(NULL, consanddata2->cons);

      assert(var1 != NULL);
      assert(var2 != NULL);

      if( SCIPvarGetIndex(var1) < SCIPvarGetIndex(var2) )
         return -1;
      else if( SCIPvarGetIndex(var1) > SCIPvarGetIndex(var2) )
         return +1;
      else
      {
         assert(var1 == var2);
         return 0;
      }
   }
}

/** gets the key of the given element */
static
SCIP_DECL_HASHGETKEY(hashGetKeyAndConsDatas)
{  /*lint --e{715}*/
   /* the key is the element itself */
   return elem;
}

/** returns TRUE iff both keys are equal; two non-linear terms are equal if they have the same variables */
static
SCIP_DECL_HASHKEYEQ(hashKeyEqAndConsDatas)
{
#ifndef NDEBUG
   SCIP* scip;
#endif
   CONSANDDATA* cdata1;
   CONSANDDATA* cdata2;
   int v;

   cdata1 = (CONSANDDATA*)key1;
   cdata2 = (CONSANDDATA*)key2;

#ifndef NDEBUG
   scip = (SCIP*)userptr;
#endif
   assert(scip != NULL);
   assert(cdata1 != NULL);
   assert(cdata2 != NULL);
   assert(cdata1->vars != NULL);
   assert(cdata1->nvars > 1);
   assert(cdata2->vars != NULL);
   assert(cdata2->nvars > 1);

#ifndef NDEBUG
   /* check that cdata1 variables are sorted */
   for( v = cdata1->nvars - 1; v > 0; --v )
      assert(SCIPvarGetIndex(cdata1->vars[v]) >= SCIPvarGetIndex(cdata1->vars[v - 1]));
   /* check that cdata2 variables are sorted */
   for( v = cdata2->nvars - 1; v > 0; --v )
      assert(SCIPvarGetIndex(cdata2->vars[v]) >= SCIPvarGetIndex(cdata2->vars[v - 1]));
#endif

   /* checks trivial case */
   if( cdata1->nvars != cdata2->nvars )
      return FALSE;

   /* checks trivial case */
   if( cdata1->cons != NULL && cdata2->cons != NULL && cdata1->cons != cdata2->cons )
      return FALSE;

   /* check each variable in both cdatas for equality */
   for( v = cdata1->nvars - 1; v >= 0; --v )
   {
      assert(cdata1->vars[v] != NULL);
      assert(cdata2->vars[v] != NULL);

      /* tests if variables are equal */
      if( cdata1->vars[v] != cdata2->vars[v] )
      {
         assert(SCIPvarCompare(cdata1->vars[v], cdata2->vars[v]) == 1 ||
            SCIPvarCompare(cdata1->vars[v], cdata2->vars[v]) == -1);
         return FALSE;
      }
      assert(SCIPvarCompare(cdata1->vars[v], cdata2->vars[v]) == 0);
   }

   return TRUE;
}

/** returns the hash value of the key */
static
SCIP_DECL_HASHKEYVAL(hashKeyValAndConsDatas)
{  /*lint --e{715}*/
   CONSANDDATA* cdata;
   int minidx;
   int mididx;
   int maxidx;

   cdata = (CONSANDDATA*)key;

   assert(cdata != NULL);
   assert(cdata->vars != NULL);
   assert(cdata->nvars > 1);
#ifndef NDEBUG
   {
      /* check that these variables are sorted */
      int v;
      for( v = cdata->nvars - 1; v > 0; --v )
         assert(SCIPvarGetIndex(cdata->vars[v]) >= SCIPvarGetIndex(cdata->vars[v - 1]));
   }
#endif

   minidx = SCIPvarGetIndex(cdata->vars[0]);
   mididx = SCIPvarGetIndex(cdata->vars[cdata->nvars / 2]);
   maxidx = SCIPvarGetIndex(cdata->vars[cdata->nvars - 1]);
   assert(minidx >= 0 && minidx <= maxidx);

   return SCIPhashFour(cdata->nvars, minidx, mididx, maxidx);
}

/** initializes the hashmap and -table used in this constraint handler data for artificial variables and specific
 *  and-constraint data objects
 */
static
SCIP_RETCODE inithashmapandtable(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONSHDLRDATA**   conshdlrdata        /**< pointer to store the constraint handler data */
   )
{
   if( ((*conshdlrdata)->inithashmapandtable) )
   {
      assert((*conshdlrdata)->hashtable != NULL);
      assert((*conshdlrdata)->hashmap != NULL);

      return SCIP_OKAY;
   }

   assert((*conshdlrdata)->hashtable == NULL);
   assert((*conshdlrdata)->hashmap == NULL);

   /* create a hash table for and-constraint data objects */
   (*conshdlrdata)->hashtablesize = HASHSIZE_PSEUDOBOOLEANNONLINEARTERMS;
   SCIP_CALL( SCIPhashtableCreate(&((*conshdlrdata)->hashtable), SCIPblkmem(scip), (*conshdlrdata)->hashtablesize,
         hashGetKeyAndConsDatas, hashKeyEqAndConsDatas, hashKeyValAndConsDatas, (void*) scip) );

   /* create a hash table for and-resultant to and-constraint data objects */
   (*conshdlrdata)->hashmapsize = HASHSIZE_PSEUDOBOOLEANNONLINEARTERMS;
   SCIP_CALL( SCIPhashmapCreate(&((*conshdlrdata)->hashmap), SCIPblkmem(scip), (*conshdlrdata)->hashmapsize) );

   (*conshdlrdata)->inithashmapandtable = TRUE;

   return SCIP_OKAY;
}

/** creates constraint handler data for pseudo boolean constraint handler */
static
SCIP_RETCODE conshdlrdataCreate(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONSHDLRDATA**   conshdlrdata        /**< pointer to store the constraint handler data */
   )
{
   assert(scip != NULL);
   assert(conshdlrdata != NULL);

   SCIP_CALL( SCIPallocBlockMemory(scip, conshdlrdata) );

   (*conshdlrdata)->allconsanddatas = NULL;
   (*conshdlrdata)->nallconsanddatas = 0;
   (*conshdlrdata)->sallconsanddatas = 10;

   SCIP_CALL( SCIPallocBlockMemoryArray(scip, &((*conshdlrdata)->allconsanddatas), (*conshdlrdata)->sallconsanddatas ) );

   /* set hashmap and -table to NULL, mark them as uninitialized */
   (*conshdlrdata)->inithashmapandtable = FALSE;
   (*conshdlrdata)->hashtable = NULL;
   (*conshdlrdata)->hashtablesize = 0;
   (*conshdlrdata)->hashmap = NULL;
   (*conshdlrdata)->hashmapsize = 0;

   /* for constraint names count number of created constraints */
   (*conshdlrdata)->nlinconss = 0;

   /* initializes how many consanddata objects are used by original constraints */
   (*conshdlrdata)->noriguses = 0;

   return SCIP_OKAY;
}


/** frees constraint handler data for pseudo boolean constraint handler */
static
SCIP_RETCODE conshdlrdataFree(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONSHDLRDATA**   conshdlrdata        /**< pointer to the constraint handler data */
   )
{
   assert(scip != NULL);
   assert(conshdlrdata != NULL);
   assert(*conshdlrdata != NULL);
   assert((*conshdlrdata)->nallconsanddatas == 0);

   /* free hash table if necessary */
   if( (*conshdlrdata)->inithashmapandtable )
   {
      SCIPhashmapFree(&((*conshdlrdata)->hashmap));
      (*conshdlrdata)->hashmapsize = 0;
      SCIPhashtableFree(&((*conshdlrdata)->hashtable));
      (*conshdlrdata)->hashtablesize = 0;
   }
   else
   {
      assert((*conshdlrdata)->hashmap == NULL);
      assert((*conshdlrdata)->hashtable == NULL);
   }
   (*conshdlrdata)->inithashmapandtable = FALSE;

   /* clear array for all consanddata objects */
   SCIPfreeBlockMemoryArray(scip, &((*conshdlrdata)->allconsanddatas), (*conshdlrdata)->sallconsanddatas );

   (*conshdlrdata)->allconsanddatas = NULL;
   (*conshdlrdata)->nallconsanddatas = 0;
   (*conshdlrdata)->sallconsanddatas = 0;

   SCIPfreeBlockMemory(scip, conshdlrdata);

   return SCIP_OKAY;
}

/** gets number of variables in linear constraint */
static
SCIP_RETCODE getLinearConsNVars(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< linear constraint */
   SCIP_LINEARCONSTYPE const constype,       /**< linear constraint type */
   int*const             nvars               /**< pointer to store number variables of linear constraint */
   )
{
   assert(scip != NULL);
   assert(cons != NULL);
   assert(nvars != NULL);

   /* determine for each special linear constranit all variables and coefficients */
   switch( constype )
   {
   case SCIP_LINEARCONSTYPE_LINEAR:
      *nvars = SCIPgetNVarsLinear(scip, cons);
      break;
   case SCIP_LINEARCONSTYPE_LOGICOR:
      *nvars = SCIPgetNVarsLogicor(scip, cons);
      break;
   case SCIP_LINEARCONSTYPE_KNAPSACK:
      *nvars = SCIPgetNVarsKnapsack(scip, cons);
      break;
   case SCIP_LINEARCONSTYPE_SETPPC:
      *nvars = SCIPgetNVarsSetppc(scip, cons);
      break;
#ifdef WITHEQKNAPSACK
   case SCIP_LINEARCONSTYPE_EQKNAPSACK:
      *nvars = SCIPgetNVarsEQKnapsack(scip, cons);
      break;
#endif
   case SCIP_LINEARCONSTYPE_INVALIDCONS:
   default:
      SCIPerrorMessage("unknown linear constraint type\n");
      return SCIP_INVALIDDATA;
   }

   return SCIP_OKAY;
}


/** gets sides of linear constraint */
static
SCIP_RETCODE getLinearConsSides(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< linear constraint */
   SCIP_LINEARCONSTYPE const constype,       /**< linear constraint type */
   SCIP_Real*const       lhs,                /**< pointer to store left hand side of linear constraint */
   SCIP_Real*const       rhs                 /**< pointer to store right hand side of linear constraint */
   )
{
   SCIP_SETPPCTYPE type;

   switch( constype )
   {
   case SCIP_LINEARCONSTYPE_LINEAR:
      *lhs = SCIPgetLhsLinear(scip, cons);
      *rhs = SCIPgetRhsLinear(scip, cons);
      break;
   case SCIP_LINEARCONSTYPE_LOGICOR:
      *lhs = 1.0;
      *rhs = SCIPinfinity(scip);
      break;
   case SCIP_LINEARCONSTYPE_KNAPSACK:
      *lhs = -SCIPinfinity(scip);
      *rhs = SCIPgetCapacityKnapsack(scip, cons);
      break;
   case SCIP_LINEARCONSTYPE_SETPPC:
      type = SCIPgetTypeSetppc(scip, cons);

      switch( type )
      {
      case SCIP_SETPPCTYPE_PARTITIONING:
         *lhs = 1.0;
         *rhs = 1.0;
         break;
      case SCIP_SETPPCTYPE_PACKING:
         *lhs = -SCIPinfinity(scip);
         *rhs = 1.0;
         break;
      case SCIP_SETPPCTYPE_COVERING:
         *lhs = 1.0;
         *rhs = SCIPinfinity(scip);
         break;
      default:
         SCIPerrorMessage("unknown setppc type\n");
         return SCIP_INVALIDDATA;
      }
      break;
#ifdef WITHEQKNAPSACK
   case SCIP_LINEARCONSTYPE_EQKNAPSACK:
      *lhs = SCIPgetCapacityEQKnapsack(scip, cons);
      *rhs = *lhs;
      break;
#endif
   case SCIP_LINEARCONSTYPE_INVALIDCONS:
   default:
      SCIPerrorMessage("unknown linear constraint type\n");
      return SCIP_INVALIDDATA;
   }

   return SCIP_OKAY;
}

/** gets variables and coefficients of linear constraint */
static
SCIP_RETCODE getLinearConsVarsData(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< linear constraint */
   SCIP_LINEARCONSTYPE const constype,       /**< linear constraint type */
   SCIP_VAR**const       vars,               /**< array to store sorted (after indices) variables of linear constraint */
   SCIP_Real*const       coefs,              /**< array to store coefficient of linear constraint, or NULL */
   int*const             nvars               /**< pointer to store number variables of linear constraint */
   )
{
   SCIP_VAR** linvars;
   int v;

   assert(scip != NULL);
   assert(cons != NULL);
   assert(vars != NULL);
   assert(nvars != NULL);

   /* determine for each special linear constrait all variables and coefficients */
   switch( constype )
   {
   case SCIP_LINEARCONSTYPE_LINEAR:
   {
      SCIP_Real* lincoefs;

      *nvars = SCIPgetNVarsLinear(scip, cons);
      linvars = SCIPgetVarsLinear(scip, cons);

      if( coefs != NULL )
      {
         lincoefs = SCIPgetValsLinear(scip, cons);

         for( v = 0; v < *nvars; ++v )
         {
            vars[v] = linvars[v];
            coefs[v] = lincoefs[v];
         }
      }
      else
      {
         for( v = 0; v < *nvars; ++v )
            vars[v] = linvars[v];
      }

      break;
   }
   case SCIP_LINEARCONSTYPE_LOGICOR:
      *nvars = SCIPgetNVarsLogicor(scip, cons);
      linvars = SCIPgetVarsLogicor(scip, cons);
      assert( linvars != NULL );

      if( coefs != NULL )
      {
         for( v = 0; v < *nvars; ++v )
         {
            vars[v] = linvars[v];
            coefs[v] = 1.0;
         }
      }
      else
      {
         for( v = 0; v < *nvars; ++v )
            vars[v] = linvars[v];
      }

      break;
   case SCIP_LINEARCONSTYPE_KNAPSACK:
   {
      SCIP_Longint* weights;

      *nvars = SCIPgetNVarsKnapsack(scip, cons);
      linvars = SCIPgetVarsKnapsack(scip, cons);
      assert( linvars != NULL );

      if( coefs != NULL )
      {
         weights = SCIPgetWeightsKnapsack(scip, cons);

         for( v = 0; v < *nvars; ++v )
         {
            vars[v] = linvars[v];
            coefs[v] = (SCIP_Real) weights[v];
         }
      }
      else
      {
         for( v = 0; v < *nvars; ++v )
            vars[v] = linvars[v];
      }

      break;
   }
   case SCIP_LINEARCONSTYPE_SETPPC:
      *nvars = SCIPgetNVarsSetppc(scip, cons);
      linvars = SCIPgetVarsSetppc(scip, cons);
      assert( linvars != NULL );

      if( coefs != NULL )
      {
         for( v = 0; v < *nvars; ++v )
         {
            vars[v] = linvars[v];
            coefs[v] = 1.0;
         }
      }
      else
      {
         for( v = 0; v < *nvars; ++v )
            vars[v] = linvars[v];
      }

      break;
#ifdef WITHEQKNAPSACK
   case SCIP_LINEARCONSTYPE_EQKNAPSACK:
   {
      SCIP_Longint* weights;

      *nvars = SCIPgetNVarsEQKnapsack(scip, cons);
      linvars = SCIPgetVarsEQKnapsack(scip, cons);
      assert( linvars != NULL );

      if( coefs != NULL )
      {
         weights = SCIPgetWeightsEQKnapsack(scip, cons);

         for( v = 0; v < *nvars; ++v )
         {
            vars[v] = linvars[v];
            coefs[v] = (SCIP_Real) weights[v];
         }
      }
      else
      {
         for( v = 0; v < *nvars; ++v )
            vars[v] = linvars[v];
      }

      break;
   }
#endif
   case SCIP_LINEARCONSTYPE_INVALIDCONS:
   default:
      SCIPerrorMessage("unknown linear constraint type\n");
      return SCIP_INVALIDDATA;
   }

   /* sort variables after indices */
   if( coefs != NULL )
   {
      SCIPsortPtrReal((void**)vars, coefs, SCIPvarComp, *nvars);
   }
   else
   {
      SCIPsortPtr((void**)vars, SCIPvarComp, *nvars);
   }

   return SCIP_OKAY;
}

/** calculate all not artificial linear variables and all artificial and-resultants which will be ordered like the
 *  'consanddatas' such that the and-resultant of the and-constraint is the and-resultant in the 'andress' array
 *  afterwards
 */
static
SCIP_RETCODE getLinVarsAndAndRess(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< pseudoboolean constraint */
   SCIP_VAR**const       vars,               /**< all variables of linear constraint */
   SCIP_Real*const       coefs,              /**< all coefficients of linear constraint, or NULL */
   int const             nvars,              /**< number of all variables of linear constraint */
   SCIP_VAR**const       linvars,            /**< array to store not and-resultant variables of linear constraint, or NULL */
   SCIP_Real*const       lincoefs,           /**< array to store coefficients of not and-resultant variables of linear
                                              *   constraint, or NULL */
   int*const             nlinvars,           /**< pointer to store number of not and-resultant variables, or NULL */
   SCIP_VAR**const       andress,            /**< array to store and-resultant variables of linear constraint, or NULL */
   SCIP_Real*const       andcoefs,           /**< array to store coefficients of and-resultant variables of linear
                                              *   constraint, or NULL */
   SCIP_Bool*const       andnegs,            /**< array to store negation status of and-resultant variables of linear
                                              *   constraint, or NULL */
   int*const             nandress            /**< pointer to store number of and-resultant variables, or NULL */
   )
{
   SCIP_CONSHDLR* conshdlr;
   SCIP_CONSHDLRDATA* conshdlrdata;
   int v;

   assert(scip != NULL);
   assert(cons != NULL);
   assert(vars != NULL);
   assert((linvars != NULL) == (nlinvars != NULL));
   assert((andress == NULL) || (nandress != NULL));
   assert((andcoefs != NULL) == (andnegs != NULL));
   assert((coefs != NULL) == ((lincoefs != NULL) || (andcoefs != NULL)));
   assert(linvars != NULL || andress != NULL);

   if( nlinvars != NULL )
      *nlinvars = 0;
   if( nandress != NULL )
      *nandress = 0;

   conshdlr = SCIPconsGetHdlr(cons);
   assert(conshdlr != NULL);
   conshdlrdata = SCIPconshdlrGetData(conshdlr);
   assert(conshdlrdata != NULL);
   assert(conshdlrdata->hashmap != NULL);

   /* @note it is necessary that the linear constraint is merged (not needed for negated variables) and sorted after
    *       indices
    */

#ifndef NDEBUG
   /* check that old variables are sorted */
   for( v = nvars - 1; v > 0; --v )
      assert(SCIPvarGetIndex(vars[v]) >= SCIPvarGetIndex(vars[v - 1]));
#endif

   /* split variables into original and artificial variables */
   for( v = 0; v < nvars; ++v )
   {
      SCIP_Bool hashmapentryexists;
      SCIP_VAR* hashmapvar;

      assert(vars[v] != NULL);

      hashmapentryexists = SCIPhashmapExists(conshdlrdata->hashmap, (void*)(vars[v]));

      if( !hashmapentryexists && SCIPvarIsNegated(vars[v]) )
      {
         hashmapvar = SCIPvarGetNegationVar(vars[v]);
         hashmapentryexists = SCIPhashmapExists(conshdlrdata->hashmap, (void*)(hashmapvar));
      }
      else
         hashmapvar = vars[v];

      /* if and resultant is not a resultant anymore (meaning the corresponding and-constraint was deleted/upgraded),
       * correct the flag and count this variable as normal linear variable
       */
      if( hashmapentryexists )
      {
         if( !SCIPconsIsOriginal(cons) )
         {
            CONSANDDATA* consanddata = (CONSANDDATA*) SCIPhashmapGetImage(conshdlrdata->hashmap, (void*)(hashmapvar));
            assert(consanddata != NULL);

            hashmapentryexists = (consanddata->istransformed);

            if( hashmapentryexists )
            {
               assert(consanddata->cons != NULL);
               hashmapentryexists = !SCIPconsIsDeleted(consanddata->cons);
            }
         }
      }

      if( !hashmapentryexists && linvars != NULL && nlinvars != NULL )
      {
         linvars[*nlinvars] = vars[v];
         if( lincoefs != NULL )
         {
            assert(coefs != NULL);
            lincoefs[*nlinvars] = coefs[v];
         }
         ++(*nlinvars);
      }
      else if( hashmapentryexists && nandress != NULL )
      {
         if( andress != NULL )
         {
            andress[*nandress] = hashmapvar;

            if( andcoefs != NULL )
            {
               assert(andnegs != NULL);
               assert(coefs != NULL);
               andcoefs[*nandress] = coefs[v];
               andnegs[*nandress] = (vars[v] != hashmapvar);
            }
         }
         ++(*nandress);
      }
   }

   /* @todo try to avoid sorting here */
   if( andress != NULL && nandress != NULL )
   {
      /* sort and resultants by their variable index */
      if( andcoefs != NULL )
      {
         assert(andnegs != NULL);
         SCIPsortPtrRealBool((void**)andress, andcoefs, andnegs, SCIPvarComp, *nandress);
      }
      else
      {
         SCIPsortPtr((void**)andress, SCIPvarComp, *nandress);
      }
   }

   return SCIP_OKAY;
}


#ifdef CHECK_CONSISTENCY
/** check constraint consistency */
static
void checkConsConsistency(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons                /**< pseudoboolean constraint */
   )
{
   SCIP_CONSDATA* consdata;
   SCIP_VAR** vars;
   SCIP_Real* coefs;
   int nvars;
   SCIP_VAR** linvars;
   SCIP_Real* lincoefs;
   int nlinvars;
   SCIP_VAR** andress;
   SCIP_Real* andcoefs;
   SCIP_Bool* andnegs;
   int nandress;
   SCIP_Bool* alreadyfound;
   SCIP_VAR* res;
   int c;
   int v;
   SCIP_Real newlhs;
   SCIP_Real newrhs;

   assert(scip != NULL);
   assert(cons != NULL);

   if( SCIPgetStage(scip) == SCIP_STAGE_FREETRANS )
      return;

   consdata = SCIPconsGetData(cons);
   assert(consdata != NULL);

   /* check standard pointers and sizes */
   assert(consdata->lincons != NULL);
   assert(!SCIPconsIsDeleted(consdata->lincons));
   assert(consdata->linconstype > SCIP_LINEARCONSTYPE_INVALIDCONS);
   assert(consdata->consanddatas != NULL);
   assert(consdata->nconsanddatas > 0);
   assert(consdata->nconsanddatas <= consdata->sconsanddatas);

   /* get sides of linear constraint */
   SCIP_CALL_ABORT( getLinearConsSides(scip, consdata->lincons, consdata->linconstype, &newlhs, &newrhs) );
   assert(!SCIPisInfinity(scip, newlhs));
   assert(!SCIPisInfinity(scip, -newrhs));
   assert(SCIPisLE(scip, newlhs, newrhs));
   assert(SCIPisEQ(scip, newrhs, consdata->rhs) || SCIPisEQ(scip, newrhs, -consdata->lhs));
   assert(SCIPisEQ(scip, newlhs, consdata->lhs) || SCIPisEQ(scip, newlhs, -consdata->rhs));

   /* check number of linear variables */
   SCIP_CALL_ABORT( getLinearConsNVars(scip, consdata->lincons, consdata->linconstype, &nvars) );
   assert(nvars == consdata->nlinvars + consdata->nconsanddatas);

   /* get temporary memory */
   SCIP_CALL_ABORT( SCIPallocBufferArray(scip, &vars, nvars) );
   SCIP_CALL_ABORT( SCIPallocBufferArray(scip, &coefs, nvars) );
   SCIP_CALL_ABORT( SCIPallocBufferArray(scip, &linvars, nvars) );
   SCIP_CALL_ABORT( SCIPallocBufferArray(scip, &lincoefs, nvars) );
   SCIP_CALL_ABORT( SCIPallocBufferArray(scip, &andress, nvars) );
   SCIP_CALL_ABORT( SCIPallocBufferArray(scip, &andcoefs, nvars) );
   SCIP_CALL_ABORT( SCIPallocBufferArray(scip, &andnegs, nvars) );
   SCIP_CALL_ABORT( SCIPallocClearBufferArray(scip, &alreadyfound, nvars) );

   /* get variables and coefficients */
   SCIP_CALL_ABORT( getLinearConsVarsData(scip, consdata->lincons, consdata->linconstype, vars, coefs, &nvars) );
   assert(nvars == 0 || (coefs != NULL));

   /* calculate all not artificial linear variables and all artificial and-resultants */
   SCIP_CALL_ABORT( getLinVarsAndAndRess(scip, cons, vars, coefs, nvars, linvars, lincoefs, &nlinvars,
         andress, andcoefs, andnegs, &nandress) );
   assert(nlinvars == consdata->nlinvars);
   assert(nandress == consdata->nconsanddatas);

   for( v = nandress - 1; v >= 0; --v )
   {
      SCIP_VAR* andresultant = andress[v];
      int nfound = 0;

      for( c = consdata->nconsanddatas - 1; c >= 0; --c )
      {
         assert(consdata->consanddatas[c] != NULL);
         if( consdata->consanddatas[c]->cons != NULL )
         {
            res = SCIPgetResultantAnd(scip, consdata->consanddatas[c]->cons);
            assert(res != NULL);

            if( res == andresultant && consdata->andnegs[c] == andnegs[v] && consdata->andcoefs[c] == andcoefs[v] )
            {
               /* resultant should be either active or a negated variable of an active one */
               assert(SCIPvarIsActive(res) || (SCIPvarIsNegated(res) && SCIPvarIsActive(SCIPvarGetNegationVar(res))));
               assert(!alreadyfound[c]);

               /* all and-resultants should be merged, so it is only allowed that each variable exists one time */
               alreadyfound[c] = TRUE;
               ++nfound;
               break;
            }
         }
      }
      assert(nfound == 1);
   }

   for( c = consdata->nconsanddatas - 1; c >= 0; --c )
   {
      assert(alreadyfound[c]);
   }

   /* free temporary memory */
   SCIPfreeBufferArray(scip, &alreadyfound);
   SCIPfreeBufferArray(scip, &andnegs);
   SCIPfreeBufferArray(scip, &andcoefs);
   SCIPfreeBufferArray(scip, &andress);
   SCIPfreeBufferArray(scip, &lincoefs);
   SCIPfreeBufferArray(scip, &linvars);
   SCIPfreeBufferArray(scip, &coefs);
   SCIPfreeBufferArray(scip, &vars);
}
#else
#define checkConsConsistency(scip, cons) /**/
#endif


/** transforming transformed consanddata object back to original space, if an corresponding original constraint exists,
 *  also clearing all transformed data, i.e. releasing transformed variables
 */
static
SCIP_RETCODE transformToOrig(
   SCIP*const            scip,               /**< SCIP data structure */
   CONSANDDATA*          consanddata,        /**< consanddata object */
   SCIP_CONSHDLRDATA*    conshdlrdata        /**< constraint handler data */
   )
{
   SCIP_VAR** tmpvars;
   SCIP_Bool origdata;
   int ntmpvars;
   int v;

   assert(scip != NULL);
   assert(consanddata != NULL);
   assert(conshdlrdata != NULL);

   origdata = TRUE;

   tmpvars = consanddata->vars;
   ntmpvars = consanddata->nvars;

   /* release all transformed variables */
   for( v = ntmpvars - 1; v >= 0; --v )
   {
      assert(tmpvars[v] != NULL);
      if( SCIPvarIsTransformed(tmpvars[v]) )
      {
         SCIP_CALL( SCIPreleaseVar(scip, &tmpvars[v]) );
         origdata = FALSE;
      }
   }

   tmpvars = consanddata->newvars;
   ntmpvars = consanddata->nnewvars;

   /* release all variables */
   for( v = ntmpvars - 1; v >= 0; --v )
   {
      assert(tmpvars[v] != NULL);
      if( SCIPvarIsTransformed(tmpvars[v]) )
      {
         SCIP_CALL( SCIPreleaseVar(scip, &tmpvars[v]) );
         origdata = FALSE;
      }
   }

   /* reinstall original data */
   if( !origdata || consanddata->nvars == 0 )
   {
      SCIPfreeBlockMemoryArrayNull(scip, &(consanddata->vars), consanddata->svars);
      SCIPfreeBlockMemoryArrayNull(scip, &(consanddata->newvars), consanddata->snewvars);

      consanddata->nuses = 0;
      consanddata->nvars = 0;
      consanddata->svars = 0;
      consanddata->nnewvars = 0;
      consanddata->snewvars = 0;
      consanddata->istransformed = FALSE;

      if( consanddata->noriguses > 0 )
      {
         assert(consanddata->origcons != NULL);
         assert(consanddata->isoriginal);

         assert(SCIPgetNVarsAnd(scip, consanddata->origcons) > 0);
         assert(SCIPgetVarsAnd(scip, consanddata->origcons) != NULL);
         consanddata->nvars = SCIPgetNVarsAnd(scip, consanddata->origcons);
         consanddata->svars = consanddata->nvars;

         if( consanddata->nvars > 0 )
         {
            SCIP_VAR** andvars = SCIPgetVarsAnd(scip, consanddata->origcons);

            SCIP_CALL( SCIPduplicateBlockMemoryArray(scip, &(consanddata->vars), andvars, consanddata->nvars) );

            /* sort variables */
            SCIPsortPtr((void**)(consanddata->vars), SCIPvarComp, consanddata->nvars);
         }

         /* check that the hash map and tabkle are still having all information */
         if( conshdlrdata->inithashmapandtable )
         {
            assert(conshdlrdata->hashmap != NULL);
            assert(conshdlrdata->hashtable != NULL);
            assert(SCIPgetResultantAnd(scip, consanddata->origcons) != NULL);
            assert(SCIPhashtableExists(conshdlrdata->hashtable, (void*)consanddata));
            assert(consanddata == (CONSANDDATA*)(SCIPhashtableRetrieve(conshdlrdata->hashtable, (void*)consanddata)));
            assert(SCIPhashmapExists(conshdlrdata->hashmap, (void*)SCIPgetResultantAnd(scip, consanddata->origcons)));
            assert(consanddata == (CONSANDDATA*)(SCIPhashmapGetImage(conshdlrdata->hashmap, (void*)SCIPgetResultantAnd(scip, consanddata->origcons))));
         }
      }
      else
         assert(consanddata->origcons == NULL);
   }
   else
   {
      assert(consanddata->nuses == 0);
      assert(consanddata->nnewvars == 0);
      assert(consanddata->snewvars == 0);
      assert(consanddata->newvars == NULL);

      consanddata->istransformed = FALSE;

      if( consanddata->noriguses > 0 )
      {
         assert(consanddata->origcons != NULL);
         assert(consanddata->nvars > 0);
         assert(consanddata->svars > 0);
         assert(consanddata->vars != NULL);
         assert(consanddata->isoriginal);

         /* check that the hash map and tabkle are still having all information */
         if( conshdlrdata->inithashmapandtable )
         {
            assert(conshdlrdata->hashmap != NULL);
            assert(conshdlrdata->hashtable != NULL);
            assert(SCIPgetResultantAnd(scip, consanddata->origcons) != NULL);
            assert(SCIPhashtableExists(conshdlrdata->hashtable, (void*)consanddata));
            assert(consanddata == (CONSANDDATA*)(SCIPhashtableRetrieve(conshdlrdata->hashtable, (void*)consanddata)));
            assert(SCIPhashmapExists(conshdlrdata->hashmap, (void*)SCIPgetResultantAnd(scip, consanddata->origcons)));
            assert(consanddata == (CONSANDDATA*)(SCIPhashmapGetImage(conshdlrdata->hashmap, (void*)SCIPgetResultantAnd(scip, consanddata->origcons))));
         }
      }
   }

   return SCIP_OKAY;
}



/** creates a pseudo boolean constraint data */
static
SCIP_RETCODE consdataCreate(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONSHDLR*const   conshdlr,           /**< pseudoboolean constraint handler */
   SCIP_CONSDATA**       consdata,           /**< pointer to linear constraint data */
   SCIP_CONS*const       lincons,            /**< linear constraint with artificial and-resultants representing this pseudoboolean constraint */
   SCIP_LINEARCONSTYPE const linconstype,    /**< type of linear constraint */
   SCIP_CONS**const      andconss,           /**< array of and-constraints which occur in this pseudoboolean constraint */
   SCIP_Real*const       andcoefs,           /**< coefficients of and-constraints */
   SCIP_Bool*const       andnegs,            /**< negation status of and-constraints (or NULL, if no negated resultants) */
   int const             nandconss,          /**< number of and-constraints */
   SCIP_VAR*const        indvar,             /**< indicator variable if it's a soft constraint, or NULL */
   SCIP_Real const       weight,             /**< weight of the soft constraint, if it is one */
   SCIP_Bool const       issoftcons,         /**< is this a soft constraint */
   SCIP_VAR* const       intvar,             /**< a artificial variable which was added only for the objective function,
                                              *   if this variable is not NULL this constraint (without this integer
                                              *   variable) describes the objective function */
   SCIP_Real             lhs,                /**< left hand side of row */
   SCIP_Real             rhs,                /**< right hand side of row */
   SCIP_Bool             check,              /**< is the new constraint a check constraint? */
   SCIP_Bool             transforming        /**< are we called by CONSTRANS */
   )
{
   SCIP_Bool transformed;
   int nvars;

   assert(scip != NULL);
   assert(conshdlr != NULL);
   assert(consdata != NULL);
   assert(lincons != NULL && linconstype > SCIP_LINEARCONSTYPE_INVALIDCONS);
   assert(nandconss == 0 || (andconss != NULL && andcoefs != NULL));
   assert(!issoftcons || (!SCIPisZero(scip, weight) && indvar != NULL));

   /* adjust right hand side */
   if( SCIPisInfinity(scip, rhs) )
      rhs = SCIPinfinity(scip);
   else if( SCIPisInfinity(scip, -rhs) )
      rhs = -SCIPinfinity(scip);

   /* adjust left hand side */
   if( SCIPisInfinity(scip, -lhs) )
      lhs = -SCIPinfinity(scip);
   else if( SCIPisInfinity(scip, lhs) )
      lhs = SCIPinfinity(scip);

   /* check left and right side */
   if( SCIPisGT(scip, lhs, rhs) )
   {
      SCIPerrorMessage("left hand side of pseudo boolean constraint greater than right hand side\n");
      SCIPerrorMessage(" -> lhs=%g, rhs=%g\n", lhs, rhs);
      return SCIP_INVALIDDATA;
   }

   transformed = SCIPisTransformed(scip);

   /* allocate memory for the constraint data */
   SCIP_CALL( SCIPallocBlockMemory(scip, consdata) );

   /* initialize the weights for soft constraints */
   (*consdata)->issoftcons = issoftcons;
   if( issoftcons )
   {
      (*consdata)->weight = weight;
      if( transformed )
      {
         SCIP_CALL( SCIPgetTransformedVar(scip, indvar, &((*consdata)->indvar)) );
      }
      else
         (*consdata)->indvar = indvar;
   }
   else
      (*consdata)->indvar = NULL;

   /* copy artificial integer variable if it exist */
   if( intvar != NULL )
   {
      if( transformed )
      {
         SCIP_CALL( SCIPgetTransformedVar(scip, intvar, &((*consdata)->intvar)) );
      }
      else
         (*consdata)->intvar = intvar;
   }
   else
      (*consdata)->intvar = NULL;

   /* copy linear constraint */
   (*consdata)->lincons = lincons;
   (*consdata)->linconstype = linconstype;

   /* get transformed linear constraint and capture it if necessary */
   if( transforming )
   {
      /* do not capture the and constraint when scip is in transformed mode; this automatically happens in
       * SCIPtransformCons()
       */
      SCIP_CALL( SCIPtransformCons(scip, (*consdata)->lincons, &((*consdata)->lincons)) );
      assert((*consdata)->lincons != NULL);
   }

   if( transforming || transformed )
   {
      assert(SCIPconsIsTransformed((*consdata)->lincons));

      /* we want to check all necessary transformed linear constraints */
      SCIP_CALL( SCIPsetConsChecked(scip, (*consdata)->lincons, check) );
   }

   /* get number of non-linear terms in pseudoboolean constraint */
   SCIP_CALL( getLinearConsNVars(scip, (*consdata)->lincons, (*consdata)->linconstype, &nvars) );
   (*consdata)->nlinvars = nvars - nandconss;

   /* copy and-constraints */
   if( nandconss > 0 )
   {
      SCIP_CONSHDLRDATA* conshdlrdata;
      SCIP_VAR** andress;
      int c;

      SCIP_CALL( SCIPallocBlockMemoryArray(scip, &((*consdata)->consanddatas), nandconss) );
      SCIP_CALL( SCIPduplicateBlockMemoryArray(scip, &((*consdata)->andcoefs), andcoefs, nandconss) );
      if( andnegs != NULL )
      {
         SCIP_CALL( SCIPduplicateBlockMemoryArray(scip, &((*consdata)->andnegs), andnegs, nandconss) );
      }
      else
      {
         SCIP_CALL( SCIPallocClearBlockMemoryArray(scip, &((*consdata)->andnegs), nandconss) );
      }
      (*consdata)->nconsanddatas = nandconss;
      (*consdata)->sconsanddatas = nandconss;

      /* allocate temporary memory */
      SCIP_CALL( SCIPallocBufferArray(scip, &andress, nandconss) );

      conshdlrdata = SCIPconshdlrGetData(conshdlr);
      assert(conshdlrdata != NULL);
      assert(conshdlrdata->hashmap != NULL);

      /* get all and-resultants for sorting */
      for( c = nandconss - 1; c >= 0; --c )
      {
         assert(andconss[c] != NULL);

         andress[c] = SCIPgetResultantAnd(scip, andconss[c]);
         assert(andress[c] != NULL);

         (*consdata)->consanddatas[c] = (CONSANDDATA*) SCIPhashmapGetImage(conshdlrdata->hashmap, (void*)andress[c]);
         assert((*consdata)->consanddatas[c] != NULL);
         assert((*consdata)->consanddatas[c]->origcons == andconss[c] || (*consdata)->consanddatas[c]->cons == andconss[c]);

         if( transforming )
         {
            /* if we perform a new transformation, we need to capture the transformed constraint */
            if( (*consdata)->consanddatas[c]->origcons != NULL && (*consdata)->consanddatas[c]->cons == NULL )
            {
               SCIP_VAR** vars;
               int ncvars;
               int v;

               /* do not capture the and constraint when scip is in transformed mode; this automatically happens in
                * SCIPtransformCons()
                */
               SCIP_CALL( SCIPtransformCons(scip, (*consdata)->consanddatas[c]->origcons, &((*consdata)->consanddatas[c]->cons)) );
               assert((*consdata)->consanddatas[c]->cons != NULL);
               assert((*consdata)->consanddatas[c]->newvars == NULL);
               assert((*consdata)->consanddatas[c]->isoriginal);

               (*consdata)->consanddatas[c]->istransformed = TRUE;

               vars = (*consdata)->consanddatas[c]->vars;
               ncvars = (*consdata)->consanddatas[c]->nvars;
               assert(vars != NULL || ncvars == 0);

               /* get transformed variables */
               SCIP_CALL( SCIPgetTransformedVars(scip, ncvars, vars, vars) );

               /* resort variables in transformed problem, because the order might change while tranforming */
               SCIPsortPtr((void**)vars, SCIPvarComp, ncvars);

               /* capture all transformed variables */
               for( v = ncvars - 1; v >= 0; --v )
               {
                  SCIP_CALL( SCIPcaptureVar(scip, vars[v]) ); /*lint !e613*/
               }
            }
            else if( (*consdata)->consanddatas[c]->cons != NULL )
               assert((*consdata)->consanddatas[c]->istransformed);

            ++((*consdata)->consanddatas[c]->nuses);
         }
         else if( transformed )
         {
            assert((*consdata)->consanddatas[c]->cons == andconss[c]);
            assert(SCIPconsIsTransformed(andconss[c]));
            assert((*consdata)->consanddatas[c]->istransformed);
         }
      }

      /* sort and-constraints after indices of corresponding and-resultants */
      SCIPsortPtrPtrRealBool((void**)andress, (void**)((*consdata)->consanddatas), (*consdata)->andcoefs, (*consdata)->andnegs, SCIPvarComp, nandconss);

      /* free temporary memory */
      SCIPfreeBufferArray(scip, &andress);
   }
   else
   {
      (*consdata)->consanddatas = NULL;
      (*consdata)->andcoefs = NULL;
      (*consdata)->andnegs = NULL;
      (*consdata)->nconsanddatas = 0;
      (*consdata)->sconsanddatas = 0;
   }

   /* copy left and right hand side */
   (*consdata)->lhs = lhs;
   (*consdata)->rhs = rhs;

   (*consdata)->changed = TRUE;
   (*consdata)->propagated = FALSE;
   (*consdata)->presolved = FALSE;
   (*consdata)->cliquesadded = FALSE;
   (*consdata)->upgradetried = TRUE;

   /* count number of used consanddata objects in original problem */
   if( SCIPgetStage(scip) == SCIP_STAGE_PROBLEM )
   {
      SCIP_CONSHDLRDATA* conshdlrdata;
      conshdlrdata = SCIPconshdlrGetData(conshdlr);
      assert(conshdlrdata != NULL);

      conshdlrdata->noriguses += (*consdata)->nconsanddatas;
   }

   return SCIP_OKAY;
}

/** free a pseudo boolean constraint data */
static
SCIP_RETCODE consdataFree(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONSDATA**       consdata,           /**< pointer to linear constraint data */
   SCIP_Bool             isorig,             /**< are we freeing an original constraint? */
   SCIP_CONSHDLRDATA*    conshdlrdata        /**< constraint handler data */
   )
{
   CONSANDDATA** consanddatas;
   int nconsanddatas;
   int c;

   assert(scip != NULL);
   assert(consdata != NULL);
   assert(*consdata != NULL);
   assert((*consdata)->nconsanddatas == 0 || (*consdata)->consanddatas != NULL);
   assert(conshdlrdata != NULL);

   /* release linear constraint */
   if( (*consdata)->lincons != NULL )
   {
      SCIP_CALL( SCIPreleaseCons(scip, &((*consdata)->lincons)) );
   }

   nconsanddatas = (*consdata)->nconsanddatas;
   consanddatas = (*consdata)->consanddatas;

   /* count down uses and if necessary release constraints and delete data from hashtable and -map */
   for( c = nconsanddatas - 1; c >= 0; --c )
   {
      assert((consanddatas[c]->origcons == NULL) == (consanddatas[c]->noriguses == 0));
      assert((consanddatas[c]->cons == NULL) == (consanddatas[c]->nuses == 0));
      assert(consanddatas[c]->nuses >= 0);
      assert(consanddatas[c]->noriguses >= 0);
      assert(isorig ? consanddatas[c]->cons == NULL : TRUE);

      /* are we deleteing a transformed constraint */
      if( !isorig && consanddatas[c]->cons != NULL )
      {
         assert(!SCIPconsIsOriginal(consanddatas[c]->cons));

         --(consanddatas[c]->nuses);

         /* if the consanddata is not used anymore, release the constraint and clear the hashmap- and table */
         if( consanddatas[c]->nuses == 0 )
         {
            if( conshdlrdata->inithashmapandtable )
            {
               assert(conshdlrdata->hashmap != NULL);
               assert(conshdlrdata->hashtable != NULL);

               /* remove consanddata from hashtable, if it existed only in transformed space */
               if( consanddatas[c]->origcons == NULL )
               {
                  assert(SCIPhashtableExists(conshdlrdata->hashtable, (void*)consanddatas[c]));
                  SCIP_CALL( SCIPhashtableRemove(conshdlrdata->hashtable, (void*)consanddatas[c]) );
               }
               assert(SCIPhashmapExists(conshdlrdata->hashmap, (void*)SCIPgetResultantAnd(scip, consanddatas[c]->cons)));
               SCIP_CALL( SCIPhashmapRemove(conshdlrdata->hashmap, (void*)SCIPgetResultantAnd(scip, consanddatas[c]->cons)) );
            }

            SCIP_CALL( SCIPreleaseCons(scip, &(consanddatas[c]->cons)) );

            /* if the consanddata object was only used in transformed space, delete the memory block */
            if( consanddatas[c]->origcons == NULL )
            {
               int d;

               assert(conshdlrdata->nallconsanddatas > 0);

               for( d = conshdlrdata->nallconsanddatas - 1; d >= 0; --d )
               {
                  if( conshdlrdata->allconsanddatas[d] == consanddatas[c] )
                  {
                     --conshdlrdata->nallconsanddatas;

                     SCIPfreeBlockMemory(scip, &(conshdlrdata->allconsanddatas[d])); /*lint !e866*/

                     conshdlrdata->allconsanddatas[d] = conshdlrdata->allconsanddatas[conshdlrdata->nallconsanddatas];
                     break;
                  }
               }
               assert(d >= 0);
               continue;
            }
         }
      }
      /* are we deleteing an original constraint */
      else if( isorig && consanddatas[c]->origcons != NULL )
      {
         assert(SCIPconsIsOriginal(consanddatas[c]->origcons));
         assert(consanddatas[c]->nuses == 0);
         assert(consanddatas[c]->nnewvars == 0);
         assert(consanddatas[c]->snewvars == 0);
         assert(consanddatas[c]->newvars == NULL);

         --(consanddatas[c]->noriguses);

         /* if the consanddata is not used anymore, release the constraint and clear the hashmap- and table */
         if( consanddatas[c]->noriguses == 0 )
         {
            int d;

            if( conshdlrdata->inithashmapandtable )
            {
               assert(conshdlrdata->hashmap != NULL);
               assert(conshdlrdata->hashtable != NULL);

               assert(SCIPhashtableExists(conshdlrdata->hashtable, (void*)consanddatas[c]));
               SCIP_CALL( SCIPhashtableRemove(conshdlrdata->hashtable, (void*)consanddatas[c]) );

               assert(SCIPhashmapExists(conshdlrdata->hashmap, (void*)SCIPgetResultantAnd(scip, consanddatas[c]->origcons)));
               SCIP_CALL( SCIPhashmapRemove(conshdlrdata->hashmap, (void*)SCIPgetResultantAnd(scip, consanddatas[c]->origcons)) );
            }

            if( consanddatas[c]->vars != NULL )
            {
               assert(consanddatas[c]->nvars > 0);
               assert(consanddatas[c]->svars > 0);
               assert(consanddatas[c]->svars >= consanddatas[c]->nvars);

               SCIPfreeBlockMemoryArrayNull(scip, &(consanddatas[c]->vars), consanddatas[c]->svars);
               consanddatas[c]->nvars = 0;
               consanddatas[c]->svars = 0;
            }
            else
            {
               assert(consanddatas[c]->nvars == 0);
               assert(consanddatas[c]->svars == 0);
            }

            SCIP_CALL( SCIPreleaseCons(scip, &(consanddatas[c]->origcons)) );
            assert(consanddatas[c]->origcons == NULL);

            /* delete consanddata object */
            assert(conshdlrdata->nallconsanddatas > 0);
            for( d = conshdlrdata->nallconsanddatas - 1; d >= 0; --d )
            {
               if( conshdlrdata->allconsanddatas[d] == consanddatas[c] )
               {
                  --conshdlrdata->nallconsanddatas;

                  SCIPfreeBlockMemory(scip, &(conshdlrdata->allconsanddatas[d])); /*lint !e866*/

                  conshdlrdata->allconsanddatas[d] = conshdlrdata->allconsanddatas[conshdlrdata->nallconsanddatas];
                  break;
               }
            }
            assert(d >= 0);

            continue;
         }
      }
      else
      {
         assert(!consanddatas[c]->istransformed);
         assert(consanddatas[c]->cons == NULL);
      }

      /* clear and remove capture of transformed consanddata */
      if( consanddatas[c]->nuses == 0 && consanddatas[c]->istransformed )
      {
         SCIP_CALL( transformToOrig(scip, consanddatas[c], conshdlrdata) );
      }
#ifndef NDEBUG
      else if( consanddatas[c]->nuses == 0 )
      {
         SCIP_VAR** tmpvars;
         int ntmpvars;
         int v;

         assert(consanddatas[c]->nnewvars == 0);
         assert(consanddatas[c]->snewvars == 0);
         assert(consanddatas[c]->newvars == NULL);

         tmpvars = consanddatas[c]->vars;
         ntmpvars = consanddatas[c]->nvars;

         /* release all variables */
         for( v = ntmpvars - 1; v >= 0; --v )
         {
            assert(tmpvars[v] != NULL);
            assert(SCIPvarIsOriginal(tmpvars[v]));
         }
      }
#endif

      /* restore original data */
      if( !consanddatas[c]->istransformed && consanddatas[c]->noriguses > 0 )
      {
         assert(consanddatas[c]->origcons != NULL);
         assert(consanddatas[c]->nuses == 0);
         assert(consanddatas[c]->nnewvars == 0);
         assert(consanddatas[c]->snewvars == 0);
         assert(consanddatas[c]->newvars == NULL);
         assert(consanddatas[c]->nvars > 0);
         assert(consanddatas[c]->svars > 0);
         assert(consanddatas[c]->svars >= consanddatas[c]->nvars);
         assert(consanddatas[c]->vars != NULL);
         assert(consanddatas[c]->isoriginal);

         assert(consanddatas[c]->nvars == SCIPgetNVarsAnd(scip, consanddatas[c]->origcons));
         assert(SCIPgetVarsAnd(scip, consanddatas[c]->origcons) != NULL);

         /* check that the hash map and tabkle are still having all information */
         if( conshdlrdata->inithashmapandtable )
         {
            assert(conshdlrdata->hashmap != NULL);
            assert(conshdlrdata->hashtable != NULL);
            assert(SCIPgetResultantAnd(scip, consanddatas[c]->origcons) != NULL);
            assert(SCIPhashtableExists(conshdlrdata->hashtable, (void*)consanddatas[c]));
            assert(consanddatas[c] == (CONSANDDATA*)(SCIPhashtableRetrieve(conshdlrdata->hashtable, (void*)consanddatas[c])));
            assert(SCIPhashmapExists(conshdlrdata->hashmap, (void*)SCIPgetResultantAnd(scip, consanddatas[c]->origcons)));
            assert(consanddatas[c] == (CONSANDDATA*)(SCIPhashmapGetImage(conshdlrdata->hashmap, (void*)SCIPgetResultantAnd(scip, consanddatas[c]->origcons))));
         }
      }
   }

   /* free array of and-constraints */
   SCIPfreeBlockMemoryArrayNull(scip, &((*consdata)->andnegs), (*consdata)->sconsanddatas);
   SCIPfreeBlockMemoryArrayNull(scip, &((*consdata)->andcoefs), (*consdata)->sconsanddatas);
   SCIPfreeBlockMemoryArrayNull(scip, &((*consdata)->consanddatas), (*consdata)->sconsanddatas);

   SCIPfreeBlockMemory(scip, consdata);

   return SCIP_OKAY;
}

/** check the locks of an AND resultant and removes it from all global structures if the resultant is not locked anymore */
static
SCIP_RETCODE checkLocksAndRes(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_VAR*             res                 /**< resultant of AND constraint */
   )
{
   assert(scip != NULL);
   assert(res != NULL);

   /* the resultant has no locks left and might be dual fixed now, we need to delete all its cliques */
   if( SCIPvarIsActive(res) && SCIPvarGetNLocksDownType(res, SCIP_LOCKTYPE_MODEL) == 0
      && SCIPvarGetNLocksUpType(res, SCIP_LOCKTYPE_MODEL) == 0 && SCIPgetStage(scip) < SCIP_STAGE_FREETRANS )
   {
      SCIP_CALL( SCIPremoveVarFromGlobalStructures(scip, res) );
   }

   return SCIP_OKAY;
}

/** installs rounding locks for the given and-constraint associated with given coefficient */
static
SCIP_RETCODE lockRoundingAndCons(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< pseudoboolean constraint */
   CONSANDDATA*const     consanddata,        /**< CONSANDDATA object for which we want to add the locks */
   SCIP_Real const       coef,               /**< coefficient which led to old locks */
   SCIP_Real const       lhs,                /**< left hand side */
   SCIP_Real const       rhs                 /**< right hand side */
   )
{
   SCIP_VAR** vars;
   int nvars;
   SCIP_VAR* res;
   SCIP_Bool haslhs;
   SCIP_Bool hasrhs;
   int v;

   assert(scip != NULL);
   assert(cons != NULL);
   assert(!SCIPconsIsLockedType(cons, SCIP_LOCKTYPE_CONFLICT));
   assert(consanddata != NULL);
   assert(!SCIPisInfinity(scip, coef) && !SCIPisInfinity(scip, -coef));
   assert(!SCIPisInfinity(scip, lhs));
   assert(!SCIPisInfinity(scip, -rhs));
   assert(SCIPisLE(scip, lhs, rhs));

   /* choose correct variable array to add locks for, we only add locks for now valid variables */
   if( consanddata->nnewvars > 0 )
   {
      vars = consanddata->newvars;
      nvars = consanddata->nnewvars;
   }
   else
   {
      vars = consanddata->vars;
      nvars = consanddata->nvars;
   }

   res = SCIPgetResultantAnd(scip, consanddata->cons);
   assert(nvars == 0 || (vars != NULL && res != NULL));

   /* check which sites are infinity */
   haslhs = !SCIPisInfinity(scip, -lhs);
   hasrhs = !SCIPisInfinity(scip, rhs);

   if( SCIPconsIsLocked(cons) )
   {
      /* locking variables */
      if( SCIPisPositive(scip, coef) )
      {
         for( v = nvars - 1; v >= 0; --v )
         {
            SCIP_CALL( SCIPlockVarCons(scip, vars[v], cons, haslhs, hasrhs) );
         }
      }
      else
      {
         for( v = nvars - 1; v >= 0; --v )
         {
            SCIP_CALL( SCIPlockVarCons(scip, vars[v], cons, hasrhs, haslhs) );
         }
      }
      SCIP_CALL( SCIPlockVarCons(scip, res, cons, TRUE, TRUE) );
   }

   return SCIP_OKAY;
}

/** removes rounding locks for the given and-constraint associated with given coefficient */
static
SCIP_RETCODE unlockRoundingAndCons(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< pseudoboolean constraint */
   CONSANDDATA*const     consanddata,        /**< CONSANDDATA object for which we want to delete the locks */
   SCIP_Real const       coef,               /**< coefficient which led to old locks */
   SCIP_Real const       lhs,                /**< left hand side which led to old locks */
   SCIP_Real const       rhs                 /**< right hand side which led to old locks */
   )
{
   SCIP_VAR** vars;
   int nvars;
   SCIP_VAR* res;
   SCIP_Bool haslhs;
   SCIP_Bool hasrhs;
   int v;

   assert(scip != NULL);
   assert(cons != NULL);
   assert(!SCIPconsIsLockedType(cons, SCIP_LOCKTYPE_CONFLICT));
   assert(consanddata != NULL);
   assert(!SCIPisInfinity(scip, coef) && !SCIPisInfinity(scip, -coef));
   assert(!SCIPisInfinity(scip, lhs));
   assert(!SCIPisInfinity(scip, -rhs));
   assert(SCIPisLE(scip, lhs, rhs));

   vars = consanddata->vars;
   nvars = consanddata->nvars;

   if( consanddata->cons != NULL )
      res = SCIPgetResultantAnd(scip, consanddata->cons);
   else
      res = NULL;
   assert(nvars == 0 || vars != NULL);

   /* check which sites are infinity */
   haslhs = !SCIPisInfinity(scip, -lhs);
   hasrhs = !SCIPisInfinity(scip, rhs);

   if( SCIPconsIsLocked(cons) )
   {
      /* unlock variables */
      if( SCIPisPositive(scip, coef) )
      {
         for( v = nvars - 1; v >= 0; --v )
         {
            SCIP_CALL( SCIPunlockVarCons(scip, vars[v], cons, haslhs, hasrhs) );
         }
      }
      else
      {
         for( v = nvars - 1; v >= 0; --v )
         {
            SCIP_CALL( SCIPunlockVarCons(scip, vars[v], cons, hasrhs, haslhs) );
         }
      }

      if( res != NULL )
      {
         SCIP_CALL( SCIPunlockVarCons(scip, res, cons, TRUE, TRUE) );

         SCIP_CALL( checkLocksAndRes(scip, res) );
      }
   }

   return SCIP_OKAY;
}

/** prints pseudoboolean constraint in CIP format to file stream */
static
SCIP_RETCODE consdataPrint(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< pseudoboolean constraint */
   FILE*const            file                /**< output file (or NULL for standard output) */
   )
{
   SCIP_CONSHDLR* conshdlr;
   SCIP_CONSHDLRDATA* conshdlrdata;
   SCIP_CONSDATA* consdata;

   SCIP_VAR** vars;
   SCIP_Real* coefs;
   int nvars;
   SCIP_Real lhs;
   SCIP_Real rhs;

   SCIP_VAR** linvars;
   SCIP_Real* lincoefs;
   int nlinvars;
   int v;

   SCIP_VAR** andress;
   SCIP_Real* andcoefs;
   SCIP_Bool* andnegs;
   int nandress;

   SCIP_Bool printed;

   assert(scip != NULL);
   assert(cons != NULL);

#ifdef WITHEQKNAPSACK
   if( SCIPconsIsDeleted(cons) )
      return SCIP_OKAY;
#endif

   consdata = SCIPconsGetData(cons);
   assert(consdata != NULL);
   assert(consdata->lincons != NULL);
   /* more than one and-constraint is needed, otherwise this pseudoboolean constraint should be upgraded to a linear constraint */
   assert(consdata->nconsanddatas >= 0);

   /* gets number of variables in linear constraint */
   SCIP_CALL( getLinearConsNVars(scip, consdata->lincons, consdata->linconstype, &nvars) );

   /* allocate temporary memory */
   SCIP_CALL( SCIPallocBufferArray(scip, &vars, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &coefs, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &linvars, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &lincoefs, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &andress, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &andcoefs, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &andnegs, nvars) );

   /* get sides of linear constraint */
   SCIP_CALL( getLinearConsSides(scip, consdata->lincons, consdata->linconstype, &lhs, &rhs) );
   assert(!SCIPisInfinity(scip, lhs));
   assert(!SCIPisInfinity(scip, -rhs));
   assert(SCIPisLE(scip, lhs, rhs));

   /* get variables and coefficient of linear constraint */
   SCIP_CALL( getLinearConsVarsData(scip, consdata->lincons, consdata->linconstype, vars, coefs, &nvars) );
   assert(nvars == 0 || (coefs != NULL));

   /* calculate all not artificial linear variables and all artificial and-resultants which will be ordered like the
    * 'consanddatas' such that the and-resultant of the and-constraint is the and-resultant in the 'andress' array
    * afterwards
    */
   SCIP_CALL( getLinVarsAndAndRess(scip, cons, vars, coefs, nvars, linvars, lincoefs, &nlinvars,
         andress, andcoefs, andnegs, &nandress) );
   assert(consdata->nconsanddatas == nandress);

   /* number of variables should be consistent, number of 'real' linear variables plus number of and-constraints should
    * have to be equal to the number of variables in the linear constraint
    */
   assert(consdata->nlinvars + consdata->nconsanddatas == nvars);

   /* print left hand side for ranged rows */
   if( !SCIPisInfinity(scip, -lhs) && !SCIPisInfinity(scip, rhs) && !SCIPisEQ(scip, lhs, rhs) )
      SCIPinfoMessage(scip, file, "%.15g <= ", lhs);

   printed = FALSE;

   /* print coefficients and variables */
   if( nlinvars > 0)
   {
      printed= TRUE;

      /* print linear part of constraint */
      SCIP_CALL( SCIPwriteVarsLinearsum(scip, file, linvars, lincoefs, nlinvars, TRUE) );
   }

   conshdlr = SCIPconsGetHdlr(cons);
   assert(conshdlr != NULL);
   conshdlrdata = SCIPconshdlrGetData(conshdlr);
   assert(conshdlrdata != NULL);
   assert(conshdlrdata->hashmap != NULL);

   /* print all non-linear terms */
   for( v = nandress - 1; v >= 0; --v )
   {
      CONSANDDATA* consanddata;
      SCIP_CONS* andcons;
      SCIP_VAR** andvars;
      int nandvars;

      if( !SCIPconsIsOriginal(cons) )
      {
         /* if the and resultant was fixed we print a constant */
         if( SCIPvarGetLbLocal(andress[v]) > 0.5 || SCIPvarGetUbLocal(andress[v]) < 0.5 )
         {
            if( SCIPvarGetLbGlobal(andress[v]) > 0.5 )
            {
               printed = TRUE;
               SCIPinfoMessage(scip, file, " %+.15g ", andcoefs[v] * SCIPvarGetLbGlobal(andress[v]));
            }
            continue;
         }
         else if( SCIPvarGetStatus(andress[v]) == SCIP_VARSTATUS_AGGREGATED )
         {
            SCIP_VAR* aggrvar;
            SCIP_Bool negated;

            SCIP_CALL( SCIPgetBinvarRepresentative(scip, andress[v], &aggrvar, &negated) );
            assert(aggrvar != NULL);
            assert(SCIPvarGetType(aggrvar) == SCIP_VARTYPE_BINARY);

            printed = TRUE;
            SCIPinfoMessage(scip, file, " %+.15g %s<%s>[B]", andcoefs[v], negated ? "~" : "", SCIPvarGetName(aggrvar));

            continue;
         }
      }

      consanddata = (CONSANDDATA*) SCIPhashmapGetImage(conshdlrdata->hashmap, (void*)andress[v]);
      assert(consanddata != NULL);

      if( SCIPconsIsOriginal(cons) )
         andcons = consanddata->origcons;
      else
         andcons = consanddata->cons;
      assert(andcons != NULL);

      andvars = SCIPgetVarsAnd(scip, andcons);
      nandvars = SCIPgetNVarsAnd(scip, andcons);
      assert(nandvars == 0 || andvars != NULL);

      if( nandvars > 0 )
      {
         printed = TRUE;
         SCIPinfoMessage(scip, file, " %+.15g %s(", andcoefs[v], andnegs[v] ? "~" : "");

         /* @todo: better write new method SCIPwriteProduct */
         /* print variable list */
         SCIP_CALL( SCIPwriteVarsList(scip, file, andvars, nandvars, TRUE, '*') );

         SCIPinfoMessage(scip, file, ")");
      }
   }

   if( !printed )
   {
      SCIPinfoMessage(scip, file, " 0 ");
   }

   /* free temporary memory */
   SCIPfreeBufferArray(scip, &andnegs);
   SCIPfreeBufferArray(scip, &andcoefs);
   SCIPfreeBufferArray(scip, &andress);
   SCIPfreeBufferArray(scip, &lincoefs);
   SCIPfreeBufferArray(scip, &linvars);
   SCIPfreeBufferArray(scip, &coefs);
   SCIPfreeBufferArray(scip, &vars);

   /* print right hand side */
   if( SCIPisEQ(scip, lhs, rhs) )
      SCIPinfoMessage(scip, file, "== %.15g", rhs);
   else if( !SCIPisInfinity(scip, rhs) )
      SCIPinfoMessage(scip, file, "<= %.15g", rhs);
   else if( !SCIPisInfinity(scip, -lhs) )
      SCIPinfoMessage(scip, file, ">= %.15g", lhs);
   else
      SCIPinfoMessage(scip, file, " [free]");

   return SCIP_OKAY;
}

/** creates and/or adds the resultant for a given term */
static
SCIP_RETCODE createAndAddAndCons(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONSHDLR*const   conshdlr,           /**< pseudoboolean constraint handler */
   SCIP_VAR**const       vars,               /**< array of variables to get and-constraints for */
   int const             nvars,              /**< number of variables to get and-constraints for */
   SCIP_Bool const       initial,            /**< should the LP relaxation of constraint be in the initial LP?
                                              *   Usually set to TRUE. Set to FALSE for 'lazy constraints'. */
   SCIP_Bool const       enforce,            /**< should the constraint be enforced during node processing?
                                              *   TRUE for model constraints, FALSE for additional, redundant
                                              *   constraints. */
   SCIP_Bool const       check,              /**< should the constraint be checked for feasibility?
                                              *   TRUE for model constraints, FALSE for additional, redundant
                                              *   constraints. */
   SCIP_Bool const       local,              /**< is constraint only valid locally?
                                              *   Usually set to FALSE. Has to be set to TRUE, e.g., for branching
                                              *   constraints. */
   SCIP_Bool const       modifiable,         /**< is constraint modifiable (subject to column generation)?
                                              *   Usually set to FALSE. In column generation applications, set to TRUE
                                              *   if pricing adds coefficients to this constraint. */
   SCIP_Bool const       dynamic,            /**< is constraint subject to aging?
                                              *   Usually set to FALSE. Set to TRUE for own cuts which
                                              *   are seperated as constraints. */
   SCIP_Bool const       stickingatnode,     /**< should the constraint always be kept at the node where it was added, even
                                              *   if it may be moved to a more global node?
                                              *   Usually set to FALSE. Set to TRUE to for constraints that represent
                                              *   node data. */
   SCIP_CONS**const      andcons             /**< pointer to store and-constraint */
   )
{
   CONSANDDATA* newdata;
   CONSANDDATA* tmpdata;
   SCIP_CONSHDLRDATA* conshdlrdata;
   char name[SCIP_MAXSTRLEN];
   SCIP_Bool separate;
   SCIP_Bool propagate;
   SCIP_Bool removable;
   SCIP_Bool transformed;

   assert(scip != NULL);
   assert(conshdlr != NULL);
   assert(vars != NULL);
   assert(nvars > 0);
   assert(andcons != NULL);

   conshdlrdata = SCIPconshdlrGetData(conshdlr);
   assert(conshdlrdata != NULL);
   assert(conshdlrdata->hashtable != NULL);

   transformed = SCIPisTransformed(scip);

   /* allocate memory for a possible new consanddata object */
   SCIP_CALL( SCIPallocBlockMemory(scip, &newdata) );
   SCIP_CALL( SCIPduplicateBlockMemoryArray(scip, &(newdata->vars), vars, nvars) );
   newdata->nvars = nvars;
   newdata->svars = nvars;
   newdata->newvars = NULL;
   newdata->nnewvars = 0;
   newdata->snewvars = 0;
   newdata->noriguses = 0;
   newdata->nuses = 0;
   newdata->istransformed = transformed;
   newdata->isoriginal = !transformed;
   newdata->cons = NULL;
   newdata->origcons = NULL;

   /* sort variables */
   SCIPsortPtr((void**)(newdata->vars), SCIPvarComp, nvars);

   /* get constraint from current hash table with same variables as cons0 */
   tmpdata = (CONSANDDATA*)(SCIPhashtableRetrieve(conshdlrdata->hashtable, (void*)newdata));

   /* if there is already the same and constraint created use this resultant */
   if( tmpdata != NULL )
   {
#ifndef NDEBUG
      SCIP_VAR* res;
#endif
      if( transformed )
      {
         assert(tmpdata->cons != NULL);
         *andcons = tmpdata->cons;

         assert(tmpdata->nuses > 0);
         /* increase usage of data object */
         ++(tmpdata->nuses);
      }
      else
      {
         assert(tmpdata->origcons != NULL);
         *andcons = tmpdata->origcons;

         assert(tmpdata->noriguses > 0);
         /* increase usage of data object */
         ++(tmpdata->noriguses);
      }
      assert(*andcons != NULL);

#ifndef NDEBUG
      res = SCIPgetResultantAnd(scip, *andcons);
      assert(res != NULL);

      /* check that we already have added this resultant to and-constraint entry */
      assert(SCIPhashmapExists(conshdlrdata->hashmap, (void*)res));
#endif
   }
   else
   {
      /* create new and-constraint */
      SCIP_CONS* newcons;
      SCIP_VAR* resultant;

      /* create auxiliary variable */
      (void)SCIPsnprintf(name, SCIP_MAXSTRLEN, ARTIFICIALVARNAMEPREFIX"%d", conshdlrdata->nallconsanddatas);
      SCIP_CALL( SCIPcreateVar(scip, &resultant, name, 0.0, 1.0, 0.0, SCIP_VARTYPE_BINARY,
            TRUE, TRUE, NULL, NULL, NULL, NULL, NULL) );

#if 1 /* @todo: check whether we want to branch on artificial variables, the test results show that it is of advantage */
      /* change branching priority of artificial variable to -1 */
      SCIP_CALL( SCIPchgVarBranchPriority(scip, resultant, -1) );
#endif

      /* add auxiliary variable to the problem */
      SCIP_CALL( SCIPaddVar(scip, resultant) );

#if 0 /* does not work for since the value of artificial resultants must not be equal to the value computed by their
       * product, since these variables are irrelevant */
#ifdef WITH_DEBUG_SOLUTION
      if( SCIPdebugIsMainscip(scip) )
      {
         SCIP_Real val;
         SCIP_Real debugsolval;
         int v;

         for( v = nvars - 1; v >= 0; --v )
         {
            SCIP_CALL( SCIPdebugGetSolVal(scip, vars[v], &val) );
            assert(SCIPisFeasZero(scip, val) || SCIPisFeasEQ(scip, val, 1.0));

            if( val < 0.5 )
               break;
         }
         val = ((val < 0.5) ? 0.0 : 1.0);

         SCIP_CALL( SCIPdebugGetSolVal(scip, resultant, &debugsolval) );
         if( (SCIPvarIsOriginal(resultant) || SCIPvarIsTransformedOrigvar(resultant)) && !SCIPisFeasEQ(scip, debugsolval, val) )
         {
            SCIPerrorMessage("computed solution value %g for resultant <%s> violates debug solution value %g\n", val, SCIPvarGetName(resultant), debugsolval);
            SCIPABORT();
            return SCIP_ERROR; /*lint !e527*/
         }
         else if( !SCIPvarIsOriginal(resultant) && !SCIPvarIsTransformedOrigvar(resultant) )
         {
            SCIP_CALL( SCIPdebugAddSolVal(scip, resultant, val) );
         }
      }
#endif
#endif

      SCIP_CALL( SCIPgetBoolParam(scip, "constraints/" CONSHDLR_NAME "/nlcseparate", &separate) );
      SCIP_CALL( SCIPgetBoolParam(scip, "constraints/" CONSHDLR_NAME "/nlcpropagate", &propagate) );
      SCIP_CALL( SCIPgetBoolParam(scip, "constraints/" CONSHDLR_NAME "/nlcremovable", &removable) );

      /* we do not want to check the and constraints, so the check flag will be FALSE */

      /* create and add "and" constraint for the multiplication of the binary variables */
      (void)SCIPsnprintf(name, SCIP_MAXSTRLEN, "andcons_%d", conshdlrdata->nallconsanddatas);
      SCIP_CALL( SCIPcreateConsAnd(scip, &newcons, name, resultant, newdata->nvars, newdata->vars,
            initial, separate, enforce, check && FALSE, propagate,
            local, modifiable, dynamic, removable, stickingatnode) ); /*lint !e506*/
      SCIP_CALL( SCIPaddCons(scip, newcons) );
      SCIPdebugPrintCons(scip, newcons, NULL);

      /* force all deriving constraint from this and constraint to be checked and not removable */
      SCIP_CALL( SCIPchgAndConsCheckFlagWhenUpgr(scip, newcons, TRUE) );
      SCIP_CALL( SCIPchgAndConsRemovableFlagWhenUpgr(scip, newcons, TRUE) );

      *andcons = newcons;
      assert(*andcons != NULL);

      /* resize data for all and-constraints if necessary */
      if( conshdlrdata->nallconsanddatas == conshdlrdata->sallconsanddatas )
      {
         SCIP_CALL( SCIPensureBlockMemoryArray(scip, &(conshdlrdata->allconsanddatas), &(conshdlrdata->sallconsanddatas), SCIPcalcMemGrowSize(scip, conshdlrdata->sallconsanddatas + 1)) );
      }

      /* add new data object to global hash table */
      conshdlrdata->allconsanddatas[conshdlrdata->nallconsanddatas] = newdata;
      ++(conshdlrdata->nallconsanddatas);

      if( transformed )
      {
         int v;

         newdata->cons = newcons;
         SCIP_CALL( SCIPcaptureCons(scip, newdata->cons) );

         /* initialize usage of data object */
         newdata->nuses = 1;

         /* capture all variables */
         for( v = newdata->nvars - 1; v >= 0; --v )
         {
            SCIP_CALL( SCIPcaptureVar(scip, newdata->vars[v]) ); /*lint !e613*/
         }
      }
      else
      {
         newdata->origcons = newcons;
         SCIP_CALL( SCIPcaptureCons(scip, newdata->origcons) );

         /* initialize usage of data object */
         newdata->noriguses = 1;
      }

      /* no such and-constraint in current hash table: insert the new object into hash table */
      SCIP_CALL( SCIPhashtableInsert(conshdlrdata->hashtable, (void*)newdata) );

      /* insert new mapping */
      assert(!SCIPhashmapExists(conshdlrdata->hashmap, (void*)resultant));
      SCIP_CALL( SCIPhashmapInsert(conshdlrdata->hashmap, (void*)resultant, (void*)newdata) );

      /* release and-resultant and -constraint */
      SCIP_CALL( SCIPreleaseVar(scip, &resultant) );
      SCIP_CALL( SCIPreleaseCons(scip, &newcons) );

      return SCIP_OKAY;
   }

   /* free memory */
   SCIPfreeBlockMemoryArray(scip, &(newdata->vars), newdata->svars);
   SCIPfreeBlockMemory(scip, &newdata);

   return SCIP_OKAY;
}

/** adds a term to the given pseudoboolean constraint */
static
SCIP_RETCODE addCoefTerm(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< pseudoboolean constraint */
   SCIP_VAR**const       vars,               /**< variables of the nonlinear term */
   int const             nvars,              /**< number of variables of the nonlinear term */
   SCIP_Real const       val                 /**< coefficient of constraint entry */
   )
{
   SCIP_CONSHDLR* conshdlr;
   SCIP_CONSHDLRDATA* conshdlrdata;
   SCIP_CONS* andcons;
   SCIP_CONSDATA* consdata;
   SCIP_VAR* res;

   assert(scip != NULL);
   assert(cons != NULL);
   assert(nvars == 0 || vars != NULL);

   if( nvars == 0 || SCIPisZero(scip, val) )
      return SCIP_OKAY;

   consdata = SCIPconsGetData(cons);
   assert(consdata != NULL);

   conshdlr = SCIPconsGetHdlr(cons);
   assert(conshdlr != NULL);

   conshdlrdata =  SCIPconshdlrGetData(conshdlr);
   assert(conshdlrdata != NULL);

   /* create (and add) and-constraint */
   SCIP_CALL( createAndAddAndCons(scip, conshdlr, vars, nvars,
         SCIPconsIsInitial(cons), SCIPconsIsEnforced(cons), SCIPconsIsChecked(cons), SCIPconsIsLocal(cons),
         SCIPconsIsModifiable(cons), SCIPconsIsDynamic(cons), SCIPconsIsStickingAtNode(cons),
         &andcons) );
   assert(andcons != NULL);

   /* ensure memory size */
   if( consdata->nconsanddatas == consdata->sconsanddatas )
   {
      SCIP_CALL( SCIPensureBlockMemoryArray(scip, &(consdata->consanddatas), &(consdata->sconsanddatas), consdata->sconsanddatas + 1) );
   }

   res = SCIPgetResultantAnd(scip, andcons);
   assert(res != NULL);
   assert(SCIPhashmapGetImage(conshdlrdata->hashmap, (void*)res) != NULL);

   consdata->consanddatas[consdata->nconsanddatas] = (CONSANDDATA*) SCIPhashmapGetImage(conshdlrdata->hashmap, (void*)res);
   ++(consdata->nconsanddatas);

   /* add auxiliary variables to linear constraint */
   switch( consdata->linconstype )
   {
   case SCIP_LINEARCONSTYPE_LINEAR:
      SCIP_CALL( SCIPaddCoefLinear(scip, consdata->lincons, res, val) );
      break;
   case SCIP_LINEARCONSTYPE_LOGICOR:
      if( !SCIPisEQ(scip, val, 1.0) )
         return SCIP_INVALIDDATA;

      SCIP_CALL( SCIPaddCoefLogicor(scip, consdata->lincons, res) );
      break;
   case SCIP_LINEARCONSTYPE_KNAPSACK:
      if( !SCIPisIntegral(scip, val) || !SCIPisPositive(scip, val) )
         return SCIP_INVALIDDATA;

      SCIP_CALL( SCIPaddCoefKnapsack(scip, consdata->lincons, res, (SCIP_Longint) val) );
      break;
   case SCIP_LINEARCONSTYPE_SETPPC:
      if( !SCIPisEQ(scip, val, 1.0) )
         return SCIP_INVALIDDATA;

      SCIP_CALL( SCIPaddCoefSetppc(scip, consdata->lincons, res) );
      break;
#ifdef WITHEQKNAPSACK
   case SCIP_LINEARCONSTYPE_EQKNAPSACK:
      if( !SCIPisIntegral(scip, val) || !SCIPisPositive(scip, val) )
         return SCIP_INVALIDDATA;

      SCIP_CALL( SCIPaddCoefEQKnapsack(scip, consdata->lincons, res, (SCIP_Longint) val) );
      break;
#endif
   case SCIP_LINEARCONSTYPE_INVALIDCONS:
   default:
      SCIPerrorMessage("unknown linear constraint type\n");
      return SCIP_INVALIDDATA;
   }

   /* install rounding locks for all new variable */
   SCIP_CALL( lockRoundingAndCons(scip, cons, consdata->consanddatas[consdata->nconsanddatas - 1], val, consdata->lhs, consdata->rhs) );

   /* change flags */
   consdata->changed = TRUE;
   consdata->propagated = FALSE;
   consdata->presolved = FALSE;
   consdata->cliquesadded = FALSE;
   consdata->upgradetried = FALSE;

   return SCIP_OKAY;
}

/** changes left hand side of linear constraint */
static
SCIP_RETCODE chgLhsLinearCons(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< linear constraint */
   SCIP_LINEARCONSTYPE const constype,       /**< linear constraint type */
   SCIP_Real const       lhs                 /**< new left hand side of linear constraint */
   )
{
   switch( constype )
   {
   case SCIP_LINEARCONSTYPE_LINEAR:
      SCIP_CALL( SCIPchgLhsLinear(scip, cons, lhs) );
      break;
   case SCIP_LINEARCONSTYPE_LOGICOR:
   case SCIP_LINEARCONSTYPE_KNAPSACK:
   case SCIP_LINEARCONSTYPE_SETPPC:
      SCIPerrorMessage("changing left hand side only allowed on standard lienar constraint \n");
      return SCIP_INVALIDDATA;
#ifdef WITHEQKNAPSACK
   case SCIP_LINEARCONSTYPE_EQKNAPSACK:
#endif
   case SCIP_LINEARCONSTYPE_INVALIDCONS:
   default:
      SCIPerrorMessage("unknown linear constraint type\n");
      return SCIP_INVALIDDATA;
   }

   return SCIP_OKAY;
}

/** changes right hand side of linear constraint */
static
SCIP_RETCODE chgRhsLinearCons(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< linear constraint */
   SCIP_LINEARCONSTYPE const constype,       /**< linear constraint type */
   SCIP_Real const       rhs                 /**< new right hand side of linear constraint */
   )
{
   switch( constype )
   {
   case SCIP_LINEARCONSTYPE_LINEAR:
      SCIP_CALL( SCIPchgRhsLinear(scip, cons, rhs) );
      break;
   case SCIP_LINEARCONSTYPE_LOGICOR:
   case SCIP_LINEARCONSTYPE_KNAPSACK:
   case SCIP_LINEARCONSTYPE_SETPPC:
      SCIPerrorMessage("changing left hand side only allowed on standard lienar constraint \n");
      return SCIP_INVALIDDATA;
#ifdef WITHEQKNAPSACK
   case SCIP_LINEARCONSTYPE_EQKNAPSACK:
#endif
   case SCIP_LINEARCONSTYPE_INVALIDCONS:
   default:
      SCIPerrorMessage("unknown linear constraint type\n");
      return SCIP_INVALIDDATA;
   }

   return SCIP_OKAY;
}

/** sets left hand side of linear constraint */
static
SCIP_RETCODE chgLhs(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< linear constraint */
   SCIP_Real             lhs                 /**< new left hand side */
   )
{
   SCIP_CONSDATA* consdata;
   SCIP_VAR** vars;
   SCIP_Real* coefs;
   int nvars;
   SCIP_VAR** linvars;
   SCIP_Real* lincoefs;
   int nlinvars;
   SCIP_VAR** andress;
   SCIP_Real* andcoefs;
   SCIP_Bool* andnegs;
   int nandress;
   SCIP_Real oldlhs;
   SCIP_Real oldrhs;

   assert(scip != NULL);
   assert(cons != NULL);
   assert(!SCIPconsIsLockedType(cons, SCIP_LOCKTYPE_CONFLICT));
   assert(!SCIPisInfinity(scip, lhs));

   /* adjust value to not be smaller than -inf */
   if ( SCIPisInfinity(scip, -lhs) )
      lhs = -SCIPinfinity(scip);

   consdata = SCIPconsGetData(cons);
   assert(consdata != NULL);

   /* get sides of linear constraint */
   SCIP_CALL( getLinearConsSides(scip, consdata->lincons, consdata->linconstype, &oldlhs, &oldrhs) );
   assert(!SCIPisInfinity(scip, oldlhs));
   assert(!SCIPisInfinity(scip, -oldrhs));
   assert(SCIPisLE(scip, oldlhs, oldrhs));

   /* check whether the side is not changed */
   if( SCIPisEQ(scip, oldlhs, lhs) )
      return SCIP_OKAY;

   /* gets number of variables in linear constraint */
   SCIP_CALL( getLinearConsNVars(scip, consdata->lincons, consdata->linconstype, &nvars) );

   /* allocate temporary memory */
   SCIP_CALL( SCIPallocBufferArray(scip, &vars, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &coefs, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &linvars, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &lincoefs, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &andress, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &andcoefs, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &andnegs, nvars) );

   /* get variables and coefficient of linear constraint */
   SCIP_CALL( getLinearConsVarsData(scip, consdata->lincons, consdata->linconstype, vars, coefs, &nvars) );
   assert(nvars == 0 || (coefs != NULL));

   /* calculate all not artificial linear variables and all artificial and-resultants which will be ordered like the
    * 'consanddatas' such that the and-resultant of the and-constraint is the and-resultant in the 'andress' array
    * afterwards
    */
   SCIP_CALL( getLinVarsAndAndRess(scip, cons, vars, coefs, nvars, linvars, lincoefs, &nlinvars, andress, andcoefs, andnegs, &nandress) );
   assert(consdata->nconsanddatas == nandress);

   /* if necessary, update the rounding locks of variables */
   if( SCIPconsIsLocked(cons) )
   {
      SCIP_VAR** andvars;
      int nandvars;
      SCIP_Real val;
      int v;
      int c;

      assert(SCIPconsIsTransformed(cons));

      if( SCIPisInfinity(scip, -oldlhs) && !SCIPisInfinity(scip, -lhs) )
      {
         /* non-linear part */
         for( c = consdata->nconsanddatas - 1; c >= 0; --c )
         {
            CONSANDDATA* consanddata;
            SCIP_CONS* andcons;

            consanddata = consdata->consanddatas[c];
            assert(consanddata != NULL);

            andcons = consanddata->cons;
            assert(andcons != NULL);

            andvars = SCIPgetVarsAnd(scip, andcons);
            nandvars = SCIPgetNVarsAnd(scip, andcons);
            val = andnegs[c] ? -andcoefs[c] : andcoefs[c];

            /* lock variables */
            if( SCIPisPositive(scip, val) )
            {
               for( v = nandvars - 1; v >= 0; --v )
               {
                  SCIP_CALL( SCIPlockVarCons(scip, andvars[v], cons, TRUE, FALSE) );
               }
            }
            else
            {
               for( v = nandvars - 1; v >= 0; --v )
               {
                  SCIP_CALL( SCIPlockVarCons(scip, andvars[v], cons, FALSE, TRUE) );
               }
            }
         }
      }
      else if( !SCIPisInfinity(scip, -oldlhs) && SCIPisInfinity(scip, -lhs) )
      {
         /* non-linear part */
         for( c = consdata->nconsanddatas - 1; c >= 0; --c )
         {
            CONSANDDATA* consanddata;
            SCIP_CONS* andcons;

            consanddata = consdata->consanddatas[c];
            assert(consanddata != NULL);

            andcons = consanddata->cons;
            assert(andcons != NULL);

            andvars = SCIPgetVarsAnd(scip, andcons);
            nandvars = SCIPgetNVarsAnd(scip, andcons);
            val = andnegs[c] ? -andcoefs[c] : andcoefs[c];

            /* lock variables */
            if( SCIPisPositive(scip, val) )
            {
               for( v = nandvars - 1; v >= 0; --v )
               {
                  SCIP_CALL( SCIPunlockVarCons(scip, andvars[v], cons, TRUE, FALSE) );
               }
            }
            else
            {
               for( v = nandvars - 1; v >= 0; --v )
               {
                  SCIP_CALL( SCIPunlockVarCons(scip, andvars[v], cons, FALSE, TRUE) );
               }
            }
         }
      }
   }

   /* check whether the left hand side is increased, if and only if that's the case we maybe can propagate, tighten and add more cliques */
   if( SCIPisLT(scip, oldlhs, lhs) )
   {
      consdata->propagated = FALSE;
   }

   /* set new left hand side and update constraint data */
   SCIP_CALL( chgLhsLinearCons(scip, consdata->lincons, consdata->linconstype, lhs) );
   consdata->lhs = lhs;
   consdata->presolved = FALSE;
   consdata->changed = TRUE;

   /* free temporary memory */
   SCIPfreeBufferArray(scip, &andnegs);
   SCIPfreeBufferArray(scip, &andcoefs);
   SCIPfreeBufferArray(scip, &andress);
   SCIPfreeBufferArray(scip, &lincoefs);
   SCIPfreeBufferArray(scip, &linvars);
   SCIPfreeBufferArray(scip, &coefs);
   SCIPfreeBufferArray(scip, &vars);

   return SCIP_OKAY;
}

/** sets right hand side of pseudoboolean constraint */
static
SCIP_RETCODE chgRhs(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< linear constraint */
   SCIP_Real             rhs                 /**< new right hand side */
   )
{
   SCIP_CONSDATA* consdata;
   SCIP_VAR** vars;
   SCIP_Real* coefs;
   int nvars;
   SCIP_VAR** linvars;
   SCIP_Real* lincoefs;
   int nlinvars;
   SCIP_VAR** andress;
   SCIP_Real* andcoefs;
   SCIP_Bool* andnegs;
   int nandress;
   SCIP_Real oldlhs;
   SCIP_Real oldrhs;

   assert(scip != NULL);
   assert(cons != NULL);
   assert(!SCIPconsIsLockedType(cons, SCIP_LOCKTYPE_CONFLICT));
   assert(!SCIPisInfinity(scip, -rhs));

   /* adjust value to not be larger than inf */
   if( SCIPisInfinity(scip, rhs) )
      rhs = SCIPinfinity(scip);

   consdata = SCIPconsGetData(cons);
   assert(consdata != NULL);

   /* get sides of linear constraint */
   SCIP_CALL( getLinearConsSides(scip, consdata->lincons, consdata->linconstype, &oldlhs, &oldrhs) );
   assert(!SCIPisInfinity(scip, oldlhs));
   assert(!SCIPisInfinity(scip, -oldrhs));
   assert(SCIPisLE(scip, oldlhs, oldrhs));

   /* check whether the side is not changed */
   if( SCIPisEQ(scip, oldrhs, rhs) )
      return SCIP_OKAY;

   /* gets number of variables in linear constraint */
   SCIP_CALL( getLinearConsNVars(scip, consdata->lincons, consdata->linconstype, &nvars) );

   /* allocate temporary memory */
   SCIP_CALL( SCIPallocBufferArray(scip, &vars, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &coefs, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &linvars, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &lincoefs, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &andress, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &andcoefs, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &andnegs, nvars) );

   /* get variables and coefficient of linear constraint */
   SCIP_CALL( getLinearConsVarsData(scip, consdata->lincons, consdata->linconstype, vars, coefs, &nvars) );
   assert(nvars == 0 || (coefs != NULL));

   /* calculate all not artificial linear variables and all artificial and-resultants which will be ordered like the
    * 'consanddatas' such that the and-resultant of the and-constraint is the and-resultant in the 'andress' array
    * afterwards
    */
   SCIP_CALL( getLinVarsAndAndRess(scip, cons, vars, coefs, nvars, linvars, lincoefs, &nlinvars, andress, andcoefs, andnegs, &nandress) );
   assert(consdata->nconsanddatas == nandress);

   /* if necessary, update the rounding locks of variables */
   if( SCIPconsIsLocked(cons) )
   {
      SCIP_VAR** andvars;
      int nandvars;
      SCIP_Real val;
      int v;
      int c;

      assert(SCIPconsIsTransformed(cons));

      if( SCIPisInfinity(scip, oldrhs) && !SCIPisInfinity(scip, rhs) )
      {
         /* non-linear part */
         for( c = consdata->nconsanddatas - 1; c >= 0; --c )
         {
            CONSANDDATA* consanddata;
            SCIP_CONS* andcons;

            consanddata = consdata->consanddatas[c];
            assert(consanddata != NULL);

            andcons = consanddata->cons;
            assert(andcons != NULL);

            andvars = SCIPgetVarsAnd(scip, andcons);
            nandvars = SCIPgetNVarsAnd(scip, andcons);
            val = andnegs[c] ? -andcoefs[c] : andcoefs[c];

            /* lock variables */
            if( SCIPisPositive(scip, val) )
            {
               for( v = nandvars - 1; v >= 0; --v )
               {
                  SCIP_CALL( SCIPlockVarCons(scip, andvars[v], cons, FALSE, TRUE) );
               }
            }
            else
            {
               for( v = nandvars - 1; v >= 0; --v )
               {
                  SCIP_CALL( SCIPlockVarCons(scip, andvars[v], cons, TRUE, FALSE) );
               }
            }
         }
      }
      else if( !SCIPisInfinity(scip, oldrhs) && SCIPisInfinity(scip, rhs) )
      {
         /* non-linear part */
         for( c = consdata->nconsanddatas - 1; c >= 0; --c )
         {
            CONSANDDATA* consanddata;
            SCIP_CONS* andcons;

            consanddata = consdata->consanddatas[c];
            assert(consanddata != NULL);

            andcons = consanddata->cons;
            assert(andcons != NULL);

            andvars = SCIPgetVarsAnd(scip, andcons);
            nandvars = SCIPgetNVarsAnd(scip, andcons);
            val = andnegs[c] ? -andcoefs[c] : andcoefs[c];

            /* lock variables */
            if( SCIPisPositive(scip, val) )
            {
               for( v = nandvars - 1; v >= 0; --v )
               {
                  SCIP_CALL( SCIPunlockVarCons(scip, andvars[v], cons, FALSE, TRUE) );
               }
            }
            else
            {
               for( v = nandvars - 1; v >= 0; --v )
               {
                  SCIP_CALL( SCIPunlockVarCons(scip, andvars[v], cons, TRUE, FALSE) );
               }
            }
         }
      }
   }

   /* check whether the right hand side is decreased, if and only if that's the case we maybe can propagate, tighten and add more cliques */
   if( SCIPisGT(scip, oldrhs, rhs) )
   {
      consdata->propagated = FALSE;
   }

   /* set new right hand side and update constraint data */
   SCIP_CALL( chgRhsLinearCons(scip, consdata->lincons, consdata->linconstype, rhs) );
   consdata->rhs = rhs;
   consdata->presolved = FALSE;
   consdata->changed = TRUE;

   /* free temporary memory */
   SCIPfreeBufferArray(scip, &andnegs);
   SCIPfreeBufferArray(scip, &andcoefs);
   SCIPfreeBufferArray(scip, &andress);
   SCIPfreeBufferArray(scip, &lincoefs);
   SCIPfreeBufferArray(scip, &linvars);
   SCIPfreeBufferArray(scip, &coefs);
   SCIPfreeBufferArray(scip, &vars);

   return SCIP_OKAY;
}

/** create and-constraints and get all and-resultants */
static
SCIP_RETCODE createAndAddAnds(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONSHDLR*const   conshdlr,           /**< pseudoboolean constraint handler */
   SCIP_VAR**const*const terms,              /**< array of term variables to get and-constraints for */
   SCIP_Real*const       termcoefs,          /**< array of coefficients for and-constraints */
   int const             nterms,             /**< number of terms to get and-constraints for */
   int const*const       ntermvars,          /**< array of number of variable in each term */
   SCIP_Bool const       initial,            /**< should the LP relaxation of constraint be in the initial LP?
                                              *   Usually set to TRUE. Set to FALSE for 'lazy constraints'. */
   SCIP_Bool const       enforce,            /**< should the constraint be enforced during node processing?
                                              *   TRUE for model constraints, FALSE for additional, redundant
                                              *   constraints. */
   SCIP_Bool const       check,              /**< should the constraint be checked for feasibility?
                                              *   TRUE for model constraints, FALSE for additional, redundant
                                              *   constraints. */
   SCIP_Bool const       local,              /**< is constraint only valid locally?
                                              *   Usually set to FALSE. Has to be set to TRUE, e.g., for branching
                                              *   constraints. */
   SCIP_Bool const       modifiable,         /**< is constraint modifiable (subject to column generation)?
                                              *   Usually set to FALSE. In column generation applications, set to TRUE
                                              *   if pricing adds coefficients to this constraint. */
   SCIP_Bool const       dynamic,            /**< is constraint subject to aging?
                                              *   Usually set to FALSE. Set to TRUE for own cuts which
                                              *   are seperated as constraints. */
   SCIP_Bool const       stickingatnode,     /**< should the constraint always be kept at the node where it was added, even
                                              *   if it may be moved to a more global node?
                                              *   Usually set to FALSE. Set to TRUE to for constraints that represent
                                              *   node data. */
   SCIP_CONS**const      andconss,           /**< array to store all created and-constraints for given terms */
   SCIP_Real*const       andvals,            /**< array to store all coefficients of and-constraints */
   SCIP_Bool*const       andnegs,            /**< array to store negation status of and-constraints */
   int*const             nandconss           /**< number of created and constraints */
   )
{
   int t;

   assert(scip != NULL);
   assert(conshdlr != NULL);
   assert(nterms == 0 || (terms != NULL && ntermvars != NULL));
   assert(andconss != NULL);
   assert(andvals != NULL);
   assert(nandconss != NULL);

   (*nandconss) = 0;

   if( nterms == 0 )
      return SCIP_OKAY;

   /* loop over all terms and create/get all and constraints */
   for( t = 0; t < nterms; ++t )
   {
      if( !SCIPisZero(scip, termcoefs[t]) && ntermvars[t] > 0 )
      {
         SCIP_CALL( createAndAddAndCons(scip, conshdlr, terms[t], ntermvars[t],
               initial, enforce, check, local, modifiable, dynamic, stickingatnode,
               &(andconss[*nandconss])) );
         assert(andconss[*nandconss] != NULL);
         andvals[*nandconss] = termcoefs[t];
         andnegs[*nandconss] = FALSE;
         ++(*nandconss);
      }
   }

   return SCIP_OKAY;
}

/** created linear constraint of pseudo boolean constraint */
static
SCIP_RETCODE createAndAddLinearCons(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONSHDLR*const   conshdlr,           /**< pseudoboolean constraint handler */
   SCIP_VAR**const       linvars,            /**< linear variables */
   int const             nlinvars,           /**< number of linear variables */
   SCIP_Real*const       linvals,            /**< linear coefficients */
   SCIP_VAR**const       andress,            /**< and-resultant variables */
   int const             nandress,           /**< number of and-resultant variables */
   SCIP_Real const*const andvals,            /**< and-resultant coefficients */
   SCIP_Bool*const       andnegs,            /**< and-resultant negation status */
   SCIP_Real*const       lhs,                /**< pointer to left hand side of linear constraint */
   SCIP_Real*const       rhs,                /**< pointer to right hand side of linear constraint */
   SCIP_Bool const       initial,            /**< should the LP relaxation of constraint be in the initial LP?
                                              *   Usually set to TRUE. Set to FALSE for 'lazy constraints'. */
   SCIP_Bool const       separate,           /**< should the constraint be separated during LP processing?
                                              *   Usually set to TRUE. */
   SCIP_Bool const       enforce,            /**< should the constraint be enforced during node processing?
                                              *   TRUE for model constraints, FALSE for additional, redundant
                                              *   constraints. */
   SCIP_Bool const       check,              /**< should the constraint be checked for feasibility?
                                              *   TRUE for model constraints, FALSE for additional, redundant
                                              *   constraints. */
   SCIP_Bool const       propagate,          /**< should the constraint be propagated during node processing?
                                              *   Usually set to TRUE. */
   SCIP_Bool const       local,              /**< is constraint only valid locally?
                                              *   Usually set to FALSE. Has to be set to TRUE, e.g., for branching
                                              *   constraints. */
   SCIP_Bool const       modifiable,         /**< is constraint modifiable (subject to column generation)?
                                              *   Usually set to FALSE. In column generation applications, set to TRUE
                                              *   if pricing adds coefficients to this constraint. */
   SCIP_Bool const       dynamic,            /**< is constraint subject to aging?
                                              *   Usually set to FALSE. Set to TRUE for own cuts which
                                              *   are seperated as constraints. */
   SCIP_Bool const       removable,          /**< should the relaxation be removed from the LP due to aging or cleanup?
                                              *   Usually set to FALSE. Set to TRUE for 'lazy constraints' and 'user
                                              *   cuts'. */
   SCIP_Bool const       stickingatnode,     /**< should the constraint always be kept at the node where it was added, even
                                              *   if it may be moved to a more global node?
                                              *   Usually set to FALSE. Set to TRUE to for constraints that represent
                                              *   node data. */
   SCIP_CONS**const      lincons,            /**< pointer to store created linear constraint */
   SCIP_LINEARCONSTYPE*const linconstype     /**< pointer to store the type of the linear constraint */
   )
{
   SCIP_CONSHDLRDATA* conshdlrdata;
   SCIP_CONSHDLR* upgrconshdlr;
   SCIP_CONS* cons;
   char name[SCIP_MAXSTRLEN];
   int v;
   SCIP_Bool created;
   SCIP_Bool integral;
   int nzero;
   int ncoeffspone;
   int ncoeffsnone;
   int ncoeffspint;
   int ncoeffsnint;

   assert(scip != NULL);
   assert(conshdlr != NULL);
   assert(nlinvars == 0 || (linvars != NULL && linvals != NULL));
   assert(nandress == 0 || (andress != NULL && andvals != NULL));
   assert(lhs != NULL);
   assert(rhs != NULL);
   assert(lincons != NULL);
   assert(linconstype != NULL);
   assert(nlinvars > 0 || nandress > 0);

   conshdlrdata = SCIPconshdlrGetData(conshdlr);
   assert(conshdlrdata != NULL);

   (*linconstype) = SCIP_LINEARCONSTYPE_INVALIDCONS;
   (*lincons) = NULL;
   cons = NULL;

   (void)SCIPsnprintf(name, SCIP_MAXSTRLEN, "pseudoboolean_linear%d", conshdlrdata->nlinconss);
   ++(conshdlrdata->nlinconss);

   created = FALSE;

   if( !modifiable )
   {
      SCIP_Real val;
      int nvars;

      /* calculate some statistics for upgrading on linear constraint */
      nzero = 0;
      ncoeffspone = 0;
      ncoeffsnone = 0;
      ncoeffspint = 0;
      ncoeffsnint = 0;
      integral = TRUE;
      nvars = nlinvars + nandress;

      /* calculate information over linear part */
      for( v = nlinvars - 1; v >= 0; --v )
      {
         val = linvals[v];

         if( SCIPisZero(scip, val) )
         {
            ++nzero;
            continue;
         }
         if( SCIPisEQ(scip, val, 1.0) )
            ++ncoeffspone;
         else if( SCIPisEQ(scip, val, -1.0) )
            ++ncoeffsnone;
         else if( SCIPisIntegral(scip, val) )
         {
            if( SCIPisPositive(scip, val) )
               ++ncoeffspint;
            else
               ++ncoeffsnint;
         }
         else
         {
            integral = FALSE;
            break;
         }
      }

      if( integral )
      {
         /* calculate information over and-resultants */
         for( v = nandress - 1; v >= 0; --v )
         {
            val = andvals[v];

            if( SCIPisZero(scip, val) )
            {
               ++nzero;
               continue;
            }
            if( SCIPisEQ(scip, val, 1.0) )
               ++ncoeffspone;
            else if( SCIPisEQ(scip, val, -1.0) )
               ++ncoeffsnone;
            else if( SCIPisIntegral(scip, val) )
            {
               if( SCIPisPositive(scip, val) )
                  ++ncoeffspint;
               else
                  ++ncoeffsnint;
            }
            else
            {
               integral = FALSE;
               break;
            }
         }
      }

      SCIPdebugMsg(scip, "While creating the linear constraint of the pseudoboolean constraint we found %d zero coefficients that were removed\n", nzero);

      /* try to upgrade to a special linear constraint */
      if( integral )
      {
         upgrconshdlr = SCIPfindConshdlr(scip, "logicor");

         /* check, if linear constraint can be upgraded to logic or constraint
          * - logic or constraints consist only of binary variables with a
          *   coefficient of +1.0 or -1.0 (variables with -1.0 coefficients can be negated):
          *        lhs     <= x1 + ... + xp - y1 - ... - yn <= rhs
          * - negating all variables y = (1-Y) with negative coefficients gives:
          *        lhs + n <= x1 + ... + xp + Y1 + ... + Yn <= rhs + n
          * - negating all variables x = (1-X) with positive coefficients and multiplying with -1 gives:
          *        p - rhs <= X1 + ... + Xp + y1 + ... + yn <= p - lhs
          * - logic or constraints have left hand side of +1.0, and right hand side of +infinity: x(S) >= 1.0
          *    -> without negations:  (lhs == 1 - n  and  rhs == +inf)  or  (lhs == -inf  and  rhs = p - 1)
          */
         if( upgrconshdlr != NULL && nvars > 2 && ncoeffspone + ncoeffsnone == nvars
            && ((SCIPisEQ(scip, *lhs, 1.0 - ncoeffsnone) && SCIPisInfinity(scip, *rhs))
               || (SCIPisInfinity(scip, -*lhs) && SCIPisEQ(scip, *rhs, ncoeffspone - 1.0))) )
         {
            SCIP_VAR** transvars;
            int mult;

            SCIPdebugMsg(scip, "linear constraint will be logic-or constraint\n");

            /* check, if we have to multiply with -1 (negate the positive vars) or with +1 (negate the negative vars) */
            mult = SCIPisInfinity(scip, *rhs) ? +1 : -1;

            /* get temporary memory */
            SCIP_CALL( SCIPallocBufferArray(scip, &transvars, nvars) );

            /* negate positive or negative variables */
            for( v = 0; v < nlinvars; ++v )
            {
               if( mult * linvals[v] > 0.0 )
                  transvars[v] = linvars[v];
               else
               {
                  SCIP_CALL( SCIPgetNegatedVar(scip, linvars[v], &transvars[v]) );
               }
               assert(transvars[v] != NULL);
            }

            /* negate positive or negative variables */
            for( v = 0; v < nandress; ++v )
            {
               if( mult * andvals[v] > 0.0 )
                  transvars[nlinvars + v] = andress[v];
               else
               {
                  SCIP_CALL( SCIPgetNegatedVar(scip, andress[v], &transvars[nlinvars + v]) );
                  andnegs[v] = TRUE;
               }
               assert(transvars[nlinvars + v] != NULL);
            }

            assert(!modifiable);
            /* create the constraint */
            SCIP_CALL( SCIPcreateConsLogicor(scip, &cons, name, nvars, transvars,
                  initial, separate, enforce, check, propagate, local, modifiable, dynamic, removable, stickingatnode) );

            created = TRUE;
            (*linconstype) = SCIP_LINEARCONSTYPE_LOGICOR;

            /* free temporary memory */
            SCIPfreeBufferArray(scip, &transvars);

            *lhs = 1.0;
            *rhs = SCIPinfinity(scip);
         }

         upgrconshdlr = SCIPfindConshdlr(scip, "setppc");

         /* check, if linear constraint can be upgraded to set partitioning, packing, or covering constraint
          * - all set partitioning / packing / covering constraints consist only of binary variables with a
          *   coefficient of +1.0 or -1.0 (variables with -1.0 coefficients can be negated):
          *        lhs     <= x1 + ... + xp - y1 - ... - yn <= rhs
          * - negating all variables y = (1-Y) with negative coefficients gives:
          *        lhs + n <= x1 + ... + xp + Y1 + ... + Yn <= rhs + n
          * - negating all variables x = (1-X) with positive coefficients and multiplying with -1 gives:
          *        p - rhs <= X1 + ... + Xp + y1 + ... + yn <= p - lhs
          * - a set partitioning constraint has left hand side of +1.0, and right hand side of +1.0 : x(S) == 1.0
          *    -> without negations:  lhs == rhs == 1 - n  or  lhs == rhs == p - 1
          * - a set packing constraint has left hand side of -infinity, and right hand side of +1.0 : x(S) <= 1.0
          *    -> without negations:  (lhs == -inf  and  rhs == 1 - n)  or  (lhs == p - 1  and  rhs = +inf)
          * - a set covering constraint has left hand side of +1.0, and right hand side of +infinity: x(S) >= 1.0
          *    -> without negations:  (lhs == 1 - n  and  rhs == +inf)  or  (lhs == -inf  and  rhs = p - 1)
          */
         if( upgrconshdlr != NULL && !created && ncoeffspone + ncoeffsnone == nvars )
         {
            SCIP_VAR** transvars;
            int mult;

            if( SCIPisEQ(scip, *lhs, *rhs) && (SCIPisEQ(scip, *lhs, 1.0 - ncoeffsnone) || SCIPisEQ(scip, *lhs, ncoeffspone - 1.0)) )
            {
               SCIPdebugMsg(scip, "linear pseudoboolean constraint will be a set partitioning constraint\n");

               /* check, if we have to multiply with -1 (negate the positive vars) or with +1 (negate the negative vars) */
               mult = SCIPisEQ(scip, *lhs, 1.0 - ncoeffsnone) ? +1 : -1;

               /* get temporary memory */
               SCIP_CALL( SCIPallocBufferArray(scip, &transvars, nvars) );

               /* negate positive or negative variables for linear variables */
               for( v = 0; v < nlinvars; ++v )
               {
                  if( mult * linvals[v] > 0.0 )
                     transvars[v] = linvars[v];
                  else
                  {
                     SCIP_CALL( SCIPgetNegatedVar(scip, linvars[v], &transvars[v]) );
                  }
                  assert(transvars[v] != NULL);
               }

               /* negate positive or negative variables for and-resultants */
               for( v = 0; v < nandress; ++v )
               {
                  if( mult * andvals[v] > 0.0 )
                     transvars[nlinvars + v] = andress[v];
                  else
                  {
                     SCIP_CALL( SCIPgetNegatedVar(scip, andress[v], &transvars[nlinvars + v]) );
                     andnegs[v] = TRUE;
                  }
                  assert(transvars[nlinvars + v] != NULL);
               }

               /* create the constraint */
               assert(!modifiable);
               SCIP_CALL( SCIPcreateConsSetpart(scip, &cons, name, nvars, transvars,
                     initial, separate, enforce, check, propagate, local, modifiable, dynamic, removable, stickingatnode) );

               created = TRUE;
               (*linconstype) = SCIP_LINEARCONSTYPE_SETPPC;

               /* release temporary memory */
               SCIPfreeBufferArray(scip, &transvars);

               *lhs = 1.0;
               *rhs = 1.0;
            }
            else if( (SCIPisInfinity(scip, -*lhs) && SCIPisEQ(scip, *rhs, 1.0 - ncoeffsnone))
               || (SCIPisEQ(scip, *lhs, ncoeffspone - 1.0) && SCIPisInfinity(scip, *rhs)) )
            {
               SCIPdebugMsg(scip, "linear pseudoboolean constraint will be a set packing constraint\n");

               /* check, if we have to multiply with -1 (negate the positive vars) or with +1 (negate the negative vars) */
               mult = SCIPisInfinity(scip, -*lhs) ? +1 : -1;

               /* get temporary memory */
               SCIP_CALL( SCIPallocBufferArray(scip, &transvars, nvars) );

               /* negate positive or negative variables for linear variables */
               for( v = 0; v < nlinvars; ++v )
               {
                  if( mult * linvals[v] > 0.0 )
                     transvars[v] = linvars[v];
                  else
                  {
                     SCIP_CALL( SCIPgetNegatedVar(scip, linvars[v], &transvars[v]) );
                  }
                  assert(transvars[v] != NULL);
               }

               /* negate positive or negative variables for and-resultants*/
               for( v = 0; v < nandress; ++v )
               {
                  if( mult * andvals[v] > 0.0 )
                     transvars[nlinvars + v] = andress[v];
                  else
                  {
                     SCIP_CALL( SCIPgetNegatedVar(scip, andress[v], &transvars[nlinvars + v]) );
                     andnegs[v] = TRUE;
                  }
                  assert(transvars[nlinvars + v] != NULL);
               }

               /* create the constraint */
               assert(!modifiable);
               SCIP_CALL( SCIPcreateConsSetpack(scip, &cons, name, nvars, transvars,
                     initial, separate, enforce, check, propagate, local, modifiable, dynamic, removable, stickingatnode) );

               created = TRUE;
               (*linconstype) = SCIP_LINEARCONSTYPE_SETPPC;

               /* release temporary memory */
               SCIPfreeBufferArray(scip, &transvars);

               *lhs = -SCIPinfinity(scip);
               *rhs = 1.0;
            }
            else if( (SCIPisEQ(scip, *lhs, 1.0 - ncoeffsnone) && SCIPisInfinity(scip, *rhs))
               || (SCIPisInfinity(scip, -*lhs) && SCIPisEQ(scip, *rhs, ncoeffspone - 1.0)) )
            {
               if( nvars != 1 )
               {
                  if( nvars == 2 )
                  {
                     SCIPwarningMessage(scip, "Does not expect this, because this constraint should be a set packing constraint.\n");
                  }
                  else
                  {
                     SCIPwarningMessage(scip, "Does not expect this, because this constraint should be a logicor constraint.\n");
                  }
               }
               SCIPdebugMsg(scip, "linear pseudoboolean constraint will be a set covering constraint\n");

               /* check, if we have to multiply with -1 (negate the positive vars) or with +1 (negate the negative vars) */
               mult = SCIPisInfinity(scip, *rhs) ? +1 : -1;

               /* get temporary memory */
               SCIP_CALL( SCIPallocBufferArray(scip, &transvars, nvars) );

               /* negate positive or negative variables for linear variables */
               for( v = 0; v < nlinvars; ++v )
               {
                  if( mult * linvals[v] > 0.0 )
                     transvars[v] = linvars[v];
                  else
                  {
                     SCIP_CALL( SCIPgetNegatedVar(scip, linvars[v], &transvars[v]) );
                  }
                  assert(transvars[v] != NULL);
               }

               /* negate positive or negative variables for and-resultants*/
               for( v = 0; v < nandress; ++v )
               {
                  if( mult * andvals[v] > 0.0 )
                     transvars[nlinvars + v] = andress[v];
                  else
                  {
                     SCIP_CALL( SCIPgetNegatedVar(scip, andress[v], &transvars[nlinvars + v]) );
                     andnegs[v] = TRUE;
                  }
                  assert(transvars[nlinvars + v] != NULL);
               }

               /* create the constraint */
               assert(!modifiable);
               SCIP_CALL( SCIPcreateConsSetcover(scip, &cons, name, nvars, transvars,
                     initial, separate, enforce, check, propagate, local, modifiable, dynamic, removable, stickingatnode) );

               created = TRUE;
               (*linconstype) = SCIP_LINEARCONSTYPE_SETPPC;

               /* release temporary memory */
               SCIPfreeBufferArray(scip, &transvars);

               *lhs = 1.0;
               *rhs = SCIPinfinity(scip);
            }
         }

         upgrconshdlr = SCIPfindConshdlr(scip, "knapsack");

         /* check, if linear constraint can be upgraded to a knapsack constraint
          * - all variables must be binary
          * - all coefficients must be integral
          * - exactly one of the sides must be infinite
          */
         if( upgrconshdlr != NULL && !created && (ncoeffspone + ncoeffsnone + ncoeffspint + ncoeffsnint == nvars) && (SCIPisInfinity(scip, -*lhs) != SCIPisInfinity(scip, *rhs)) )
         {
            SCIP_VAR** transvars;
            SCIP_Longint* weights;
            SCIP_Longint capacity;
            SCIP_Longint weight;
            int mult;

            SCIPdebugMsg(scip, "linear pseudoboolean constraint will be a knapsack constraint\n");

            /* get temporary memory */
            SCIP_CALL( SCIPallocBufferArray(scip, &transvars, nvars) );
            SCIP_CALL( SCIPallocBufferArray(scip, &weights, nvars) );

            /* if the right hand side is non-infinite, we have to negate all variables with negative coefficient;
             * otherwise, we have to negate all variables with positive coefficient and multiply the row with -1
             */
            if( SCIPisInfinity(scip, *rhs) )
            {
               mult = -1;
               capacity = (SCIP_Longint)SCIPfeasFloor(scip, -*lhs);
            }
            else
            {
               mult = +1;
               capacity = (SCIP_Longint)SCIPfeasFloor(scip, *rhs);
            }

            /* negate positive or negative variables for linear variables */
            for( v = 0; v < nlinvars; ++v )
            {
               assert(SCIPisFeasIntegral(scip, linvals[v]));
               weight = mult * (SCIP_Longint)SCIPfeasFloor(scip, linvals[v]);
               if( weight > 0 )
               {
                  transvars[v] = linvars[v];
                  weights[v] = weight;
               }
               else
               {
                  SCIP_CALL( SCIPgetNegatedVar(scip, linvars[v], &transvars[v]) );
                  weights[v] = -weight;
                  capacity -= weight;
               }
               assert(transvars[v] != NULL);
            }
            /* negate positive or negative variables for and-resultants */
            for( v = 0; v < nandress; ++v )
            {
               assert(SCIPisFeasIntegral(scip, andvals[v]));
               weight = mult * (SCIP_Longint)SCIPfeasFloor(scip, andvals[v]);
               if( weight > 0 )
               {
                  transvars[nlinvars + v] = andress[v];
                  weights[nlinvars + v] = weight;
               }
               else
               {
                  SCIP_CALL( SCIPgetNegatedVar(scip, andress[v], &transvars[nlinvars + v]) );
                  andnegs[v] = TRUE;
                  weights[nlinvars + v] = -weight;
                  capacity -= weight;
               }
               assert(transvars[nlinvars + v] != NULL);
            }

            /* create the constraint */
            SCIP_CALL( SCIPcreateConsKnapsack(scip, &cons, name, nvars, transvars, weights, capacity,
                  initial, separate, enforce, check, propagate, local, modifiable, dynamic, removable, stickingatnode) );

            created = TRUE;
            (*linconstype) = SCIP_LINEARCONSTYPE_KNAPSACK;

            /* free temporary memory */
            SCIPfreeBufferArray(scip, &weights);
            SCIPfreeBufferArray(scip, &transvars);

            *lhs = -SCIPinfinity(scip);
            *rhs = capacity;
         }
#ifdef WITHEQKNAPSACK

         upgrconshdlr = SCIPfindConshdlr(scip, "eqknapsack");

         /* check, if linear constraint can be upgraded to a knapsack constraint
          * - all variables must be binary
          * - all coefficients must be integral
          * - both sides must be infinite
          */
         if( upgrconshdlr != NULL && !created && (ncoeffspone + ncoeffsnone + ncoeffspint + ncoeffsnint == nvars) && SCIPisEQ(scip, *lhs, *rhs) )
         {
            SCIP_VAR** transvars;
            SCIP_Longint* weights;
            SCIP_Longint capacity;
            SCIP_Longint weight;
            int mult;

            assert(!SCIPisInfinity(scip, *rhs));

            SCIPdebugMsg(scip, "linear pseudoboolean constraint will be a equality-knapsack constraint\n");

            /* get temporary memory */
            SCIP_CALL( SCIPallocBufferArray(scip, &transvars, nvars) );
            SCIP_CALL( SCIPallocBufferArray(scip, &weights, nvars) );

            if( SCIPisPositive(scip, *rhs) )
            {
               mult = +1;
               capacity = (SCIP_Longint)SCIPfeasFloor(scip, *rhs);
            }
            else
            {
               mult = -1;
               capacity = (SCIP_Longint)SCIPfeasFloor(scip, -*rhs);
            }

            /* negate positive or negative variables for linear variables */
            for( v = 0; v < nlinvars; ++v )
            {
               assert(SCIPisFeasIntegral(scip, linvals[v]));
               weight = mult * (SCIP_Longint)SCIPfeasFloor(scip, linvals[v]);
               if( weight > 0 )
               {
                  transvars[v] = linvars[v];
                  weights[v] = weight;
               }
               else
               {
                  SCIP_CALL( SCIPgetNegatedVar(scip, linvars[v], &transvars[v]) );
                  weights[v] = -weight;
                  capacity -= weight;
               }
               assert(transvars[v] != NULL);
            }
            /* negate positive or negative variables for and-resultants */
            for( v = 0; v < nandress; ++v )
            {
               assert(SCIPisFeasIntegral(scip, andvals[v]));
               weight = mult * (SCIP_Longint)SCIPfeasFloor(scip, andvals[v]);
               if( weight > 0 )
               {
                  transvars[nlinvars + v] = andress[v];
                  weights[nlinvars + v] = weight;
               }
               else
               {
                  SCIP_CALL( SCIPgetNegatedVar(scip, andress[v], &transvars[nlinvars + v]) );
                  andnegs[v] = TRUE;
                  weights[nlinvars + v] = -weight;
                  capacity -= weight;
               }
               assert(transvars[nlinvars + v] != NULL);
            }

            /* create the constraint */
            SCIP_CALL( SCIPcreateConsEqKnapsack(scip, &cons, name, nvars, transvars, weights, capacity,
                  initial, separate, enforce, check, propagate, local, modifiable, dynamic, removable, stickingatnode) );

            created = TRUE;
            (*linconstype) = SCIP_LINEARCONSTYPE_EQKNAPSACK;

            /* free temporary memory */
            SCIPfreeBufferArray(scip, &weights);
            SCIPfreeBufferArray(scip, &transvars);

            *lhs = capacity;
            *rhs = capacity;
         }
#endif
      }
   }

   upgrconshdlr = SCIPfindConshdlr(scip, "linear");
   assert(created || upgrconshdlr != NULL);

   if( !created )
   {
      SCIP_CALL( SCIPcreateConsLinear(scip, &cons, name, nlinvars, linvars, linvals, *lhs, *rhs,
            initial, separate, enforce, check, propagate, local, modifiable, dynamic, removable, stickingatnode) );

      (*linconstype) = SCIP_LINEARCONSTYPE_LINEAR;

      /* add all and-resultants */
      for( v = 0; v < nandress; ++v )
      {
         assert(andress[v] != NULL);

         /* add auxiliary variables to linear constraint */
         SCIP_CALL( SCIPaddCoefLinear(scip, cons, andress[v], andvals[v]) );
      }
   }

   assert(cons != NULL && *linconstype > SCIP_LINEARCONSTYPE_INVALIDCONS);

   SCIP_CALL( SCIPaddCons(scip, cons) );
   SCIPdebugPrintCons(scip, cons, NULL);

   *lincons = cons;
   SCIP_CALL( SCIPcaptureCons(scip, *lincons) );

   /* mark linear constraint not to be upgraded - otherwise we loose control over it */
   SCIPconsAddUpgradeLocks(cons, 1);

   SCIP_CALL( SCIPreleaseCons(scip, &cons) );

   return SCIP_OKAY;
}

/** checks one original pseudoboolean constraint for feasibility of given solution */
static
SCIP_RETCODE checkOrigPbCons(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< pseudo boolean constraint */
   SCIP_SOL*const        sol,                /**< solution to be checked, or NULL for current solution */
   SCIP_Bool*const       violated,           /**< pointer to store whether the constraint is violated */
   SCIP_Bool const       printreason         /**< should violation of constraint be printed */
   )
{
   SCIP_CONSDATA* consdata;
   SCIP_CONSHDLR* conshdlr;
   SCIP_CONSHDLRDATA* conshdlrdata;

   SCIP_VAR** vars;
   SCIP_Real* coefs;
   int nvars;
   SCIP_Real lhs;
   SCIP_Real rhs;

   SCIP_VAR** linvars;
   SCIP_Real* lincoefs;
   int nlinvars;
   int v;

   SCIP_VAR** andress;
   SCIP_Real* andcoefs;
   int nandress;

   SCIP_CONS* andcons;
   SCIP_Real andvalue;
   SCIP_Real activity;
   int c;

   SCIP_Real lhsviol;
   SCIP_Real rhsviol;
   SCIP_Real absviol;
   SCIP_Real relviol;

   assert(scip != NULL);
   assert(cons != NULL);
   assert(SCIPconsIsOriginal(cons));
   assert(violated != NULL);

   *violated = FALSE;

   SCIPdebugMsg(scip, "checking original pseudo boolean constraint <%s>\n", SCIPconsGetName(cons));
   SCIPdebugPrintCons(scip, cons, NULL);

   consdata = SCIPconsGetData(cons);
   assert(consdata != NULL);
   assert(consdata->lincons != NULL);
   assert(consdata->linconstype > SCIP_LINEARCONSTYPE_INVALIDCONS);
   assert(SCIPconsIsOriginal(consdata->lincons));

   /* gets number of variables in linear constraint */
   SCIP_CALL( getLinearConsNVars(scip, consdata->lincons, consdata->linconstype, &nvars) );

   /* allocate temporary memory */
   SCIP_CALL( SCIPallocBufferArray(scip, &vars, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &coefs, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &linvars, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &lincoefs, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &andress, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &andcoefs, nvars) );

   /* get sides of linear constraint */
   SCIP_CALL( getLinearConsSides(scip, consdata->lincons, consdata->linconstype, &lhs, &rhs) );
   assert(!SCIPisInfinity(scip, lhs));
   assert(!SCIPisInfinity(scip, -rhs));
   assert(SCIPisLE(scip, lhs, rhs));

   /* get variables and coefficient of linear constraint */
   SCIP_CALL( getLinearConsVarsData(scip, consdata->lincons, consdata->linconstype, vars, coefs, &nvars) );
   assert(nvars == 0 || (coefs != NULL));

   /* number of variables should be consistent, number of 'real' linear variables plus number of and-constraints should
    * have to be equal to the number of variables in the linear constraint
    */
   assert(consdata->nlinvars + consdata->nconsanddatas == nvars);

   nlinvars = 0;

   conshdlr = SCIPconsGetHdlr(cons);
   assert(conshdlr != NULL);
   conshdlrdata = SCIPconshdlrGetData(conshdlr);
   assert(conshdlrdata != NULL);
   assert(conshdlrdata->hashmap != NULL);

   nandress = 0;

   activity = 0.0;

   /* split variables into original and artificial variables and compute activity on normal linear variables (without
    * terms)
    */
   for( v = 0; v < nvars; ++v )
   {
      SCIP_VAR* hashmapvar;
      SCIP_Bool negated;

      assert(vars[v] != NULL);

      /* negated variables can also exist in the original problem, so we need to check */
      if( !SCIPhashmapExists(conshdlrdata->hashmap, (void*)(vars[v])) && SCIPvarIsNegated(vars[v]) )
      {
         hashmapvar = SCIPvarGetNegationVar(vars[v]);
         negated = TRUE;
      }
      else
      {
         hashmapvar = vars[v];
         negated = FALSE;
      }
      assert(hashmapvar != NULL);

      if( !SCIPhashmapExists(conshdlrdata->hashmap, (void*)(hashmapvar)) )
      {
         assert(!SCIPhashmapExists(conshdlrdata->hashmap, (void*)(vars[v])));

         activity += coefs[v] * SCIPgetSolVal(scip, sol, vars[v]);

         linvars[nlinvars] = vars[v];
         lincoefs[nlinvars] = coefs[v];
         ++nlinvars;
      }
      else
      {
         /* negate coefficient in case of an original negated variable */
         andress[nandress] = hashmapvar;
         if( negated )
         {
            if( !SCIPisInfinity(scip, -lhs) )
               lhs -= coefs[v];
            if( !SCIPisInfinity(scip, rhs) )
               rhs -= coefs[v];
            andcoefs[nandress] = -coefs[v];
         }
         else
            andcoefs[nandress] = coefs[v];
         ++nandress;
      }
   }
   assert(nandress == consdata->nconsanddatas);

   SCIPsortPtrReal((void**)andress, andcoefs, SCIPvarComp, nandress);

   SCIPdebugMsg(scip, "nlinvars = %d, nandress = %d\n", nlinvars, nandress);
   SCIPdebugMsg(scip, "linear activity = %g\n", activity);

   /* compute and add solution values on terms */
   for( c = consdata->nconsanddatas - 1; c >= 0; --c )
   {
      SCIP_VAR** andvars;
      int nandvars;
#ifndef NDEBUG
      SCIP_VAR* res;
#endif
      andcons = consdata->consanddatas[c]->origcons;

      /* if after during or before presolving a solution will be transformed into original space and will be checked
       * there, but origcons was already removed and only the pointer to the transformed and-constraint is existing
       */
      if( andcons == NULL )
      {
         andcons = consdata->consanddatas[c]->cons;
      }
      assert(andcons != NULL);

      andvars = SCIPgetVarsAnd(scip, andcons);
      nandvars = SCIPgetNVarsAnd(scip, andcons);

#ifndef NDEBUG
      res = SCIPgetResultantAnd(scip, andcons);
      assert(nandvars == 0 || (andvars != NULL && res != NULL));
      assert(res == andress[c]);
#endif

      andvalue = 1;
      /* check if the and-constraint is violated */
      for( v = nandvars - 1; v >= 0; --v )
      {
         andvalue *= SCIPgetSolVal(scip, sol, andvars[v]);
         if( SCIPisFeasZero(scip, andvalue) )
            break;
      }
      activity += andvalue * andcoefs[c];
   }
   SCIPdebugMsg(scip, "lhs = %g, overall activity = %g, rhs = %g\n", lhs, activity, rhs);

   /* calculate absolute and relative violation */
   lhsviol = lhs - activity;
   rhsviol = activity - rhs;

   if(lhsviol > rhsviol)
   {
      absviol = lhsviol;
      relviol = SCIPrelDiff(lhs, activity);
   }
   else
   {
      absviol = rhsviol;
      relviol = SCIPrelDiff(activity, rhs);
   }

   /* update absolute and relative violation of the solution */
   if( sol != NULL )
      SCIPupdateSolConsViolation(scip, sol, absviol, relviol);

   /* check left hand side for violation */
   if( SCIPisFeasLT(scip, activity, lhs) )
   {
      if( printreason )
      {
         SCIP_CALL( SCIPprintCons(scip, cons, NULL ) );
         SCIPinfoMessage(scip, NULL, ";\n");
         SCIPinfoMessage(scip, NULL, "violation: left hand side is violated by %.15g\n", lhs - activity);

         /* print linear constraint in SCIP_DEBUG mode too */
         SCIPdebugPrintCons(scip, SCIPconsGetData(cons)->lincons, NULL);
      }

      *violated = TRUE;
   }

   /* check right hand side for violation */
   if( SCIPisFeasGT(scip, activity, rhs) )
   {
      if( printreason )
      {
         SCIP_CALL( SCIPprintCons(scip, cons, NULL ) );
         SCIPinfoMessage(scip, NULL, ";\n");
         SCIPinfoMessage(scip, NULL, "violation: right hand side is violated by %.15g\n", activity - rhs);
      }

      *violated = TRUE;
   }

   /* free temporary memory */
   SCIPfreeBufferArray(scip, &andcoefs);
   SCIPfreeBufferArray(scip, &andress);
   SCIPfreeBufferArray(scip, &lincoefs);
   SCIPfreeBufferArray(scip, &linvars);
   SCIPfreeBufferArray(scip, &coefs);
   SCIPfreeBufferArray(scip, &vars);

   return SCIP_OKAY;
}

/** checks all and-constraints inside the pseudoboolean constraint handler for feasibility of given solution or current
 *  solution
 */
static
SCIP_RETCODE checkAndConss(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONSHDLR*const   conshdlr,           /**< pseudo boolean constraint handler */
   SCIP_SOL*const        sol,                /**< solution to be checked, or NULL for current solution */
   SCIP_Bool*const       violated            /**< pointer to store whether the constraint is violated */
   )
{
   SCIP_CONSHDLRDATA* conshdlrdata;
   SCIP_CONS* andcons;
   SCIP_VAR** vars;
   SCIP_VAR* res;
   int nvars;
   SCIP_Real andvalue;
   int c;
   int v;

   assert(scip != NULL);
   assert(conshdlr != NULL);
   assert(violated != NULL);

   conshdlrdata = SCIPconshdlrGetData(conshdlr);
   assert(conshdlrdata != NULL);

   *violated = FALSE;

   for( c = conshdlrdata->nallconsanddatas - 1; c >= 0; --c )
   {
      if( !conshdlrdata->allconsanddatas[c]->istransformed )
         continue;

      andcons = conshdlrdata->allconsanddatas[c]->cons;

      /* need to check even locally deleted constraints */
      if( andcons == NULL ) /*|| !SCIPconsIsActive(andcons) )*/
         continue;

      vars = SCIPgetVarsAnd(scip, andcons);
      nvars = SCIPgetNVarsAnd(scip, andcons);
      res = SCIPgetResultantAnd(scip, andcons);
      assert(nvars == 0 || (vars != NULL && res != NULL));

      andvalue = 1;
      /* check if the and-constraint is violated */
      for( v = nvars - 1; v >= 0; --v )
      {
         andvalue *= SCIPgetSolVal(scip, sol, vars[v]);
         if( SCIPisFeasZero(scip, andvalue) )
            break;
      }

      /* check for violation and update aging */
      if( !SCIPisFeasEQ(scip, andvalue, SCIPgetSolVal(scip, sol, res)) )
      {
         /* only reset constraint age if we are in enforcement */
         if( sol == NULL )
         {
            SCIP_CALL( SCIPresetConsAge(scip, andcons) );
         }

         *violated = TRUE;
         break;
      }
      else if( sol == NULL )
      {
         SCIP_CALL( SCIPincConsAge(scip, andcons) );
      }
   }

   return SCIP_OKAY;
}

/** creates by copying and captures a linear constraint */
static
SCIP_RETCODE copyConsPseudoboolean(
   SCIP*const            targetscip,         /**< target SCIP data structure */
   SCIP_CONS**           targetcons,         /**< pointer to store the created target constraint */
   SCIP*const            sourcescip,         /**< source SCIP data structure */
   SCIP_CONS*const       sourcecons,         /**< source constraint which will be copied */
   const char*           name,               /**< name of constraint */
   SCIP_HASHMAP*const    varmap,             /**< a SCIP_HASHMAP mapping variables of the source SCIP to corresponding
                                              *   variables of the target SCIP */
   SCIP_HASHMAP*const    consmap,            /**< a hashmap to store the mapping of source constraints to the corresponding
                                              *   target constraints */
   SCIP_Bool const       initial,            /**< should the LP relaxation of constraint be in the initial LP? */
   SCIP_Bool const       separate,           /**< should the constraint be separated during LP processing? */
   SCIP_Bool const       enforce,            /**< should the constraint be enforced during node processing? */
   SCIP_Bool const       check,              /**< should the constraint be checked for feasibility? */
   SCIP_Bool const       propagate,          /**< should the constraint be propagated during node processing? */
   SCIP_Bool const       local,              /**< is constraint only valid locally? */
   SCIP_Bool const       modifiable,         /**< is constraint modifiable (subject to column generation)? */
   SCIP_Bool const       dynamic,            /**< is constraint subject to aging? */
   SCIP_Bool const       removable,          /**< should the relaxation be removed from the LP due to aging or cleanup? */
   SCIP_Bool const       stickingatnode,     /**< should the constraint always be kept at the node where it was added, even
                                              *   if it may be moved to a more global node? */
   SCIP_Bool const       global,             /**< create a global or a local copy? */
   SCIP_Bool*const       valid               /**< pointer to store if the copying was valid */
   )
{
   SCIP_CONSDATA* sourceconsdata;
   SCIP_CONS* sourcelincons;

   assert(targetscip != NULL);
   assert(targetcons != NULL);
   assert(sourcescip != NULL);
   assert(sourcecons != NULL);
   assert(strcmp(SCIPconshdlrGetName(SCIPconsGetHdlr(sourcecons)), CONSHDLR_NAME) == 0);
   assert(valid != NULL);

   *valid = TRUE;

   sourceconsdata = SCIPconsGetData(sourcecons);
   assert(sourceconsdata != NULL);

   /* get linear constraint */
   sourcelincons = sourceconsdata->lincons;
   assert(sourcelincons != NULL);

   /* get copied version of linear constraint */
   if( !SCIPconsIsDeleted(sourcelincons) )
   {
      SCIP_CONSHDLR* conshdlrlinear;
      SCIP_CONS* targetlincons;
      SCIP_CONS** targetandconss;
      SCIP_Real* targetandcoefs;
      int ntargetandconss;
      SCIP_LINEARCONSTYPE targetlinconstype;

      targetlinconstype = sourceconsdata->linconstype;

      switch( targetlinconstype )
      {
      case SCIP_LINEARCONSTYPE_LINEAR:
         conshdlrlinear = SCIPfindConshdlr(sourcescip, "linear");
         assert(conshdlrlinear != NULL);
         break;
      case SCIP_LINEARCONSTYPE_LOGICOR:
         conshdlrlinear = SCIPfindConshdlr(sourcescip, "logicor");
         assert(conshdlrlinear != NULL);
         break;
      case SCIP_LINEARCONSTYPE_KNAPSACK:
         conshdlrlinear = SCIPfindConshdlr(sourcescip, "knapsack");
         assert(conshdlrlinear != NULL);
         break;
      case SCIP_LINEARCONSTYPE_SETPPC:
         conshdlrlinear = SCIPfindConshdlr(sourcescip, "setppc");
         assert(conshdlrlinear != NULL);
         break;
#ifdef WITHEQKNAPSACK
      case SCIP_LINEARCONSTYPE_EQKNAPSACK:
         conshdlrlinear = SCIPfindConshdlr(sourcescip, "eqknapsack");
         assert(conshdlrlinear != NULL);
         break;
#endif
      case SCIP_LINEARCONSTYPE_INVALIDCONS:
      default:
         SCIPerrorMessage("unknown linear constraint type\n");
         return SCIP_INVALIDDATA;
      }

      if( conshdlrlinear == NULL ) /*lint !e774*/
      {
         SCIPerrorMessage("linear constraint handler not found\n");
         return SCIP_INVALIDDATA;
      }

      targetlincons = NULL;

      /* copy linear constraint */
      SCIP_CALL( SCIPgetConsCopy(sourcescip, targetscip, sourcelincons, &targetlincons, conshdlrlinear, varmap, consmap, SCIPconsGetName(sourcelincons),
            SCIPconsIsInitial(sourcelincons), SCIPconsIsSeparated(sourcelincons), SCIPconsIsEnforced(sourcelincons), SCIPconsIsChecked(sourcelincons),
            SCIPconsIsPropagated(sourcelincons), SCIPconsIsLocal(sourcelincons), SCIPconsIsModifiable(sourcelincons), SCIPconsIsDynamic(sourcelincons),
            SCIPconsIsRemovable(sourcelincons), SCIPconsIsStickingAtNode(sourcelincons), global, valid) );

      if( *valid )
      {
         assert(targetlincons != NULL);
         assert(SCIPconsGetHdlr(targetlincons) != NULL);
         /* @note  due to copying special linear constraints, now leads only to simple linear constraints, we check that
          *        our target constraint handler is the same as our source constraint handler of the linear constraint,
          *        if not copying was not valid
          */
         if( strcmp(SCIPconshdlrGetName(SCIPconsGetHdlr(targetlincons)), "linear") == 0 )
            targetlinconstype = SCIP_LINEARCONSTYPE_LINEAR;
      }

      targetandconss = NULL;
      targetandcoefs = NULL;
      ntargetandconss = 0;

      if( *valid )
      {
         SCIP_CONSHDLR* conshdlrand;
         int c;
         int nsourceandconss;
         SCIP_HASHTABLE* linconsvarsmap;
         SCIP_VAR** targetlinvars;
         SCIP_Real* targetlincoefs;
         int ntargetlinvars;

         conshdlrand = SCIPfindConshdlr(sourcescip, "and");
         assert(conshdlrand != NULL);

         nsourceandconss = sourceconsdata->nconsanddatas;

         /* allocate temporary memory */
         SCIP_CALL( SCIPallocBufferArray(sourcescip, &targetandconss, nsourceandconss) );
         SCIP_CALL( SCIPallocBufferArray(sourcescip, &targetandcoefs, nsourceandconss) );

         /* get the number of vars in the copied linear constraint and allocate buffers
          * for the variables and the coefficients
          */
         SCIP_CALL( getLinearConsNVars(targetscip, targetlincons, targetlinconstype, &ntargetlinvars) );
         SCIP_CALL( SCIPallocBufferArray(sourcescip, &targetlinvars, ntargetlinvars) );
         SCIP_CALL( SCIPallocBufferArray(sourcescip, &targetlincoefs, ntargetlinvars) );

         /* retrieve the variables of the copied linear constraint */
         SCIP_CALL( getLinearConsVarsData(targetscip, targetlincons, targetlinconstype,
                                          targetlinvars, targetlincoefs, &ntargetlinvars) );

         /* now create a hashtable and insert the variables into it, so that it
          * can be checked in constant time if a variable was removed due to
          * compressed copying when looping over the and resultants
          */
         SCIP_CALL( SCIPhashtableCreate(&linconsvarsmap, SCIPblkmem(targetscip), ntargetlinvars, SCIPvarGetHashkey,
                                        SCIPvarIsHashkeyEq, SCIPvarGetHashkeyVal, NULL) );

         for( c = 0 ; c < ntargetlinvars; ++c )
         {
            SCIP_CALL( SCIPhashtableInsert(linconsvarsmap, targetlinvars[c]) );
         }

         /* free the buffer arrays that were only required for building the hastable */
         SCIPfreeBufferArray(sourcescip, &targetlincoefs);
         SCIPfreeBufferArray(sourcescip, &targetlinvars);

         for( c = 0 ; c < nsourceandconss; ++c )
         {
            CONSANDDATA* consanddata;
            SCIP_CONS* oldcons;
            SCIP_VAR* targetandresultant;
            SCIP_Bool validand;

            consanddata = sourceconsdata->consanddatas[c];
            assert(consanddata != NULL);

            oldcons = consanddata->cons;
            assert(oldcons != NULL);

            targetandresultant = (SCIP_VAR*) SCIPhashmapGetImage(varmap, SCIPgetResultantAnd(sourcescip, oldcons));
            assert(targetandresultant != NULL);

            /* if compressed copying is active, the resultant might not have been copied by the linear
             * constraint and we don't need to add it to the pseudo boolean constraint in this case
             */
            if( !SCIPhashtableExists(linconsvarsmap, targetandresultant) )
               continue;

            validand = TRUE;

            targetandconss[ntargetandconss] = NULL;

            /* copy and-constraints */
            SCIP_CALL( SCIPgetConsCopy(sourcescip, targetscip, oldcons, &targetandconss[ntargetandconss], conshdlrand, varmap, consmap, SCIPconsGetName(oldcons),
                  SCIPconsIsInitial(oldcons), SCIPconsIsSeparated(oldcons), SCIPconsIsEnforced(oldcons), SCIPconsIsChecked(oldcons),
                  SCIPconsIsPropagated(oldcons), SCIPconsIsLocal(oldcons), SCIPconsIsModifiable(oldcons), SCIPconsIsDynamic(oldcons),
                  SCIPconsIsRemovable(oldcons), SCIPconsIsStickingAtNode(oldcons), global, &validand) );

            *valid &= validand;

            if( validand )
            {
               targetandcoefs[ntargetandconss] = sourceconsdata->andcoefs[c];
               ++ntargetandconss;
            }
         }

         SCIPhashtableFree(&linconsvarsmap);
         assert(ntargetandconss <= ntargetlinvars);
      }

      /* no correct pseudoboolean constraint */
      if( ntargetandconss == 0 )
      {
         SCIPdebugMsg(sourcescip, "no and-constraints copied for pseudoboolean constraint <%s>\n", SCIPconsGetName(sourcecons));
         *valid = FALSE;
      }

      if( *valid )
      {
         SCIP_Real targetrhs;
         SCIP_Real targetlhs;

         SCIP_VAR* intvar;
         SCIP_VAR* indvar;
         const char* consname;

         /* third the indicator and artificial integer variable part */
         assert(sourceconsdata->issoftcons == (sourceconsdata->indvar != NULL));
         indvar = sourceconsdata->indvar;
         intvar = sourceconsdata->intvar;

         /* copy indicator variable */
         if( indvar != NULL )
         {
            assert(*valid);
            SCIP_CALL( SCIPgetVarCopy(sourcescip, targetscip, indvar, &indvar, varmap, consmap, global, valid) );
            assert(!(*valid) || indvar != NULL);
         }
         /* copy artificial integer variable */
         if( intvar != NULL && *valid )
         {
            SCIP_CALL( SCIPgetVarCopy(sourcescip, targetscip, intvar, &intvar, varmap, consmap, global, valid) );
            assert(!(*valid) || intvar != NULL);
         }

         if( *valid )
         {
            if( name != NULL )
               consname = name;
            else
               consname = SCIPconsGetName(sourcecons);

            /* get new left and right hand sides of copied linear constraint since
             * they might have changed if compressed copying is used
             */
            SCIP_CALL( getLinearConsSides(targetscip, targetlincons, targetlinconstype, &targetlhs, &targetrhs) );

            /* create new pseudoboolean constraint */
            /* coverity[var_deref_op] */
            /* coverity[var_deref_model] */
            SCIP_CALL( SCIPcreateConsPseudobooleanWithConss(targetscip, targetcons, consname,
                  targetlincons, targetlinconstype, targetandconss, targetandcoefs, ntargetandconss,
                  indvar, sourceconsdata->weight, sourceconsdata->issoftcons, intvar, targetlhs, targetrhs,
                  initial, separate, enforce, check, propagate, local, modifiable, dynamic, removable, stickingatnode) );
         }
      }

      if( !(*valid) && !SCIPisConsCompressionEnabled(sourcescip) )
      {
         SCIPverbMessage(sourcescip, SCIP_VERBLEVEL_MINIMAL, NULL, "could not copy constraint <%s>\n", SCIPconsGetName(sourcecons));
      }

      /* release copied linear constraint */
      if( targetlincons != NULL )
      {
         SCIP_CALL( SCIPreleaseCons(targetscip, &targetlincons) );
      }

      /* release copied and constraint */
      if( targetandconss != NULL )
      {
         int c;

         assert(ntargetandconss <= sourceconsdata->nconsanddatas);

         for( c = 0 ; c < ntargetandconss; ++c )
         {
            if( targetandconss[c] != NULL )
            {
               SCIP_CALL( SCIPreleaseCons(targetscip, &targetandconss[c]) );
            }
         }
      }

      /* free temporary memory */
      SCIPfreeBufferArrayNull(sourcescip, &targetandcoefs);
      SCIPfreeBufferArrayNull(sourcescip, &targetandconss);
   }
   else
      *valid = FALSE;

   return SCIP_OKAY;
}

/** compute all changes in consanddatas array */
static
SCIP_RETCODE computeConsAndDataChanges(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONSHDLRDATA*const conshdlrdata      /**< pseudoboolean constraint handler data */
   )
{
   CONSANDDATA** allconsanddatas;
   CONSANDDATA* consanddata;
   int c;

   assert(scip != NULL);
   assert(conshdlrdata != NULL);

   allconsanddatas = conshdlrdata->allconsanddatas;
   assert(allconsanddatas != NULL);
   assert(conshdlrdata->nallconsanddatas > 0);
   assert(conshdlrdata->nallconsanddatas <= conshdlrdata->sallconsanddatas);

   for( c = conshdlrdata->nallconsanddatas - 1; c >= 0; --c )
   {
      SCIP_CONS* cons;
      SCIP_VAR** vars;
      int nvars;
      SCIP_VAR** newvars;
      int nnewvars;
      int v;

      consanddata = allconsanddatas[c];

      if( !consanddata->istransformed )
         continue;

      if( consanddata->nuses == 0 )
         continue;

      vars = consanddata->vars;
      nvars = consanddata->nvars;
      assert(nvars == 0 || vars != NULL);
      assert(consanddata->nnewvars == 0 && ((consanddata->snewvars > 0) == (consanddata->newvars != NULL)));

      if( nvars == 0 )
      {
#ifndef NDEBUG
         /* if an old consanddata-object has no variables left there should be no new variables */
         if( consanddata->cons != NULL )
            assert(SCIPgetNVarsAnd(scip, consanddata->cons) == 0);
#endif
         continue;
      }

      cons = consanddata->cons;
      assert(cons != NULL);

      if( SCIPconsIsDeleted(cons) )
         continue;

      /* sort and-variables */
      if( !SCIPisAndConsSorted(scip, consanddata->cons) )
      {
         SCIP_CALL( SCIPsortAndCons(scip, consanddata->cons) );
         assert(SCIPisAndConsSorted(scip, consanddata->cons));
      }

      /* get new and-variables */
      nnewvars = SCIPgetNVarsAnd(scip, consanddata->cons);
      newvars = SCIPgetVarsAnd(scip, consanddata->cons);

      /* stop if the constraint has no variables or there was an error (coverity issue) */
      if( nnewvars <= 0 )
         continue;

#ifndef NDEBUG
      /* check that old variables are sorted */
      for( v = nvars - 1; v > 0; --v )
         assert(SCIPvarGetIndex(vars[v]) >= SCIPvarGetIndex(vars[v - 1]));
      /* check that new variables are sorted */
      for( v = nnewvars - 1; v > 0; --v )
         assert(SCIPvarGetIndex(newvars[v]) >= SCIPvarGetIndex(newvars[v - 1]));
#endif

      /* check for changings, if and-constraint did not change we do not need to copy all variables */
      if( nvars == nnewvars )
      {
         SCIP_Bool changed;

         changed = FALSE;

         /* check each variable */
         for( v = nvars - 1; v >= 0; --v )
         {
            if( vars[v] != newvars[v] )
            {
               changed = TRUE;
               break;
            }
         }

         if( !changed )
            continue;
      }

      /* resize newvars array if necessary */
      if( nnewvars > consanddata->snewvars )
      {
         SCIP_CALL( SCIPensureBlockMemoryArray(scip, &(consanddata->newvars), &(consanddata->snewvars), nnewvars) );
      }

      /* copy all variables */
      BMScopyMemoryArray(consanddata->newvars, newvars, nnewvars);
      consanddata->nnewvars = nnewvars;

      /* capture all variables */
      for( v = consanddata->nnewvars - 1; v >= 0; --v )
      {
         /* in original problem the variables was already deleted */
         assert(consanddata->newvars[v] != NULL);
         SCIP_CALL( SCIPcaptureVar(scip, consanddata->newvars[v]) );
      }
   }

   return SCIP_OKAY;
}

/** remove old locks */
static
SCIP_RETCODE removeOldLocks(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< pseudoboolean constraint */
   CONSANDDATA*const     consanddata,        /**< CONSANDDATA object for which we want to delete the locks and the
                                              *   capture of the corresponding and-constraint */
   SCIP_Real const       coef,               /**< coefficient which led to old locks */
   SCIP_Real const       lhs,                /**< left hand side which led to old locks */
   SCIP_Real const       rhs                 /**< right hand side which led to old locks */
   )
{
   assert(scip != NULL);
   assert(cons != NULL);
   assert(consanddata != NULL);
   assert(!SCIPisInfinity(scip, coef) && !SCIPisInfinity(scip, -coef));
   assert(!SCIPisInfinity(scip, lhs));
   assert(!SCIPisInfinity(scip, -rhs));
   assert(SCIPisLE(scip, lhs, rhs));

   /* remove rounding locks */
   SCIP_CALL( unlockRoundingAndCons(scip, cons, consanddata, coef, lhs, rhs) );

   assert(consanddata->cons != NULL);

   return SCIP_OKAY;
}

/** add new locks */
static
SCIP_RETCODE addNewLocks(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< pseudoboolean constraint */
   CONSANDDATA*const     consanddata,        /**< CONSANDDATA object for which we want to delete the locks and the
                                              *   capture of the corresponding and-constraint */
   SCIP_Real const       coef,               /**< coefficient which lead to new locks */
   SCIP_Real const       lhs,                /**< left hand side which lead to new locks */
   SCIP_Real const       rhs                 /**< right hand side which lead to new locks */
   )
{
   assert(scip != NULL);
   assert(cons != NULL);
   assert(consanddata != NULL);
   assert(!SCIPisInfinity(scip, coef) && !SCIPisInfinity(scip, -coef));
   assert(!SCIPisInfinity(scip, lhs));
   assert(!SCIPisInfinity(scip, -rhs));
   assert(SCIPisLE(scip, lhs, rhs));

   /* add rounding locks due to old variables in consanddata object */
   SCIP_CALL( lockRoundingAndCons(scip, cons, consanddata, coef, lhs, rhs) );

   assert(consanddata->cons != NULL);

   return SCIP_OKAY;
}

/** update all locks inside this constraint and all captures on all and-constraints */
static
SCIP_RETCODE correctLocksAndCaptures(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< pseudoboolean constraint */
   SCIP_CONSHDLRDATA*const conshdlrdata,     /**< pseudoboolean constraint handler data */
   SCIP_Real const       newlhs,             /**< new left hand side of pseudoboolean constraint */
   SCIP_Real const       newrhs,             /**< new right hand side of pseudoboolean constraint */
   SCIP_VAR**const       andress,            /**< current and-resultants in pseudoboolean constraint */
   SCIP_Real*const       andcoefs,           /**< current and-resultants-coeffcients in pseudoboolean constraint */
   SCIP_Bool*const       andnegs,            /**< current negation status of and-resultants in pseudoboolean constraint */
   int const             nandress            /**< number of current and-resultants in pseudoboolean constraint */
   )
{
   CONSANDDATA** newconsanddatas;
   int nnewconsanddatas;
   int snewconsanddatas;
   SCIP_Real* newandcoefs;
   SCIP_Real* oldandcoefs;
   SCIP_Bool* newandnegs;
   SCIP_Bool* oldandnegs;
   CONSANDDATA** consanddatas;
   int nconsanddatas;
   SCIP_CONSDATA* consdata;
   int oldnvars;
   int c;
   int c1;

   assert(scip != NULL);
   assert(cons != NULL);
   assert(conshdlrdata != NULL);
   assert(conshdlrdata->hashmap != NULL);
   assert(nandress == 0 || (andress != NULL && andcoefs != NULL));
   assert(!SCIPisInfinity(scip, newlhs));
   assert(!SCIPisInfinity(scip, -newrhs));
   assert(SCIPisLE(scip, newlhs, newrhs));

   consdata = SCIPconsGetData(cons);
   assert(consdata != NULL);

   /* sort and-constraints after indices of corresponding and-resultants */
   SCIPsortPtrRealBool((void**)(consdata->consanddatas), consdata->andcoefs, consdata->andnegs, resvarCompWithInactive, consdata->nconsanddatas);

   consanddatas = consdata->consanddatas;
   oldandcoefs = consdata->andcoefs;
   oldandnegs = consdata->andnegs;
   nconsanddatas = consdata->nconsanddatas;
   assert(nconsanddatas == 0 || (consanddatas != NULL && oldandcoefs != NULL));

#ifndef NDEBUG
   /* check that and-resultants are sorted, and coefficents are not zero */
   for( c = nandress - 1; c > 0; --c )
   {
      assert(!SCIPisZero(scip, andcoefs[c]));
      assert(SCIPvarGetIndex(andress[c]) > SCIPvarGetIndex(andress[c - 1]));
   }
   /* check that consanddata objects are sorted due to the index of the corresponding resultants, and coefficents are
    * not zero
    */
   for( c = nconsanddatas - 1; c > 0; --c )
   {
      SCIP_VAR* res1;
      SCIP_VAR* res2;

      assert(consanddatas[c] != NULL);

      if( !consanddatas[c]->istransformed )
         continue;

      assert(!SCIPisZero(scip, oldandcoefs[c]));
      assert(consanddatas[c - 1] != NULL);

      if( !consanddatas[c - 1]->istransformed )
         continue;

      assert(!SCIPisZero(scip, oldandcoefs[c - 1]));

      if( SCIPconsIsDeleted(consanddatas[c]->cons) || SCIPconsIsDeleted(consanddatas[c - 1]->cons) )
         continue;

      assert(consanddatas[c]->cons != NULL);
      res1 = SCIPgetResultantAnd(scip, consanddatas[c]->cons);
      assert(res1 != NULL);
      assert(consanddatas[c - 1]->cons != NULL);
      res2 = SCIPgetResultantAnd(scip, consanddatas[c - 1]->cons);
      assert(res2 != NULL);

      assert(SCIPvarGetIndex(res1) >= SCIPvarGetIndex(res2));
   }
#endif

   snewconsanddatas = nconsanddatas + nandress;

   /* allocate new block memory arrays */
   SCIP_CALL( SCIPallocBlockMemoryArray(scip, &newconsanddatas, snewconsanddatas) );
   SCIP_CALL( SCIPallocBlockMemoryArray(scip, &newandcoefs, snewconsanddatas) );
   SCIP_CALL( SCIPallocBlockMemoryArray(scip, &newandnegs, snewconsanddatas) );

   nnewconsanddatas = 0;

   /* collect new consanddata objects and update locks and captures */
   for( c = 0, c1 = 0; c < nconsanddatas && c1 < nandress; )
   {
      SCIP_CONS* andcons;
      SCIP_VAR* res1;
      SCIP_VAR* res2;

      assert(consanddatas[c] != NULL);

      /* consanddata object could have been deleted in the last presolving round */
      if( !consanddatas[c]->istransformed )
      {
         ++c;
         consdata->changed = TRUE;
         consdata->upgradetried = FALSE;
         continue;
      }

      andcons = consanddatas[c]->cons;
      assert(andcons != NULL);

      if( andcons == NULL ) /*lint !e774*/
      {
         ++c;
         consdata->changed = TRUE;
         consdata->upgradetried = FALSE;
         continue;
      }
      else if( SCIPconsIsDeleted(andcons) )
      {
         /* remove rounding locks, because the and constraint was deleted  */
         SCIP_CALL( unlockRoundingAndCons(scip, cons, consanddatas[c],
               oldandnegs[c] ? -oldandcoefs[c] : oldandcoefs[c], consdata->lhs, consdata->rhs) );
         ++c;
         consdata->changed = TRUE;
         consdata->upgradetried = FALSE;
         continue;
      }
      assert(andcons != NULL);

      /* get and-resultants of consanddata object in constraint data */
      res1 = SCIPgetResultantAnd(scip, andcons);
      assert(res1 != NULL);
      assert(SCIPhashmapGetImage(conshdlrdata->hashmap, (void*)res1) == consanddatas[c]);

      /* get and-resultants in new corresponding linear constraint */
      res2 = andress[c1];
      assert(res2 != NULL);
      assert(SCIPhashmapGetImage(conshdlrdata->hashmap, (void*)res2) != NULL);

      /* collect new consanddata objects in sorted order due to the variable index of corresponding and-resultants */
      if( SCIPvarGetIndex(res1) < SCIPvarGetIndex(res2) )
      {
         assert(consanddatas[c]->nuses > 0);
         --(consanddatas[c]->nuses);

         /* remove old locks */
         SCIP_CALL( removeOldLocks(scip, cons, consanddatas[c], oldandnegs[c] ? -oldandcoefs[c] : oldandcoefs[c],
               consdata->lhs, consdata->rhs) );
         ++c;
         consdata->changed = TRUE;
         consdata->upgradetried = FALSE;
         consdata->propagated = FALSE;
         consdata->presolved = FALSE;
      }
      else if( SCIPvarGetIndex(res1) > SCIPvarGetIndex(res2) )
      {
         assert(SCIPhashmapExists(conshdlrdata->hashmap, (void*)res2));
         newconsanddatas[nnewconsanddatas] = (CONSANDDATA*) SCIPhashmapGetImage(conshdlrdata->hashmap, (void*)res2);
         newandcoefs[nnewconsanddatas] = andcoefs[c1];
         newandnegs[nnewconsanddatas] = andnegs[c1];
         ++(newconsanddatas[nnewconsanddatas]->nuses);

         /* add new locks */
         SCIP_CALL( addNewLocks(scip, cons, newconsanddatas[nnewconsanddatas], newandnegs[nnewconsanddatas] ?
               -newandcoefs[nnewconsanddatas] : newandcoefs[nnewconsanddatas], newlhs, newrhs) );
         ++c1;
         consdata->changed = TRUE;
         consdata->upgradetried = FALSE;
         consdata->cliquesadded = FALSE;
         consdata->propagated = FALSE;
         consdata->presolved = FALSE;

         ++nnewconsanddatas;
      }
      else
      {
         SCIP_Bool coefsignchanged;
         SCIP_Bool lhschanged;
         SCIP_Bool rhschanged;

         assert(SCIPhashmapGetImage(conshdlrdata->hashmap, (void*)res2) == consanddatas[c]);

         /* copy old consanddata object and new coefficent */
         newconsanddatas[nnewconsanddatas] = consanddatas[c];

         newandcoefs[nnewconsanddatas] = andcoefs[c1];
         newandnegs[nnewconsanddatas] = andnegs[c1];

         if( ((oldandnegs[c] == andnegs[c1]) && !SCIPisEQ(scip, oldandcoefs[c], newandcoefs[c1]))
            || ((oldandnegs[c] != newandnegs[c1]) && !SCIPisEQ(scip, oldandcoefs[c], -newandcoefs[c1])) )
            consdata->upgradetried = FALSE;

         coefsignchanged = (oldandnegs[c] == andnegs[c1]) &&
            ((oldandcoefs[c] < 0 && andcoefs[c1] > 0) || (oldandcoefs[c] > 0 && andcoefs[c1] < 0));
         coefsignchanged = coefsignchanged || ((oldandnegs[c] != andnegs[c1]) &&
            ((oldandcoefs[c] < 0 && andcoefs[c1] < 0) || (oldandcoefs[c] > 0 && andcoefs[c1] > 0)));
         lhschanged = (SCIPisInfinity(scip, -consdata->lhs) && !SCIPisInfinity(scip, -newlhs)) || (!SCIPisInfinity(scip, -consdata->lhs) && SCIPisInfinity(scip, -newlhs))
            || (consdata->lhs < 0 && newlhs > 0) || (consdata->lhs > 0 && newlhs < 0);
         rhschanged = (SCIPisInfinity(scip, consdata->rhs) && !SCIPisInfinity(scip, newrhs)) || (!SCIPisInfinity(scip, consdata->rhs) && SCIPisInfinity(scip, newrhs))
            || (consdata->rhs < 0 && newrhs > 0) || (consdata->rhs > 0 && newrhs < 0);

         /* update or renew locks */
         if( coefsignchanged || lhschanged || rhschanged || newconsanddatas[nnewconsanddatas]->nnewvars > 0)
         {
            /* renew locks */
            SCIP_CALL( removeOldLocks(scip, cons, newconsanddatas[nnewconsanddatas], oldandnegs[c] ?
                  -oldandcoefs[c] : oldandcoefs[c], consdata->lhs, consdata->rhs) );
            SCIP_CALL( addNewLocks(scip, cons, newconsanddatas[nnewconsanddatas], newandnegs[nnewconsanddatas] ?
                  -newandcoefs[nnewconsanddatas] : newandcoefs[nnewconsanddatas], newlhs, newrhs) );

            consdata->changed = TRUE;
            consdata->upgradetried = FALSE;
            consdata->cliquesadded = FALSE;
            consdata->propagated = FALSE;
            consdata->presolved = FALSE;
         }

         ++c;
         ++c1;
         ++nnewconsanddatas;
      }
   }

   /* add all remaining consanddatas and update locks and captures */
   if( c < nconsanddatas )
   {
      assert(c1 == nandress);

      for( ; c < nconsanddatas; ++c )
      {
         SCIP_CONS* andcons;
#ifndef NDEBUG
         SCIP_VAR* res1;

         assert(consanddatas[c] != NULL);
#endif
         andcons = consanddatas[c]->cons;
#ifndef NDEBUG
         if( andcons != NULL )
         {
            res1 = SCIPgetResultantAnd(scip, andcons);
            assert(res1 != NULL);
            assert(SCIPhashmapGetImage(conshdlrdata->hashmap, (void*)res1) == consanddatas[c]);
         }
#endif
         if( andcons == NULL )
         {
            consdata->changed = TRUE;
            consdata->upgradetried = FALSE;
            continue;
         }

         assert(consanddatas[c]->nuses > 0);
         --(consanddatas[c]->nuses);

         /* remove old locks */
         SCIP_CALL( removeOldLocks(scip, cons, consanddatas[c], oldandnegs[c] ? -oldandcoefs[c] : oldandcoefs[c],
               consdata->lhs, consdata->rhs) );
         consdata->changed = TRUE;
         consdata->upgradetried = FALSE;
         consdata->propagated = FALSE;
         consdata->presolved = FALSE;
      }
   }
   else if( c1 < nandress )
   {
      for( ; c1 < nandress; ++c1 )
      {
         SCIP_VAR* res2;

         res2 = andress[c1];
         assert(res2 != NULL);
         assert(SCIPhashmapExists(conshdlrdata->hashmap, (void*)res2));
         newconsanddatas[nnewconsanddatas] = (CONSANDDATA*) SCIPhashmapGetImage(conshdlrdata->hashmap, (void*)res2);
         newandcoefs[nnewconsanddatas] = andcoefs[c1];
         newandnegs[nnewconsanddatas] = andnegs[c1];
         ++(newconsanddatas[nnewconsanddatas]->nuses);

         /* add new locks */
         SCIP_CALL( addNewLocks(scip, cons, newconsanddatas[nnewconsanddatas], newandnegs[nnewconsanddatas] ?
               -newandcoefs[nnewconsanddatas] : newandcoefs[nnewconsanddatas], newlhs, newrhs) );

         ++nnewconsanddatas;
         consdata->changed = TRUE;
         consdata->upgradetried = FALSE;
         consdata->cliquesadded = FALSE;
         consdata->propagated = FALSE;
         consdata->presolved = FALSE;
      }
   }
   assert(c == nconsanddatas && c1 == nandress);

   /* delete old and-coefficients and consanddata objects */
   SCIPfreeBlockMemoryArray(scip, &(consdata->andcoefs), consdata->sconsanddatas);
   SCIPfreeBlockMemoryArray(scip, &(consdata->andnegs), consdata->sconsanddatas);
   SCIPfreeBlockMemoryArray(scip, &(consdata->consanddatas), consdata->sconsanddatas);

   if( !SCIPisEQ(scip, consdata->lhs, newlhs) || !SCIPisEQ(scip, consdata->rhs, newrhs) )
   {
      consdata->upgradetried = FALSE;
      consdata->lhs = newlhs;
      consdata->rhs = newrhs;
   }

   consdata->consanddatas = newconsanddatas;
   consdata->andcoefs = newandcoefs;
   consdata->andnegs = newandnegs;
   consdata->nconsanddatas = nnewconsanddatas;
   consdata->sconsanddatas = snewconsanddatas;

   oldnvars = consdata->nlinvars;
   /* update number of linear variables without and-resultants */
   SCIP_CALL( getLinearConsNVars(scip, consdata->lincons, consdata->linconstype, &(consdata->nlinvars)) );
   consdata->nlinvars -= nnewconsanddatas;

   if( oldnvars != consdata->nlinvars )
   {
      consdata->changed = TRUE;
      consdata->upgradetried = FALSE;
      consdata->cliquesadded = FALSE;
      consdata->propagated = FALSE;
      consdata->presolved = FALSE;
   }

   /* we need to re-sort and-constraints after indices of corresponding and-resultants, since we might have replaced
    * negated variables
    */
   SCIPsortPtrRealBool((void**)(consdata->consanddatas), consdata->andcoefs, consdata->andnegs, resvarCompWithInactive, consdata->nconsanddatas);

#ifndef NDEBUG
   consanddatas = consdata->consanddatas;
   nconsanddatas = consdata->nconsanddatas;
   assert(nconsanddatas == 0 || consanddatas != NULL);

   /* check that consanddata objects are sorted with respect to the index of the corresponding resultants */
   for( c = nconsanddatas - 1; c > 0; --c )
   {
      SCIP_VAR* res1;
      SCIP_VAR* res2;

      assert(consanddatas[c] != NULL);
      assert(consanddatas[c]->cons != NULL);
      res1 = SCIPgetResultantAnd(scip, consanddatas[c]->cons);
      assert(res1 != NULL);
      assert(consanddatas[c - 1] != NULL);
      assert(consanddatas[c - 1]->cons != NULL);
      res2 = SCIPgetResultantAnd(scip, consanddatas[c - 1]->cons);
      assert(res2 != NULL);

      assert(SCIPvarGetIndex(res1) > SCIPvarGetIndex(res2));
   }
#endif

   return SCIP_OKAY;
}

/** adds cliques of the pseudoboolean constraint to the global clique table */
static
SCIP_RETCODE addCliques(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< pseudoboolean constraint */
   SCIP_Bool*const       cutoff,             /**< pointer to store whether the node can be cut off */
   int*const             naggrvars,          /**< pointer to count the number of aggregated variables */
   int*const             nchgbds             /**< pointer to count the number of performed bound changes */
   )
{
   SCIP_CONSDATA* consdata;
   SCIP_VAR** vars;
   int nvars;
   SCIP_VAR** linvars;
   SCIP_VAR* andres;
   SCIP_VAR* andres2;
   int nlinvars;
   int nandress;
   int c;
   int v2;
   int v1;
   int nchgbdslocal;

   assert(scip != NULL);
   assert(cons != NULL);
   assert(cutoff != NULL);
   assert(naggrvars != NULL);
   assert(nchgbds != NULL);
   assert(SCIPconsIsActive(cons));

   *cutoff = FALSE;

   consdata = SCIPconsGetData(cons);
   assert(consdata != NULL);
   /* if we have no and-constraints left, we should not be here and this constraint should be deleted (only the linaer should survive) */
   assert(consdata->nconsanddatas > 0);

   /* check whether the cliques have already been added */
   if( consdata->cliquesadded )
      return SCIP_OKAY;

   consdata->cliquesadded = TRUE;

   checkConsConsistency(scip, cons);

   /* check standard pointers and sizes */
   assert(consdata->lincons != NULL);
   assert(SCIPconsIsActive(consdata->lincons));
   assert(consdata->linconstype > SCIP_LINEARCONSTYPE_INVALIDCONS);
   assert(consdata->consanddatas != NULL);
   assert(consdata->nconsanddatas > 0);
   assert(consdata->nconsanddatas <= consdata->sconsanddatas);

   /* check number of linear variables */
   SCIP_CALL( getLinearConsNVars(scip, consdata->lincons, consdata->linconstype, &nvars) );
   assert(nvars == consdata->nlinvars + consdata->nconsanddatas);

   /* get temporary memory */
   SCIP_CALL( SCIPallocBufferArray(scip, &vars, nvars) );
   SCIP_CALL( SCIPallocBufferArray(scip, &linvars, nvars) );

   /* get variables and coefficients */
   SCIP_CALL( getLinearConsVarsData(scip, consdata->lincons, consdata->linconstype, vars, NULL, &nvars) );

   /* calculate all not artificial linear variables and all artificial and-resultants which will be ordered like the
    * 'consanddatas' such that the and-resultant of the and-constraint is the and-resultant in the 'andress' array
    * afterwards
    * @todo should we take into accout the negation status of the cliques?
    */
   SCIP_CALL( getLinVarsAndAndRess(scip, cons, vars, NULL, nvars, linvars, NULL, &nlinvars,
         NULL, NULL, NULL, &nandress) );

   assert(nandress == consdata->nconsanddatas);
   assert(consdata->consanddatas != NULL);

   /* find cliques from linear variable to and-resultant */
   for( c = nandress - 1; c >= 0; --c )
   {
      CONSANDDATA* consanddata;
      SCIP_VAR** andvars;
      int nandvars;

      consanddata = consdata->consanddatas[c];
      assert(consanddata != NULL);

      andres = SCIPgetResultantAnd(scip, consanddata->cons);

      /* choose correct variable array */
      if( consanddata->nnewvars > 0 )
      {
         andvars = consanddata->newvars;
         nandvars = consanddata->nnewvars;
      }
      else
      {
         andvars = consanddata->vars;
         nandvars = consanddata->nvars;
      }

      for( v1 = nandvars - 1; v1 >= 0; --v1 )
      {
         SCIP_VAR* var1;
         SCIP_Bool values[2];

         var1 = andvars[v1];
         if( !SCIPvarIsActive(var1) && (!SCIPvarIsNegated(var1) || !SCIPvarIsActive(SCIPvarGetNegationVar(var1))) )
            continue;

         /* get active counterpart to check for common cliques */
         if( SCIPvarGetStatus(var1) == SCIP_VARSTATUS_NEGATED )
         {
            var1 = SCIPvarGetNegationVar(var1);
            values[0] = FALSE;
         }
         else
            values[0] = TRUE;

         for( v2 = nlinvars - 1; v2 >= 0; --v2 )
         {
            SCIP_VAR* var2;

            var2 = linvars[v2];
            if( !SCIPvarIsActive(var2) && (!SCIPvarIsNegated(var2) || !SCIPvarIsActive(SCIPvarGetNegationVar(var2))) )
               continue;

            /* get active counterpart to check for common cliques */
            if( SCIPvarGetStatus(var2) == SCIP_VARSTATUS_NEGATED )
            {
               var2 = SCIPvarGetNegationVar(var2);
               values[1] = FALSE;
            }
            else
               values[1] = TRUE;

            /* if variable in and-constraint1 is the negated variable of a normal linear variable, than we can add a
             * clique between the and-resultant and the normal linear variable, negated variables are not save in
             * cliquetables
             *
             * set r_1 = var1 * z; (z is some product)
             * var1 == ~var2
             *
             * if:
             * var1 + ~var1 <= 1;          r_1
             *    0 +     1 <= 1             0   \
             *    1 +     0 <= 1   ==>  1 or 0    >   ==>    r_1 + var2 <= 1
             *    0 +     0 <= 1             0   /
             */
            if( values[0] != values[1] && var1 == var2 )
            {
               SCIP_CONS* newcons;
               SCIP_VAR* clqvars[2];
               char consname[SCIP_MAXSTRLEN];

               clqvars[0] = andres;
               clqvars[1] = values[1] ? var2 : SCIPvarGetNegatedVar(var2);
               assert(clqvars[1] != NULL);

               /* @todo: check whether it is better to only add the clique or to add the setppc constraint or do both */

               /* add clique */
               SCIP_CALL( SCIPaddClique(scip, clqvars, NULL, 2, FALSE, cutoff, &nchgbdslocal) );
               if( *cutoff )
                  goto TERMINATE;

               *nchgbds += nchgbdslocal;

               (void) SCIPsnprintf(consname, SCIP_MAXSTRLEN, "%s_clq_%s_%s", SCIPconsGetName(cons), SCIPvarGetName(clqvars[0]), SCIPvarGetName(clqvars[1]) );
               SCIP_CALL( SCIPcreateConsSetpack(scip, &newcons, consname, 2, clqvars,
                     SCIPconsIsInitial(cons), SCIPconsIsSeparated(cons), SCIPconsIsEnforced(cons),
                     FALSE, SCIPconsIsPropagated(cons),
                     SCIPconsIsLocal(cons), SCIPconsIsModifiable(cons),
                     SCIPconsIsDynamic(cons), SCIPconsIsRemovable(cons), SCIPconsIsStickingAtNode(cons)) );

               SCIP_CALL( SCIPaddCons(scip, newcons) );
               SCIPdebugMsg(scip, "added a clique/setppc constraint <%s> \n", SCIPconsGetName(newcons));
               SCIPdebugPrintCons(scip, newcons, NULL);

               SCIP_CALL( SCIPreleaseCons(scip, &newcons) );
            }
            /* if a variable in an and-constraint is in a clique with another normal linear variable, we can add the
             * clique between the linear variable and the and-resultant
             *
             * set r_1 = var1 * z; (z is some product)
             *
             * if:
             * var1 + var2 <= 1;          r_1
             *    0 +    1 <= 1             0   \
             *    1 +    0 <= 1   ==>  1 or 0    >   ==>    r_1 + var2 <= 1
             *    0 +    0 <= 1             0   /
             */
            if( (var1 != var2) && SCIPvarsHaveCommonClique(var1, values[0], var2, values[1], TRUE) )
            {
               SCIP_CONS* newcons;
               SCIP_VAR* clqvars[2];
               char consname[SCIP_MAXSTRLEN];

               clqvars[0] = andres;
               clqvars[1] = values[1] ? var2 : SCIPvarGetNegatedVar(var2);
               assert(clqvars[1] != NULL);

               /* @todo: check whether it is better to only add the clique or to add the setppc constraint or do both */

               /* add clique */
               SCIP_CALL( SCIPaddClique(scip, clqvars, NULL, 2, FALSE, cutoff, &nchgbdslocal) );
               if( *cutoff )
                  goto TERMINATE;

               *nchgbds += nchgbdslocal;

               (void) SCIPsnprintf(consname, SCIP_MAXSTRLEN, "%s_clq_%s_%s", SCIPconsGetName(cons), SCIPvarGetName(clqvars[0]), SCIPvarGetName(clqvars[1]) );
               SCIP_CALL( SCIPcreateConsSetpack(scip, &newcons, consname, 2, clqvars,
                     SCIPconsIsInitial(cons), SCIPconsIsSeparated(cons), SCIPconsIsEnforced(cons),
                     FALSE, SCIPconsIsPropagated(cons),
                     SCIPconsIsLocal(cons), SCIPconsIsModifiable(cons),
                     SCIPconsIsDynamic(cons), SCIPconsIsRemovable(cons), SCIPconsIsStickingAtNode(cons)) );

               SCIP_CALL( SCIPaddCons(scip, newcons) );
               SCIPdebugMsg(scip, "added a clique/setppc constraint <%s> \n", SCIPconsGetName(newcons));
               SCIPdebugPrintCons(scip, newcons, NULL);

               SCIP_CALL( SCIPreleaseCons(scip, &newcons) );
            }
         }
      }
   }

   /* find cliques over variables which are in different and-constraints */
   for( c = nandress - 1; c > 0; --c )
   {
      CONSANDDATA* consanddata1;
      CONSANDDATA* consanddata2;
      SCIP_VAR** andvars1;
      int nandvars1;
      SCIP_VAR** andvars2;
      int nandvars2;

      consanddata1 = consdata->consanddatas[c];
      assert(consanddata1 != NULL);
      consanddata2 = consdata->consanddatas[c - 1];
      assert(consanddata2 != NULL);

      andres = SCIPgetResultantAnd(scip, consanddata1->cons);
      andres2 = SCIPgetResultantAnd(scip, consanddata2->cons);

      /* choose correct variable array of consanddata object 1 */
      if( consanddata1->nnewvars > 0 )
      {
         andvars1 = consanddata1->newvars;
         nandvars1 = consanddata1->nnewvars;
      }
      else
      {
         andvars1 = consanddata1->vars;
         nandvars1 = consanddata1->nvars;
      }

      /* choose correct variable array of consanddata object 2 */
      if( consanddata2->nnewvars > 0 )
      {
         andvars2 = consanddata2->newvars;
         nandvars2 = consanddata2->nnewvars;
      }
      else
      {
         andvars2 = consanddata2->vars;
         nandvars2 = consanddata2->nvars;
      }

      /* compare both terms for finding new aggregated variables and new cliques */
      for( v1 = nandvars1 - 1; v1 >= 0; --v1 )
      {
         SCIP_VAR* var1;
         SCIP_Bool values[2];

         var1 = andvars1[v1];
         if( !SCIPvarIsActive(var1) && (!SCIPvarIsNegated(var1) || !SCIPvarIsActive(SCIPvarGetNegationVar(var1))) )
            continue;

         /* get active counterpart to check for common cliques */
         if( SCIPvarGetStatus(var1) == SCIP_VARSTATUS_NEGATED )
         {
            var1 = SCIPvarGetNegationVar(var1);
            values[0] = FALSE;
         }
         else
            values[0] = TRUE;

         for( v2 = nandvars2 - 1; v2 >= 0; --v2 )
         {
            SCIP_VAR* var2;

            var2 = andvars2[v2];
            if( !SCIPvarIsActive(var2) && (!SCIPvarIsNegated(var2) || !SCIPvarIsActive(SCIPvarGetNegationVar(var2))) )
               continue;

            /* get active counterpart to check for common cliques */
            if( SCIPvarGetStatus(var2) == SCIP_VARSTATUS_NEGATED )
            {
               var2 = SCIPvarGetNegationVar(var2);
               values[1] = FALSE;
            }
            else
               values[1] = TRUE;

            /* if a variable in and-constraint1 is the negated variable of a variable in and-constraint2, than we can
             * add a clique between both and-resultants, negated variables are not save in cliquetables
             *
             * set r_1 = var1 * z_1; (z_1 is some product)
             * set r_2 = var2 * z_2; (z_2 is some product)
             * var1 == ~var2
             *
             * if:
             * var1 + ~var1 <= 1;          r_1     r_2
             *    0 +     1 <= 1             0  1 or 0   \
             *    1 +     0 <= 1   ==>  1 or 0       0    >   ==>    r_1 + r_2 <= 1
             *    0 +     0 <= 1             0       0   /
             */
            if( values[0] != values[1] && var1 == var2 )
            {
               SCIP_CONS* newcons;
               SCIP_VAR* clqvars[2];
               char consname[SCIP_MAXSTRLEN];

               clqvars[0] = andres;
               clqvars[1] = andres2;

               /* @todo: check whether it is better to only add the clique or to add the setppc constraint or do both */

               /* add clique */
               SCIP_CALL( SCIPaddClique(scip, clqvars, NULL, 2, FALSE, cutoff, &nchgbdslocal) );
               if( *cutoff )
                  goto TERMINATE;

               *nchgbds += nchgbdslocal;

               (void) SCIPsnprintf(consname, SCIP_MAXSTRLEN, "%s_clq_%s_%s", SCIPconsGetName(cons), SCIPvarGetName(clqvars[0]), SCIPvarGetName(clqvars[1]) );
               SCIP_CALL( SCIPcreateConsSetpack(scip, &newcons, consname, 2, clqvars,
                     SCIPconsIsInitial(cons), SCIPconsIsSeparated(cons), SCIPconsIsEnforced(cons),
                     FALSE, SCIPconsIsPropagated(cons),
                     SCIPconsIsLocal(cons), SCIPconsIsModifiable(cons),
                     SCIPconsIsDynamic(cons), SCIPconsIsRemovable(cons), SCIPconsIsStickingAtNode(cons)) );

               SCIP_CALL( SCIPaddCons(scip, newcons) );
               SCIPdebugMsg(scip, "added a clique/setppc constraint <%s> \n", SCIPconsGetName(newcons));
               SCIPdebugPrintCons(scip, newcons, NULL);

               SCIP_CALL( SCIPreleaseCons(scip, &newcons) );
            }
            /* if a variable in an and-constraint is in a clique with a variable in another and-constraint, we can add
             * the clique between both and-resultant
             *
             * let r_1 = var1 * z_1; (z_1 is some product)
             * let r_2 = var2 * z_2; (z_2 is some product)
             *
             * if:
             * var1 + var2 <= 1;          r_1     r_2
             *    0 +    1 <= 1             0  1 or 0   \
             *    1 +    0 <= 1   ==>  1 or 0       0    >   ==>    r_1 + r_2 <= 1
             *    0 +    0 <= 1             0       0   /
             */
            else if( SCIPvarsHaveCommonClique(var1, values[0], var2, values[1], TRUE) && (var1 != var2) )
            {
               SCIP_CONS* newcons;
               SCIP_VAR* clqvars[2];
               char consname[SCIP_MAXSTRLEN];

               clqvars[0] = andres;
               clqvars[1] = values[1] ? var2 : SCIPvarGetNegatedVar(var2);
               assert(clqvars[1] != NULL);

               /* @todo: check whether it is better to only add the clique or to add the setppc constraint or do both */

               /* add clique */
               SCIP_CALL( SCIPaddClique(scip, clqvars, NULL, 2, FALSE, cutoff, &nchgbdslocal) );
               if( *cutoff )
                  goto TERMINATE;

               *nchgbds += nchgbdslocal;

               (void) SCIPsnprintf(consname, SCIP_MAXSTRLEN, "%s_clq_%s_%s", SCIPconsGetName(cons), SCIPvarGetName(clqvars[0]), SCIPvarGetName(clqvars[1]) );
               SCIP_CALL( SCIPcreateConsSetpack(scip, &newcons, consname, 2, clqvars,
                     SCIPconsIsInitial(cons), SCIPconsIsSeparated(cons), SCIPconsIsEnforced(cons),
                     FALSE, SCIPconsIsPropagated(cons),
                     SCIPconsIsLocal(cons), SCIPconsIsModifiable(cons),
                     SCIPconsIsDynamic(cons), SCIPconsIsRemovable(cons), SCIPconsIsStickingAtNode(cons)) );

               SCIP_CALL( SCIPaddCons(scip, newcons) );
               SCIPdebugMsg(scip, "added a clique/setppc constraint <%s> \n", SCIPconsGetName(newcons));
               SCIPdebugPrintCons(scip, newcons, NULL);

               SCIP_CALL( SCIPreleaseCons(scip, &newcons) );
            }
         }
      }
   }

 TERMINATE:
   /* free temporary memory */
   SCIPfreeBufferArray(scip, &linvars);
   SCIPfreeBufferArray(scip, &vars);

   return SCIP_OKAY;
}

/** propagation method for pseudoboolean constraints */
static
SCIP_RETCODE propagateCons(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< knapsack constraint */
   SCIP_Bool*const       cutoff,             /**< pointer to store whether the node can be cut off */
   int*const             ndelconss           /**< pointer to count number of deleted constraints */
   )
{
   SCIP_CONSDATA* consdata;

   assert(scip != NULL);
   assert(cons != NULL);
   assert(cutoff != NULL);
   assert(ndelconss != NULL);

   *cutoff = FALSE;

   consdata = SCIPconsGetData(cons);
   assert(consdata != NULL);
   assert(consdata->lincons != NULL);

   /* if linear constraint is redundant, than pseudoboolean constraint is redundant too */
   if( SCIPconsIsDeleted(consdata->lincons) )
   {
      SCIP_CALL( SCIPdelConsLocal(scip, cons) );
      ++(*ndelconss);
   }

   /* check if the constraint was already propagated */
   if( consdata->propagated )
      return SCIP_OKAY;

   /* mark the constraint propagated */
   consdata->propagated = TRUE;

   return SCIP_OKAY;
}

/** update and-constraint flags due to pseudoboolean constraint flags */
static
SCIP_RETCODE updateAndConss(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons                /**< pseudoboolean constraint */
   )
{
   CONSANDDATA** consanddatas;
   int nconsanddatas;
   SCIP_CONSDATA* consdata;
   int c;

   assert(scip != NULL);
   assert(cons != NULL);

   consdata = SCIPconsGetData(cons);
   assert(consdata != NULL);

   consanddatas = consdata->consanddatas;
   nconsanddatas = consdata->nconsanddatas;
   assert(nconsanddatas == 0 || consanddatas != NULL);

   if( !SCIPconsIsActive(cons) )
      return SCIP_OKAY;

   /* release and-constraints and change check flag of and-constraint */
   for( c = nconsanddatas - 1; c >= 0; --c )
   {
      SCIP_CONS* andcons;

      assert(consanddatas[c] != NULL);

      if( !consanddatas[c]->istransformed )
         continue;

      andcons = consanddatas[c]->cons;
      assert(andcons != NULL);

      SCIP_CALL( SCIPsetConsChecked(scip, andcons, SCIPconsIsChecked(cons)) );
   }

   return SCIP_OKAY;
}

/** delete unused information in constraint handler data */
static
SCIP_RETCODE correctConshdlrdata(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONSHDLRDATA*const conshdlrdata,     /**< pseudoboolean constraint handler data */
   int*const             ndelconss           /**< pointer to count number of deleted constraints */
   )
{
   CONSANDDATA** allconsanddatas;
   CONSANDDATA* consanddata;
   int c;

   assert(scip != NULL);
   assert(conshdlrdata != NULL);
   assert(ndelconss != NULL);

   allconsanddatas = conshdlrdata->allconsanddatas;
   assert(allconsanddatas != NULL);
   assert(conshdlrdata->nallconsanddatas > 0);
   assert(conshdlrdata->nallconsanddatas <= conshdlrdata->sallconsanddatas);

   for( c = conshdlrdata->nallconsanddatas - 1; c >= 0; --c )
   {
      SCIP_VAR** tmpvars;
      int stmpvars;
      SCIP_CONS* cons;
      int v;

      consanddata = allconsanddatas[c];

      assert(consanddata->nvars == 0 || (consanddata->vars != NULL && consanddata->svars > 0));
      assert(consanddata->nnewvars == 0 || (consanddata->newvars != NULL && consanddata->snewvars > 0));

      if( !consanddata->istransformed )
      {
         assert(consanddata->vars == NULL || consanddata->origcons != NULL);
         assert(consanddata->nvars == 0 || consanddata->origcons != NULL);
         assert(consanddata->svars == 0 || consanddata->origcons != NULL);
         assert(consanddata->newvars == NULL);
         assert(consanddata->nnewvars == 0);
         assert(consanddata->snewvars == 0);

         continue;
      }

      /* if no variables are left, delete variables arrays */
      if( consanddata->nvars == 0 )
      {
         SCIP_VAR* resvar = SCIPgetResultantAnd(scip, consanddata->cons);

         /* if we have no old variables, than also no new variables */
         assert(consanddata->nnewvars == 0);
         assert(consanddata->nuses > 0);
         assert(resvar != NULL);

         /* delete and-constraint */
         SCIP_CALL( SCIPdelCons(scip, consanddata->cons) );
         ++(*ndelconss);

         SCIP_CALL( transformToOrig(scip, consanddata, conshdlrdata) );

         /* release and-constraint */
         SCIP_CALL( SCIPreleaseCons(scip, &consanddata->cons) );
         consanddata->nuses = 0;

         /* remove consanddata from hashtable, if it existed only in transformed space */
         if( consanddata->origcons == NULL )
         {
            assert(SCIPhashtableExists(conshdlrdata->hashtable, (void*)consanddata));
            SCIP_CALL( SCIPhashtableRemove(conshdlrdata->hashtable, (void*)consanddata) );
         }
         assert(SCIPhashmapExists(conshdlrdata->hashmap, (void*)resvar));
         SCIP_CALL( SCIPhashmapRemove(conshdlrdata->hashmap, (void*)resvar) );

         continue;
      }

      /* the consanddata object is not used anymore, so extract the and constraint and delete other data */
      if( consanddata->nuses == 0 )
      {
         SCIP_Bool looseorcolumn;
         SCIP_VARSTATUS varstatus;

         if( consanddata->cons == NULL )
         {
            assert(!consanddata->istransformed || consanddata->noriguses > 0);
            assert((consanddata->noriguses > 0) == (consanddata->origcons != NULL));
            assert(consanddata->vars == NULL || consanddata->origcons != NULL);
            assert(consanddata->nvars == 0 || consanddata->origcons != NULL);
            assert(consanddata->svars == 0 || consanddata->origcons != NULL);
            assert(consanddata->newvars == NULL);
            assert(consanddata->nnewvars == 0);
            assert(consanddata->snewvars == 0);

            continue;
         }

         SCIP_CALL( transformToOrig(scip, consanddata, conshdlrdata) );

         varstatus = SCIPvarGetStatus(SCIPgetResultantAnd(scip, consanddata->cons));
         looseorcolumn = (varstatus == SCIP_VARSTATUS_LOOSE || varstatus == SCIP_VARSTATUS_COLUMN);

#if 1
         /* @note  due to aggregations or fixings the resultant may need to be propagated later on, so we can only
          *        delete the and-constraint if the resultant is of column or loose status
          *        and is not an active variable of another (multi-)aggregated/negated variable
          */
         if( looseorcolumn )
         {
            SCIP_Bool del = TRUE;
            int nfixedvars = SCIPgetNFixedVars(scip);

            if( nfixedvars > 0 )
            {
               SCIP_VAR** fixedvars;
               SCIP_VAR** scipfixedvars;
               SCIP_VAR** activevars = NULL;
               SCIP_Real* activescalars = NULL;
               SCIP_Real activeconstant;
               int nactivevars;
               int requiredsize;
               int pos;
               int w;

               scipfixedvars = SCIPgetFixedVars(scip);
               SCIP_CALL( SCIPduplicateBufferArray(scip, &fixedvars, scipfixedvars, nfixedvars) );

               SCIPvarsGetProbvar(fixedvars, nfixedvars);

               /* all inactive variables have a loose, column, fixed or multi-aggregated variable as counterpart,
                * for multi-aggregated variables, we need to check all active representatives
                * @todo move this outside of the consanddata loop
                */
               for( w = nfixedvars - 1; w >= 0; --w )
               {
                  if( SCIPvarGetStatus(fixedvars[w]) == SCIP_VARSTATUS_MULTAGGR )
                  {
                     if( activevars == NULL )
                     {
                        SCIP_CALL( SCIPallocBufferArray(scip, &activevars, SCIPgetNVars(scip)) );
                        SCIP_CALL( SCIPallocBufferArray(scip, &activescalars, SCIPgetNVars(scip)) );
                     }
                     assert(activevars != NULL);
                     assert(activescalars != NULL);

                     activevars[0] = fixedvars[w];
                     activescalars[0] = 1.0;
                     activeconstant = 0.0;
                     nactivevars = 1;

                     SCIP_CALL( SCIPgetProbvarLinearSum(scip, activevars, activescalars, &nactivevars, SCIPgetNVars(scip),
                           &activeconstant, &requiredsize, TRUE) );
                     assert(requiredsize <= SCIPgetNVars(scip));

                     if( nactivevars == 0 )
                     {
                        --nfixedvars;
                        fixedvars[w] = fixedvars[nfixedvars];
                     }
                     else
                     {
                        fixedvars[w] = activevars[0];

                        if( nactivevars > 1 )
                        {
                           int i;

                           SCIP_CALL( SCIPreallocBufferArray(scip, &fixedvars, nfixedvars + nactivevars - 1) );
                           for( i = 1; i < nactivevars; ++i )
                           {
                              assert(SCIPvarGetStatus(activevars[i]) == SCIP_VARSTATUS_LOOSE || SCIPvarGetStatus(activevars[i]) == SCIP_VARSTATUS_COLUMN || SCIPvarGetStatus(activevars[i]) == SCIP_VARSTATUS_FIXED);
                              fixedvars[nfixedvars] = activevars[i];
                              ++nfixedvars;
                           }
                        }
                     }
                  }

                  assert(SCIPvarGetStatus(fixedvars[w]) == SCIP_VARSTATUS_LOOSE || SCIPvarGetStatus(fixedvars[w]) == SCIP_VARSTATUS_COLUMN || SCIPvarGetStatus(fixedvars[w]) == SCIP_VARSTATUS_FIXED);
               }

               if( activevars != NULL )
               {
                  SCIPfreeBufferArray(scip, &activevars);
                  SCIPfreeBufferArray(scip, &activescalars);
               }

               SCIPsortPtr((void**)fixedvars, SCIPvarComp, nfixedvars);

               if( SCIPsortedvecFindPtr((void**)fixedvars, SCIPvarComp, SCIPgetResultantAnd(scip, consanddata->cons), nfixedvars, &pos) )
                  del = FALSE;

               SCIPfreeBufferArray(scip, &fixedvars);
            }

            if( del )
            {
               SCIP_CALL( SCIPdelCons(scip, consanddata->cons) );
            }
         }
#endif

         if( !SCIPconsIsDeleted(consanddata->cons) )
         {
            /* change flags */
            if( !looseorcolumn )
            {
               SCIP_CALL( SCIPsetConsInitial(scip, consanddata->cons, FALSE) );
#if 0
               SCIP_CALL( SCIPsetConsSeparated(scip, consanddata->cons, FALSE) );
#endif
            }
            SCIP_CALL( SCIPsetConsChecked(scip, consanddata->cons, TRUE) );
         }

         /* remove consanddata from hashtable, if it existed only in transformed space */
         if( consanddata->origcons == NULL )
         {
            assert(SCIPhashtableExists(conshdlrdata->hashtable, (void*)consanddata));
            SCIP_CALL( SCIPhashtableRemove(conshdlrdata->hashtable, (void*)consanddata) );
         }
         assert(SCIPhashmapExists(conshdlrdata->hashmap, (void*)SCIPgetResultantAnd(scip, consanddata->cons)));
         SCIP_CALL( SCIPhashmapRemove(conshdlrdata->hashmap, (void*)SCIPgetResultantAnd(scip, consanddata->cons)) );

         SCIP_CALL( SCIPreleaseCons(scip, &(consanddata->cons)) );
         ++(*ndelconss);

         continue;
      }

      cons = consanddata->cons;
      assert(cons != NULL);

      /* if and-constraint is deleted, delete variables arrays */
      if( SCIPconsIsDeleted(cons) )
      {
         SCIP_VAR* resvar = SCIPgetResultantAnd(scip, consanddata->cons);

         assert(consanddata->nuses > 0);
         assert(resvar != NULL);

         SCIP_CALL( transformToOrig(scip, consanddata, conshdlrdata) );

         /* release and-constraint */
         SCIP_CALL( SCIPreleaseCons(scip, &consanddata->cons) );
         consanddata->nuses = 0;

         /* remove consanddata from hashtable, if it existed only in transformed space */
         if( consanddata->origcons == NULL )
         {
            assert(SCIPhashtableExists(conshdlrdata->hashtable, (void*)consanddata));
            SCIP_CALL( SCIPhashtableRemove(conshdlrdata->hashtable, (void*)consanddata) );
         }
         assert(SCIPhashmapExists(conshdlrdata->hashmap, (void*)resvar));
         SCIP_CALL( SCIPhashmapRemove(conshdlrdata->hashmap, (void*)resvar) );

         continue;
      }

      /* if no new variables exist, we do not need to do anything here */
      if( consanddata->nnewvars == 0 )
         continue;

      tmpvars = consanddata->vars;
      /* release all variables */
      for( v = consanddata->nvars - 1; v >= 0; --v )
      {
         /* in original problem the variables was already deleted */
         assert(tmpvars[v] != NULL);
         SCIP_CALL( SCIPreleaseVar(scip, &tmpvars[v]) );
      }

      /* exchange newvars with old vars array */
      tmpvars = consanddata->vars;
      stmpvars = consanddata->svars;
      consanddata->vars = consanddata->newvars;
      consanddata->svars = consanddata->snewvars;
      consanddata->nvars = consanddata->nnewvars;
      consanddata->newvars = tmpvars;
      consanddata->snewvars = stmpvars;
      /* reset number of variables in newvars array */
      consanddata->nnewvars = 0;
   }

   return SCIP_OKAY;
}

/** update the uses counter of consandata objects which are used in pseudoboolean constraint, that were deleted and
 *  probably delete and-constraints
 */
static
SCIP_RETCODE updateConsanddataUses(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_CONS*const       cons,               /**< pseudoboolean constraint */
   SCIP_CONSHDLRDATA*const conshdlrdata,     /**< pseudoboolean constraint handler data */
   int*const             ndelconss           /**< pointer to store number of deleted constraints */
   )
{
   CONSANDDATA** consanddatas;
   int nconsanddatas;
   SCIP_CONSDATA* consdata;
   int c;

   assert(scip != NULL);
   assert(cons != NULL);
   assert(conshdlrdata != NULL);
   assert(ndelconss != NULL);

   /* can only be called when constraint was deleted */
   assert(SCIPconsIsDeleted(cons));

   consdata = SCIPconsGetData(cons);
   assert(consdata != NULL);

   consanddatas = consdata->consanddatas;
   nconsanddatas = consdata->nconsanddatas;
   assert(nconsanddatas > 0 && consanddatas != NULL);
   assert(consdata->andcoefs != NULL);

   /* remove old locks */
   for( c = nconsanddatas - 1; c >= 0; --c )
   {
      CONSANDDATA* consanddata;

      consanddata = consanddatas[c];
      assert(consanddata != NULL);

      if( !consanddata->istransformed )
         continue;

      SCIP_CALL( removeOldLocks(scip, cons, consanddata, consdata->andcoefs[c], consdata->lhs, consdata->rhs) );
   }

   /* correct consandata usage counters and data */
   for( c = nconsanddatas - 1; c >= 0; --c )
   {
      CONSANDDATA* consanddata;

      consanddata = consanddatas[c];
      assert(consanddata != NULL);
      assert(consanddatas[c]->istransformed);

      assert(consanddata->nuses > 0);

      if( consanddata->nuses > 0 )
         --(consanddata->nuses);

      /* if data object is not used anymore, delete it */
      if( consanddata->nuses == 0 )
      {
         SCIP_VAR* resvar;
         SCIP_VARSTATUS varstatus;
         SCIP_Bool looseorcolumn;

         SCIP_CALL( transformToOrig(scip, consanddata, conshdlrdata) );

         resvar = SCIPgetResultantAnd(scip, consanddata->cons);
         assert(resvar != NULL);

         varstatus = SCIPvarGetStatus(resvar);
         looseorcolumn = (varstatus == SCIP_VARSTATUS_LOOSE || varstatus == SCIP_VARSTATUS_COLUMN);

#if 1
         /* @note  due to aggregations or fixings the resultant may need to be propagated later on, so we can only
          *        delete the and-constraint if the resultant is of column or loose status
          *        and is not an active variable of another (multi-)aggregated/negated variable
          */
         if( looseorcolumn )
         {
            SCIP_Bool delcons = TRUE;
#if 0
            const int nfixedvars = SCIPgetNFixedVars(scip);

            if( nfixedvars > 0 )
            {
               SCIP_VAR** fixedvars;
               SCIP_Bool foundmultiaggrvar = FALSE; /* workaround for multi-aggregated variables */
               int pos;
               int w;

               SCIP_CALL( SCIPduplicateBufferArray(scip, &fixedvars, SCIPgetFixedVars(scip), nfixedvars) );

               SCIPvarsGetProbvar(fixedvars, nfixedvars);

               /* all inactive variables have a loose, column, fixed or multi-aggregated variable as counterpart, but
                * because we have only binary variables (in pseudobbolean contest) there should also be no
                * multi-aggregated variable
                *
                * @todo for multi-aggregated variables check also all active representatives for this resultant
                */
               for( w = nfixedvars - 1; w >= 0; --w )
               {
                  if( SCIPvarGetStatus(fixedvars[w]) == SCIP_VARSTATUS_MULTAGGR )
                     foundmultiaggrvar = TRUE;
                  else
                     assert(SCIPvarGetStatus(fixedvars[w]) == SCIP_VARSTATUS_LOOSE || SCIPvarGetStatus(fixedvars[w]) == SCIP_VARSTATUS_COLUMN || SCIPvarGetStatus(fixedvars[w]) == SCIP_VARSTATUS_FIXED);
               }

               SCIPsortPtr((void**)fixedvars, SCIPvarComp, nfixedvars);

               if( foundmultiaggrvar )
                  delcons = FALSE;
               else if( SCIPsortedvecFindPtr((void**)fixedvars, SCIPvarComp, resvar, nfixedvars, &pos) )
                  delcons = FALSE;

               SCIPfreeBufferArray(scip, &fixedvars);
            }
#endif
            /* we can only delete and constraints if the resultant is an artificial variable and also active, because
             * then the assigned value is not of interest and the artificial and constraint does not need to be
             * fulfilled
             *
             * if this variable is not such an artificial variable we need the IRRELEVANT vartype which should be the
             * correct way to fix this
             */
            if( delcons
#if 0
               && strlen(SCIPvarGetName(resvar)) > strlen(ARTIFICIALVARNAMEPREFIX) &&
               strncmp(SCIPvarGetName(resvar)+2, ARTIFICIALVARNAMEPREFIX, strlen(ARTIFICIALVARNAMEPREFIX)) == 0
#endif
               ) /*lint !e774*/
            {
               assert(!SCIPconsIsChecked(consanddata->cons));
               SCIP_CALL( SCIPdelCons(scip, consanddata->cons) );
            }
         }
#endif

#if 0
         /* @note  due to aggregations or fixings the resultant may need to be propagated later on, so we can only
          *        delete the and-constraint if the resultant is of column or loose status
          *        and is not an active variable of another (multi-)aggregated/negated variable
          */
         if( looseorcolumn )
         {
            SCIP_CALL( SCIPdelCons(scip, consanddata->cons) );
         }
#endif

         if( !SCIPconsIsDeleted(consanddata->cons) )
         {
            /* change flags */
            if( !looseorcolumn )
            {
               SCIP_CALL( SCIPsetConsInitial(scip, consanddata->cons, FALSE) );
#if 0
               SCIP_CALL( SCIPsetConsSeparated(scip, consanddata->cons, FALSE) );
#endif
            }
            SCIP_CALL( SCIPsetConsChecked(scip, consanddata->cons, TRUE) );
         }

         /* remove consanddata from hashtable, if it existed only in transformed space */
         if( consanddata->origcons == NULL )
         {
            assert(SCIPhashtableExists(conshdlrdata->hashtable, (void*)consanddata));
            SCIP_CALL( SCIPhashtableRemove(conshdlrdata->hashtable, (void*)consanddata) );
         }
         assert(SCIPhashmapExists(conshdlrdata->hashmap, (void*)SCIPgetResultantAnd(scip, consanddata->cons)));
         SCIP_CALL( SCIPhashmapRemove(conshdlrdata->hashmap, (void*)SCIPgetResultantAnd(scip, consanddata->cons)) );

         SCIP_CALL( SCIPreleaseCons(scip, &(consanddata->cons)) );
         ++(*ndelconss);
      }
   }

   consdata->nconsanddatas = 0;

   return SCIP_OKAY;
}


/* maximal number to enumerate solutions for one pseudoboolean constraint to check for an upgrade to an XOR constraint */
#define MAXNVARS 10 /* note that this cannot be bigger than 31 */

/** calculate result for a given pseudoboolean constraint with given values, this is used to decide whether a
 *  pseudoboolean constraint can be upgrade to an XOR constraint
 */
static
SCIP_RETCODE checkSolution(
   SCIP*const            scip,               /**< SCIP data structure */
   SCIP_VAR**const       vars,               /**< all variables which occur */
   int const             nvars,              /**< number of all variables which appear in the pseudoboolean
                                              *   constraint
                                              */
   SCIP_Bool*const       values,             /**< values of all variables which appear in the pseudoboolean
                                              *   constraint
                                              */
   SCIP_VAR**const       linvars,            /**< linear variables */
   SCIP_Real*const       lincoefs,           /**< linear coefficients */
   int const             nlinvars,           /**< number of linear variables */
   SCIP_Real const       constant,           /**< offset to the linear part */
   SCIP_Real const       side,               /**< side of pseudoboolean constraint */
   CONSANDDATA**const    consanddatas,       /**< all consanddata objects in a constraint */
   SCIP_Real*const       consanddatacoefs,   /**< nonlinear coefficients */
   SCIP_Bool*const       consanddatanegs,    /**< negation status of and resultants in pseudo-boolean constraint */
   int const             nconsanddatas,      /**< number of all consanddata objects */
   int const             cnt,                /**< number of variables set to 1 */
   int*const             xortype             /**< pointer to save the possible xor type if a solution was valid and does
                                              *   not violate the old xortype
                                              */
   )
{
   CONSANDDATA* consanddata;
   SCIP_VAR** termvars;
   SCIP_VAR** repvars;
   int ntermvars;
   SCIP_Bool* negated;
   SCIP_Real value;
   int pos;
   int v;
   int c;

   assert(scip != NULL);
   assert(vars != NULL);
   assert(nvars > 0);
   assert(values != NULL);
   assert(linvars != NULL || nlinvars == 0);
   assert(lincoefs != NULL || nlinvars == 0);
   assert(nvars >= nlinvars);
   assert(SCIPisEQ(scip, side, 1.0) || SCIPisZero(scip, side));
   assert(consanddatas != NULL);
   assert(consanddatacoefs != NULL);
   assert(nconsanddatas > 0);
   assert(*xortype >= -1 && *xortype <= 1);

   /* order the variables after index, to compare them easier */
   SCIPsortPtr((void**)linvars, SCIPvarCompActiveAndNegated, nlinvars);
   SCIPsortPtr((void**)vars, SCIPvarCompActiveAndNegated, nvars);

   value = constant;
   for( v = nlinvars - 1; v >= 0; --v )
   {
      if( SCIPsortedvecFindPtr((void**)vars, SCIPvarCompActiveAndNegated, linvars[v], nvars, &pos) ) /*lint !e613*/
      {
         if( values[pos] )
            value += lincoefs[v]; /*lint !e613*/
      }
      else
      {
         /* this cannot happen, all linear variables should be a part of 'vars' */
         SCIPABORT();

         *xortype = -1;  /*lint !e527*/
         return SCIP_OKAY;
      }
   }

   SCIP_CALL( SCIPallocBufferArray(scip, &repvars, MAXNVARS) );
   SCIP_CALL( SCIPallocBufferArray(scip, &negated, MAXNVARS) );

   for( c = nconsanddatas - 1; c >= 0; --c )
   {
      SCIP_Bool val = TRUE;

      consanddata = consanddatas[c];
      assert(consanddata != NULL);
      assert(consanddata->istransformed);

      /* choose correct variable array to add locks for, we only add locks for now valid variables */
      if( consanddata->nnewvars > 0 )
      {
         termvars = consanddata->newvars;
         ntermvars = consanddata->nnewvars;
      }
      else
      {
         termvars = consanddata->vars;
         ntermvars = consanddata->nvars;
      }
      assert(ntermvars > 0 && termvars != NULL);

      BMSclearMemoryArray(negated, MAXNVARS);

      /* get linear active representation */
      SCIP_CALL( SCIPgetBinvarRepresentatives(scip, ntermvars, termvars, repvars, negated) );
      SCIPsortPtrBool((