Uses of Interface
org.sat4j.specs.IVecInt

Packages that use IVecInt

org.sat4j.core	Implementation of the data structures available in org.sat4j.specs.
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.
org.sat4j.opt	Built-in optimization framework.
org.sat4j.reader	Some utility classes to read problems from plain text files.
org.sat4j.specs	Those classes are intented for users dealing with SAT solvers as blackboxes.
org.sat4j.tools	Tools to be used on top of an ISolver.

Uses of IVecInt in org.sat4j.core

Classes in org.sat4j.core that implement IVecInt

class

VecInt A vector specific for primitive integers, widely used in the solver.

Fields in org.sat4j.core declared as IVecInt

static IVecInt

VecInt.EMPTY

Methods in org.sat4j.core that return IVecInt

IVecInt	VecInt.pop() depile le dernier element du vecteur.
IVecInt	VecInt.push(int elem)

Methods in org.sat4j.core with parameters of type IVecInt

void	VecInt.copyTo(IVecInt copy) C'est operations devraient se faire en temps constant.
void	VecInt.moveTo(IVecInt dest)
void	VecInt.moveTo2(IVecInt dest)
void	VecInt.pushAll(IVecInt vec)

Uses of IVecInt in org.sat4j.minisat.constraints

Methods in org.sat4j.minisat.constraints with parameters of type IVecInt

