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

Packages that use ILits

org.sat4j.csp	Classes needed for CSP to SAT translation.
org.sat4j.minisat.constraints	Implementations of various constraints for MiniSAT.
org.sat4j.minisat.constraints.card	Implementations of cardinality constraints.
org.sat4j.minisat.constraints.cnf	Implementations of clausal constraints.
org.sat4j.minisat.core	Implementation of the MiniSAT solver skeleton.
org.sat4j.minisat.learning	Various learning strategies.
org.sat4j.minisat.orders	Various heuristics to select the next variable to branch on.
org.sat4j.pb.constraints	Implementation of data structures for pseudo boolean constraints.
org.sat4j.pb.constraints.pb	Implementations of pseudo boolean constraints.

Uses of ILits in org.sat4j.csp

Methods in org.sat4j.csp with type parameters of type ILits

static <L extends ILits> Solver<DataStructureFactory>

SolverFactory.newMiniSAT(DataStructureFactory dsf)

Uses of ILits in org.sat4j.minisat.constraints

Fields in org.sat4j.minisat.constraints declared as ILits

protected ILits

AbstractDataStructureFactory.lits

Methods in org.sat4j.minisat.constraints that return ILits

protected ILits	MixedDataStructureSingleWL.createLits()
protected ILits	MixedDataStructureDanielWL.createLits()
protected ILits	MixedDataStructureDanielHT.createLits()
protected ILits	ClausalDataStructureWL.createLits()
protected abstract ILits	AbstractDataStructureFactory.createLits()
protected ILits	AbstractCardinalityDataStructure.createLits()
ILits	AbstractDataStructureFactory.getVocabulary()

Uses of ILits in org.sat4j.minisat.constraints.card

Fields in org.sat4j.minisat.constraints.card declared as ILits

protected ILits

AtLeast.voc

Methods in org.sat4j.minisat.constraints.card that return ILits

ILits	MinWatchCard.getVocabulary()
ILits	MaxWatchCard.getVocabulary()

Methods in org.sat4j.minisat.constraints.card with parameters of type ILits

static Constr	AtLeast.atLeastNew(UnitPropagationListener s, ILits voc, IVecInt ps, int n)
protected static int	MinWatchCard.linearisation(ILits voc, IVecInt ps) Simplifies the constraint w.r.t. the assignments of the literals
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)

Constructors in org.sat4j.minisat.constraints.card with parameters of type ILits

AtLeast(ILits voc, IVecInt ps, int degree)

MinWatchCard(ILits voc, IVecInt ps, boolean moreThan, int degree)
Constructs and normalizes a cardinality constraint. used by minWatchCardNew in the non-normalized case.

MinWatchCard(ILits voc, IVecInt ps, int degree)
Constructs and normalizes a cardinality constraint. used by MinWatchCardPB.normalizedMinWatchCardNew() in the normalized case.

Uses of ILits in org.sat4j.minisat.constraints.cnf

Classes in org.sat4j.minisat.constraints.cnf that implement ILits

class

Lits

Fields in org.sat4j.minisat.constraints.cnf declared as ILits

protected ILits	WLClause.voc
protected ILits	HTClause.voc

Methods in org.sat4j.minisat.constraints.cnf that return ILits

ILits	WLClause.getVocabulary()
ILits	HTClause.getVocabulary()
ILits	BinaryClause.getVocabulary()

Methods in org.sat4j.minisat.constraints.cnf with parameters of type ILits

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.
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

Constructors in org.sat4j.minisat.constraints.cnf with parameters of type ILits

BinaryClause(IVecInt ps, ILits voc)
Creates a new basic clause

HTClause(IVecInt ps, ILits voc)
Creates a new basic clause

LearntBinaryClause(IVecInt ps, ILits voc)

LearntHTClause(IVecInt ps, ILits voc)

LearntWLClause(IVecInt ps, ILits voc)

OriginalBinaryClause(IVecInt ps, ILits voc)

OriginalHTClause(IVecInt ps, ILits voc)

OriginalWLClause(IVecInt ps, ILits voc)

WLClause(IVecInt ps, ILits voc)
Creates a new basic clause

Uses of ILits in org.sat4j.minisat.core

Fields in org.sat4j.minisat.core declared as ILits

protected ILits

Solver.voc

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) Method used to provide an easy access the the solver vocabulary.

Uses of ILits in org.sat4j.minisat.learning

Fields in org.sat4j.minisat.learning declared as ILits

protected ILits

LimitedLearning.lits

Uses of ILits in org.sat4j.minisat.orders

Fields in org.sat4j.minisat.orders declared as ILits

protected ILits

VarOrderHeap.lits

Methods in org.sat4j.minisat.orders that return ILits

ILits

VarOrderHeap.getVocabulary()

Methods in org.sat4j.minisat.orders with parameters of type ILits

void	VarOrderHeap.setLits(ILits lits)
void	TabuListDecorator.setLits(ILits lits)
void	RandomWalkDecorator.setLits(ILits lits)

Uses of ILits in org.sat4j.pb.constraints

Methods in org.sat4j.pb.constraints that return ILits

protected ILits

AbstractPBDataStructureFactory.createLits()

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

Constr	MinCardPBConstructor.constructCard(UnitPropagationListener solver, ILits voc, IVecInt theLits, int degree)
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	AtLeastCardConstructor.constructCard(UnitPropagationListener solver, ILits voc, IVecInt theLits, int degree)
Constr	UnitBinaryWLClauseConstructor.constructClause(UnitPropagationListener solver, ILits voc, IVecInt v)
Constr	UnitBinaryHTClausePBConstructor.constructClause(UnitPropagationListener solver, ILits voc, IVecInt v)
Constr	UnitBinaryHTClauseConstructor.constructClause(UnitPropagationListener solver, ILits voc, IVecInt v)
Constr	IClauseConstructor.constructClause(UnitPropagationListener solver, ILits voc, IVecInt v)
Constr	MinCardPBConstructor.constructLearntCard(ILits voc, IDataStructurePB dspb)
Constr	MinCardConstructor.constructLearntCard(ILits voc, IDataStructurePB dspb)
Constr	ICardConstructor.constructLearntCard(ILits voc, IDataStructurePB dspb)
Constr	AtLeastCardPBConstructor.constructLearntCard(ILits voc, IDataStructurePB dspb)
Constr	AtLeastCardConstructor.constructLearntCard(ILits voc, IDataStructurePB dspb)
Constr	UnitBinaryWLClauseConstructor.constructLearntClause(ILits voc, IVecInt literals)
Constr	UnitBinaryHTClausePBConstructor.constructLearntClause(ILits voc, IVecInt literals)
Constr	UnitBinaryHTClauseConstructor.constructLearntClause(ILits voc, IVecInt literals)
Constr	IClauseConstructor.constructLearntClause(ILits voc, IVecInt literals)
Constr	PuebloMinWatchPBConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
Constr	MinWatchPBConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
Constr	MinLongWatchPBCPConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
Constr	MinLongWatchPBConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
Constr	MaxWatchPBConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
Constr	MaxLongWatchPBCPConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
Constr	MaxLongWatchPBConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
Constr	IPBConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
Constr	PuebloMinWatchPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)
Constr	MinWatchPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)
Constr	MinLongWatchPBCPConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)
Constr	MinLongWatchPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)
Constr	MaxWatchPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)
Constr	MaxLongWatchPBCPConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)
Constr	MaxLongWatchPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)
Constr	IPBConstructor.constructPB(UnitPropagationListener solver, ILits voc, int[] theLits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)

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

Fields in org.sat4j.pb.constraints.pb declared as ILits

protected ILits	WatchPbLongCP.voc constraint's vocabulary
protected ILits	WatchPbLong.voc constraint's vocabulary
protected ILits	WatchPb.voc constraint's vocabulary

Methods in org.sat4j.pb.constraints.pb that return ILits

ILits	WatchPbLongCP.getVocabulary()
ILits	WatchPbLong.getVocabulary()
ILits	WatchPb.getVocabulary()
ILits	UnitClausesPB.getVocabulary()
ILits	UnitClausePB.getVocabulary()
ILits	PBConstr.getVocabulary()
ILits	AtLeastPB.getVocabulary()

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

static AtLeastPB	AtLeastPB.atLeastNew(ILits voc, IVecInt ps, int n)
static PBConstr	AtLeastPB.atLeastNew(UnitPropagationListener s, ILits voc, IVecInt ps, int n)
static OriginalHTClausePB	OriginalHTClausePB.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals) Creates a brand new clause, presumably from external data.
static OriginalBinaryClausePB	OriginalBinaryClausePB.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals) Creates a brand new clause, presumably from external data.
static PBConstr	MinWatchCardPB.minWatchCardPBNew(UnitPropagationListener s, ILits voc, IVecInt ps, boolean moreThan, int degree) Permet la cr?
static IDataStructurePB	Pseudos.niceCheckedParameters(IVecInt ps, IVec<BigInteger> bigCoefs, boolean moreThan, BigInteger bigDeg, ILits voc)
static IDataStructurePB	Pseudos.niceParameters(IVecInt ps, IVec<BigInteger> bigCoefs, boolean moreThan, BigInteger bigDeg, ILits voc)
static MaxWatchPbLongCP	MaxWatchPbLongCP.normalizedMaxWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs) build a pseudo boolean constraint.
static MaxWatchPbLong	MaxWatchPbLong.normalizedMaxWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs) build a pseudo boolean constraint.
static MaxWatchPb	MaxWatchPb.normalizedMaxWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs) build a pseudo boolean constraint.
static PBConstr	MinWatchCardPB.normalizedMinWatchCardPBNew(UnitPropagationListener s, ILits voc, IVecInt ps, int degree) Permet la cr?
static PuebloMinWatchPb	PuebloMinWatchPb.normalizedMinWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree)
static MinWatchPbLongLimit	MinWatchPbLongLimit.normalizedMinWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs) build a pseudo boolean constraint.
static MinWatchPbLongCP	MinWatchPbLongCP.normalizedMinWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs) build a pseudo boolean constraint.
static MinWatchPbLong	MinWatchPbLong.normalizedMinWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs) build a pseudo boolean constraint.
static MinWatchPb	MinWatchPb.normalizedMinWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs) build a pseudo boolean constraint.
static WatchPb	PuebloMinWatchPb.normalizedWatchPbNew(ILits voc, IDataStructurePB mpb)
static WatchPbLong	MinWatchPbLongLimit.normalizedWatchPbNew(ILits voc, IDataStructurePB mpb) build a pseudo boolean constraint from a specific data structure.
static WatchPbLongCP	MinWatchPbLongCP.normalizedWatchPbNew(ILits voc, IDataStructurePB mpb) build a pseudo boolean constraint from a specific data structure.
static WatchPbLong	MinWatchPbLong.normalizedWatchPbNew(ILits voc, IDataStructurePB mpb) build a pseudo boolean constraint from a specific data structure.
static WatchPb	MinWatchPb.normalizedWatchPbNew(ILits voc, IDataStructurePB mpb) build a pseudo boolean constraint from a specific data structure.
static WatchPbLongCP	MaxWatchPbLongCP.normalizedWatchPbNew(ILits voc, IDataStructurePB mpb) build a pseudo boolean constraint from a specific data structure.
static WatchPbLong	MaxWatchPbLong.normalizedWatchPbNew(ILits voc, IDataStructurePB mpb) build a pseudo boolean constraint from a specific data structure.
static WatchPb	MaxWatchPb.normalizedWatchPbNew(ILits voc, IDataStructurePB mpb) build a pseudo boolean constraint from a specific data structure.

Constructors in org.sat4j.pb.constraints.pb with parameters of type ILits

LearntBinaryClausePB(IVecInt ps, ILits voc)

LearntHTClausePB(IVecInt ps, ILits voc)

MinWatchCardPB(ILits voc, IVecInt ps, boolean moreThan, int degree)

MinWatchCardPB(ILits voc, IVecInt ps, int degree)

MinWatchPb(ILits voc, IDataStructurePB mpb)
Basic constructor for pb constraint a0.x0 + a1.x1 + ... + an.xn >= k This constructor is called for learnt pseudo boolean constraints.

MinWatchPb(ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)
Basic constructor for PB constraint a0.x0 + a1.x1 + ... + an.xn >= k

MinWatchPbLong(ILits voc, IDataStructurePB mpb)
Basic constructor for pb constraint a0.x0 + a1.x1 + ... + an.xn >= k This constructor is called for learnt pseudo boolean constraints.

MinWatchPbLong(ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)
Basic constructor for PB constraint a0.x0 + a1.x1 + ... + an.xn >= k

MinWatchPbLongCP(ILits voc, IDataStructurePB mpb)
Basic constructor for pb constraint a0.x0 + a1.x1 + ... + an.xn >= k This constructor is called for learnt pseudo boolean constraints.

MinWatchPbLongCP(ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)
Basic constructor for PB constraint a0.x0 + a1.x1 + ... + an.xn >= k

MinWatchPbLongLimit(ILits voc, IDataStructurePB mpb)
Basic constructor for pb constraint a0.x0 + a1.x1 + ... + an.xn >= k This constructor is called for learnt pseudo boolean constraints.

MinWatchPbLongLimit(ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs)
Basic constructor for PB constraint a0.x0 + a1.x1 + ... + an.xn >= k

OriginalBinaryClausePB(IVecInt ps, ILits voc)

OriginalHTClausePB(IVecInt ps, ILits voc)

UnitClausePB(int value, ILits voc)