Uses of Interface
org.sat4j.specs.IVecInt

Packages that use IVecInt

Package	Description
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 constraints.
org.sat4j.minisat.constraints.cnf	Implementations of clausal constraints.
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 intended for users dealing with SAT solvers as black boxes.
org.sat4j.tools	Tools to be used on top of an ISolver.
org.sat4j.tools.encoding	Implementation of different encodings.
org.sat4j.tools.xplain	Implementation of an explanation engine in case of unsatisfiability.

Uses of IVecInt in org.sat4j.core

Classes in org.sat4j.core that implement IVecInt

Modifier and Type	Class and Description
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

Modifier and Type	Field and Description
static IVecInt	VecInt.EMPTY

Methods in org.sat4j.core that return IVecInt

Modifier and Type	Method and Description
IVecInt	ReadOnlyVecInt.pop()
IVecInt	VecInt.pop() depile le dernier element du vecteur.
IVecInt	ReadOnlyVecInt.push(int elem)
IVecInt	VecInt.push(int elem)
IVecInt[]	VecInt.subset(int cardinal)

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

Modifier and Type	Method and Description
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

Constructor and Description
ReadOnlyVecInt(IVecInt vec)

Uses of IVecInt in org.sat4j.minisat.constraints

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

Modifier and Type	Method and Description
Constr	AbstractDataStructureFactory.createCardinalityConstraint(IVecInt literals, int degree)
Constr	MixedDataStructureSingleWL.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	MixedDataStructureSingleWL.createClause(IVecInt literals)
Constr	CardinalityDataStructure.createClause(IVecInt literals)
Constr	MixedDataStructureDanielHT.createClause(IVecInt literals)
Constr	MixedDataStructureDanielWL.createClause(IVecInt literals)
Constr	CardinalityDataStructureYanMin.createClause(IVecInt literals)
Constr	CardinalityDataStructureYanMax.createClause(IVecInt literals)
Constr	AbstractDataStructureFactory.createUnregisteredCardinalityConstraint(IVecInt literals, int degree)
Constr	MixedDataStructureSingleWL.createUnregisteredCardinalityConstraint(IVecInt literals, int degree)
Constr	CardinalityDataStructure.createUnregisteredCardinalityConstraint(IVecInt literals, int degree)
Constr	MixedDataStructureDanielHT.createUnregisteredCardinalityConstraint(IVecInt literals, int degree)
Constr	MixedDataStructureDanielWL.createUnregisteredCardinalityConstraint(IVecInt literals, int degree)
Constr	CardinalityDataStructureYanMin.createUnregisteredCardinalityConstraint(IVecInt literals, int degree)
Constr	CardinalityDataStructureYanMax.createUnregisteredCardinalityConstraint(IVecInt literals, int degree)
Constr	ClausalDataStructureWL.createUnregisteredClause(IVecInt literals)
Constr	MixedDataStructureSingleWL.createUnregisteredClause(IVecInt literals)
Constr	CardinalityDataStructure.createUnregisteredClause(IVecInt literals)
Constr	MixedDataStructureDanielHT.createUnregisteredClause(IVecInt literals)
Constr	MixedDataStructureDanielWL.createUnregisteredClause(IVecInt literals)
Constr	CardinalityDataStructureYanMin.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

Modifier and Type	Method and Description
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
void	MaxWatchCard.calcReasonOnTheFly(int p, IVecInt trail, IVecInt outReason)
void	AtLeast.calcReasonOnTheFly(int p, IVecInt trail, IVecInt outReason)
void	MinWatchCard.calcReasonOnTheFly(int p, IVecInt trail, IVecInt outReason)
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 IVecInt

Constructor and Description
AtLeast(ILits voc, IVecInt ps, int degree)
MaxWatchCard(ILits voc, IVecInt ps, boolean moreThan, int degree) Constructeur de base cr?
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

Modifier and Type

Method and Description

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

Modifier and Type	Method and Description
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.
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)
void	HTClause.calcReasonOnTheFly(int p, IVecInt trail, IVecInt outReason)
void	UnitClause.calcReasonOnTheFly(int p, IVecInt trail, IVecInt outReason)
void	UnitClauses.calcReasonOnTheFly(int p, IVecInt trail, IVecInt outReason)
void	WLClause.calcReasonOnTheFly(int p, IVecInt trail, IVecInt outReason)
void	BinaryClause.calcReasonOnTheFly(int p, IVecInt trail, 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

Constructor and Description
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)
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