protected PBConstr	PuebloPBMinDataStructure.constraintFactory(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)
protected WatchPb	PBMaxDataStructure.constraintFactory(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)
protected PBConstr	PBMinDataStructure.constraintFactory(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)
protected abstract PBConstr	AbstractPBDataStructureFactory.constraintFactory(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)
protected PBConstr	AbstractPBClauseCardConstrDataStructure.constraintFactory(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)
protected PBConstr	PuebloPBMinDataStructure.constraintFactory(IVecInt literals, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
protected WatchPb	PBMaxDataStructure.constraintFactory(IVecInt literals, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
protected PBConstr	PBMinDataStructure.constraintFactory(IVecInt literals, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
protected abstract PBConstr	AbstractPBDataStructureFactory.constraintFactory(IVecInt literals, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
protected PBConstr	AbstractPBClauseCardConstrDataStructure.constraintFactory(IVecInt literals, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
protected PBConstr	PuebloPBMinDataStructure.constraintFactory(IVecInt literals, IVecInt coefs, boolean moreThan, int degree)
protected WatchPb	PBMaxDataStructure.constraintFactory(IVecInt literals, IVecInt coefs, boolean moreThan, int degree)
protected PBConstr	PBMinDataStructure.constraintFactory(IVecInt literals, IVecInt coefs, boolean moreThan, int degree)
protected abstract PBConstr	AbstractPBDataStructureFactory.constraintFactory(IVecInt literals, IVecInt coefs, boolean moreThan, int degree)
protected PBConstr	AbstractPBClauseCardConstrDataStructure.constraintFactory(IVecInt literals, IVecInt coefs, boolean moreThan, int degree)
protected PBConstr	PuebloPBMinDataStructure.constraintFactory(IVecInt literals, IVecInt coefs, int degree)
protected WatchPb	PBMaxDataStructure.constraintFactory(IVecInt literals, IVecInt coefs, int degree)
protected PBConstr	PBMinDataStructure.constraintFactory(IVecInt literals, IVecInt coefs, int degree)
protected abstract PBConstr	AbstractPBDataStructureFactory.constraintFactory(IVecInt literals, IVecInt coefs, int degree)
protected PBConstr	AbstractPBClauseCardConstrDataStructure.constraintFactory(IVecInt literals, IVecInt coefs, int degree)
protected PBConstr	PBMaxClauseAtLeastConstrDataStructure.constructCard(IVecInt lits, int degree)
protected PBConstr	PuebloPBMinClauseAtLeastConstrDataStructure.constructCard(IVecInt lits, int degree)
protected PBConstr	PuebloPBMinClauseCardConstrDataStructure.constructCard(IVecInt lits, int degree)
protected abstract PBConstr	AbstractPBClauseCardConstrDataStructure.constructCard(IVecInt lits, int degree)
protected PBConstr	PBMaxCBClauseCardConstrDataStructure.constructClause(IVecInt v)
protected PBConstr	PuebloPBMinClauseCardConstrDataStructure.constructClause(IVecInt v)
protected abstract PBConstr	AbstractPBClauseCardConstrDataStructure.constructClause(IVecInt v)
protected PBConstr	PBMaxClauseAtLeastConstrDataStructure.constructLearntCard(IVecInt literals, int degree)
protected PBConstr	PuebloPBMinClauseAtLeastConstrDataStructure.constructLearntCard(IVecInt literals, int degree)
protected PBConstr	PuebloPBMinClauseCardConstrDataStructure.constructLearntCard(IVecInt literals, int degree)
protected abstract PBConstr	AbstractPBClauseCardConstrDataStructure.constructLearntCard(IVecInt literals, int degree)
protected PBConstr	PBMaxCBClauseCardConstrDataStructure.constructLearntClause(IVecInt literals)
protected PBConstr	PuebloPBMinClauseCardConstrDataStructure.constructLearntClause(IVecInt literals)
protected abstract PBConstr	AbstractPBClauseCardConstrDataStructure.constructLearntClause(IVecInt literals)
protected PBConstr	PBMaxClauseCardConstrDataStructure.constructLearntPB(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)
protected PBConstr	PuebloPBMinClauseCardConstrDataStructure.constructLearntPB(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)
protected PBConstr	PBMinClauseCardConstrDataStructure.constructLearntPB(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)
protected abstract PBConstr	AbstractPBClauseCardConstrDataStructure.constructLearntPB(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)
Constr	AbstractPBDataStructureFactory.createCardinalityConstraint(IVecInt literals, int degree)
Constr	CardinalityDataStructureYanMax.createCardinalityConstraint(IVecInt literals, int degree)
Constr	CardinalityDataStructure.createCardinalityConstraint(IVecInt literals, int degree)
Constr	CardinalityDataStructureYanMin.createCardinalityConstraint(IVecInt literals, int degree)
Constr	MixedDataStructureDaniel.createCardinalityConstraint(IVecInt literals, int degree)
Constr	AbstractDataStructureFactory.createCardinalityConstraint(IVecInt literals, int degree)
Constr	MixedDataStructureDanielCBWL.createClause(IVecInt literals)
Constr	AbstractPBDataStructureFactory.createClause(IVecInt literals)
Constr	CardinalityDataStructureYanMax.createClause(IVecInt literals)
Constr	CardinalityDataStructure.createClause(IVecInt literals)
Constr	CardinalityDataStructureYanMin.createClause(IVecInt literals)
Constr	ClausalDataStructureWL.createClause(IVecInt literals)
Constr	ClausalDataStructureCBWL.createClause(IVecInt literals)
Constr	ClausalDataStructureCB.createClause(IVecInt literals)
Constr	MixedDataStructureWithBinaryAndTernary.createClause(IVecInt literals)
Constr	MixedDataStructureDaniel.createClause(IVecInt literals)
Constr	MixedDataStructureWithBinary.createClause(IVecInt literals)
Constr	AbstractPBDataStructureFactory.createPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
Constr	AbstractCardinalityDataStructure.createPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
Constr	AbstractDataStructureFactory.createPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
Constr	AbstractPBDataStructureFactory.createUnregisteredClause(IVecInt literals)
Constr	CardinalityDataStructureYanMax.createUnregisteredClause(IVecInt literals)
Constr	CardinalityDataStructure.createUnregisteredClause(IVecInt literals)
Constr	CardinalityDataStructureYanMin.createUnregisteredClause(IVecInt literals)
Constr	ClausalDataStructureWL.createUnregisteredClause(IVecInt literals)
Constr	ClausalDataStructureCBWL.createUnregisteredClause(IVecInt literals)
Constr	ClausalDataStructureCB.createUnregisteredClause(IVecInt literals)
Constr	MixedDataStructureWithBinaryAndTernary.createUnregisteredClause(IVecInt literals)
Constr	MixedDataStructureDaniel.createUnregisteredClause(IVecInt literals)
Constr	MixedDataStructureWithBinary.createUnregisteredClause(IVecInt literals)
Constr	AbstractPBDataStructureFactory.createUnregisteredPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)
Constr	AbstractDataStructureFactory.createUnregisteredPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)
IConstr	AbstractPBDataStructureFactory.createUnregisteredPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)

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

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

static AtLeast	AtLeast.atLeastNew(UnitPropagationListener s, ILits voc, IVecInt ps, int n)
void	MaxWatchCard.calcReason(int p, IVecInt outReason) Calcule la cause de l'affection d'un litt?
void	MinWatchCard.calcReason(int p, IVecInt outReason) computes the reason for a literal
void	AtLeast.calcReason(int p, IVecInt outReason)
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 IVecInt

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 IVecInt in org.sat4j.minisat.constraints.cnf

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

IVecInt	MarkableLits.getMarkedLiterals()
IVecInt	MarkableLits.getMarkedLiterals(int mark)
IVecInt	MarkableLits.getMarkedVariables()
IVecInt	MarkableLits.getMarkedVariables(int mark)
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

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

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)
void	WLClause.calcReason(int p, IVecInt outReason)
void	CBClause.calcReason(int p, IVecInt outReason)
void	TernaryClauses.calcReason(int p, IVecInt outReason)
void	BinaryClauses.calcReason(int p, IVecInt outReason)
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

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

CBClause(IVecInt ps, ILits voc)

CBClause(IVecInt ps, ILits voc, boolean learnt)

DefaultWLClause(IVecInt ps, ILits voc)

LearntWLClause(IVecInt ps, ILits voc)

MixableCBClause(IVecInt ps, ILits voc)

MixableCBClause(IVecInt ps, ILits voc, boolean learnt)

OriginalWLClause(IVecInt ps, ILits voc)

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

Uses of IVecInt in org.sat4j.minisat.constraints.pb

Methods in org.sat4j.minisat.constraints.pb that return IVecInt

IVecInt	MixableCBClausePB.computeAnImpliedClause()
IVecInt	MinWatchCardPB.computeAnImpliedClause()
IVecInt	AtLeastPB.computeAnImpliedClause()
IVecInt	WLClausePB.computeAnImpliedClause()
IVecInt	WatchPb.computeAnImpliedClause() compute an implied clause on the literals with the greater coefficients
IVecInt	PBConstr.computeAnImpliedClause()

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

IConstr	PBSolverWithImpliedClause.addPseudoBoolean(IVecInt literals, IVec<java.math.BigInteger> coeffs, boolean moreThan, java.math.BigInteger degree)
static AtLeastPB	AtLeastPB.atLeastNew(ILits voc, IVecInt ps, int n)
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.
void	MapPb.buildConstraintFromConflict(IVecInt resLits, IVec<java.math.BigInteger> resCoefs)
void	IDataStructurePB.buildConstraintFromConflict(IVecInt resLits, IVec<java.math.BigInteger> resCoefs)
void	WatchPb.calcReason(int p, IVecInt outReason) compute the reason for the assignment of a literal
IConstr	IInternalPBConstraintCreator.createUnregisteredPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)
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, 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 IDataStructurePB	WatchPb.niceCheckedParameters(IVecInt ps, IVec<java.math.BigInteger> bigCoefs, boolean moreThan, java.math.BigInteger bigDeg, ILits voc)
static IDataStructurePB	WatchPb.niceParameters(IVecInt ps, IVec<java.math.BigInteger> bigCoefs, boolean moreThan, java.math.BigInteger bigDeg, ILits voc)
static MinWatchCardPB	MinWatchCardPB.normalizedMinWatchCardPBNew(UnitPropagationListener s, ILits voc, IVecInt ps, int degree) Permet la cr?
static IVec<java.math.BigInteger>	WatchPb.toVecBigInt(IVecInt vec)
static WatchPb	MaxWatchPb.watchPbNew(ILits voc, IVecInt lits, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
static WatchPb	PuebloMinWatchPb.watchPbNew(ILits voc, IVecInt lits, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
static WatchPb	MinWatchPb.watchPbNew(ILits voc, IVecInt lits, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
static WatchPb	MaxWatchPb.watchPbNew(ILits voc, IVecInt lits, IVecInt coefs, boolean moreThan, int degree)
static WatchPb	PuebloMinWatchPb.watchPbNew(ILits voc, IVecInt lits, IVecInt coefs, boolean moreThan, int degree)
static WatchPb	MinWatchPb.watchPbNew(ILits voc, IVecInt lits, IVecInt coefs, boolean moreThan, int degree)

Constructors in org.sat4j.minisat.constraints.pb with parameters of type IVecInt

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

MinWatchCardPB(ILits voc, IVecInt ps, int degree)

MixableCBClausePB(IVecInt ps, ILits voc)

MixableCBClausePB(IVecInt ps, ILits voc, boolean learnt)

WLClausePB(IVecInt ps, ILits voc)

Uses of IVecInt in org.sat4j.minisat.core

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

protected IVecInt	Solver.trail affectation en ordre chronologique
protected IVecInt	Solver.trailLim indice des s?

Methods in org.sat4j.minisat.core that return IVecInt

protected IVecInt	Solver.dimacs2internal(IVecInt in)
IVecInt	IMarkableLits.getMarkedLiterals() Returns the set of all marked literals.
IVecInt	IMarkableLits.getMarkedLiterals(int mark) Returns that set of all the literals having a specific mark.
IVecInt	IMarkableLits.getMarkedVariables() Returns the set of all marked variables.
IVecInt	IMarkableLits.getMarkedVariables(int mark) Returns the set of all variables having a specific mark.
IVecInt	Solver.getOutLearnt()

Methods in org.sat4j.minisat.core with parameters of type IVecInt

IConstr	Solver.addAtLeast(IVecInt literals, int degree)
IConstr	Solver.addAtMost(IVecInt literals, int degree)
IConstr	Solver.addClause(IVecInt literals)
IConstr	Solver.addPseudoBoolean(IVecInt literals, IVec<java.math.BigInteger> coeffs, boolean moreThan, java.math.BigInteger degree)
void	Constr.calcReason(int p, IVecInt outReason) Compute the reason for a given assignment.
Constr	DataStructureFactory.createCardinalityConstraint(IVecInt literals, int degree)
Constr	DataStructureFactory.createClause(IVecInt literals)
Constr	DataStructureFactory.createPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
Constr	DataStructureFactory.createUnregisteredClause(IVecInt literals)
Constr	DataStructureFactory.createUnregisteredPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)
protected IVecInt	Solver.dimacs2internal(IVecInt in)
int[]	Solver.findModel(IVecInt assumps)
boolean	Solver.isSatisfiable(IVecInt assumps)

Method parameters in org.sat4j.minisat.core with type arguments of type IVecInt

void	Solver.addAllClauses(IVec<IVecInt> clauses)

Uses of IVecInt in org.sat4j.opt

Methods in org.sat4j.opt that return IVecInt

IVecInt

ObjectiveFunction.getVars()

Methods in org.sat4j.opt with parameters of type IVecInt

IConstr	MaxSatDecorator.addClause(IVecInt literals)
IConstr	WeightedMaxSatDecorator.addClause(IVecInt literals)

Constructors in org.sat4j.opt with parameters of type IVecInt

ObjectiveFunction(IVecInt vars, IVec<java.math.BigInteger> coeffs)

Uses of IVecInt in org.sat4j.reader

Methods in org.sat4j.reader that return IVecInt

IVecInt

OPBReader2005.getVars()

Methods in org.sat4j.reader with parameters of type IVecInt

protected boolean	ExtendedDimacsReader.handleConstr(java.lang.String line, IVecInt literals)
protected boolean	DimacsReader.handleConstr(java.lang.String line, IVecInt literals)
protected void	OPBReader2007.literalInAProduct(java.lang.String var, IVecInt lits) callback called when we read a term of a constraint
protected void	OPBReader2007.negateLiteralInAProduct(java.lang.String var, IVecInt lits) callback called when we read a term of a constraint

Uses of IVecInt in org.sat4j.specs

Methods in org.sat4j.specs that return IVecInt

IVecInt	IVecInt.pop() depile le dernier element du vecteur.
IVecInt	IVecInt.push(int elem)

Methods in org.sat4j.specs with parameters of type IVecInt

IConstr	ISolver.addAtLeast(IVecInt literals, int degree) Create a cardinality constraint of the type "at least n of those literals must be satisfied"
IConstr	ISolver.addAtMost(IVecInt literals, int degree) Create a cardinality constraint of the type "at most n of those literals must be satisfied"
IConstr	ISolver.addClause(IVecInt literals) Create a clause from a set of literals The literals are represented by non null integers such that opposite literals a represented by opposite values.
IConstr	ISolver.addPseudoBoolean(IVecInt lits, IVec<java.math.BigInteger> coeffs, boolean moreThan, java.math.BigInteger d) Create a Pseudo-Boolean constraint of the type "at least n of those literals must be satisfied"
void	IVecInt.copyTo(IVecInt copy) C'est operations devraient se faire en temps constant.
int[]	IProblem.findModel(IVecInt assumps) Look for a model satisfying all the clauses available in the problem.
boolean	IProblem.isSatisfiable(IVecInt assumps) Check the satisfiability of the set of constraints contained inside the solver.
void	IVecInt.moveTo(IVecInt dest)
void	IVecInt.moveTo2(IVecInt dest)

Method parameters in org.sat4j.specs with type arguments of type IVecInt

void	ISolver.addAllClauses(IVec<IVecInt> clauses) Create clauses from a set of set of literals.

Uses of IVecInt in org.sat4j.tools

Methods in org.sat4j.tools that return IVecInt

static IVecInt

RemiUtils.backbone(ISolver s) Compute the set of literals common to all models of the formula.

Methods in org.sat4j.tools with parameters of type IVecInt

IConstr	DimacsOutputSolver.addAtLeast(IVecInt literals, int degree)
IConstr	SolverDecorator.addAtLeast(IVecInt literals, int degree)
IConstr	DimacsOutputSolver.addAtMost(IVecInt literals, int degree)
IConstr	SolverDecorator.addAtMost(IVecInt literals, int degree)
IConstr	DimacsOutputSolver.addClause(IVecInt literals)
IConstr	SolverDecorator.addClause(IVecInt literals)
IConstr	DimacsOutputSolver.addPseudoBoolean(IVecInt lits, IVec<java.math.BigInteger> coeffs, boolean moreThan, java.math.BigInteger d)
IConstr	SolverDecorator.addPseudoBoolean(IVecInt literals, IVec<java.math.BigInteger> coeffs, boolean moreThan, java.math.BigInteger degree)
void	GateTranslator.and(int y, IVecInt literals) Translate y <=> x1 /\ x2 /\ ... /\ xn into clauses.
int[]	DimacsOutputSolver.findModel(IVecInt assumps)
int[]	SolverDecorator.findModel(IVecInt assumps)
boolean	SingleSolutionDetector.hasASingleSolution(IVecInt assumptions) Please use that method only after a positive answer from isSatisfiable(assumptions) (else a runtime exception will be launched).
void	GateTranslator.iff(int y, IVecInt literals) translate y <=> (x1 <=> x2 <=> ... <=> xn) into clauses.
boolean	ModelIterator.isSatisfiable(IVecInt assumps)
boolean	DimacsOutputSolver.isSatisfiable(IVecInt assumps)
boolean	SolverDecorator.isSatisfiable(IVecInt assumps)
void	GateTranslator.or(int y, IVecInt literals) translate y <=> x1 \/ x2 \/ ... \/ xn into clauses.
void	GateTranslator.xor(int y, IVecInt literals) translate y <=> x1 xor x2 xor ... xor xn into clauses.

Method parameters in org.sat4j.tools with type arguments of type IVecInt

void	DimacsOutputSolver.addAllClauses(IVec<IVecInt> clauses)
void	SolverDecorator.addAllClauses(IVec<IVecInt> clauses)