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

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)
java.math.BigInteger	reduceInConstraint(WatchPb wpb, java.math.BigInteger[] coefsBis, int indLitImplied, java.math.BigInteger degreeBis) constraint reduction : removes a literal of the constraint.
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

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

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

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

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