Modifier and Type	Field and Description
protected IVecInt	Solver.trail variable assignments (literals) in chronological order.
protected IVecInt	Solver.trailLim position of the decision levels on the trail.

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

Modifier and Type	Method and Description
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

Modifier and Type	Method and Description
IConstr	Solver.addAtLeast(IVecInt literals, int degree)
IConstr	Solver.addAtMost(IVecInt literals, int degree)
IConstr	Solver.addBlockingClause(IVecInt literals)
IConstr	Solver.addClause(IVecInt literals)
IConstr	Solver.addExactly(IVecInt literals, int n)
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.
void	Constr.calcReasonOnTheFly(int p, IVecInt trail, IVecInt outReason) Compute the reason for a given assignment in a the constraint created on the fly in the solver.
Constr	DataStructureFactory.createCardinalityConstraint(IVecInt literals, int degree) Create a cardinality constraint of the form sum li >= degree.
Constr	DataStructureFactory.createClause(IVecInt literals)
Constr	DataStructureFactory.createUnregisteredCardinalityConstraint(IVecInt literals, int degree)
Constr	DataStructureFactory.createUnregisteredClause(IVecInt literals)
protected IVecInt	Solver.dimacs2internal(IVecInt in)
int[]	Solver.findModel(IVecInt assumps)
protected Set<Integer>	Solver.fromLastDecisionLevel(IVecInt lits)
boolean	Solver.isSatisfiable(IVecInt assumps)
boolean	Solver.isSatisfiable(IVecInt assumps, boolean global)
void	ISimplifier.simplify(IVecInt outLearnt)

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

Modifier and Type	Method and Description
void	Solver.addAllClauses(IVec<IVecInt> clauses)

Uses of IVecInt in org.sat4j.opt

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

Modifier and Type	Method and Description
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.reader

Fields in org.sat4j.reader declared as IVecInt

Modifier and Type	Field and Description
protected IVecInt	DimacsReader.literals

Methods in org.sat4j.reader that return IVecInt

Modifier and Type	Method and Description
protected IVecInt	JSONReader.getLiterals(String constraint)

Uses of IVecInt in org.sat4j.specs

Methods in org.sat4j.specs that return IVecInt

Modifier and Type	Method and Description
IVecInt	IVecInt.pop() depile le dernier element du vecteur.
IVecInt	IVecInt.push(int elem)
IVecInt[]	IVecInt.subset(int k) Compute all subsets of cardinal k of the vector.
IVecInt	ISolver.unsatExplanation() Retrieve an explanation of the inconsistency in terms of assumption literals.

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

Modifier and Type	Method and Description
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.
IConstr	IGroupSolver.addClause(IVecInt literals, int desc)
IConstr	ISolver.addExactly(IVecInt literals, int n) Create a cardinality constraint of the type "exactly n of those literals must be satisfied".
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

Modifier and Type	Method and Description
void	ISolver.addAllClauses(IVec<IVecInt> clauses) Create clauses from a set of set of literals.

Uses of IVecInt in org.sat4j.tools

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

Modifier and Type	Field and Description
protected List<IVecInt>	LexicoDecorator.criteria

Methods in org.sat4j.tools that return IVecInt

Modifier and Type	Method and Description
static IVecInt	RemiUtils.backbone(ISolver s) Compute the set of literals common to all models of the formula.
static IVecInt	Backbone.compute(ISolver solver) Computes the backbone of a formula following the algorithm described in João Marques-Silva, Mikolás Janota, Inês Lynce: On Computing Backbones of Propositional Theories.
static IVecInt	Backbone.compute(ISolver solver, int[] implicant)
static IVecInt	Backbone.compute(ISolver solver, int[] implicant, IVecInt assumptions)
static IVecInt	Backbone.compute(ISolver solver, IVecInt assumptions) Computes the backbone of a formula following the algorithm described in João Marques-Silva, Mikolás Janota, Inês Lynce: On Computing Backbones of Propositional Theories.
IVecInt	FullClauseSelectorSolver.getLastClause()
static IVecInt	AbstractMinimalModel.negativeLiterals(ISolver solver)
static IVecInt	AbstractMinimalModel.positiveLiterals(ISolver solver)
IVecInt	AbstractOutputSolver.unsatExplanation()
IVecInt	ManyCore.unsatExplanation()
IVecInt	StatisticsSolver.unsatExplanation()
IVecInt	SolverDecorator.unsatExplanation()

