org.sat4j.minisat.constraints.pb
Class ConflictMapClause

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

All Implemented Interfaces:

IConflict, IDataStructurePB

public class ConflictMapClause
extends ConflictMap

Field Summary

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

byLevel, coefMult, coefMultCons, currentLevel, currentSlack

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

coefs, degree

Constructor Summary

ConflictMapClause(java.util.Map<java.lang.Integer,java.math.BigInteger> m, java.math.BigInteger d, ILits voc, 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.minisat.constraints.pb.ConflictMap

getBacktrackLevel, isAssertive, oldGetBacktrackLevel, oldIsAssertive, ppcm, reduceInConstraint, resolve, slackConflict, slackIsCorrect, toString, updateSlack

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

Constructor Detail

ConflictMapClause

public ConflictMapClause(java.util.Map<java.lang.Integer,java.math.BigInteger> m,
                         java.math.BigInteger d,
                         ILits voc,
                         int level)

Method Detail

createConflict

public static IConflict createConflict(PBConstr cpb,
                                       int level)

reduceUntilConflict

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.

Overrides:

reduceUntilConflict in class ConflictMap

Parameters:

litImplied -

ind -

reducedCoefs -

wpb -

Returns:

BigInteger.ONE