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.maxsat	MAXSAT and Weighted Max SAT framework.
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.multicore
org.sat4j.opt	Built-in optimization framework.
org.sat4j.pb
org.sat4j.pb.constraints
org.sat4j.pb.constraints.pb	Implementations of pseudo boolean contraints.
org.sat4j.pb.core
org.sat4j.pb.reader
org.sat4j.pb.tools
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.
org.sat4j.tools.xplain

Uses of IVecInt in org.sat4j.core

Classes in org.sat4j.core that implement IVecInt

class	ReadOnlyVecInt Utility class to allow Read Only access only to an 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	ReadOnlyVecInt.pop()
IVecInt	VecInt.pop() depile le dernier element du vecteur.
IVecInt	ReadOnlyVecInt.push(int elem)
IVecInt	VecInt.push(int elem)

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

void	ReadOnlyVecInt.copyTo(IVecInt copy)
void	VecInt.copyTo(IVecInt copy) Copy the content of this vector into another one.
void	ReadOnlyVecInt.moveTo(IVecInt dest)
void	VecInt.moveTo(IVecInt dest)
void	ReadOnlyVecInt.moveTo2(IVecInt dest)
void	VecInt.moveTo2(IVecInt dest)
void	VecInt.pushAll(IVecInt vec)

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

ReadOnlyVecInt(IVecInt vec)

Uses of IVecInt in org.sat4j.maxsat

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

IConstr	WeightedMaxSatDecorator.addClause(IVecInt literals) Add a set of literals to the solver.
IConstr	WeightedMaxSatDecorator.addHardClause(IVecInt literals) Add a hard clause in the solver, i.e. a clause that must be satisfied.
void	WeightedMaxSatDecorator.addLiteralsToMinimize(IVecInt literals) Set some literals whose sum must be minimized.
IConstr	WeightedMaxSatDecorator.addSoftClause(BigInteger weight, IVecInt literals)
IConstr	WeightedMaxSatDecorator.addSoftClause(int weight, IVecInt literals) Add a soft clause to the solver.
IConstr	WeightedMaxSatDecorator.addSoftClause(IVecInt literals) Add a soft clause in the solver, i.e. a clause with a weight of 1.
void	WeightedMaxSatDecorator.addWeightedLiteralsToMinimize(IVecInt literals, IVec<BigInteger> coefficients) Set some literals whose sum must be minimized.
void	WeightedMaxSatDecorator.addWeightedLiteralsToMinimize(IVecInt literals, IVecInt coefficients) Set some literals whose sum must be minimized.
boolean	WeightedMaxSatDecorator.admitABetterSolution(IVecInt assumps)
boolean	MinCostDecorator.admitABetterSolution(IVecInt assumps)

Uses of IVecInt in org.sat4j.minisat.constraints

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

Constr	AbstractDataStructureFactory.createCardinalityConstraint(IVecInt literals, int degree)
Constr	CardinalityDataStructure.createCardinalityConstraint(IVecInt literals, int degree)
Constr	MixedDataStructureDanielHT.createCardinalityConstraint(IVecInt literals, int degree)
Constr	MixedDataStructureDanielWL.createCardinalityConstraint(IVecInt literals, int degree)
Constr	CardinalityDataStructureYanMin.createCardinalityConstraint(IVecInt literals, int degree)
Constr	CardinalityDataStructureYanMax.createCardinalityConstraint(IVecInt literals, int degree)
Constr	ClausalDataStructureWL.createClause(IVecInt literals)
Constr	ClausalDataStructureCB.createClause(IVecInt literals)
Constr	CardinalityDataStructure.createClause(IVecInt literals)
Constr	MixedDataStructureDanielHT.createClause(IVecInt literals)
Constr	MixedDataStructureDanielWL.createClause(IVecInt literals)
Constr	MixedDataStructureDanielCBWL.createClause(IVecInt literals)
Constr	CardinalityDataStructureYanMin.createClause(IVecInt literals)
Constr	ClausalDataStructureCBWL.createClause(IVecInt literals)
Constr	CardinalityDataStructureYanMax.createClause(IVecInt literals)
Constr	ClausalDataStructureWL.createUnregisteredClause(IVecInt literals)
Constr	ClausalDataStructureCB.createUnregisteredClause(IVecInt literals)
Constr	CardinalityDataStructure.createUnregisteredClause(IVecInt literals)
Constr	MixedDataStructureDanielHT.createUnregisteredClause(IVecInt literals)
Constr	MixedDataStructureDanielWL.createUnregisteredClause(IVecInt literals)
Constr	CardinalityDataStructureYanMin.createUnregisteredClause(IVecInt literals)
Constr	ClausalDataStructureCBWL.createUnregisteredClause(IVecInt literals)
Constr	CardinalityDataStructureYanMax.createUnregisteredClause(IVecInt literals)

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

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

