org.sat4j.minisat.constraints.pb
Class ConflictMap

java.lang.Object
  org.sat4j.minisat.constraints.pb.MapPb
      org.sat4j.minisat.constraints.pb.ConflictMap

All Implemented Interfaces:

IConflict, IDataStructurePB

Direct Known Subclasses:

ConflictMapCardinality, ConflictMapClause, ConflictMapMerging

public class ConflictMap
extends MapPb
implements IConflict

Author:

parrain TODO To change the template for this generated type comment go to Window - Preferences - Java - Code Style - Code Templates

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 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

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

coefs, degree

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.
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(WatchPb 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, WatchPb wpb)
java.math.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).
java.math.BigInteger	slackConflict() computes the slack of the current instance
boolean	slackIsCorrect(int dl)
java.lang.String	toString()
void	updateSlack(int level)

Methods inherited from class org.sat4j.minisat.constraints.pb.MapPb

buildConstraintFromConflict, buildConstraintFromMapPb, cuttingPlane, cuttingPlane, cuttingPlane, cuttingPlane, getDegree, 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.minisat.constraints.pb.IDataStructurePB

buildConstraintFromConflict, buildConstraintFromMapPb, cuttingPlane, cuttingPlane, cuttingPlane, cuttingPlane, getDegree, saturation, size

Field Detail

currentSlack

protected java.math.BigInteger currentSlack

to store the slack of the current resolvant

currentLevel

protected int currentLevel

byLevel

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.

coefMult

protected java.math.BigInteger coefMult

coefMultCons

protected java.math.BigInteger coefMultCons

Method Detail

createConflict

public static IConflict createConflict(PBConstr cpb,
                                       int level)

constructs the data structure needed to perform cutting planes

Parameters:

cpb - pseudo-boolean constraint which rosed the conflict

level - current decision level

Returns:

a conflict on which cutting plane can be performed.

resolve

public java.math.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).

Specified by:

resolve in interface IConflict

Parameters:

cpb - constraint to compute with the cutting plane

litImplied - literal that must be resolved by the cutting plane

val - TODO

Returns:

an update of the degree of the current instance

reduceUntilConflict

protected java.math.BigInteger reduceUntilConflict(int litImplied,
                                                   int ind,
                                                   java.math.BigInteger[] reducedCoefs,
                                                   WatchPb wpb)

slackConflict

public java.math.BigInteger slackConflict()

computes the slack of the current instance

Specified by:

slackConflict in interface IConflict

oldIsAssertive

public boolean oldIsAssertive(int dl)

isAssertive

public boolean isAssertive(int dl)

tests if the conflict is assertive (allows to imply a literal) at a particular decision level

Specified by:

isAssertive in interface IConflict

Parameters:

dl - the decision level

Returns:

true if the conflict is assertive at the decision level

ppcm

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)

Parameters:

a - first integer

b - second integer

Returns:

the least common factor

reduceInConstraint

public java.math.BigInteger reduceInConstraint(WatchPb wpb,
                                               java.math.BigInteger[] coefsBis,
                                               int indLitImplied,
                                               java.math.BigInteger degreeBis)

constraint reduction : removes a literal of the constraint. The literal should be either unassigned or satisfied. The literal can not be the literal that should be resolved.

Specified by:

reduceInConstraint in interface IConflict

Parameters:

wpb - the initial constraint to reduce

coefsBis - the coefficients of the constraint wrt which the reduction will be proposed

indLitImplied - index in wpb of the literal that should be resolved

degreeBis - the degree of the constraint wrt which the reduction will be proposed

Returns:

new degree of the reduced constraint

getBacktrackLevel

public int getBacktrackLevel(int maxLevel)

computes the level for the backtrack : the highest decision level for which the conflict is assertive.

Specified by:

getBacktrackLevel in interface IConflict

Parameters:

maxLevel - the lowest level for which the conflict is assertive

Returns:

the highest level (smaller int) for which the constraint is assertive.

oldGetBacktrackLevel

public int oldGetBacktrackLevel(int maxLevel)

updateSlack

public void updateSlack(int level)

Specified by:

updateSlack in interface IConflict

slackIsCorrect

public boolean slackIsCorrect(int dl)

Specified by:

slackIsCorrect in interface IConflict

toString

public java.lang.String toString()

Overrides:

toString in class MapPb