|
||||||||||
PREV NEXT | FRAMES NO FRAMES |
Packages that use UnitPropagationListener | |
---|---|
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. |
Uses of UnitPropagationListener in org.sat4j.minisat.constraints |
---|
Methods in org.sat4j.minisat.constraints with parameters of type UnitPropagationListener | |
---|---|
void |
AbstractDataStructureFactory.setUnitPropagationListener(UnitPropagationListener s)
|
Uses of UnitPropagationListener in org.sat4j.minisat.constraints.card |
---|
Methods in org.sat4j.minisat.constraints.card with parameters of type UnitPropagationListener | |
---|---|
void |
MinWatchCard.assertConstraint(UnitPropagationListener s)
|
void |
MaxWatchCard.assertConstraint(UnitPropagationListener s)
|
void |
AtLeast.assertConstraint(UnitPropagationListener s)
|
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? |
boolean |
MinWatchCard.propagate(UnitPropagationListener s,
int p)
Propagation de la valeur de v? |
boolean |
MaxWatchCard.propagate(UnitPropagationListener s,
int p)
Propagation de la valeur de v? |
boolean |
AtLeast.propagate(UnitPropagationListener s,
int p)
|
Uses of UnitPropagationListener in org.sat4j.minisat.constraints.cnf |
---|
Methods in org.sat4j.minisat.constraints.cnf with parameters of type UnitPropagationListener | |
---|---|
void |
WLClause.assertConstraint(UnitPropagationListener s)
|
void |
TernaryClauses.assertConstraint(UnitPropagationListener s)
|
void |
CBClause.assertConstraint(UnitPropagationListener s)
|
void |
BinaryClauses.assertConstraint(UnitPropagationListener s)
|
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)
|
boolean |
WLClause.propagate(UnitPropagationListener s,
int p)
|
boolean |
MixableCBClause.propagate(UnitPropagationListener s,
int p)
|
boolean |
TernaryClauses.propagate(UnitPropagationListener s,
int p)
|
boolean |
CBClause.propagate(UnitPropagationListener s,
int p)
|
boolean |
BinaryClauses.propagate(UnitPropagationListener s,
int p)
|
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 |
Uses of UnitPropagationListener in org.sat4j.minisat.constraints.pb |
---|
Classes in org.sat4j.minisat.constraints.pb that implement UnitPropagationListener | |
---|---|
class |
PBSolver
|
Methods in org.sat4j.minisat.constraints.pb with parameters of type UnitPropagationListener | |
---|---|
void |
WatchPb.assertConstraint(UnitPropagationListener s)
|
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)
|
boolean |
MinWatchPb.propagate(UnitPropagationListener s,
int p)
Propagation de la valeur de v??? |
boolean |
MaxWatchPb.propagate(UnitPropagationListener s,
int p)
Propagation de la valeur de v? |
Uses of UnitPropagationListener in org.sat4j.minisat.core |
---|
Classes in org.sat4j.minisat.core that implement UnitPropagationListener | |
---|---|
class |
Solver
|
Methods in org.sat4j.minisat.core with parameters of type UnitPropagationListener | |
---|---|
void |
Constr.assertConstraint(UnitPropagationListener s)
Method called when the constraint is to be asserted. |
boolean |
Propagatable.propagate(UnitPropagationListener s,
int p)
Propagate the truth value of a literal in constraints in which that literal is falsified. |
void |
DataStructureFactory.setUnitPropagationListener(UnitPropagationListener s)
|
|
||||||||||
PREV NEXT | FRAMES NO FRAMES |