Methods in org.sat4j.tools that return types with arguments of type IVecInt

Modifier and Type	Method and Description
List<IVecInt>	AllMUSes.computeAllMSS()
List<IVecInt>	AllMUSes.computeAllMSS(SolutionFoundListener listener)
List<IVecInt>	AllMUSes.computeAllMSSOrdered(SolutionFoundListener listener)
List<IVecInt>	AllMUSes.computeAllMUSes()
List<IVecInt>	AllMUSes.computeAllMUSes(SolutionFoundListener listener) Computes all the MUSes associated to the set of constraints added to the solver
List<IVecInt>	AllMUSes.computeAllMUSesOrdered(SolutionFoundListener listener)
List<IVecInt>	AllMUSes.getMssList()

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

Modifier and Type	Method and Description
IConstr	NegationDecorator.addAtLeast(IVecInt literals, int degree)
IConstr	ManyCore.addAtLeast(IVecInt literals, int degree)
IConstr	ClausalCardinalitiesDecorator.addAtLeast(IVecInt literals, int k)
IConstr	DimacsOutputSolver.addAtLeast(IVecInt literals, int degree)
IConstr	StatisticsSolver.addAtLeast(IVecInt literals, int degree)
IConstr	DimacsStringSolver.addAtLeast(IVecInt literals, int degree)
IConstr	SolverDecorator.addAtLeast(IVecInt literals, int degree)
IConstr	NegationDecorator.addAtMost(IVecInt literals, int degree)
IConstr	ManyCore.addAtMost(IVecInt literals, int degree)
IConstr	ClausalCardinalitiesDecorator.addAtMost(IVecInt literals, int k)
IConstr	DimacsOutputSolver.addAtMost(IVecInt literals, int degree)
IConstr	StatisticsSolver.addAtMost(IVecInt literals, int degree)
IConstr	DimacsStringSolver.addAtMost(IVecInt literals, int degree)
IConstr	SolverDecorator.addAtMost(IVecInt literals, int degree)
IConstr	AbstractOutputSolver.addBlockingClause(IVecInt literals)
IConstr	ManyCore.addBlockingClause(IVecInt literals)
IConstr	StatisticsSolver.addBlockingClause(IVecInt literals)
IConstr	SolverDecorator.addBlockingClause(IVecInt literals)
IConstr	NegationDecorator.addClause(IVecInt literals)
IConstr	ManyCore.addClause(IVecInt literals)
IConstr	FullClauseSelectorSolver.addClause(IVecInt literals)
IConstr	DimacsOutputSolver.addClause(IVecInt literals)
IConstr	StatisticsSolver.addClause(IVecInt literals)
IConstr	DimacsStringSolver.addClause(IVecInt literals)
IConstr	SolverDecorator.addClause(IVecInt literals)
IConstr	GroupClauseSelectorSolver.addClause(IVecInt literals, int desc)
IConstr	FullClauseSelectorSolver.addControlableClause(IVecInt literals)
IConstr	GroupClauseSelectorSolver.addControlableClause(IVecInt literals, int desc)
void	LexicoDecorator.addCriterion(IVecInt literals)
IConstr	NegationDecorator.addExactly(IVecInt literals, int n)
IConstr	ManyCore.addExactly(IVecInt literals, int n)
IConstr	ClausalCardinalitiesDecorator.addExactly(IVecInt literals, int k)
IConstr	DimacsOutputSolver.addExactly(IVecInt literals, int n)
IConstr	StatisticsSolver.addExactly(IVecInt literals, int n)
IConstr	DimacsStringSolver.addExactly(IVecInt literals, int n)
IConstr	SolverDecorator.addExactly(IVecInt literals, int n)
IConstr	FullClauseSelectorSolver.addNonControlableClause(IVecInt literals)
IConstr	GroupClauseSelectorSolver.addNonControlableClause(IVecInt literals)
void	CheckMUSSolutionListener.addOriginalClause(IVecInt clause)
boolean	LexicoDecorator.admitABetterSolution(IVecInt assumps)
IConstr[]	GateTranslator.and(int y, IVecInt literals) Translate y <=> x1 /\ x2 /\ ... /\ xn into clauses.
boolean	CheckMUSSolutionListener.checkThatItIsAMUS(IVecInt mus)
static IVecInt	Backbone.compute(ISolver solver, int[] implicant, IVecInt assumptions)
static IVecInt	Backbone.compute(ISolver solver, IVecInt assumptions) Computes the backbone of a formula following the algorithm described in João Marques-Silva, Mikolás Janota, Inês Lynce: On Computing Backbones of Propositional Theories.
protected int	AbstractClauseSelectorSolver.createNewVar(IVecInt literals)
int[]	AbstractOutputSolver.findModel(IVecInt assumps)
int[]	ManyCore.findModel(IVecInt assumps)
int[]	OptToSatAdapter.findModel(IVecInt assumps)
int[]	StatisticsSolver.findModel(IVecInt assumps)
int[]	SolverDecorator.findModel(IVecInt assumps)
IConstr[]	GateTranslator.halfOr(int y, IVecInt literals) translate y <= x1 \/ x2 \/ ... \/ xn into clauses.
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	AbstractClauseSelectorSolver.isSatisfiable(IVecInt assumps)
boolean	AbstractOutputSolver.isSatisfiable(IVecInt assumps)
boolean	ModelIteratorToSATAdapter.isSatisfiable(IVecInt assumps)
boolean	ManyCore.isSatisfiable(IVecInt assumps)
boolean	OptToSatAdapter.isSatisfiable(IVecInt myAssumps)
boolean	StatisticsSolver.isSatisfiable(IVecInt assumps)
boolean	ModelIterator.isSatisfiable(IVecInt assumps)
boolean	SolverDecorator.isSatisfiable(IVecInt assumps)
boolean	AbstractClauseSelectorSolver.isSatisfiable(IVecInt assumps, boolean global)
boolean	AbstractOutputSolver.isSatisfiable(IVecInt assumps, boolean global)
boolean	NegationDecorator.isSatisfiable(IVecInt assumps, boolean global)
boolean	ManyCore.isSatisfiable(IVecInt assumps, boolean globalTimeout)
boolean	OptToSatAdapter.isSatisfiable(IVecInt myAssumps, boolean global)
boolean	StatisticsSolver.isSatisfiable(IVecInt assumps, boolean globalTimeout)
boolean	SolverDecorator.isSatisfiable(IVecInt assumps, boolean global)
void	CheckMUSSolutionListener.onSolutionFound(IVecInt solution)
void	SolutionFoundListener.onSolutionFound(IVecInt solution) Callback method called when a new solution is found.
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