static Constr	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	AtLeast.calcReason(int p, IVecInt outReason)
void	MinWatchCard.calcReason(int p, IVecInt outReason) computes the reason for a literal
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

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

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

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.
void	CBClause.calcReason(int p, IVecInt outReason)
void	HTClause.calcReason(int p, IVecInt outReason)
void	UnitClause.calcReason(int p, IVecInt outReason)
void	UnitClauses.calcReason(int p, IVecInt outReason)
void	WLClause.calcReason(int p, IVecInt outReason)
void	BinaryClause.calcReason(int p, IVecInt outReason)
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 IVecInt

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)

UnitClauses(IVecInt values)

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

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

IVecInt	Solver.analyzeFinalConflictInTermsOfAssumptions(Constr confl, IVecInt assumps, int conflictingLiteral) Derive a subset of the assumptions causing the inconistency.
protected IVecInt	Solver.dimacs2internal(IVecInt in)
IVecInt	Solver.getOutLearnt()
IVecInt	Solver.unsatExplanation()

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.addBlockingClause(IVecInt literals)
IConstr	Solver.addClause(IVecInt literals)
IVecInt	Solver.analyzeFinalConflictInTermsOfAssumptions(Constr confl, IVecInt assumps, int conflictingLiteral) Derive a subset of the assumptions causing the inconistency.
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.createUnregisteredClause(IVecInt literals)
protected IVecInt	Solver.dimacs2internal(IVecInt in)
int[]	Solver.findModel(IVecInt assumps)
boolean	Solver.isSatisfiable(IVecInt assumps)
boolean	Solver.isSatisfiable(IVecInt assumps, boolean global)

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

Methods in org.sat4j.multicore that return IVecInt

IVecInt

ManyCore.unsatExplanation()

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

IConstr	ManyCore.addAtLeast(IVecInt literals, int degree)
IConstr	ManyCore.addAtMost(IVecInt literals, int degree)
IConstr	ManyCore.addBlockingClause(IVecInt literals)
IConstr	ManyCore.addClause(IVecInt literals)
IConstr	ManyCorePB.addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d)
int[]	ManyCore.findModel(IVecInt assumps)
boolean	ManyCore.isSatisfiable(IVecInt assumps)
boolean	ManyCore.isSatisfiable(IVecInt assumps, boolean globalTimeout)

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

void	ManyCore.addAllClauses(IVec<IVecInt> clauses)

Uses of IVecInt in org.sat4j.opt

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

IConstr	MaxSatDecorator.addClause(IVecInt literals)
boolean	AbstractSelectorVariablesDecorator.admitABetterSolution(IVecInt assumps)
boolean	MaxSatDecorator.admitABetterSolution(IVecInt assumps)
boolean	MinOneDecorator.admitABetterSolution(IVecInt assumps)

Uses of IVecInt in org.sat4j.pb

Methods in org.sat4j.pb that return IVecInt

IVecInt

ObjectiveFunction.getVars()

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

