|
||||||||||
PREV NEXT | FRAMES NO FRAMES |
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.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. |
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.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.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.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)
|
|
||||||||||
PREV NEXT | FRAMES NO FRAMES |