Modifier and Type	Method and Description
void	AbstractOutputSolver.addAllClauses(IVec<IVecInt> clauses)
void	ManyCore.addAllClauses(IVec<IVecInt> clauses)
void	StatisticsSolver.addAllClauses(IVec<IVecInt> clauses)
void	SolverDecorator.addAllClauses(IVec<IVecInt> clauses)

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

Constructor and Description
AbstractMinimalModel(ISolver solver, IVecInt p)
AbstractMinimalModel(ISolver solver, IVecInt p, SolutionFoundListener modelListener)
Minimal4CardinalityModel(ISolver solver, IVecInt p)
Minimal4CardinalityModel(ISolver solver, IVecInt p, SolutionFoundListener modelListener)
Minimal4InclusionModel(ISolver solver, IVecInt p)
Minimal4InclusionModel(ISolver solver, IVecInt p, SolutionFoundListener modelListener)

Uses of IVecInt in org.sat4j.tools.encoding

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

Modifier and Type	Method and Description
IConstr	Policy.addAtLeast(ISolver solver, IVecInt literals, int n)
IConstr	EncodingStrategyAdapter.addAtLeast(ISolver solver, IVecInt literals, int degree)
IConstr	EncodingStrategyAdapter.addAtLeastOne(ISolver solver, IVecInt literals)
IConstr	Sequential.addAtMost(ISolver solver, IVecInt literals, int k) This encoding adds (n-1)*k variables (n is the number of variables in the at most constraint and k is the degree of the constraint) and 2nk+n-3k-1 clauses.
IConstr	Policy.addAtMost(ISolver solver, IVecInt literals, int k)
IConstr	EncodingStrategyAdapter.addAtMost(ISolver solver, IVecInt literals, int degree)
IConstr	Product.addAtMost(ISolver solver, IVecInt literals, int k)
IConstr	Commander.addAtMost(ISolver solver, IVecInt literals, int degree)
IConstr	Binary.addAtMost(ISolver solver, IVecInt literals, int k)
IConstr	Binomial.addAtMost(ISolver solver, IVecInt literals, int degree)
IConstr	Product.addAtMostNonOpt(ISolver solver, IVecInt literals, int k)
IConstr	Sequential.addAtMostOne(ISolver solver, IVecInt literals)
IConstr	Ladder.addAtMostOne(ISolver solver, IVecInt literals)
IConstr	EncodingStrategyAdapter.addAtMostOne(ISolver solver, IVecInt literals)
IConstr	Product.addAtMostOne(ISolver solver, IVecInt literals)
IConstr	Commander.addAtMostOne(ISolver solver, IVecInt literals) In this encoding, variables are partitioned in groups.
IConstr	Binary.addAtMostOne(ISolver solver, IVecInt literals) p being the smaller integer greater than log_2(n), this encoding adds p variables and n*p clauses.
IConstr	Binomial.addAtMostOne(ISolver solver, IVecInt literals)
IConstr	Sequential.addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	Policy.addExactly(ISolver solver, IVecInt literals, int n)
IConstr	EncodingStrategyAdapter.addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	Product.addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	Commander.addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	Binary.addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	Binomial.addExactly(ISolver solver, IVecInt literals, int degree)
IConstr	Sequential.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	Ladder.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	EncodingStrategyAdapter.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	Product.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	Commander.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	Binary.addExactlyOne(ISolver solver, IVecInt literals)
IConstr	Binomial.addExactlyOne(ISolver solver, IVecInt literals)

Uses of IVecInt in org.sat4j.tools.xplain

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

Modifier and Type	Method and Description
IVecInt	QuickXplainStrategy.explain(ISolver solver, Map<Integer,?> constrs, IVecInt assumps)
IVecInt	QuickXplain2001Strategy.explain(ISolver solver, Map<Integer,?> constrs, IVecInt assumps)
IVecInt	MinimizationStrategy.explain(ISolver solver, Map<Integer,?> constrs, IVecInt assumps)
IVecInt	DeletionStrategy.explain(ISolver solver, Map<Integer,?> constrs, IVecInt assumps)
IVecInt	InsertionStrategy.explain(ISolver solver, Map<Integer,?> constrs, IVecInt assumps)

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

Modifier and Type	Method and Description
IConstr	Xplain.addAtLeast(IVecInt literals, int degree)
IConstr	HighLevelXplain.addAtLeast(IVecInt literals, int degree)
IConstr	Xplain.addAtMost(IVecInt literals, int degree)
IConstr	HighLevelXplain.addAtMost(IVecInt literals, int degree)
IConstr	Xplain.addExactly(IVecInt literals, int n)
IVecInt	QuickXplainStrategy.explain(ISolver solver, Map<Integer,?> constrs, IVecInt assumps)
IVecInt	QuickXplain2001Strategy.explain(ISolver solver, Map<Integer,?> constrs, IVecInt assumps)
IVecInt	MinimizationStrategy.explain(ISolver solver, Map<Integer,?> constrs, IVecInt assumps)
IVecInt	DeletionStrategy.explain(ISolver solver, Map<Integer,?> constrs, IVecInt assumps)
IVecInt	InsertionStrategy.explain(ISolver solver, Map<Integer,?> constrs, IVecInt assumps)
int[]	Xplain.findModel(IVecInt assumps)
int[]	HighLevelXplain.findModel(IVecInt assumps)
boolean	Xplain.isSatisfiable(IVecInt assumps)
boolean	HighLevelXplain.isSatisfiable(IVecInt assumps)
boolean	Xplain.isSatisfiable(IVecInt assumps, boolean global)
boolean	HighLevelXplain.isSatisfiable(IVecInt assumps, boolean global)