Uses of Interface
org.sat4j.minisat.core.UnitPropagationListener

Packages that use UnitPropagationListener
org.sat4j.minisat.constraints Implementations of various constraints for MiniSAT. 
org.sat4j.minisat.constraints.card Implementations of cardinality contraints. 
org.sat4j.minisat.constraints.cnf Implementations of clausal contraints. 
org.sat4j.minisat.constraints.pb Implementations of pseudo boolean contraints. 
org.sat4j.minisat.core Implementation of the MiniSAT solver skeleton. 
 

Uses of UnitPropagationListener in org.sat4j.minisat.constraints
 

Methods in org.sat4j.minisat.constraints with parameters of type UnitPropagationListener
 void AbstractDataStructureFactory.setUnitPropagationListener(UnitPropagationListener s)
           
 

Uses of UnitPropagationListener in org.sat4j.minisat.constraints.card
 

Methods in org.sat4j.minisat.constraints.card with parameters of type UnitPropagationListener
 void MinWatchCard.assertConstraint(UnitPropagationListener s)
           
 void MaxWatchCard.assertConstraint(UnitPropagationListener s)
           
 void AtLeast.assertConstraint(UnitPropagationListener s)
           
static AtLeast AtLeast.atLeastNew(UnitPropagationListener s, ILits voc, IVecInt ps, int n)
           
static MaxWatchCard MaxWatchCard.maxWatchCardNew(UnitPropagationListener s, ILits voc, IVecInt ps, boolean moreThan, int degree)
          Permet la cr?
static MinWatchCard MinWatchCard.minWatchCardNew(UnitPropagationListener s, ILits voc, IVecInt ps, boolean moreThan, int degree)
          Permet la cr?
 boolean MinWatchCard.propagate(UnitPropagationListener s, int p)
          Propagation de la valeur de v?
 boolean MaxWatchCard.propagate(UnitPropagationListener s, int p)
          Propagation de la valeur de v?
 boolean AtLeast.propagate(UnitPropagationListener s, int p)
           
 

Uses of UnitPropagationListener in org.sat4j.minisat.constraints.cnf
 

Methods in org.sat4j.minisat.constraints.cnf with parameters of type UnitPropagationListener
 void WLClause.assertConstraint(UnitPropagationListener s)
           
 void TernaryClauses.assertConstraint(UnitPropagationListener s)
           
 void CBClause.assertConstraint(UnitPropagationListener s)
           
 void BinaryClauses.assertConstraint(UnitPropagationListener s)
           
static WLClause WLClause.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals)
          Creates a brand new clause, presumably from external data.
static CBClause MixableCBClause.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals)
           
static CBClause CBClause.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals)
           
 boolean WLClause.propagate(UnitPropagationListener s, int p)
           
 boolean MixableCBClause.propagate(UnitPropagationListener s, int p)
           
 boolean TernaryClauses.propagate(UnitPropagationListener s, int p)
           
 boolean CBClause.propagate(UnitPropagationListener s, int p)
           
 boolean BinaryClauses.propagate(UnitPropagationListener s, int p)
           
static IVecInt WLClause.sanityCheck(IVecInt ps, ILits voc, UnitPropagationListener s)
          Perform some sanity check before constructing a clause a) if a literal is assigned true, return null (the clause is satisfied) b) if a literal is assigned false, remove it c) if a clause contains a literal and its opposite (tautology) return null d) remove duplicate literals e) if the clause is empty, return null f) if the clause if unit, transmit it to the object responsible for unit propagation
 

Uses of UnitPropagationListener in org.sat4j.minisat.constraints.pb
 

Classes in org.sat4j.minisat.constraints.pb that implement UnitPropagationListener
 class PBSolver
           
 

Methods in org.sat4j.minisat.constraints.pb with parameters of type UnitPropagationListener
 void WatchPb.assertConstraint(UnitPropagationListener s)
           
static MaxWatchPb MaxWatchPb.maxWatchPbNew(UnitPropagationListener s, ILits voc, IVecInt ps, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
           
static MaxWatchPb MaxWatchPb.maxWatchPbNew(UnitPropagationListener s, ILits voc, IVecInt ps, IVecInt coefs, boolean moreThan, int degree)
           
static MinWatchPb MinWatchPb.minWatchPbNew(UnitPropagationListener s, ILits voc, IVecInt ps, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
           
static MinWatchPb MinWatchPb.minWatchPbNew(UnitPropagationListener s, ILits voc, IVecInt ps, IVecInt coefs, boolean moreThan, int degree)
           
 boolean MinWatchPb.propagate(UnitPropagationListener s, int p)
          Propagation de la valeur de v???
 boolean MaxWatchPb.propagate(UnitPropagationListener s, int p)
          Propagation de la valeur de v?
 

Uses of UnitPropagationListener in org.sat4j.minisat.core
 

Classes in org.sat4j.minisat.core that implement UnitPropagationListener
 class Solver
           
 

Methods in org.sat4j.minisat.core with parameters of type UnitPropagationListener
 void Constr.assertConstraint(UnitPropagationListener s)
          Method called when the constraint is to be asserted.
 boolean Propagatable.propagate(UnitPropagationListener s, int p)
          Propagate the truth value of a literal in constraints in which that literal is falsified.
 void DataStructureFactory.setUnitPropagationListener(UnitPropagationListener s)