IConstr	UserFriendlyPBStringSolver.addAtLeast(IVecInt literals, int degree)
IConstr	OPBStringSolver.addAtLeast(IVecInt literals, int degree)
IConstr	UserFriendlyPBStringSolver.addAtMost(IVecInt literals, int degree)
IConstr	OPBStringSolver.addAtMost(IVecInt literals, int degree)
IConstr	UserFriendlyPBStringSolver.addClause(IVecInt literals)
IConstr	OPBStringSolver.addClause(IVecInt literals)
IConstr	IPBSolver.addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d) Create a Pseudo-Boolean constraint of the type "at least n of those literals must be satisfied"
IConstr	UserFriendlyPBStringSolver.addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d)
IConstr	PBSolverDecorator.addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d)
IConstr	OPBStringSolver.addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d)
boolean	PseudoOptDecorator.admitABetterSolution(IVecInt assumps)
boolean	PseudoOptDecorator.isSatisfiable(IVecInt assumps)
boolean	OptToPBSATAdapter.isSatisfiable(IVecInt myAssumps)
boolean	OPBStringSolver.isSatisfiable(IVecInt assumps)
boolean	PseudoOptDecorator.isSatisfiable(IVecInt assumps, boolean global)
boolean	OptToPBSATAdapter.isSatisfiable(IVecInt myAssumps, boolean global)
boolean	OPBStringSolver.isSatisfiable(IVecInt assumps, boolean global)
void	UserFriendlyPBStringSolver.setListOfVariablesForExplanation(IVecInt listOfVariables)
void	OPBStringSolver.setListOfVariablesForExplanation(IVecInt listOfVariables)

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

ObjectiveFunction(IVecInt vars, IVec<BigInteger> coeffs)

Uses of IVecInt in org.sat4j.pb.constraints

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

protected Constr	CompetResolutionPBMixedHTClauseCardConstrDataStructure.constructCard(IVecInt theLits, int degree)
protected PBConstr	PBMaxClauseAtLeastConstrDataStructure.constructCard(IVecInt theLits, int degree)
protected abstract Constr	AbstractPBClauseCardConstrDataStructure.constructCard(IVecInt theLits, int degree)
protected Constr	CompetResolutionPBMixedWLClauseCardConstrDataStructure.constructCard(IVecInt theLits, int degree)
protected Constr	CompetMinHTmixedClauseCardConstrDataStructureFactory.constructCard(IVecInt theLits, int degree)
protected PBConstr	PuebloPBMinClauseAtLeastConstrDataStructure.constructCard(IVecInt theLits, int degree)
protected Constr	PuebloPBMinClauseCardConstrDataStructure.constructCard(IVecInt theLits, int degree)
protected Constr	CompetResolutionPBMixedHTClauseCardConstrDataStructure.constructClause(IVecInt v)
protected abstract Constr	AbstractPBClauseCardConstrDataStructure.constructClause(IVecInt v)
protected Constr	CompetResolutionPBMixedWLClauseCardConstrDataStructure.constructClause(IVecInt v)
protected Constr	CompetMinHTmixedClauseCardConstrDataStructureFactory.constructClause(IVecInt v)
protected Constr	PuebloPBMinClauseCardConstrDataStructure.constructClause(IVecInt v)
protected PBConstr	PBMaxCBClauseCardConstrDataStructure.constructClause(IVecInt v)
protected Constr	CompetResolutionPBMixedHTClauseCardConstrDataStructure.constructLearntClause(IVecInt resLits)
protected abstract Constr	AbstractPBClauseCardConstrDataStructure.constructLearntClause(IVecInt literals)
protected Constr	CompetResolutionPBMixedWLClauseCardConstrDataStructure.constructLearntClause(IVecInt resLits)
protected Constr	CompetMinHTmixedClauseCardConstrDataStructureFactory.constructLearntClause(IVecInt resLits)
protected Constr	PuebloPBMinClauseCardConstrDataStructure.constructLearntClause(IVecInt literals)
Constr	AbstractPBDataStructureFactory.createCardinalityConstraint(IVecInt literals, int degree)
Constr	CompetResolutionPBMixedHTClauseCardConstrDataStructure.createClause(IVecInt literals)
Constr	AbstractPBDataStructureFactory.createClause(IVecInt literals)
Constr	CompetResolutionPBMixedWLClauseCardConstrDataStructure.createClause(IVecInt literals)
Constr	PuebloPBMinClauseCardConstrDataStructure.createClause(IVecInt literals)
Constr	AbstractPBDataStructureFactory.createPseudoBooleanConstraint(IVecInt literals, IVec<BigInteger> coefs, boolean moreThan, BigInteger degree)
Constr	AbstractPBDataStructureFactory.createUnregisteredClause(IVecInt literals)

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

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

