|
||||||||||
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.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 that return ILits | |
---|---|
ILits |
MinWatchCard.getVocabulary()
|
ILits |
MaxWatchCard.getVocabulary()
|
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)
Constructs a cardinality constraint with a minimal set of watched literals Permet la cr? |
Constructors in org.sat4j.minisat.constraints.card with parameters of type ILits | |
---|---|
MinWatchCard(ILits voc,
IVecInt ps,
boolean moreThan,
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
|
class |
Lits2
|
class |
Lits23
|
class |
MarkableLits
|
Methods in org.sat4j.minisat.constraints.cnf that return ILits | |
---|---|
ILits |
WLClause.getVocabulary()
|
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 that return ILits | |
---|---|
ILits |
MixableCBClausePB.getVocabulary()
|
ILits |
AtLeastPB.getVocabulary()
|
ILits |
WatchPb.getVocabulary()
|
ILits |
PBConstr.getVocabulary()
|
Methods in org.sat4j.minisat.constraints.pb with parameters of type ILits | |
---|---|
static AtLeastPB |
AtLeastPB.atLeastNew(ILits voc,
IVecInt ps,
int n)
|
static AtLeastPB |
AtLeastPB.atLeastNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
int n)
|
static WLClausePB |
WLClausePB.brandNewClause(UnitPropagationListener s,
ILits voc,
IVecInt literals)
Creates a brand new clause, presumably from external data. |
static MixableCBClausePB |
MixableCBClausePB.brandNewClause(UnitPropagationListener s,
ILits voc,
IVecInt literals)
|
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 MinWatchCardPB |
MinWatchCardPB.minWatchCardPBNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
boolean moreThan,
int degree)
Permet la cr? |
static PuebloMinWatchPb |
PuebloMinWatchPb.minWatchPbNew(UnitPropagationListener s,
ILits voc,
IDataStructurePB mpb)
|
static PuebloMinWatchPb |
PuebloMinWatchPb.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,
IVec<java.math.BigInteger> coefs,
boolean moreThan,
java.math.BigInteger degree)
|
static PuebloMinWatchPb |
PuebloMinWatchPb.minWatchPbNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
IVecInt coefs,
boolean moreThan,
int degree)
|
static MinWatchPb |
MinWatchPb.minWatchPbNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
IVecInt coefs,
boolean moreThan,
int degree)
|
static IDataStructurePB |
WatchPb.niceCheckedParameters(IVecInt ps,
IVec<java.math.BigInteger> bigCoefs,
boolean moreThan,
java.math.BigInteger bigDeg,
ILits voc)
|
static IDataStructurePB |
WatchPb.niceParameters(IVecInt ps,
IVec<java.math.BigInteger> bigCoefs,
boolean moreThan,
java.math.BigInteger bigDeg,
ILits voc)
|
static MaxWatchPb |
MaxWatchPb.normalizedMaxWatchPbNew(UnitPropagationListener s,
ILits voc,
ArrayPb mpb)
|
static MaxWatchPb |
MaxWatchPb.normalizedMaxWatchPbNew(UnitPropagationListener s,
ILits voc,
IDataStructurePB mpb)
|
static MinWatchCardPB |
MinWatchCardPB.normalizedMinWatchCardPBNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
int degree)
Permet la cr? |
static MinWatchPb |
MinWatchPb.normalizedMinWatchPbNew(UnitPropagationListener s,
ILits voc,
IDataStructurePB mpb)
|
static WatchPb |
PuebloMinWatchPb.normalizedWatchPbNew(ILits voc,
IDataStructurePB mpb)
|
static WatchPb |
MinWatchPb.normalizedWatchPbNew(ILits voc,
IDataStructurePB mpb)
|
static WatchPb |
PuebloMinWatchPb.watchPbNew(ILits voc,
IVecInt lits,
IVec<java.math.BigInteger> coefs,
boolean moreThan,
java.math.BigInteger 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 |
PuebloMinWatchPb.watchPbNew(ILits voc,
IVecInt lits,
IVecInt coefs,
boolean moreThan,
int 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)
|
Constructors in org.sat4j.minisat.constraints.pb with parameters of type ILits | |
---|---|
ConflictArrayCard(int[] lits,
java.math.BigInteger[] coefs,
java.math.BigInteger d,
ILits voc)
|
|
ConflictArrayClause(int[] lits,
java.math.BigInteger[] coefs,
java.math.BigInteger d,
ILits voc)
|
|
MinWatchCardPB(ILits voc,
IVecInt ps,
boolean moreThan,
int degree)
|
|
MinWatchCardPB(ILits voc,
IVecInt ps,
int degree)
|
|
MixableCBClausePB(IVecInt ps,
ILits voc)
|
|
MixableCBClausePB(IVecInt ps,
ILits voc,
boolean learnt)
|
|
WLClausePB(IVecInt ps,
ILits voc)
|
Uses of ILits in org.sat4j.minisat.core |
---|
Subinterfaces of ILits in org.sat4j.minisat.core | |
---|---|
interface |
ILits2
|
interface |
ILits23
|
interface |
IMarkableLits
|
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)
|
|
||||||||||
PREV NEXT | FRAMES NO FRAMES |