public final class ConflictMapClause extends ConflictMap
byLevel, coefMult, coefMultCons, currentLevel, currentSlack, hasBeenReduced, numberOfReductions
assertiveLiteral, degree, weightedLits
Constructor and Description |
---|
ConflictMapClause(PBConstr cpb,
int level) |
Modifier and Type | Method and Description |
---|---|
static IConflict |
createConflict(PBConstr cpb,
int level) |
protected BigInteger |
reduceUntilConflict(int litImplied,
int ind,
BigInteger[] reducedCoefs,
IWatchPb wpb)
reduces the constraint defined by wpb until the result of the cutting
plane is a conflict. this reduction returns a clause.
|
getBacktrackLevel, getNumberOfReductions, hasBeenReduced, isAssertive, oldGetBacktrackLevel, oldIsAssertive, ppcm, reduceInConstraint, resolve, slackConflict, slackIsCorrect, toString, updateSlack
buildConstraintFromConflict, buildConstraintFromMapPb, cuttingPlane, cuttingPlane, cuttingPlane, cuttingPlane, getAssertiveLiteral, getDegree, isCardinality, isLongSufficient, saturation, size
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
buildConstraintFromConflict, buildConstraintFromMapPb, cuttingPlane, cuttingPlane, cuttingPlane, cuttingPlane, getAssertiveLiteral, getDegree, isCardinality, isLongSufficient, saturation, size
public ConflictMapClause(PBConstr cpb, int level)
protected BigInteger reduceUntilConflict(int litImplied, int ind, BigInteger[] reducedCoefs, IWatchPb wpb)
reduceUntilConflict
in class ConflictMap
litImplied
- ind
- reducedCoefs
- wpb
- Copyright © 2013 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.