|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectorg.sat4j.pb.constraints.pb.MapPb
org.sat4j.pb.constraints.pb.ConflictMap
public class ConflictMap
Field Summary | |
---|---|
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
|
Fields inherited from class org.sat4j.pb.constraints.pb.MapPb |
---|
assertiveLiteral, degree, weightedLits |
Method Summary | |
---|---|
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)
|
Methods inherited from class org.sat4j.pb.constraints.pb.MapPb |
---|
buildConstraintFromConflict, buildConstraintFromMapPb, cuttingPlane, cuttingPlane, cuttingPlane, cuttingPlane, getAssertiveLiteral, getDegree, isCardinality, isLongSufficient, saturation, size |
Methods inherited from class java.lang.Object |
---|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait |
Methods inherited from interface org.sat4j.pb.constraints.pb.IDataStructurePB |
---|
buildConstraintFromConflict, buildConstraintFromMapPb, cuttingPlane, cuttingPlane, cuttingPlane, cuttingPlane, getAssertiveLiteral, getDegree, isCardinality, isLongSufficient, saturation, size |
Field Detail |
---|
protected boolean hasBeenReduced
protected long numberOfReductions
protected BigInteger currentSlack
protected int currentLevel
protected VecInt[] byLevel
protected BigInteger coefMult
protected BigInteger coefMultCons
Method Detail |
---|
public static IConflict createConflict(PBConstr cpb, int level)
cpb
- pseudo-boolean constraint which rosed the conflictlevel
- current decision level
public BigInteger resolve(PBConstr cpb, int litImplied, VarActivityListener val)
resolve
in interface IConflict
cpb
- constraint to compute with the cutting planelitImplied
- literal that must be resolved by the cutting planeval
- TODO
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 level
protected static BigInteger ppcm(BigInteger a, BigInteger b)
a
- first integerb
- second integer
public 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
proposed
public int getBacktrackLevel(int maxLevel)
getBacktrackLevel
in interface IConflict
maxLevel
- the lowest level for which the conflict is assertive
public int oldGetBacktrackLevel(int maxLevel)
public void updateSlack(int level)
updateSlack
in interface IConflict
public boolean slackIsCorrect(int dl)
slackIsCorrect
in interface IConflict
public String toString()
toString
in class MapPb
public boolean hasBeenReduced()
public long getNumberOfReductions()
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |