org.sat4j.minisat.constraints.pb
Class ConflictMapClause

java.lang.Object
  extended by org.sat4j.minisat.constraints.pb.MapPb
      extended by org.sat4j.minisat.constraints.pb.ConflictMap
          extended by 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


Copyright © 2007 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.