|
||||||||||
PREV NEXT | FRAMES NO FRAMES |
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)
|
|
||||||||||
PREV NEXT | FRAMES NO FRAMES |