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.core	Implementation of the MiniSAT solver skeleton.
org.sat4j.pb.constraints
org.sat4j.pb.constraints.pb	Implementations of pseudo boolean contraints.
org.sat4j.pb.core

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 Constr	MaxWatchCard.maxWatchCardNew(UnitPropagationListener s, ILits voc, IVecInt ps, boolean moreThan, int degree) Permet la cr?
static Constr	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	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	UnitClause.assertConstraint(UnitPropagationListener s)
void	UnitClauses.assertConstraint(UnitPropagationListener s)
void	WLClause.assertConstraint(UnitPropagationListener s)
void	BinaryClause.assertConstraint(UnitPropagationListener s)
static OriginalWLClause	OriginalWLClause.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.
static OriginalBinaryClause	OriginalBinaryClause.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals) Creates a brand new clause, presumably from external data.
boolean	HTClause.propagate(UnitPropagationListener s, int p)
boolean	UnitClause.propagate(UnitPropagationListener s, int p)
boolean	UnitClauses.propagate(UnitPropagationListener s, int p)
boolean	WLClause.propagate(UnitPropagationListener s, int p)
boolean	BinaryClause.propagate(UnitPropagationListener s, int p)
void	HTClause.remove(UnitPropagationListener upl)
void	UnitClause.remove(UnitPropagationListener upl)
void	UnitClauses.remove(UnitPropagationListener upl)
void	WLClause.remove(UnitPropagationListener upl)
void	BinaryClause.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)

Uses of UnitPropagationListener in org.sat4j.pb.constraints

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

Constr	MinCardConstructor.constructCard(UnitPropagationListener solver, ILits voc, IVecInt theLits, int degree)
Constr	ICardConstructor.constructCard(UnitPropagationListener solver, ILits voc, IVecInt theLits, int degree)
Constr	AtLeastCardPBConstructor.constructCard(UnitPropagationListener solver, ILits voc, IVecInt theLits, int degree)
Constr	MinCardPBConstructor.constructCard(UnitPropagationListener solver, ILits voc, IVecInt theLits, int degree)
Constr	AtLeastCardConstructor.constructCard(UnitPropagationListener solver, ILits voc, IVecInt theLits, int degree)
Constr	UnitBinaryHTClauseConstructor.constructClause(UnitPropagationListener solver, ILits voc, IVecInt v)
Constr	UnitBinaryWLClauseConstructor.constructClause(UnitPropagationListener solver, ILits voc, IVecInt v)
Constr	UnitBinaryHTClausePBConstructor.constructClause(UnitPropagationListener solver, ILits voc, IVecInt v)
Constr	IClauseConstructor.constructClause(UnitPropagationListener solver, ILits voc, IVecInt v)
Constr	MinLongWatchPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree)
Constr	MaxLongWatchPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree)
Constr	MinWatchPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree)
Constr	MaxWatchPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree)
Constr	MinLongWatchPBCPConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree)
Constr	MaxLongWatchPBCPConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree)
Constr	IPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree)
Constr	PuebloMinWatchPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree)

Uses of UnitPropagationListener in org.sat4j.pb.constraints.pb

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

