|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object org.sat4j.pb.constraints.pb.MapPb org.sat4j.pb.constraints.pb.ConflictMap org.sat4j.pb.constraints.pb.ConflictMapClause
public class ConflictMapClause
Field Summary |
---|
Fields inherited from class org.sat4j.pb.constraints.pb.ConflictMap |
---|
byLevel, coefMult, coefMultCons, currentLevel, currentSlack |
Fields inherited from class org.sat4j.pb.constraints.pb.MapPb |
---|
assertiveLiteral, degree, weightedLits |
Constructor Summary | |
---|---|
ConflictMapClause(PBConstr cpb,
int level)
|
Method Summary | |
---|---|
static IConflict |
createConflict(PBConstr cpb,
int level)
|
protected java.math.BigInteger |
reduceUntilConflict(int litImplied,
int ind,
java.math.BigInteger[] reducedCoefs,
WatchPb wpb)
reduces the constraint defined by wpb until the result of the cutting plane is a conflict. this reduction returns a clause. |
Methods inherited from class org.sat4j.pb.constraints.pb.ConflictMap |
---|
getBacktrackLevel, isAssertive, oldGetBacktrackLevel, oldIsAssertive, ppcm, reduceInConstraint, resolve, slackConflict, slackIsCorrect, toString, updateSlack |
Methods inherited from class org.sat4j.pb.constraints.pb.MapPb |
---|
buildConstraintFromConflict, buildConstraintFromMapPb, cuttingPlane, cuttingPlane, cuttingPlane, cuttingPlane, getAssertiveLiteral, getDegree, isCardinality, 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, saturation, size |
Constructor Detail |
---|
public ConflictMapClause(PBConstr cpb, int level)
Method Detail |
---|
public static IConflict createConflict(PBConstr cpb, int level)
protected java.math.BigInteger reduceUntilConflict(int litImplied, int ind, java.math.BigInteger[] reducedCoefs, WatchPb wpb)
reduceUntilConflict
in class ConflictMap
litImplied
- ind
- reducedCoefs
- wpb
-
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |