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 contraints.
org.sat4j.minisat.constraints.cnf	Implementations of clausal contraints.
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
org.sat4j.pb.constraints.pb	Implementations of pseudo boolean contraints.

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	ClausalDataStructureWL.createLits()
protected abstract ILits	AbstractDataStructureFactory.createLits()
protected ILits	MixedDataStructureSingleWL.createLits()
protected ILits	AbstractCardinalityDataStructure.createLits()
protected ILits	MixedDataStructureDanielHT.createLits()
protected ILits	MixedDataStructureDanielWL.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	MaxWatchCard.getVocabulary()
ILits	MinWatchCard.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	HTClause.voc
protected ILits	WLClause.voc

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

ILits	HTClause.getVocabulary()
ILits	WLClause.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	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	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	MinCardConstructor.constructLearntCard(ILits voc, IDataStructurePB dspb)
Constr	ICardConstructor.constructLearntCard(ILits voc, IDataStructurePB dspb)
Constr	AtLeastCardPBConstructor.constructLearntCard(ILits voc, IDataStructurePB dspb)
Constr	MinCardPBConstructor.constructLearntCard(ILits voc, IDataStructurePB dspb)
Constr	AtLeastCardConstructor.constructLearntCard(ILits voc, IDataStructurePB dspb)
Constr	UnitBinaryHTClauseConstructor.constructLearntClause(ILits voc, IVecInt literals)
Constr	UnitBinaryWLClauseConstructor.constructLearntClause(ILits voc, IVecInt literals)
Constr	UnitBinaryHTClausePBConstructor.constructLearntClause(ILits voc, IVecInt literals)
Constr	IClauseConstructor.constructLearntClause(ILits voc, IVecInt literals)
Constr	MinLongWatchPBConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
Constr	MaxLongWatchPBConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
Constr	MinWatchPBConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
Constr	MaxWatchPBConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
Constr	MinLongWatchPBCPConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
Constr	MaxLongWatchPBCPConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
Constr	IPBConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
Constr	PuebloMinWatchPBConstructor.constructLearntPB(ILits voc, IDataStructurePB dspb)
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 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	WatchPb.voc constraint's vocabulary
protected ILits	WatchPbLong.voc constraint's vocabulary

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

ILits	WatchPbLongCP.getVocabulary()
ILits	AtLeastPB.getVocabulary()
ILits	WatchPb.getVocabulary()
ILits	PBConstr.getVocabulary()
ILits	UnitClausesPB.getVocabulary()
ILits	WatchPbLong.getVocabulary()
ILits	UnitClausePB.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 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.
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 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)
static WatchPb	MaxWatchPb.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 WatchPbLong	MinWatchPbLongLimit.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 WatchPb	MinWatchPb.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 WatchPb	PuebloMinWatchPb.normalizedWatchPbNew(ILits voc, IDataStructurePB mpb)
static WatchPbLong	MaxWatchPbLong.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)
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)
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)
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)
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)