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