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

Packages that use ILits
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. 
org.sat4j.minisat.orders Various heuristics to select the next variable to branch on. 
 

Uses of ILits in org.sat4j.minisat.constraints
 

Methods in org.sat4j.minisat.constraints that return ILits
 ILits MixedDataStructureWithBinaryAndTernary.getVocabulary()
           
 ILits MixedDataStructureWithBinary.getVocabulary()
           
 ILits AbstractDataStructureFactory.getVocabulary()
           
 

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

Methods in org.sat4j.minisat.constraints.card with parameters of type ILits
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?
 

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

Classes in org.sat4j.minisat.constraints.cnf that implement ILits
 class Lits
           
 class Lits2
           
 class Lits23
           
 

Methods in org.sat4j.minisat.constraints.cnf with parameters of type ILits
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)
           
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
 

Constructors in org.sat4j.minisat.constraints.cnf with parameters of type ILits
BinaryClauses(ILits voc, int p)
           
CBClause(IVecInt ps, ILits voc)
           
CBClause(IVecInt ps, ILits voc, boolean learnt)
           
MixableCBClause(IVecInt ps, ILits voc)
           
MixableCBClause(IVecInt ps, ILits voc, boolean learnt)
           
TernaryClauses(ILits voc, int p)
           
WLClause(IVecInt ps, ILits voc)
          Creates a new basic clause
 

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

Methods in org.sat4j.minisat.constraints.pb with parameters of type ILits
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)
           
static WatchPb MinWatchPb.watchPbNew(ILits voc, IVecInt lits, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
           
static WatchPb MaxWatchPb.watchPbNew(ILits voc, IVecInt lits, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
           
static WatchPb MinWatchPb.watchPbNew(ILits voc, IVecInt lits, IVecInt coefs, boolean moreThan, int degree)
           
static WatchPb MaxWatchPb.watchPbNew(ILits voc, IVecInt lits, IVecInt coefs, boolean moreThan, int degree)
           
 

Uses of ILits in org.sat4j.minisat.core
 

Subinterfaces of ILits in org.sat4j.minisat.core
 interface ILits2
           
 interface ILits23
           
 

Methods in org.sat4j.minisat.core that return ILits
 ILits Solver.getVocabulary()
           
 ILits DataStructureFactory.getVocabulary()
           
 

Methods in org.sat4j.minisat.core with parameters of type ILits
 void IOrder.setLits(ILits lits)
           
 

Uses of ILits in org.sat4j.minisat.orders
 

Methods in org.sat4j.minisat.orders that return ILits
 ILits VarOrderHeap.getVocabulary()
           
 ILits VarOrder.getVocabulary()
           
 

Methods in org.sat4j.minisat.orders with parameters of type ILits
 void VarOrderHeap.setLits(ILits lits)
           
 void MyOrder.setLits(ILits lits)
           
 void VarOrder.setLits(ILits lits)
           
 void JWOrder.setLits(ILits lits)