void	MinWatchCardPB.assertConstraint(UnitPropagationListener s)
void	WatchPbLongCP.assertConstraint(UnitPropagationListener s)
void	AtLeastPB.assertConstraint(UnitPropagationListener s)
void	WatchPb.assertConstraint(UnitPropagationListener s)
void	WatchPbLong.assertConstraint(UnitPropagationListener s)
void	LearntHTClausePB.assertConstraint(UnitPropagationListener s)
static PBConstr	AtLeastPB.atLeastNew(UnitPropagationListener s, ILits voc, IVecInt ps, int n)
static OriginalBinaryClausePB	OriginalBinaryClausePB.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals) Creates a brand new clause, presumably from external data.
static OriginalHTClausePB	OriginalHTClausePB.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals) Creates a brand new clause, presumably from external data.
protected void	MaxWatchPb.computePropagation(UnitPropagationListener s)
protected void	MinWatchPbLong.computePropagation(UnitPropagationListener s)
protected void	MinWatchPbLongLimit.computePropagation(UnitPropagationListener s)
protected abstract void	WatchPbLongCP.computePropagation(UnitPropagationListener s)
protected abstract void	WatchPb.computePropagation(UnitPropagationListener s)
protected void	MaxWatchPbLongCP.computePropagation(UnitPropagationListener s)
protected void	MinWatchPb.computePropagation(UnitPropagationListener s)
protected abstract void	WatchPbLong.computePropagation(UnitPropagationListener s)
protected void	MinWatchPbLongCP.computePropagation(UnitPropagationListener s)
protected void	MaxWatchPbLong.computePropagation(UnitPropagationListener s)
static PBConstr	MinWatchCardPB.minWatchCardPBNew(UnitPropagationListener s, ILits voc, IVecInt ps, boolean moreThan, int degree) Permet la cr?
static MaxWatchPb	MaxWatchPb.normalizedMaxWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree) build a pseudo boolean constraint.
static MaxWatchPbLongCP	MaxWatchPbLongCP.normalizedMaxWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree) build a pseudo boolean constraint.
static MaxWatchPbLong	MaxWatchPbLong.normalizedMaxWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree) build a pseudo boolean constraint.
static PBConstr	MinWatchCardPB.normalizedMinWatchCardPBNew(UnitPropagationListener s, ILits voc, IVecInt ps, int degree) Permet la cr?
static MinWatchPbLong	MinWatchPbLong.normalizedMinWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree) build a pseudo boolean constraint.
static MinWatchPbLongLimit	MinWatchPbLongLimit.normalizedMinWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree) build a pseudo boolean constraint.
static MinWatchPb	MinWatchPb.normalizedMinWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree) build a pseudo boolean constraint.
static MinWatchPbLongCP	MinWatchPbLongCP.normalizedMinWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree) build a pseudo boolean constraint.
static PuebloMinWatchPb	PuebloMinWatchPb.normalizedMinWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree)
boolean	MaxWatchPb.propagate(UnitPropagationListener s, int p) Propagation of a falsified literal
boolean	MinWatchPbLong.propagate(UnitPropagationListener s, int p) Propagation of a falsified literal
boolean	MinWatchPbLongLimit.propagate(UnitPropagationListener s, int p) Propagation of a falsified literal
boolean	MaxWatchPbLongCP.propagate(UnitPropagationListener s, int p) Propagation of a falsified literal
boolean	MinWatchPb.propagate(UnitPropagationListener s, int p) Propagation of a falsified literal
boolean	WatchPbLong.propagate(UnitPropagationListener s, int p)
boolean	MinWatchPbLongCP.propagate(UnitPropagationListener s, int p) Propagation of a falsified literal
boolean	MaxWatchPbLong.propagate(UnitPropagationListener s, int p) Propagation of a falsified literal
void	MaxWatchPb.remove(UnitPropagationListener upl) Remove a constraint from the solver
void	MinWatchPbLong.remove(UnitPropagationListener upl) Remove the constraint from the solver
void	MinWatchPbLongLimit.remove(UnitPropagationListener upl) Remove the constraint from the solver
void	MaxWatchPbLongCP.remove(UnitPropagationListener upl) Remove a constraint from the solver
void	MinWatchPb.remove(UnitPropagationListener upl) Remove the constraint from the solver
void	WatchPbLong.remove(UnitPropagationListener upl)
void	MinWatchPbLongCP.remove(UnitPropagationListener upl) Remove the constraint from the solver
void	MaxWatchPbLong.remove(UnitPropagationListener upl) Remove a constraint from the solver

Uses of UnitPropagationListener in org.sat4j.pb.core

Classes in org.sat4j.pb.core that implement UnitPropagationListener

class	PBSolver
class	PBSolverCautious
class	PBSolverClause
class	PBSolverCP
class	PBSolverMerging
class	PBSolverResCP
class	PBSolverResolution
class	PBSolverWithImpliedClause