IVecInt	MinWatchCardPB.computeAnImpliedClause()
IVecInt	AtLeastPB.computeAnImpliedClause()
IVecInt	WatchPb.computeAnImpliedClause() compute an implied clause on the literals with the greater coefficients.
IVecInt	OriginalBinaryClausePB.computeAnImpliedClause()
IVecInt	PBConstr.computeAnImpliedClause()
IVecInt	LearntBinaryClausePB.computeAnImpliedClause()
IVecInt	MixableCBClausePB.computeAnImpliedClause()
IVecInt	OriginalHTClausePB.computeAnImpliedClause()
IVecInt	LearntHTClausePB.computeAnImpliedClause()
IVecInt	UnitClausePB.computeAnImpliedClause()

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

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.
void	MapPb.buildConstraintFromConflict(IVecInt resLits, IVec<BigInteger> resCoefs)
void	IDataStructurePB.buildConstraintFromConflict(IVecInt resLits, IVec<BigInteger> resCoefs)
void	WatchPb.calcReason(int p, IVecInt outReason) compute the reason for the assignment of a literal
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 MinWatchCardPB	MinWatchCardPB.normalizedMinWatchCardPBNew(UnitPropagationListener s, ILits voc, IVecInt ps, int degree) Permet la cr?
static IVec<BigInteger>	Pseudos.toVecBigInt(IVecInt vec)

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

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)

MixableCBClausePB(IVecInt ps, ILits voc)

MixableCBClausePB(IVecInt ps, ILits voc, boolean learnt)

OriginalBinaryClausePB(IVecInt ps, ILits voc)

OriginalHTClausePB(IVecInt ps, ILits voc)

Uses of IVecInt in org.sat4j.pb.core

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

IConstr	PBSolver.addPseudoBoolean(IVecInt literals, IVec<BigInteger> coeffs, boolean moreThan, BigInteger degree)
IConstr	PBSolverWithImpliedClause.addPseudoBoolean(IVecInt literals, IVec<BigInteger> coeffs, boolean moreThan, BigInteger degree)
Constr	PBDataStructureFactory.createPseudoBooleanConstraint(IVecInt literals, IVec<BigInteger> coefs, boolean moreThan, BigInteger degree)

Uses of IVecInt in org.sat4j.pb.reader

Fields in org.sat4j.pb.reader declared as IVecInt

protected IVecInt

OPBReader2005.lits

Methods in org.sat4j.pb.reader that return IVecInt

IVecInt	OPBReader2005.getListOfVariables()
IVecInt	OPBEclipseReader2007.getListOfVariables()
IVecInt	OPBReader2005.getVars()

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

protected void	OPBReader2007.literalInAProduct(String var, IVecInt lits) callback called when we read a term of a constraint
protected void	OPBReader2007.negateLiteralInAProduct(String var, IVecInt lits) callback called when we read a term of a constraint

Uses of IVecInt in org.sat4j.pb.tools

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

IConstr	XplainPB.addAtLeast(IVecInt literals, int degree)
IConstr	XplainPB.addAtMost(IVecInt literals, int degree)
IConstr	XplainPB.addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs, boolean moreThan, BigInteger d)

Constructors in org.sat4j.pb.tools with parameters of type IVecInt

DisjunctionRHS(DependencyHelper<T,C> helper, IVecInt literals)

ImplicationAnd(DependencyHelper<T,C> helper, IVecInt clause)

ImplicationRHS(DependencyHelper<T,C> helper, IVecInt clause)

Uses of IVecInt in org.sat4j.reader

Fields in org.sat4j.reader declared as IVecInt

protected IVecInt

DimacsReader.literals

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)
IVecInt	ISolver.unsatExplanation() Retrieve an explanation of the inconsistency in terms of assumption literals.

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.addBlockingClause(IVecInt literals) Add a clause in order to prevent an assignment to occur.
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.
boolean	IOptimizationProblem.admitABetterSolution(IVecInt assumps) Look for a solution of the optimization problem when some literals are 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.
boolean	IProblem.isSatisfiable(IVecInt assumps, boolean globalTimeout) 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.
IVecInt	DimacsOutputSolver.unsatExplanation()
IVecInt	DimacsStringSolver.unsatExplanation()
IVecInt	SolverDecorator.unsatExplanation()

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

