org.sat4j.pb.constraints.pb

Class ConflictMapSwitchToClause

java.lang.Object

org.sat4j.pb.constraints.pb.MapPb

org.sat4j.pb.constraints.pb.ConflictMap

org.sat4j.pb.constraints.pb.ConflictMapSwitchToClause

All Implemented Interfaces:

IConflict, IDataStructurePB

public final class ConflictMapSwitchToClause
extends ConflictMap

Field Summary

Fields

Modifier and Type	Field and Description
static int	UpperBound

Fields inherited from class org.sat4j.pb.constraints.pb.ConflictMap

byLevel, coefMult, coefMultCons, currentLevel, currentSlack, hasBeenReduced, numberOfReductions

Fields inherited from class org.sat4j.pb.constraints.pb.MapPb

assertiveLiteral, degree, weightedLits

Constructor Summary

Constructors

Constructor and Description
ConflictMapSwitchToClause(PBConstr cpb, int level)

Method Summary

Methods

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 either a clause if .

Methods inherited from class org.sat4j.pb.constraints.pb.ConflictMap

getBacktrackLevel, getNumberOfReductions, hasBeenReduced, 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, 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

UpperBound

public static int UpperBound

Constructor Detail

ConflictMapSwitchToClause

public ConflictMapSwitchToClause(PBConstr cpb,
                         int level)

Method Detail

createConflict

public static IConflict createConflict(PBConstr cpb,
                       int level)

reduceUntilConflict

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 either a clause if .

Overrides:

reduceUntilConflict in class ConflictMap

Parameters:

litImplied -

ind -

reducedCoefs -

wpb -

Returns:

BigInteger.ONE