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.core Implementation of the MiniSAT solver skeleton. 
org.sat4j.minisat.learning Various learning strategies. 
org.sat4j.minisat.orders Various heuristics to select the next variable to branch on. 
 

Uses of ILits in org.sat4j.minisat.constraints
 

Fields in org.sat4j.minisat.constraints declared as ILits
protected  ILits AbstractDataStructureFactory.lits
           
 

Methods in org.sat4j.minisat.constraints that return ILits
protected abstract  ILits AbstractDataStructureFactory.createLits()
           
protected  ILits ClausalDataStructureCB.createLits()
           
protected  ILits AbstractCardinalityDataStructure.createLits()
           
protected  ILits ClausalDataStructureCBWL.createLits()
           
protected  ILits ClausalDataStructureWL.createLits()
           
protected  ILits MixedDataStructureDanielHT.createLits()
           
protected  ILits MixedDataStructureDanielWL.createLits()
           
 ILits AbstractDataStructureFactory.getVocabulary()
           
 

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

Fields in org.sat4j.minisat.constraints.card declared as ILits
protected  ILits AtLeast.voc
           
 

Methods in org.sat4j.minisat.constraints.card that return ILits
 ILits MaxWatchCard.getVocabulary()
           
 ILits MinWatchCard.getVocabulary()
           
 

Methods in org.sat4j.minisat.constraints.card with parameters of type ILits
static Constr AtLeast.atLeastNew(UnitPropagationListener s, ILits voc, IVecInt ps, int n)
           
protected static int MinWatchCard.linearisation(ILits voc, IVecInt ps)
          Simplifies the constraint w.r.t.
static MaxWatchCard MaxWatchCard.maxWatchCardNew(UnitPropagationListener s, ILits voc, IVecInt ps, boolean moreThan, int degree)
          Permet la cr?ation de contrainte de cardinalit? ? observation minimale
static MinWatchCard MinWatchCard.minWatchCardNew(UnitPropagationListener s, ILits voc, IVecInt ps, boolean moreThan, int degree)
          Constructs a cardinality constraint with a minimal set of watched literals Permet la cr?ation de contrainte de cardinalit? ? observation minimale
protected static int AtLeast.niceParameters(UnitPropagationListener s, ILits voc, IVecInt ps, int deg)
           
 

Constructors in org.sat4j.minisat.constraints.card with parameters of type ILits
AtLeast(ILits voc, IVecInt ps, int degree)
           
MinWatchCard(ILits voc, IVecInt ps, boolean moreThan, int degree)
          Constructs and normalizes a cardinality constraint.
MinWatchCard(ILits voc, IVecInt ps, int degree)
          Constructs and normalizes a cardinality constraint.
 

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

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

Fields in org.sat4j.minisat.constraints.cnf declared as ILits
protected  ILits HTClause.voc
           
protected  ILits WLClause.voc
           
protected  ILits CBClause.voc
           
 

Methods in org.sat4j.minisat.constraints.cnf that return ILits
 ILits HTClause.getVocabulary()
           
 ILits BinaryClause.getVocabulary()
           
 ILits WLClause.getVocabulary()
           
 

Methods in org.sat4j.minisat.constraints.cnf with parameters of type ILits
static OriginalWLClause OriginalWLClause.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals)
          Creates a brand new clause, presumably from external data.
static CBClause CBClause.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals)
           
static CBClause MixableCBClause.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals)
           
static OriginalBinaryClause OriginalBinaryClause.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals)
          Creates a brand new clause, presumably from external data.
static OriginalHTClause OriginalHTClause.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals)
          Creates a brand new clause, presumably from external data.
static IVecInt Clauses.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
BinaryClause(IVecInt ps, ILits voc)
          Creates a new basic clause
CBClause(IVecInt ps, ILits voc)
           
CBClause(IVecInt ps, ILits voc, boolean learnt)
           
HTClause(IVecInt ps, ILits voc)
          Creates a new basic clause
LearntBinaryClause(IVecInt ps, ILits voc)
           
LearntHTClause(IVecInt ps, ILits voc)
           
LearntWLClause(IVecInt ps, ILits voc)
           
MixableCBClause(IVecInt ps, ILits voc)
           
MixableCBClause(IVecInt ps, ILits voc, boolean learnt)
           
OriginalBinaryClause(IVecInt ps, ILits voc)
           
OriginalHTClause(IVecInt ps, ILits voc)
           
OriginalWLClause(IVecInt ps, ILits voc)
           
WLClause(IVecInt ps, ILits voc)
          Creates a new basic clause
 

Uses of ILits in org.sat4j.minisat.core
 

Fields in org.sat4j.minisat.core declared as ILits
protected  ILits Solver.voc
           
 

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

Methods in org.sat4j.minisat.core with parameters of type ILits
 void IOrder.setLits(ILits lits)
          Method used to provide an easy access the the solver vocabulary.
 

Uses of ILits in org.sat4j.minisat.learning
 

Fields in org.sat4j.minisat.learning declared as ILits
protected  ILits LimitedLearning.lits
           
 

Uses of ILits in org.sat4j.minisat.orders
 

Fields in org.sat4j.minisat.orders declared as ILits
protected  ILits VarOrderHeap.lits
           
 

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

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



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