IConstr	DimacsOutputSolver.addAtLeast(IVecInt literals, int degree)
IConstr	DimacsStringSolver.addAtLeast(IVecInt literals, int degree)
IConstr	SolverDecorator.addAtLeast(IVecInt literals, int degree)
IConstr	DimacsOutputSolver.addAtMost(IVecInt literals, int degree)
IConstr	DimacsStringSolver.addAtMost(IVecInt literals, int degree)
IConstr	SolverDecorator.addAtMost(IVecInt literals, int degree)
IConstr	DimacsOutputSolver.addBlockingClause(IVecInt literals)
IConstr	DimacsStringSolver.addBlockingClause(IVecInt literals)
IConstr	SolverDecorator.addBlockingClause(IVecInt literals)
IConstr	DimacsOutputSolver.addClause(IVecInt literals)
IConstr	DimacsStringSolver.addClause(IVecInt literals)
IConstr	SolverDecorator.addClause(IVecInt literals)
IConstr[]	GateTranslator.and(int y, IVecInt literals) Translate y <=> x1 /\ x2 /\ ... /\ xn into clauses.
int[]	DimacsOutputSolver.findModel(IVecInt assumps)
int[]	DimacsStringSolver.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).
IConstr[]	GateTranslator.iff(int y, IVecInt literals) translate y <=> (x1 <=> x2 <=> ... <=> xn) into clauses.
boolean	DimacsOutputSolver.isSatisfiable(IVecInt assumps)
boolean	OptToSatAdapter.isSatisfiable(IVecInt assumps)
boolean	DimacsStringSolver.isSatisfiable(IVecInt assumps)
boolean	ModelIterator.isSatisfiable(IVecInt assumps)
boolean	SolverDecorator.isSatisfiable(IVecInt assumps)
boolean	DimacsOutputSolver.isSatisfiable(IVecInt assumps, boolean global)
boolean	OptToSatAdapter.isSatisfiable(IVecInt assumps, boolean global)
boolean	DimacsStringSolver.isSatisfiable(IVecInt assumps, boolean global)
boolean	SolverDecorator.isSatisfiable(IVecInt assumps, boolean global)
void	GateTranslator.optimisationFunction(IVecInt literals, IVec<BigInteger> coefs, IVecInt result) Translate an optimization function into constraints and provides the binary literals in results.
IConstr[]	GateTranslator.or(int y, IVecInt literals) translate y <=> x1 \/ x2 \/ ... \/ xn into clauses.
IConstr[]	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	DimacsStringSolver.addAllClauses(IVec<IVecInt> clauses)
void	SolverDecorator.addAllClauses(IVec<IVecInt> clauses)

Uses of IVecInt in org.sat4j.tools.xplain

Fields in org.sat4j.tools.xplain declared as IVecInt

protected IVecInt

Xplain.assump

Methods in org.sat4j.tools.xplain that return IVecInt

IVecInt	QuickXplainStrategy.explain(ISolver solver, Map<Integer,IConstr> constrs, IVecInt assumps)
IVecInt	ReplayXplainStrategy.explain(ISolver solver, Map<Integer,IConstr> constrs, IVecInt assumps)
IVecInt	XplainStrategy.explain(ISolver solver, Map<Integer,IConstr> constrs, IVecInt assumps)

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

IConstr	Xplain.addAtLeast(IVecInt literals, int degree)
IConstr	Xplain.addAtMost(IVecInt literals, int degree)
IConstr	Xplain.addClause(IVecInt literals)
protected int	Xplain.createNewVar(IVecInt literals)
IVecInt	QuickXplainStrategy.explain(ISolver solver, Map<Integer,IConstr> constrs, IVecInt assumps)
IVecInt	ReplayXplainStrategy.explain(ISolver solver, Map<Integer,IConstr> constrs, IVecInt assumps)
IVecInt	XplainStrategy.explain(ISolver solver, Map<Integer,IConstr> constrs, IVecInt assumps)
int[]	Xplain.findModel(IVecInt assumps)
boolean	Xplain.isSatisfiable(IVecInt assumps)
boolean	Xplain.isSatisfiable(IVecInt assumps, boolean global)