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 java.math.BigInteger |
coefMult |
protected java.math.BigInteger |
coefMultCons |
protected int |
currentLevel |
protected java.math.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 java.math.BigInteger |
ppcm(java.math.BigInteger a,
java.math.BigInteger b)
computes the least common factor of two integers (Plus Petit Commun
Multiple in french)
|
java.math.BigInteger |
reduceInConstraint(IWatchPb wpb,
java.math.BigInteger[] coefsBis,
int indLitImplied,
java.math.BigInteger degreeBis)
constraint reduction : removes a literal of the constraint.
|
protected java.math.BigInteger |
reduceUntilConflict(int litImplied,
int ind,
java.math.BigInteger[] reducedCoefs,
IWatchPb wpb) |
java.math.BigInteger |
resolve(PBConstr cpb,
int litImplied,
VarActivityListener val)
computes a cutting plane with a pseudo-boolean constraint.
|
java.math.BigInteger |
slackConflict()
computes the slack of the current instance
|
boolean |
slackIsCorrect(int dl) |
java.lang.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 java.math.BigInteger currentSlack
protected int currentLevel
protected VecInt[] byLevel
protected java.math.BigInteger coefMult
protected java.math.BigInteger coefMultCons
public static IConflict createConflict(PBConstr cpb, int level)
cpb
- pseudo-boolean constraint which rosed the conflictlevel
- current decision levelpublic java.math.BigInteger resolve(PBConstr cpb, int litImplied, VarActivityListener val)
protected java.math.BigInteger reduceUntilConflict(int litImplied, int ind, java.math.BigInteger[] reducedCoefs, IWatchPb wpb)
public java.math.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 java.math.BigInteger ppcm(java.math.BigInteger a, java.math.BigInteger b)
a
- first integerb
- second integerpublic java.math.BigInteger reduceInConstraint(IWatchPb wpb, java.math.BigInteger[] coefsBis, int indLitImplied, java.math.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()