|
||||||||||
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.core | Implementation of the MiniSAT solver skeleton. |
Uses of UnitPropagationListener in org.sat4j.minisat.constraints |
---|
Fields in org.sat4j.minisat.constraints declared as UnitPropagationListener | |
---|---|
protected UnitPropagationListener |
AbstractDataStructureFactory.solver
|
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 |
MaxWatchCard.assertConstraint(UnitPropagationListener s)
|
void |
AtLeast.assertConstraint(UnitPropagationListener s)
|
void |
MinWatchCard.assertConstraint(UnitPropagationListener s)
|
static Constr |
AtLeast.atLeastNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
int n)
|
protected MinWatchCard |
MinWatchCard.computePropagation(UnitPropagationListener s)
|
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)
|
boolean |
MaxWatchCard.propagate(UnitPropagationListener s,
int p)
Propagation de la valeur de v?rit? d'un litt?ral falsifi? |
boolean |
AtLeast.propagate(UnitPropagationListener s,
int p)
|
boolean |
MinWatchCard.propagate(UnitPropagationListener s,
int p)
propagates the value of a falsified literal |
void |
MaxWatchCard.remove(UnitPropagationListener upl)
|
void |
AtLeast.remove(UnitPropagationListener upl)
|
void |
MinWatchCard.remove(UnitPropagationListener upl)
Removes a constraint from the solver |
Uses of UnitPropagationListener in org.sat4j.minisat.constraints.cnf |
---|
Methods in org.sat4j.minisat.constraints.cnf with parameters of type UnitPropagationListener | |
---|---|
void |
HTClause.assertConstraint(UnitPropagationListener s)
|
void |
BinaryClause.assertConstraint(UnitPropagationListener s)
|
void |
WLClause.assertConstraint(UnitPropagationListener s)
|
void |
CBClause.assertConstraint(UnitPropagationListener s)
|
void |
UnitClauses.assertConstraint(UnitPropagationListener s)
|
void |
UnitClause.assertConstraint(UnitPropagationListener s)
|
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. |
boolean |
HTClause.propagate(UnitPropagationListener s,
int p)
|
boolean |
BinaryClause.propagate(UnitPropagationListener s,
int p)
|
boolean |
WLClause.propagate(UnitPropagationListener s,
int p)
|
boolean |
CBClause.propagate(UnitPropagationListener s,
int p)
|
boolean |
UnitClauses.propagate(UnitPropagationListener s,
int p)
|
boolean |
MixableCBClause.propagate(UnitPropagationListener s,
int p)
|
boolean |
UnitClause.propagate(UnitPropagationListener s,
int p)
|
void |
HTClause.remove(UnitPropagationListener upl)
|
void |
BinaryClause.remove(UnitPropagationListener upl)
|
void |
WLClause.remove(UnitPropagationListener upl)
|
void |
CBClause.remove(UnitPropagationListener upl)
|
void |
UnitClauses.remove(UnitPropagationListener upl)
|
void |
UnitClause.remove(UnitPropagationListener upl)
|
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 |
Uses of UnitPropagationListener in org.sat4j.minisat.core |
---|
Classes in org.sat4j.minisat.core that implement UnitPropagationListener | |
---|---|
class |
Solver<D extends DataStructureFactory>
The backbone of the library providing the modular implementation of a MiniSAT (Chaff) like 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 |
Constr.remove(UnitPropagationListener upl)
Remove a constraint from the solver. |
void |
DataStructureFactory.setUnitPropagationListener(UnitPropagationListener s)
|
|
||||||||||
PREV NEXT | FRAMES NO FRAMES |