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	ClausalDataStructureCB.createLits()
protected ILits	AbstractCardinalityDataStructure.createLits()
protected ILits	MixedDataStructureDanielHT.createLits()
protected ILits	MixedDataStructureDanielWL.createLits()
protected ILits	ClausalDataStructureCBWL.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 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)

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	CBClause.voc
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 CBClause	CBClause.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 OriginalHTClause	OriginalHTClause.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals) Creates a brand new clause, presumably from external data.
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 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

CBClause(IVecInt ps, ILits voc)

CBClause(IVecInt ps, ILits voc, boolean learnt)

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)

MixableCBClause(IVecInt ps, ILits voc)

MixableCBClause(IVecInt ps, ILits voc, boolean learnt)

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()

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

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

protected ILits

WatchPb.voc constraint's vocabulary

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

ILits	AtLeastPB.getVocabulary()
ILits	WatchPb.getVocabulary()
ILits	PBConstr.getVocabulary()
ILits	MixableCBClausePB.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 AtLeastPB	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 MixableCBClausePB	MixableCBClausePB.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals)
static OriginalHTClausePB	OriginalHTClausePB.brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals) Creates a brand new clause, presumably from external data.
static MinWatchCardPB	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 MinWatchCardPB	MinWatchCardPB.normalizedMinWatchCardPBNew(UnitPropagationListener s, ILits voc, IVecInt ps, int degree) Permet la cr?
static MinWatchPb	MinWatchPb.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 WatchPb	MinWatchPb.normalizedWatchPbNew(ILits voc, IDataStructurePB mpb) build a pseudo boolean constraint from a specific data structure.
static WatchPb	PuebloMinWatchPb.normalizedWatchPbNew(ILits voc, IDataStructurePB mpb)

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

MixableCBClausePB(IVecInt ps, ILits voc)

MixableCBClausePB(IVecInt ps, ILits voc, boolean learnt)

OriginalBinaryClausePB(IVecInt ps, ILits voc)

OriginalHTClausePB(IVecInt ps, ILits voc)

UnitClausePB(int value, ILits voc)