public class ConflictMap extends MapPb implements IConflict
Modifier and Type | Field and Description |
---|---|
protected VecInt[] |
byLevel
allows to access directly to all variables belonging to a particular
level At index 0, unassigned literals are stored (usually level -1); so
there is always a step between index and levels.
|
protected BigInteger |
coefMult |
protected BigInteger |
coefMultCons |
protected int |
currentLevel |
protected BigInteger |
currentSlack
to store the slack of the current resolvant
|
protected boolean |
hasBeenReduced |
protected long |
numberOfReductions |
assertiveLiteral, degree, weightedLits
Modifier and Type | Method and Description |
---|---|
static IConflict |
createConflict(PBConstr cpb,
int level)
constructs the data structure needed to perform cutting planes
|
int |
getBacktrackLevel(int maxLevel)
computes the level for the backtrack : the highest decision level for
which the conflict is assertive.
|
long |
getNumberOfReductions() |
boolean |
hasBeenReduced() |
boolean |
isAssertive(int dl)
tests if the conflict is assertive (allows to imply a literal) at a
particular decision level
|
int |
oldGetBacktrackLevel(int maxLevel) |
boolean |
oldIsAssertive(int dl) |
protected static BigInteger |
ppcm(BigInteger a,
BigInteger b)
computes the least common factor of two integers (Plus Petit Commun
Multiple in french)
|
BigInteger |
reduceInConstraint(IWatchPb wpb,
BigInteger[] coefsBis,
int indLitImplied,
BigInteger degreeBis)
constraint reduction : removes a literal of the constraint.
|
protected BigInteger |
reduceUntilConflict(int litImplied,
int ind,
BigInteger[] reducedCoefs,
IWatchPb wpb) |
BigInteger |
resolve(PBConstr cpb,
int litImplied,
VarActivityListener val)
computes a cutting plane with a pseudo-boolean constraint. this method
updates the current instance (of ConflictMap).
|
BigInteger |
slackConflict()
computes the slack of the current instance
|
boolean |
slackIsCorrect(int dl) |
String |
toString() |
void |
updateSlack(int level) |
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
protected boolean hasBeenReduced
protected long numberOfReductions
protected BigInteger currentSlack
protected int currentLevel
protected VecInt[] byLevel
protected BigInteger coefMult
protected BigInteger coefMultCons
public static IConflict createConflict(PBConstr cpb, int level)
cpb
- pseudo-boolean constraint which rosed the conflictlevel
- current decision levelpublic BigInteger resolve(PBConstr cpb, int litImplied, VarActivityListener val)
protected BigInteger reduceUntilConflict(int litImplied, int ind, BigInteger[] reducedCoefs, IWatchPb wpb)
public BigInteger slackConflict()
slackConflict
in interface IConflict
public boolean oldIsAssertive(int dl)
public boolean isAssertive(int dl)
isAssertive
in interface IConflict
dl
- the decision levelprotected static BigInteger ppcm(BigInteger a, BigInteger b)
a
- first integerb
- second integerpublic BigInteger reduceInConstraint(IWatchPb wpb, BigInteger[] coefsBis, int indLitImplied, BigInteger degreeBis)
reduceInConstraint
in interface IConflict
wpb
- the initial constraint to reducecoefsBis
- the coefficients of the constraint wrt which the reduction
will be proposedindLitImplied
- index in wpb of the literal that should be resolveddegreeBis
- the degree of the constraint wrt which the reduction will be
proposedpublic int getBacktrackLevel(int maxLevel)
getBacktrackLevel
in interface IConflict
maxLevel
- the lowest level for which the conflict is assertivepublic int oldGetBacktrackLevel(int maxLevel)
public void updateSlack(int level)
updateSlack
in interface IConflict
public boolean slackIsCorrect(int dl)
slackIsCorrect
in interface IConflict
public boolean hasBeenReduced()
public long getNumberOfReductions()
Copyright © 2013 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.