Uses of Interface
org.sat4j.minisat.core.UnitPropagationListener

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

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	MinWatchCard.assertConstraint(UnitPropagationListener s)
void	AtLeast.assertConstraint(UnitPropagationListener s)
static AtLeast	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?
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?
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?
boolean	MinWatchCard.propagate(UnitPropagationListener s, int p) propagates the value of a falsified literal
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	CBClause.assertConstraint(UnitPropagationListener s)
void	TernaryClauses.assertConstraint(UnitPropagationListener s)
void	BinaryClauses.assertConstraint(UnitPropagationListener s)
static CBClause	MixableCBClause.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals)
static OriginalWLClause	OriginalWLClause.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals) Creates a brand new clause, presumably from external data.
static WLClause	WLClause.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)
boolean	MixableCBClause.propagate(UnitPropagationListener s, int p)
boolean	WLClause.propagate(UnitPropagationListener s, int p)
boolean	CBClause.propagate(UnitPropagationListener s, int p)
boolean	TernaryClauses.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<L extends ILits>
class	PBSolverClause
class	PBSolverMerging
class	PBSolverWithImpliedClause

Methods in org.sat4j.minisat.constraints.pb with parameters of type UnitPropagationListener

void	MixableCBClausePB.assertConstraint(UnitPropagationListener s)
void	MinWatchCardPB.assertConstraint(UnitPropagationListener s)
void	AtLeastPB.assertConstraint(UnitPropagationListener s)
void	WLClausePB.assertConstraint(UnitPropagationListener s)
void	WatchPb.assertConstraint(UnitPropagationListener s)
static AtLeastPB	AtLeastPB.atLeastNew(UnitPropagationListener s, ILits voc, IVecInt ps, int n)
static MixableCBClausePB	MixableCBClausePB.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals)
static WLClausePB	WLClausePB.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals) Creates a brand new clause, presumably from external data.
protected void	MaxWatchPb.computePropagation(UnitPropagationListener s)
protected void	MinWatchPb.computePropagation(UnitPropagationListener s)
protected abstract void	WatchPb.computePropagation(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 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 MaxWatchPb	MaxWatchPb.normalizedMaxWatchPbNew(UnitPropagationListener s, ILits voc, IDataStructurePB mpb)
static MaxWatchPb	MaxWatchPb.normalizedMaxWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, java.math.BigInteger[] coefs, java.math.BigInteger degree)
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 MinWatchPb	MinWatchPb.normalizedMinWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, java.math.BigInteger[] coefs, java.math.BigInteger degree)
boolean	MaxWatchPb.propagate(UnitPropagationListener s, int p) Propagation de la valeur de v?
boolean	MinWatchPb.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<L extends ILits> 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	DataStructureFactory.setUnitPropagationListener(UnitPropagationListener s)