A B C D E F G H I L M N O P R S T U V W X

A

AbstractPBClauseCardConstrDataStructure - Class in org.sat4j.pb.constraints
 
AbstractPBClauseCardConstrDataStructure() - Constructor for class org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure
 
AbstractPBDataStructureFactory - Class in org.sat4j.pb.constraints
 
AbstractPBDataStructureFactory() - Constructor for class org.sat4j.pb.constraints.AbstractPBDataStructureFactory
 
activity - Variable in class org.sat4j.pb.constraints.pb.WatchPb
constraint activity
addAtLeast(IVecInt, int) - Method in class org.sat4j.pb.OPBStringSolver
 
addAtLeast(IVecInt, int) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver
 
addAtMost(IVecInt, int) - Method in class org.sat4j.pb.OPBStringSolver
 
addAtMost(IVecInt, int) - Method in class org.sat4j.pb.tools.XplainPB
 
addAtMost(IVecInt, int) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver
 
addClause(IVecInt) - Method in class org.sat4j.pb.OPBStringSolver
 
addClause(IVecInt) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver
 
addPseudoBoolean(IVecInt, IVec<BigInteger>, boolean, BigInteger) - Method in class org.sat4j.pb.core.PBSolver
 
addPseudoBoolean(IVecInt, IVec<BigInteger>, boolean, BigInteger) - Method in class org.sat4j.pb.core.PBSolverWithImpliedClause
 
addPseudoBoolean(IVecInt, IVec<BigInteger>, boolean, BigInteger) - Method in interface org.sat4j.pb.IPBSolver
Create a Pseudo-Boolean constraint of the type "at least n of those literals must be satisfied"
addPseudoBoolean(IVecInt, IVec<BigInteger>, boolean, BigInteger) - Method in class org.sat4j.pb.OPBStringSolver
 
addPseudoBoolean(IVecInt, IVec<BigInteger>, boolean, BigInteger) - Method in class org.sat4j.pb.PBSolverDecorator
 
addPseudoBoolean(IVecInt, IVec<BigInteger>, boolean, BigInteger) - Method in class org.sat4j.pb.tools.XplainPB
 
addPseudoBoolean(IVecInt, IVec<BigInteger>, boolean, BigInteger) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver
 
addToObjectiveFunction(T, int) - Method in class org.sat4j.pb.tools.DependencyHelper
Add a weighted literal to the objective function.
addToObjectiveFunction(T, BigInteger) - Method in class org.sat4j.pb.tools.DependencyHelper
Add a weighted literal to the objective function.
admitABetterSolution() - Method in class org.sat4j.pb.PseudoOptDecorator
 
admitABetterSolution(IVecInt) - Method in class org.sat4j.pb.PseudoOptDecorator
 
analyze(Constr, Pair) - Method in class org.sat4j.pb.core.PBSolverCP
 
and(C, T, T...) - Method in class org.sat4j.pb.tools.DependencyHelper
Create a constraint of the form thing <=> (thing1 and thing 2 ... and thingn)
and(T) - Method in class org.sat4j.pb.tools.ImplicationAnd
Add a new positive literal to the conjunction of literals.
andNot(T) - Method in class org.sat4j.pb.tools.ImplicationAnd
Add a new negative literal to the conjunction of literals.
assertConstraint(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.AtLeastPB
 
assertConstraint(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.LearntHTClausePB
 
assertConstraint(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.MinWatchCardPB
 
assertConstraint(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.MixableCBClausePB
 
assertConstraint(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.WatchPb
 
assertiveLiteral - Variable in class org.sat4j.pb.constraints.pb.MapPb
 
ATLEAST - Static variable in class org.sat4j.pb.constraints.pb.WatchPb
constant for the initial type of inequality more than or equal
atLeastNew(UnitPropagationListener, ILits, IVecInt, int) - Static method in class org.sat4j.pb.constraints.pb.AtLeastPB
 
atLeastNew(ILits, IVecInt, int) - Static method in class org.sat4j.pb.constraints.pb.AtLeastPB
 
AtLeastPB - Class in org.sat4j.pb.constraints.pb
 
ATMOST - Static variable in class org.sat4j.pb.constraints.pb.WatchPb
constant for the initial type of inequality less than or equal
atMost(int, T...) - Method in class org.sat4j.pb.tools.DependencyHelper
Create a constraint stating that at most i domain object should be set to true.

B

beginConstraint() - Method in class org.sat4j.pb.reader.OPBReader2005
callback called before we read a constraint
beginListOfVariables() - Method in class org.sat4j.pb.reader.OPBEclipseReader2007
callback called before we read the list for variables explanation
beginObjective() - Method in class org.sat4j.pb.reader.OPBReader2005
callback called before we read the objective function
brandNewClause(UnitPropagationListener, ILits, IVecInt) - Static method in class org.sat4j.pb.constraints.pb.MixableCBClausePB
 
brandNewClause(UnitPropagationListener, ILits, IVecInt) - Static method in class org.sat4j.pb.constraints.pb.OriginalBinaryClausePB
Creates a brand new clause, presumably from external data.
brandNewClause(UnitPropagationListener, ILits, IVecInt) - Static method in class org.sat4j.pb.constraints.pb.OriginalHTClausePB
Creates a brand new clause, presumably from external data.
buildConstraintFromConflict(IVecInt, IVec<BigInteger>) - Method in interface org.sat4j.pb.constraints.pb.IDataStructurePB
 
buildConstraintFromConflict(IVecInt, IVec<BigInteger>) - Method in class org.sat4j.pb.constraints.pb.MapPb
 
buildConstraintFromMapPb(int[], BigInteger[]) - Method in interface org.sat4j.pb.constraints.pb.IDataStructurePB
 
buildConstraintFromMapPb(int[], BigInteger[]) - Method in class org.sat4j.pb.constraints.pb.MapPb
 
byLevel - Variable in class org.sat4j.pb.constraints.pb.ConflictMap
allows to access directly to all variables belonging to a particular level At index 0, unassigned literals are stored (usually level -1); so there is always a step between index and levels.

C

calcReason(int, IVecInt) - Method in class org.sat4j.pb.constraints.pb.WatchPb
compute the reason for the assignment of a literal
calculateDegree(int[]) - Method in class org.sat4j.pb.ObjectiveFunction
 
calculateObjective() - Method in class org.sat4j.pb.PseudoOptDecorator
 
checkId(StringBuffer) - Method in class org.sat4j.pb.reader.OPBReader2005
 
checkId(StringBuffer) - Method in class org.sat4j.pb.reader.OPBReader2007
 
clause(C, T...) - Method in class org.sat4j.pb.tools.DependencyHelper
Create a clause (thing1 or thing 2 ... or thingn)
coefficientsEqualToOne() - Method in class org.sat4j.pb.constraints.pb.WatchPb
 
coefMult - Variable in class org.sat4j.pb.constraints.pb.ConflictMap
 
coefMultCons - Variable in class org.sat4j.pb.constraints.pb.ConflictMap
 
coefs - Variable in class org.sat4j.pb.constraints.pb.WatchPb
coefficients of the literals of the constraint
compareTo(WeightedObject<T>) - Method in class org.sat4j.pb.tools.WeightedObject
 
CompetMinHTmixedClauseCardConstrDataStructureFactory - Class in org.sat4j.pb.constraints
 
CompetMinHTmixedClauseCardConstrDataStructureFactory() - Constructor for class org.sat4j.pb.constraints.CompetMinHTmixedClauseCardConstrDataStructureFactory
 
CompetPBMaxMixedHTClauseCardConstrDataStructure - Class in org.sat4j.pb.constraints
 
CompetPBMaxMixedHTClauseCardConstrDataStructure() - Constructor for class org.sat4j.pb.constraints.CompetPBMaxMixedHTClauseCardConstrDataStructure
 
CompetResolutionPBMixedHTClauseCardConstrDataStructure - Class in org.sat4j.pb.constraints
 
CompetResolutionPBMixedHTClauseCardConstrDataStructure() - Constructor for class org.sat4j.pb.constraints.CompetResolutionPBMixedHTClauseCardConstrDataStructure
 
computeAnImpliedClause() - Method in class org.sat4j.pb.constraints.pb.AtLeastPB
 
computeAnImpliedClause() - Method in class org.sat4j.pb.constraints.pb.LearntBinaryClausePB
 
computeAnImpliedClause() - Method in class org.sat4j.pb.constraints.pb.LearntHTClausePB
 
computeAnImpliedClause() - Method in class org.sat4j.pb.constraints.pb.MinWatchCardPB
 
computeAnImpliedClause() - Method in class org.sat4j.pb.constraints.pb.MixableCBClausePB
 
computeAnImpliedClause() - Method in class org.sat4j.pb.constraints.pb.OriginalBinaryClausePB
 
computeAnImpliedClause() - Method in class org.sat4j.pb.constraints.pb.OriginalHTClausePB
 
computeAnImpliedClause() - Method in interface org.sat4j.pb.constraints.pb.PBConstr
 
computeAnImpliedClause() - Method in class org.sat4j.pb.constraints.pb.UnitClausePB
 
computeAnImpliedClause() - Method in class org.sat4j.pb.constraints.pb.WatchPb
compute an implied clause on the literals with the greater coefficients
computePropagation(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.MaxWatchPb
 
computePropagation(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.MinWatchPb
 
computePropagation(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.WatchPb
 
computeWatches() - Method in class org.sat4j.pb.constraints.pb.MaxWatchPb
Permet l'observation de tous les litt???
computeWatches() - Method in class org.sat4j.pb.constraints.pb.MinWatchPb
 
computeWatches() - Method in class org.sat4j.pb.constraints.pb.WatchPb
 
configureSolver(String[]) - Method in class org.sat4j.pb.LanceurPseudo2005
 
configureSolver(String[]) - Method in class org.sat4j.pb.LanceurPseudo2007Eclipse
 
ConflictMap - Class in org.sat4j.pb.constraints.pb
 
ConflictMapCardinality - Class in org.sat4j.pb.constraints.pb
 
ConflictMapCardinality(PBConstr, int) - Constructor for class org.sat4j.pb.constraints.pb.ConflictMapCardinality
 
ConflictMapClause - Class in org.sat4j.pb.constraints.pb
 
ConflictMapClause(PBConstr, int) - Constructor for class org.sat4j.pb.constraints.pb.ConflictMapClause
 
ConflictMapMerging - Class in org.sat4j.pb.constraints.pb
 
ConflictMapMerging(PBConstr, int) - Constructor for class org.sat4j.pb.constraints.pb.ConflictMapMerging
 
constraintFactory(int[], BigInteger[], BigInteger) - Method in class org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure
 
constraintFactory(int[], BigInteger[], BigInteger) - Method in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory
 
constraintFactory(int[], BigInteger[], BigInteger) - Method in class org.sat4j.pb.constraints.PBMaxDataStructure
 
constraintFactory(int[], BigInteger[], BigInteger) - Method in class org.sat4j.pb.constraints.PBMinDataStructure
 
constraintFactory(int[], BigInteger[], BigInteger) - Method in class org.sat4j.pb.constraints.PuebloPBMinDataStructure
 
constraintRelOp(String) - Method in class org.sat4j.pb.reader.OPBReader2005
callback called when we read the relational operator of a constraint
constraintRightTerm(BigInteger) - Method in class org.sat4j.pb.reader.OPBReader2005
callback called when we read the right term of a constraint (also known as the degree)
constructCard(IVecInt, int) - Method in class org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure
 
constructCard(IVecInt, int) - Method in class org.sat4j.pb.constraints.CompetMinHTmixedClauseCardConstrDataStructureFactory
 
constructCard(IVecInt, int) - Method in class org.sat4j.pb.constraints.CompetResolutionPBMixedHTClauseCardConstrDataStructure
 
constructCard(IVecInt, int) - Method in class org.sat4j.pb.constraints.PBMaxClauseAtLeastConstrDataStructure
 
constructCard(IVecInt, int) - Method in class org.sat4j.pb.constraints.PuebloPBMinClauseAtLeastConstrDataStructure
 
constructCard(IVecInt, int) - Method in class org.sat4j.pb.constraints.PuebloPBMinClauseCardConstrDataStructure
 
constructClause(IVecInt) - Method in class org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure
 
constructClause(IVecInt) - Method in class org.sat4j.pb.constraints.CompetMinHTmixedClauseCardConstrDataStructureFactory
 
constructClause(IVecInt) - Method in class org.sat4j.pb.constraints.CompetPBMaxMixedHTClauseCardConstrDataStructure
 
constructClause(IVecInt) - Method in class org.sat4j.pb.constraints.CompetResolutionPBMixedHTClauseCardConstrDataStructure
 
constructClause(IVecInt) - Method in class org.sat4j.pb.constraints.PBMaxCBClauseCardConstrDataStructure
 
constructClause(IVecInt) - Method in class org.sat4j.pb.constraints.PuebloPBMinClauseCardConstrDataStructure
 
constructLearntCard(IDataStructurePB) - Method in class org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure
 
constructLearntCard(IDataStructurePB) - Method in class org.sat4j.pb.constraints.CompetMinHTmixedClauseCardConstrDataStructureFactory
 
constructLearntCard(IDataStructurePB) - Method in class org.sat4j.pb.constraints.CompetResolutionPBMixedHTClauseCardConstrDataStructure
 
constructLearntCard(IDataStructurePB) - Method in class org.sat4j.pb.constraints.PBMaxClauseAtLeastConstrDataStructure
 
constructLearntCard(IDataStructurePB) - Method in class org.sat4j.pb.constraints.PuebloPBMinClauseAtLeastConstrDataStructure
 
constructLearntCard(IDataStructurePB) - Method in class org.sat4j.pb.constraints.PuebloPBMinClauseCardConstrDataStructure
 
constructLearntClause(IVecInt) - Method in class org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure
 
constructLearntClause(IVecInt) - Method in class org.sat4j.pb.constraints.CompetMinHTmixedClauseCardConstrDataStructureFactory
 
constructLearntClause(IVecInt) - Method in class org.sat4j.pb.constraints.CompetPBMaxMixedHTClauseCardConstrDataStructure
 
constructLearntClause(IVecInt) - Method in class org.sat4j.pb.constraints.CompetResolutionPBMixedHTClauseCardConstrDataStructure
 
constructLearntClause(IVecInt) - Method in class org.sat4j.pb.constraints.PuebloPBMinClauseCardConstrDataStructure
 
constructLearntPB(IDataStructurePB) - Method in class org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure
 
constructLearntPB(IDataStructurePB) - Method in class org.sat4j.pb.constraints.PBMaxClauseCardConstrDataStructure
 
constructLearntPB(IDataStructurePB) - Method in class org.sat4j.pb.constraints.PBMinClauseCardConstrDataStructure
 
constructLearntPB(IDataStructurePB) - Method in class org.sat4j.pb.constraints.PuebloPBMinClauseCardConstrDataStructure
 
constructPB(int[], BigInteger[], BigInteger) - Method in class org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure
 
constructPB(int[], BigInteger[], BigInteger) - Method in class org.sat4j.pb.constraints.PBMaxClauseCardConstrDataStructure
 
constructPB(int[], BigInteger[], BigInteger) - Method in class org.sat4j.pb.constraints.PBMinClauseCardConstrDataStructure
 
constructPB(int[], BigInteger[], BigInteger) - Method in class org.sat4j.pb.constraints.PuebloPBMinClauseCardConstrDataStructure
 
createCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory
 
createClause(IVecInt) - Method in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory
 
createConflict(PBConstr, int) - Static method in class org.sat4j.pb.constraints.pb.ConflictMap
constructs the data structure needed to perform cutting planes
createConflict(PBConstr, int) - Static method in class org.sat4j.pb.constraints.pb.ConflictMapClause
 
createConflict(PBConstr, int) - Static method in class org.sat4j.pb.constraints.pb.ConflictMapMerging
 
createLits() - Method in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory
 
createPseudoBooleanConstraint(IVecInt, IVec<BigInteger>, boolean, BigInteger) - Method in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory
 
createPseudoBooleanConstraint(IVecInt, IVec<BigInteger>, boolean, BigInteger) - Method in interface org.sat4j.pb.core.PBDataStructureFactory
 
createReader(ISolver, String) - Method in class org.sat4j.pb.LanceurPseudo2005
 
createReader(ISolver, String) - Method in class org.sat4j.pb.LanceurPseudo2007
 
createReader(ISolver, String) - Method in class org.sat4j.pb.LanceurPseudo2007Eclipse
 
createUnregisteredClause(IVecInt) - Method in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory
 
createUnregisteredPseudoBooleanConstraint(IDataStructurePB) - Method in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory
 
createUnregisteredPseudoBooleanConstraint(IDataStructurePB) - Method in interface org.sat4j.pb.core.PBDataStructureFactory
 
currentLevel - Variable in class org.sat4j.pb.constraints.pb.ConflictMap
 
currentSlack - Variable in class org.sat4j.pb.constraints.pb.ConflictMap
to store the slack of the current resolvant
cuttingPlane(PBConstr, BigInteger, BigInteger[], VarActivityListener) - Method in interface org.sat4j.pb.constraints.pb.IDataStructurePB
 
cuttingPlane(PBConstr, BigInteger, BigInteger[], BigInteger, VarActivityListener) - Method in interface org.sat4j.pb.constraints.pb.IDataStructurePB
 
cuttingPlane(int[], BigInteger[], BigInteger) - Method in interface org.sat4j.pb.constraints.pb.IDataStructurePB
 
cuttingPlane(int[], BigInteger[], BigInteger, BigInteger) - Method in interface org.sat4j.pb.constraints.pb.IDataStructurePB
 
cuttingPlane(PBConstr, BigInteger, BigInteger[], VarActivityListener) - Method in class org.sat4j.pb.constraints.pb.MapPb
 
cuttingPlane(PBConstr, BigInteger, BigInteger[], BigInteger, VarActivityListener) - Method in class org.sat4j.pb.constraints.pb.MapPb
 
cuttingPlane(int[], BigInteger[], BigInteger) - Method in class org.sat4j.pb.constraints.pb.MapPb
 
cuttingPlane(int[], BigInteger[], BigInteger, BigInteger) - Method in class org.sat4j.pb.constraints.pb.MapPb
 

D

decode(int[]) - Method in class org.sat4j.pb.reader.OPBReader2005
 
decode(int[], PrintWriter) - Method in class org.sat4j.pb.reader.OPBReader2005
 
decode(int[]) - Method in class org.sat4j.pb.reader.PBInstanceReader
Deprecated. 
decode(int[], PrintWriter) - Method in class org.sat4j.pb.reader.PBInstanceReader
 
defaultSolver() - Method in class org.sat4j.pb.SolverFactory
 
degree - Variable in class org.sat4j.pb.constraints.pb.MapPb
 
degree - Variable in class org.sat4j.pb.constraints.pb.WatchPb
degree of the pseudo-boolean constraint
DependencyHelper<T,C> - Class in org.sat4j.pb.tools
Helper class intended to make life easier to people to feed a sat solver programmatically.
DependencyHelper(IPBSolver) - Constructor for class org.sat4j.pb.tools.DependencyHelper
 
DependencyHelper(IPBSolver, boolean) - Constructor for class org.sat4j.pb.tools.DependencyHelper
 
discard() - Method in class org.sat4j.pb.PseudoOptDecorator
 
discard(IVec<T>) - Method in class org.sat4j.pb.tools.DependencyHelper
 
discardCurrentSolution() - Method in class org.sat4j.pb.PseudoIteratorDecorator
 
discardCurrentSolution() - Method in class org.sat4j.pb.PseudoOptDecorator
 
disjunction(T...) - Method in class org.sat4j.pb.tools.DependencyHelper
 
DisjunctionRHS<T,C> - Class in org.sat4j.pb.tools
 
DisjunctionRHS(DependencyHelper<T, C>, IVecInt) - Constructor for class org.sat4j.pb.tools.DisjunctionRHS
 
displayAnswer() - Method in class org.sat4j.pb.LanceurPseudo2007Eclipse
 

E

endConstraint() - Method in class org.sat4j.pb.reader.OPBReader2005
 
endListOfVariables() - Method in class org.sat4j.pb.reader.OPBEclipseReader2007
callback called after we've read the list for variable explanation
endObjective() - Method in class org.sat4j.pb.reader.OPBReader2005
callback called after we've read the objective function
eof() - Method in class org.sat4j.pb.reader.OPBReader2005
return true iff we've reached EOF
eol() - Method in class org.sat4j.pb.reader.OPBReader2005
 
equals(Object) - Method in class org.sat4j.pb.constraints.pb.WatchPb
 
equals(Object) - Method in class org.sat4j.pb.tools.WeightedObject
 
explanationEnabled - Variable in class org.sat4j.pb.tools.DependencyHelper
 

F

FOR_COMPETITION - Static variable in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory
 
forceObjectiveValueTo(Number) - Method in class org.sat4j.pb.PseudoOptDecorator
 
forwardActivity(double) - Method in class org.sat4j.pb.constraints.pb.WatchPb
 

G

get(int) - Method in class org.sat4j.pb.constraints.pb.WatchPb
to obtain the i-th literal of the constraint
get() - Method in class org.sat4j.pb.reader.OPBReader2005
get the next character from the stream
getActivity() - Method in class org.sat4j.pb.constraints.pb.WatchPb
to obtain the activity value of the constraint
getAssertiveLiteral() - Method in interface org.sat4j.pb.constraints.pb.IDataStructurePB
 
getAssertiveLiteral() - Method in class org.sat4j.pb.constraints.pb.MapPb
 
getBacktrackLevel(int) - Method in class org.sat4j.pb.constraints.pb.ConflictMap
computes the level for the backtrack : the highest decision level for which the conflict is assertive.
getBacktrackLevel(int) - Method in interface org.sat4j.pb.constraints.pb.IConflict
retourne le niveau de backtrack : c'est-?
getBooleanValueFor(T) - Method in class org.sat4j.pb.tools.DependencyHelper
Retrieve the boolean value associated with a domain object in the solution found by the solver.
getCoef(int) - Method in class org.sat4j.pb.constraints.pb.AtLeastPB
 
getCoef(int) - Method in class org.sat4j.pb.constraints.pb.LearntBinaryClausePB
 
getCoef(int) - Method in class org.sat4j.pb.constraints.pb.LearntHTClausePB
 
getCoef(int) - Method in class org.sat4j.pb.constraints.pb.MinWatchCardPB
 
getCoef(int) - Method in class org.sat4j.pb.constraints.pb.MixableCBClausePB
 
getCoef(int) - Method in class org.sat4j.pb.constraints.pb.OriginalBinaryClausePB
 
getCoef(int) - Method in class org.sat4j.pb.constraints.pb.OriginalHTClausePB
 
getCoef(int) - Method in interface org.sat4j.pb.constraints.pb.PBConstr
 
getCoef(int) - Method in class org.sat4j.pb.constraints.pb.UnitClausePB
 
getCoef(int) - Method in class org.sat4j.pb.constraints.pb.WatchPb
to obtain the coefficient of the i-th literal of the constraint
getCoeffs() - Method in class org.sat4j.pb.ObjectiveFunction
 
getCoeffs() - Method in class org.sat4j.pb.reader.OPBReader2005
 
getCoefs() - Method in class org.sat4j.pb.constraints.pb.AtLeastPB
 
getCoefs() - Method in class org.sat4j.pb.constraints.pb.LearntBinaryClausePB
 
getCoefs() - Method in class org.sat4j.pb.constraints.pb.LearntHTClausePB
 
getCoefs() - Method in class org.sat4j.pb.constraints.pb.MinWatchCardPB
 
getCoefs() - Method in class org.sat4j.pb.constraints.pb.MixableCBClausePB
 
getCoefs() - Method in class org.sat4j.pb.constraints.pb.OriginalBinaryClausePB
 
getCoefs() - Method in class org.sat4j.pb.constraints.pb.OriginalHTClausePB
 
getCoefs() - Method in interface org.sat4j.pb.constraints.pb.PBConstr
 
getCoefs() - Method in class org.sat4j.pb.constraints.pb.UnitClausePB
 
getCoefs() - Method in class org.sat4j.pb.constraints.pb.WatchPb
 
getDegree() - Method in class org.sat4j.pb.constraints.pb.AtLeastPB
 
getDegree() - Method in interface org.sat4j.pb.constraints.pb.IDataStructurePB
 
getDegree() - Method in class org.sat4j.pb.constraints.pb.LearntBinaryClausePB
 
getDegree() - Method in class org.sat4j.pb.constraints.pb.LearntHTClausePB
 
getDegree() - Method in class org.sat4j.pb.constraints.pb.MapPb
 
getDegree() - Method in class org.sat4j.pb.constraints.pb.MinWatchCardPB
 
getDegree() - Method in class org.sat4j.pb.constraints.pb.MixableCBClausePB
 
getDegree() - Method in class org.sat4j.pb.constraints.pb.OriginalBinaryClausePB
 
getDegree() - Method in class org.sat4j.pb.constraints.pb.OriginalHTClausePB
 
getDegree() - Method in interface org.sat4j.pb.constraints.pb.PBConstr
 
getDegree() - Method in class org.sat4j.pb.constraints.pb.UnitClausePB
 
getDegree() - Method in class org.sat4j.pb.constraints.pb.WatchPb
 
getExplanation() - Method in class org.sat4j.pb.OPBStringSolver
 
getExplanation() - Method in class org.sat4j.pb.UserFriendlyPBStringSolver
 
getInstanceName(String[]) - Method in class org.sat4j.pb.LanceurPseudo2005
 
getListOfVariables() - Method in class org.sat4j.pb.reader.OPBEclipseReader2007
 
getListOfVariables() - Method in class org.sat4j.pb.reader.OPBReader2005
 
getLits() - Method in class org.sat4j.pb.constraints.pb.AtLeastPB
 
getLits() - Method in class org.sat4j.pb.constraints.pb.MixableCBClausePB
 
getLits() - Method in interface org.sat4j.pb.constraints.pb.PBConstr
 
getLits() - Method in class org.sat4j.pb.constraints.pb.UnitClausePB
 
getLits() - Method in class org.sat4j.pb.constraints.pb.WatchPb
 
getNormalizer() - Method in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory
 
getNumberOfConstraints() - Method in class org.sat4j.pb.tools.DependencyHelper
 
getNumberOfVariables() - Method in class org.sat4j.pb.tools.DependencyHelper
 
getObjectiveFunction() - Method in class org.sat4j.pb.core.PBSolver
 
getObjectiveFunction() - Method in interface org.sat4j.pb.IPBSolver
 
getObjectiveFunction() - Method in class org.sat4j.pb.OPBStringSolver
 
getObjectiveFunction() - Method in class org.sat4j.pb.PBSolverDecorator
 
getObjectiveFunction() - Method in class org.sat4j.pb.reader.OPBReader2005
 
getObjectiveFunction() - Method in class org.sat4j.pb.tools.DependencyHelper
 
getObjectiveFunction() - Method in class org.sat4j.pb.tools.XplainPB
 
getObjectiveFunction() - Method in class org.sat4j.pb.UserFriendlyPBStringSolver
 
getObjectiveValue() - Method in class org.sat4j.pb.PseudoOptDecorator
 
getSolution() - Method in class org.sat4j.pb.tools.DependencyHelper
Retrieve the solution found.
getSolutionCost() - Method in class org.sat4j.pb.tools.DependencyHelper
 
getVars() - Method in class org.sat4j.pb.ObjectiveFunction
 
getVars() - Method in class org.sat4j.pb.reader.OPBReader2005
 
getVocabulary() - Method in class org.sat4j.pb.constraints.pb.AtLeastPB
 
getVocabulary() - Method in class org.sat4j.pb.constraints.pb.MixableCBClausePB
 
getVocabulary() - Method in interface org.sat4j.pb.constraints.pb.PBConstr
 
getVocabulary() - Method in class org.sat4j.pb.constraints.pb.UnitClausePB
 
getVocabulary() - Method in class org.sat4j.pb.constraints.pb.WatchPb
 
getWeight() - Method in class org.sat4j.pb.tools.WeightedObject
 

H

hasASolution() - Method in class org.sat4j.pb.tools.DependencyHelper
 
hasASolution(IVec<T>) - Method in class org.sat4j.pb.tools.DependencyHelper
 
hasASolution(Collection<T>) - Method in class org.sat4j.pb.tools.DependencyHelper
 
hashCode() - Method in class org.sat4j.pb.constraints.pb.WatchPb
 
hashCode() - Method in class org.sat4j.pb.tools.WeightedObject
 
hasNoObjectiveFunction() - Method in class org.sat4j.pb.PseudoOptDecorator
 
hasVariablesExplanation - Variable in class org.sat4j.pb.reader.OPBReader2005
 

I

IConflict - Interface in org.sat4j.pb.constraints.pb
 
IDataStructurePB - Interface in org.sat4j.pb.constraints.pb
 
iff(C, T, T...) - Method in class org.sat4j.pb.tools.DependencyHelper
Create a constraint using equivalency chains thing <=> (thing1 <=> thing2 <=> ... <=> thingn)
ifThenElse(C, T, T, T, T) - Method in class org.sat4j.pb.tools.DependencyHelper
Create a constraint of the form thing <=> (if conditionThing then thenThing else elseThing)
implication(T...) - Method in class org.sat4j.pb.tools.DependencyHelper
Create a logical implication of the form lhs -> rhs
ImplicationAnd<T,C> - Class in org.sat4j.pb.tools
That class is used to represent a conjunction of literals in the RHS of an implication.
ImplicationAnd(DependencyHelper<T, C>, IVecInt) - Constructor for class org.sat4j.pb.tools.ImplicationAnd
 
ImplicationNamer<T,C> - Class in org.sat4j.pb.tools
That class is used to associate each constraint with another object that must be used to represent it in an explanation.
ImplicationNamer(DependencyHelper<T, C>, IVec<IConstr>) - Constructor for class org.sat4j.pb.tools.ImplicationNamer
 
ImplicationRHS<T,C> - Class in org.sat4j.pb.tools
That class represents the RHS of an implication.
ImplicationRHS(DependencyHelper<T, C>, IVecInt) - Constructor for class org.sat4j.pb.tools.ImplicationRHS
 
implies(T...) - Method in class org.sat4j.pb.tools.DisjunctionRHS
 
implies(T) - Method in class org.sat4j.pb.tools.ImplicationRHS
Build an implication with a conjunction of literals in the RHS.
implies(T...) - Method in class org.sat4j.pb.tools.ImplicationRHS
Build an implication with a disjunction of literals in the RHS.
impliesNot(T) - Method in class org.sat4j.pb.tools.ImplicationRHS
Build an implication with a conjunction of literals in the RHS.
incActivity(double) - Method in class org.sat4j.pb.constraints.pb.WatchPb
increase activity value of the constraint
increaseWeight(BigInteger) - Method in class org.sat4j.pb.tools.WeightedObject
 
INegator<T> - Interface in org.sat4j.pb.tools
 
init() - Method in class org.sat4j.pb.orders.VarOrderHeapObjective
 
instance() - Static method in class org.sat4j.pb.SolverFactory
Access to the single instance of the factory.
instance - Static variable in class org.sat4j.pb.tools.StringNegator
 
InternalMapPBStructure - Class in org.sat4j.pb.constraints.pb
 
IPBSolver - Interface in org.sat4j.pb
A solver able to deal with pseudo boolean constraints.
isAssertive(int) - Method in class org.sat4j.pb.constraints.pb.ConflictMap
tests if the conflict is assertive (allows to imply a literal) at a particular decision level
isAssertive(int) - Method in interface org.sat4j.pb.constraints.pb.IConflict
 
isAssertive(int) - Method in class org.sat4j.pb.constraints.pb.WatchPb
This predicate tests wether the constraint is assertive at decision level dl
isCardinality() - Method in interface org.sat4j.pb.constraints.pb.IDataStructurePB
 
isCardinality() - Method in class org.sat4j.pb.constraints.pb.MapPb
 
isGoodFirstCharacter(char) - Method in class org.sat4j.pb.reader.OPBReader2005
 
isGoodFirstCharacter(char) - Method in class org.sat4j.pb.reader.OPBReader2007
 
isGoodFollowingCharacter(char) - Method in class org.sat4j.pb.reader.OPBReader2005
 
isNegated(T) - Method in interface org.sat4j.pb.tools.INegator
 
isNegated(String) - Method in class org.sat4j.pb.tools.StringNegator
 
isSatisfiable() - Method in class org.sat4j.pb.constraints.pb.WatchPb
D?
isSatisfiable() - Method in class org.sat4j.pb.OptToPBSATAdapter
 
isSatisfiable(boolean) - Method in class org.sat4j.pb.OptToPBSATAdapter
 
isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.pb.OptToPBSATAdapter
 
isSatisfiable(IVecInt) - Method in class org.sat4j.pb.OptToPBSATAdapter
 
isSatisfiable() - Method in class org.sat4j.pb.PseudoOptDecorator
 
isSatisfiable(boolean) - Method in class org.sat4j.pb.PseudoOptDecorator
 
isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.pb.PseudoOptDecorator
 
isSatisfiable(IVecInt) - Method in class org.sat4j.pb.PseudoOptDecorator
 

L

LanceurPseudo2005 - Class in org.sat4j.pb
Launcher especially dedicated to the pseudo boolean 05 evaluation (@link http://www.cril.univ-artois.fr/PB05/).
LanceurPseudo2005() - Constructor for class org.sat4j.pb.LanceurPseudo2005
 
LanceurPseudo2007 - Class in org.sat4j.pb
Launcher for the Pseudo Boolean 2007 competition.
LanceurPseudo2007() - Constructor for class org.sat4j.pb.LanceurPseudo2007
 
LanceurPseudo2007Eclipse - Class in org.sat4j.pb
 
LanceurPseudo2007Eclipse() - Constructor for class org.sat4j.pb.LanceurPseudo2007Eclipse
 
learnt() - Method in class org.sat4j.pb.constraints.pb.AtLeastPB
D?
learnt() - Method in class org.sat4j.pb.constraints.pb.MinWatchCardPB
D?
learnt - Variable in class org.sat4j.pb.constraints.pb.WatchPb
true if the constraint is a learned constraint
learnt() - Method in class org.sat4j.pb.constraints.pb.WatchPb
is the constraint a learnt constrainte ?
LearntBinaryClausePB - Class in org.sat4j.pb.constraints.pb
 
LearntBinaryClausePB(IVecInt, ILits) - Constructor for class org.sat4j.pb.constraints.pb.LearntBinaryClausePB
 
learntConstraintFactory(IDataStructurePB) - Method in class org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure
 
learntConstraintFactory(IDataStructurePB) - Method in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory
 
learntConstraintFactory(IDataStructurePB) - Method in class org.sat4j.pb.constraints.PBMaxDataStructure
 
learntConstraintFactory(IDataStructurePB) - Method in class org.sat4j.pb.constraints.PBMinDataStructure
 
learntConstraintFactory(IDataStructurePB) - Method in class org.sat4j.pb.constraints.PuebloPBMinDataStructure
 
LearntHTClausePB - Class in org.sat4j.pb.constraints.pb
 
LearntHTClausePB(IVecInt, ILits) - Constructor for class org.sat4j.pb.constraints.pb.LearntHTClausePB
 
lightSolver() - Method in class org.sat4j.pb.SolverFactory
 
literalInAProduct(String, IVecInt) - Method in class org.sat4j.pb.reader.OPBReader2007
callback called when we read a term of a constraint
lits - Variable in class org.sat4j.pb.constraints.pb.WatchPb
literals of the constraint
locked() - Method in class org.sat4j.pb.constraints.pb.WatchPb
The constraint is the reason of a unit propagation.

M

main(String[]) - Static method in class org.sat4j.pb.LanceurPseudo2005
Lance le prouveur sur un fichier Dimacs
main(String[]) - Static method in class org.sat4j.pb.LanceurPseudo2007
Lance le prouveur sur un fichier Dimacs
main(String[]) - Static method in class org.sat4j.pb.LanceurPseudo2007Eclipse
Lance le prouveur sur un fichier Dimacs
MapPb - Class in org.sat4j.pb.constraints.pb
 
maximalCoefficient(int) - Method in class org.sat4j.pb.constraints.pb.MinWatchPb
 
maximalCoefficient(int) - Method in class org.sat4j.pb.constraints.pb.PuebloMinWatchPb
 
MaxWatchPb - Class in org.sat4j.pb.constraints.pb
 
metaData(int, int) - Method in class org.sat4j.pb.reader.OPBReader2005
callback called when we get the number of variables and the expected number of constraints
MinWatchCardPB - Class in org.sat4j.pb.constraints.pb
 
MinWatchCardPB(ILits, IVecInt, boolean, int) - Constructor for class org.sat4j.pb.constraints.pb.MinWatchCardPB
 
MinWatchCardPB(ILits, IVecInt, int) - Constructor for class org.sat4j.pb.constraints.pb.MinWatchCardPB
 
minWatchCardPBNew(UnitPropagationListener, ILits, IVecInt, boolean, int) - Static method in class org.sat4j.pb.constraints.pb.MinWatchCardPB
Permet la cr?
MinWatchPb - Class in org.sat4j.pb.constraints.pb
 
MinWatchPb(ILits, IDataStructurePB) - Constructor for class org.sat4j.pb.constraints.pb.MinWatchPb
Constructeur de base des contraintes
MinWatchPb(ILits, int[], BigInteger[], BigInteger) - Constructor for class org.sat4j.pb.constraints.pb.MinWatchPb
 
MixableCBClausePB - Class in org.sat4j.pb.constraints.pb
 
MixableCBClausePB(IVecInt, ILits, boolean) - Constructor for class org.sat4j.pb.constraints.pb.MixableCBClausePB
 
MixableCBClausePB(IVecInt, ILits) - Constructor for class org.sat4j.pb.constraints.pb.MixableCBClausePB
 
model() - Method in class org.sat4j.pb.OptToPBSATAdapter
 
model(int) - Method in class org.sat4j.pb.OptToPBSATAdapter
 
model() - Method in class org.sat4j.pb.PseudoOptDecorator
 
model(int) - Method in class org.sat4j.pb.PseudoOptDecorator
 

N

named(C) - Method in class org.sat4j.pb.tools.ImplicationAnd
"name" the constraint for the explanation.
named(C) - Method in class org.sat4j.pb.tools.ImplicationNamer
Associate the current constraint with a specific object that will be used to represent it in an explanation.
nbConstr - Variable in class org.sat4j.pb.reader.OPBReader2005
 
nbConstraintsRead - Variable in class org.sat4j.pb.reader.OPBReader2005
 
nbOfWatched() - Method in class org.sat4j.pb.constraints.pb.MinWatchPb
Nombre de litt???
nbVars - Variable in class org.sat4j.pb.reader.OPBReader2005
 
negateLiteralInAProduct(String, IVecInt) - Method in class org.sat4j.pb.reader.OPBReader2007
callback called when we read a term of a constraint
newCompetPBCPMixedConstraintsObjective() - Static method in class org.sat4j.pb.SolverFactory
 
newCompetPBCPMixedConstraintsObjectiveLearnJustClauses() - Static method in class org.sat4j.pb.SolverFactory
 
newCompetPBKillerClassic() - Static method in class org.sat4j.pb.SolverFactory
 
newCompetPBKillerFixed() - Static method in class org.sat4j.pb.SolverFactory
 
newCompetPBKillerRSAT() - Static method in class org.sat4j.pb.SolverFactory
 
newCompetPBResHTMixedConstraintsObjective() - Static method in class org.sat4j.pb.SolverFactory
 
newCompetPBResHTMixedConstraintsObjectiveExpSimp() - Static method in class org.sat4j.pb.SolverFactory
 
newCompetPBResMinHTMixedConstraintsObjective() - Static method in class org.sat4j.pb.SolverFactory
 
newCompetPBResMinHTMixedConstraintsObjectiveExpSimp() - Static method in class org.sat4j.pb.SolverFactory
 
newCompetPBResMixedConstraintsObjectiveExpSimp() - Static method in class org.sat4j.pb.SolverFactory
 
newCuttingPlanes() - Static method in class org.sat4j.pb.SolverFactory
Cutting Planes based solver.
newDefault() - Static method in class org.sat4j.pb.SolverFactory
Default solver of the SolverFactory.
newDefaultNonNormalized() - Static method in class org.sat4j.pb.SolverFactory
Default solver of the SolverFactory for instances not normalized.
newDimacsOutput() - Static method in class org.sat4j.pb.SolverFactory
 
newEclipseP2() - Static method in class org.sat4j.pb.SolverFactory
 
newLight() - Static method in class org.sat4j.pb.SolverFactory
Small footprint SAT solver.
newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalReductionToClause() - Static method in class org.sat4j.pb.SolverFactory
 
newMiniOPBClauseAtLeastConstrMax() - Static method in class org.sat4j.pb.SolverFactory
 
newMiniOPBClauseAtLeastMinPueblo() - Static method in class org.sat4j.pb.SolverFactory
 
newMiniOPBClauseCardMin() - Static method in class org.sat4j.pb.SolverFactory
 
newMiniOPBClauseCardMinPueblo() - Static method in class org.sat4j.pb.SolverFactory
 
newMiniOPBCounterBasedClauseCardConstrMax() - Static method in class org.sat4j.pb.SolverFactory
 
newOPBStringSolver() - Static method in class org.sat4j.pb.SolverFactory
 
newPBCPAllPB() - Static method in class org.sat4j.pb.SolverFactory
 
newPBCPAllPBWL() - Static method in class org.sat4j.pb.SolverFactory
 
newPBCPAllPBWLPueblo() - Static method in class org.sat4j.pb.SolverFactory
 
newPBCPMixedConstrainsImplied() - Static method in class org.sat4j.pb.SolverFactory
 
newPBCPMixedConstraints() - Static method in class org.sat4j.pb.SolverFactory
 
newPBCPMixedConstraintsObjective() - Static method in class org.sat4j.pb.SolverFactory
 
newPBCPMixedConstraintsObjectiveLearnJustClauses() - Static method in class org.sat4j.pb.SolverFactory
 
newPBCPMixedConstraintsObjectiveNoLearning() - Static method in class org.sat4j.pb.SolverFactory
 
newPBCPMixedConstraintsReduceToClause() - Static method in class org.sat4j.pb.SolverFactory
 
newPBKillerClassic() - Static method in class org.sat4j.pb.SolverFactory
 
newPBKillerFixed() - Static method in class org.sat4j.pb.SolverFactory
 
newPBKillerRSAT() - Static method in class org.sat4j.pb.SolverFactory
 
newPBResAllPB() - Static method in class org.sat4j.pb.SolverFactory
 
newPBResAllPBWL() - Static method in class org.sat4j.pb.SolverFactory
 
newPBResAllPBWLPueblo() - Static method in class org.sat4j.pb.SolverFactory
 
newPBResHTMixedConstraintsObjective() - Static method in class org.sat4j.pb.SolverFactory
 
newPBResHTMixedConstraintsObjectiveExpSimp() - Static method in class org.sat4j.pb.SolverFactory
 
newPBResMinHTMixedConstraintsObjective() - Static method in class org.sat4j.pb.SolverFactory
 
newPBResMixedConstraintsObjective() - Static method in class org.sat4j.pb.SolverFactory
 
newResolution() - Static method in class org.sat4j.pb.SolverFactory
Resolution based solver (i.e. classic SAT solver able to handle generic constraints.
newVar(int) - Method in class org.sat4j.pb.OPBStringSolver
 
newVar(int) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver
 
newWO(E, int) - Static method in class org.sat4j.pb.tools.WeightedObject
 
newWO(E, BigInteger) - Static method in class org.sat4j.pb.tools.WeightedObject
 
niceCheckedParameters(IVecInt, IVec<BigInteger>, boolean, BigInteger, ILits) - Static method in class org.sat4j.pb.constraints.pb.Pseudos
 
niceCheckedParametersForCompetition(int[], BigInteger[], boolean, BigInteger) - Static method in class org.sat4j.pb.constraints.pb.Pseudos
 
niceParameters(IVecInt, IVec<BigInteger>, boolean, BigInteger, ILits) - Static method in class org.sat4j.pb.constraints.pb.Pseudos
 
niceParametersForCompetition(int[], BigInteger[], boolean, BigInteger) - Static method in class org.sat4j.pb.constraints.pb.Pseudos
 
NO_COMPETITION - Static variable in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory
 
NO_NEGATION - Variable in class org.sat4j.pb.tools.DependencyHelper
 
nonOptimalMeansSatisfiable() - Method in class org.sat4j.pb.PseudoOptDecorator
 
normalizedMaxWatchPbNew(UnitPropagationListener, ILits, int[], BigInteger[], BigInteger) - Static method in class org.sat4j.pb.constraints.pb.MaxWatchPb
 
normalizedMinWatchCardPBNew(UnitPropagationListener, ILits, IVecInt, int) - Static method in class org.sat4j.pb.constraints.pb.MinWatchCardPB
Permet la cr?
normalizedMinWatchPbNew(UnitPropagationListener, ILits, int[], BigInteger[], BigInteger) - Static method in class org.sat4j.pb.constraints.pb.MinWatchPb
 
normalizedMinWatchPbNew(UnitPropagationListener, ILits, int[], BigInteger[], BigInteger) - Static method in class org.sat4j.pb.constraints.pb.PuebloMinWatchPb
 
normalizedWatchPbNew(ILits, IDataStructurePB) - Static method in class org.sat4j.pb.constraints.pb.MaxWatchPb
 
normalizedWatchPbNew(ILits, IDataStructurePB) - Static method in class org.sat4j.pb.constraints.pb.MinWatchPb
 
normalizedWatchPbNew(ILits, IDataStructurePB) - Static method in class org.sat4j.pb.constraints.pb.PuebloMinWatchPb
 

O

obfct - Variable in class org.sat4j.pb.LanceurPseudo2005
 
ObjectiveFunction - Class in org.sat4j.pb
Abstraction for an Objective Function for Pseudo Boolean Optimization.
ObjectiveFunction(IVecInt, IVec<BigInteger>) - Constructor for class org.sat4j.pb.ObjectiveFunction
 
oldGetBacktrackLevel(int) - Method in class org.sat4j.pb.constraints.pb.ConflictMap
 
oldIsAssertive(int) - Method in class org.sat4j.pb.constraints.pb.ConflictMap
 
OPBEclipseReader2007 - Class in org.sat4j.pb.reader
 
OPBEclipseReader2007(IPBSolver) - Constructor for class org.sat4j.pb.reader.OPBEclipseReader2007
 
OPBReader2005 - Class in org.sat4j.pb.reader
Based on the "Official" reader for the Pseudo Boolean evaluation 2005.
OPBReader2005(IPBSolver) - Constructor for class org.sat4j.pb.reader.OPBReader2005
 
OPBReader2006 - Class in org.sat4j.pb.reader
Reader complying to the PB06 input format.
OPBReader2006(IPBSolver) - Constructor for class org.sat4j.pb.reader.OPBReader2006
 
OPBReader2007 - Class in org.sat4j.pb.reader
Reader complying with the PB07 input format.
OPBReader2007(IPBSolver) - Constructor for class org.sat4j.pb.reader.OPBReader2007
 
OPBStringSolver - Class in org.sat4j.pb
Solver used to display in a string the pb-instance in OPB format.
OPBStringSolver() - Constructor for class org.sat4j.pb.OPBStringSolver
 
OPBStringSolver(int) - Constructor for class org.sat4j.pb.OPBStringSolver
 
OptToPBSATAdapter - Class in org.sat4j.pb
Utility class to use optimization solvers instead of simple SAT solvers in code meant for SAT solvers.
OptToPBSATAdapter(IOptimizationProblem) - Constructor for class org.sat4j.pb.OptToPBSATAdapter
 
or(C, T, T...) - Method in class org.sat4j.pb.tools.DependencyHelper
Create a constraint of the form thing <=> (thing1 or thing 2 ... or thingn)
org.sat4j.pb - package org.sat4j.pb
 
org.sat4j.pb.constraints - package org.sat4j.pb.constraints
 
org.sat4j.pb.constraints.pb - package org.sat4j.pb.constraints.pb
Implementations of pseudo boolean contraints.
org.sat4j.pb.core - package org.sat4j.pb.core
 
org.sat4j.pb.orders - package org.sat4j.pb.orders
 
org.sat4j.pb.reader - package org.sat4j.pb.reader
 
org.sat4j.pb.tools - package org.sat4j.pb.tools
 
OriginalBinaryClausePB - Class in org.sat4j.pb.constraints.pb
 
OriginalBinaryClausePB(IVecInt, ILits) - Constructor for class org.sat4j.pb.constraints.pb.OriginalBinaryClausePB
 
OriginalHTClausePB - Class in org.sat4j.pb.constraints.pb
 
OriginalHTClausePB(IVecInt, ILits) - Constructor for class org.sat4j.pb.constraints.pb.OriginalHTClausePB
 

P

parse() - Method in class org.sat4j.pb.reader.OPBReader2005
parses the file and uses the callbacks to send to send the data back to the program
parseInstance(Reader) - Method in class org.sat4j.pb.reader.OPBReader2005
 
parseInstance(String) - Method in class org.sat4j.pb.reader.PBInstanceReader
 
parseInstance(Reader) - Method in class org.sat4j.pb.reader.PBInstanceReader
 
PBConstr - Interface in org.sat4j.pb.constraints.pb
 
PBDataStructureFactory - Interface in org.sat4j.pb.core
 
PBInstanceReader - Class in org.sat4j.pb.reader
An reader having the responsibility to choose the right reader according to the input.
PBInstanceReader(IPBSolver) - Constructor for class org.sat4j.pb.reader.PBInstanceReader
 
PBMaxCBClauseCardConstrDataStructure - Class in org.sat4j.pb.constraints
 
PBMaxCBClauseCardConstrDataStructure() - Constructor for class org.sat4j.pb.constraints.PBMaxCBClauseCardConstrDataStructure
 
PBMaxClauseAtLeastConstrDataStructure - Class in org.sat4j.pb.constraints
 
PBMaxClauseAtLeastConstrDataStructure() - Constructor for class org.sat4j.pb.constraints.PBMaxClauseAtLeastConstrDataStructure
 
PBMaxClauseCardConstrDataStructure - Class in org.sat4j.pb.constraints
 
PBMaxClauseCardConstrDataStructure() - Constructor for class org.sat4j.pb.constraints.PBMaxClauseCardConstrDataStructure
 
PBMaxDataStructure - Class in org.sat4j.pb.constraints
 
PBMaxDataStructure() - Constructor for class org.sat4j.pb.constraints.PBMaxDataStructure
 
PBMinClauseCardConstrDataStructure - Class in org.sat4j.pb.constraints
 
PBMinClauseCardConstrDataStructure() - Constructor for class org.sat4j.pb.constraints.PBMinClauseCardConstrDataStructure
 
PBMinDataStructure - Class in org.sat4j.pb.constraints
 
PBMinDataStructure() - Constructor for class org.sat4j.pb.constraints.PBMinDataStructure
 
PBSolver - Class in org.sat4j.pb.core
 
PBSolver(AssertingClauseGenerator, LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, IOrder, RestartStrategy) - Constructor for class org.sat4j.pb.core.PBSolver
 
PBSolver(AssertingClauseGenerator, LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, SearchParams, IOrder, RestartStrategy) - Constructor for class org.sat4j.pb.core.PBSolver
 
PBSolverClause - Class in org.sat4j.pb.core
 
PBSolverClause(AssertingClauseGenerator, LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, IOrder) - Constructor for class org.sat4j.pb.core.PBSolverClause
 
PBSolverCP - Class in org.sat4j.pb.core
 
PBSolverCP(AssertingClauseGenerator, LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, IOrder) - Constructor for class org.sat4j.pb.core.PBSolverCP
 
PBSolverCP(AssertingClauseGenerator, LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, SearchParams, IOrder, RestartStrategy) - Constructor for class org.sat4j.pb.core.PBSolverCP
 
PBSolverCP(AssertingClauseGenerator, LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, SearchParams, IOrder) - Constructor for class org.sat4j.pb.core.PBSolverCP
 
PBSolverDecorator - Class in org.sat4j.pb
A decorator for the PB solvers.
PBSolverDecorator(IPBSolver) - Constructor for class org.sat4j.pb.PBSolverDecorator
 
PBSolverMerging - Class in org.sat4j.pb.core
 
PBSolverMerging(AssertingClauseGenerator, LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, IOrder) - Constructor for class org.sat4j.pb.core.PBSolverMerging
 
PBSolverResolution - Class in org.sat4j.pb.core
 
PBSolverResolution(AssertingClauseGenerator, LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, SearchParams, IOrder, RestartStrategy) - Constructor for class org.sat4j.pb.core.PBSolverResolution
 
PBSolverResolution(AssertingClauseGenerator, LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, IOrder, RestartStrategy) - Constructor for class org.sat4j.pb.core.PBSolverResolution
 
PBSolverWithImpliedClause - Class in org.sat4j.pb.core
 
PBSolverWithImpliedClause(AssertingClauseGenerator, LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, IOrder) - Constructor for class org.sat4j.pb.core.PBSolverWithImpliedClause
 
ppcm(BigInteger, BigInteger) - Static method in class org.sat4j.pb.constraints.pb.ConflictMap
computes the least common factor of two integers (Plus Petit Commun Multiple in french)
ppcm(BigInteger, BigInteger) - Static method in class org.sat4j.pb.constraints.pb.WatchPb
Calcule le ppcm de deux nombres
propagate(UnitPropagationListener, int) - Method in class org.sat4j.pb.constraints.pb.MaxWatchPb
Propagation de la valeur de v?
propagate(UnitPropagationListener, int) - Method in class org.sat4j.pb.constraints.pb.MinWatchPb
Propagation de la valeur de v???
PseudoIteratorDecorator - Class in org.sat4j.pb
A decorator that computes all pseudo boolean models.
PseudoIteratorDecorator(IPBSolver) - Constructor for class org.sat4j.pb.PseudoIteratorDecorator
 
PseudoOptDecorator - Class in org.sat4j.pb
A decorator that computes minimal pseudo boolean models.
PseudoOptDecorator(IPBSolver) - Constructor for class org.sat4j.pb.PseudoOptDecorator
 
Pseudos - Class in org.sat4j.pb.constraints.pb
 
Pseudos() - Constructor for class org.sat4j.pb.constraints.pb.Pseudos
 
PuebloMinWatchPb - Class in org.sat4j.pb.constraints.pb
 
PuebloPBMinClauseAtLeastConstrDataStructure - Class in org.sat4j.pb.constraints
 
PuebloPBMinClauseAtLeastConstrDataStructure() - Constructor for class org.sat4j.pb.constraints.PuebloPBMinClauseAtLeastConstrDataStructure
 
PuebloPBMinClauseCardConstrDataStructure - Class in org.sat4j.pb.constraints
 
PuebloPBMinClauseCardConstrDataStructure() - Constructor for class org.sat4j.pb.constraints.PuebloPBMinClauseCardConstrDataStructure
 
PuebloPBMinDataStructure - Class in org.sat4j.pb.constraints
 
PuebloPBMinDataStructure() - Constructor for class org.sat4j.pb.constraints.PuebloPBMinDataStructure
 
putback(char) - Method in class org.sat4j.pb.reader.OPBReader2005
put back a character into the stream (only one chr can be put back)

R

readIdentifier(StringBuffer) - Method in class org.sat4j.pb.reader.OPBReader2005
read an identifier from stream and store it in s
readInteger(StringBuffer) - Method in class org.sat4j.pb.reader.OPBReader2005
read a integer from file
readMetaData() - Method in class org.sat4j.pb.reader.OPBReader2005
read the first comment line to get the number of variables and the number of constraints in the file calls metaData with the data that was read
readMetaData() - Method in class org.sat4j.pb.reader.OPBReader2007
read the first comment line to get the number of variables and the number of constraints in the file calls metaData with the data that was read
readTerm(StringBuffer, StringBuffer) - Method in class org.sat4j.pb.reader.OPBReader2005
read a term into coeff and var
readTerm(StringBuffer, StringBuffer) - Method in class org.sat4j.pb.reader.OPBReader2006
read a term into coeff and var
readTerm(StringBuffer, StringBuffer) - Method in class org.sat4j.pb.reader.OPBReader2007
 
readVariablesExplanation() - Method in class org.sat4j.pb.reader.OPBEclipseReader2007
read the list for variables explanation (if any) calls beginListOfVariables and endListOfVariables
readVariablesExplanation() - Method in class org.sat4j.pb.reader.OPBReader2005
 
readWord() - Method in class org.sat4j.pb.reader.OPBReader2005
read a word from file
recalcLeftSide(BigInteger[]) - Method in class org.sat4j.pb.constraints.pb.WatchPb
compute the sum of the coefficients of the satisfied or non-assigned literals of a described constraint (usually called poss)
recalcLeftSide() - Method in class org.sat4j.pb.constraints.pb.WatchPb
compute the sum of the coefficients of the satisfied or non-assigned literals of the current constraint (usually called poss)
reduceInConstraint(WatchPb, BigInteger[], int, BigInteger) - Method in class org.sat4j.pb.constraints.pb.ConflictMap
constraint reduction : removes a literal of the constraint.
reduceInConstraint(WatchPb, BigInteger[], int, BigInteger) - Method in interface org.sat4j.pb.constraints.pb.IConflict
Reduction d'une contrainte On supprime un litteral non assigne prioritairement, vrai sinon.
reduceUntilConflict(int, int, BigInteger[], WatchPb) - Method in class org.sat4j.pb.constraints.pb.ConflictMap
 
reduceUntilConflict(int, int, BigInteger[], WatchPb) - Method in class org.sat4j.pb.constraints.pb.ConflictMapClause
reduces the constraint defined by wpb until the result of the cutting plane is a conflict. this reduction returns a clause.
reduceUntilConflict(int, int, BigInteger[], WatchPb) - Method in class org.sat4j.pb.constraints.pb.ConflictMapMerging
reduces the constraint defined by wpb until the result of the cutting plane is a conflict. this reduction returns a PB constraint.
register() - Method in class org.sat4j.pb.constraints.pb.AtLeastPB
 
register() - Method in class org.sat4j.pb.constraints.pb.MinWatchCardPB
 
register() - Method in class org.sat4j.pb.constraints.pb.WatchPb
 
remove(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.MaxWatchPb
Enl???
remove(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.MinWatchPb
Enl???
rescaleBy(double) - Method in class org.sat4j.pb.constraints.pb.WatchPb
Permet le r??????
reset() - Method in class org.sat4j.pb.PseudoOptDecorator
 
resolve(PBConstr, int, VarActivityListener) - Method in class org.sat4j.pb.constraints.pb.ConflictMap
computes a cutting plane with a pseudo-boolean constraint. this method updates the current instance (of ConflictMap).
resolve(PBConstr, int, VarActivityListener) - Method in interface org.sat4j.pb.constraints.pb.IConflict
Effectue une resolution avec une contrainte PB.

S

saturation() - Method in interface org.sat4j.pb.constraints.pb.IDataStructurePB
 
saturation() - Method in class org.sat4j.pb.constraints.pb.MapPb
 
setExpectedNumberOfClauses(int) - Method in class org.sat4j.pb.OPBStringSolver
 
setExpectedNumberOfClauses(int) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver
 
setFalse(T, C) - Method in class org.sat4j.pb.tools.DependencyHelper
Add a constraint to set the value of a domain object to false.
setLearnt() - Method in class org.sat4j.pb.constraints.pb.AtLeastPB
 
setLearnt() - Method in class org.sat4j.pb.constraints.pb.MinWatchCardPB
 
setLearnt() - Method in class org.sat4j.pb.constraints.pb.WatchPb
La contrainte est apprise
setListOfVariablesForExplanation(IVecInt) - Method in class org.sat4j.pb.OPBStringSolver
 
setListOfVariablesForExplanation(IVecInt) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver
 
setMapping(Map<Integer, T>) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver
 
setNegator(INegator<T>) - Method in class org.sat4j.pb.tools.DependencyHelper
 
setNormalizer(String) - Method in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory
 
setNormalizer(AbstractPBDataStructureFactory.INormalizer) - Method in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory
 
setObjectiveFunction(ObjectiveFunction) - Method in class org.sat4j.pb.core.PBSolver
 
setObjectiveFunction(ObjectiveFunction) - Method in interface org.sat4j.pb.IPBSolver
 
setObjectiveFunction(ObjectiveFunction) - Method in class org.sat4j.pb.OPBStringSolver
 
setObjectiveFunction(ObjectiveFunction) - Method in class org.sat4j.pb.orders.VarOrderHeapObjective
 
setObjectiveFunction(ObjectiveFunction) - Method in class org.sat4j.pb.PBSolverDecorator
 
setObjectiveFunction(ObjectiveFunction) - Method in class org.sat4j.pb.PseudoOptDecorator
 
setObjectiveFunction(WeightedObject<T>...) - Method in class org.sat4j.pb.tools.DependencyHelper
Add an objective function to ask for a solution that minimize the objective function.
setObjectiveFunction(ObjectiveFunction) - Method in class org.sat4j.pb.tools.XplainPB
 
setObjectiveFunction(ObjectiveFunction) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver
 
setTrue(T, C) - Method in class org.sat4j.pb.tools.DependencyHelper
Add a constraint to set the value of a domain object to true.
simplify() - Method in class org.sat4j.pb.constraints.pb.WatchPb
Simplifie la contrainte(l'all???
size() - Method in interface org.sat4j.pb.constraints.pb.IDataStructurePB
 
size() - Method in class org.sat4j.pb.constraints.pb.MapPb
 
size() - Method in class org.sat4j.pb.constraints.pb.WatchPb
 
skipSpaces() - Method in class org.sat4j.pb.reader.OPBReader2005
skip white spaces
slackConflict() - Method in class org.sat4j.pb.constraints.pb.ConflictMap
computes the slack of the current instance
slackConflict() - Method in interface org.sat4j.pb.constraints.pb.IConflict
 
slackConstraint() - Method in class org.sat4j.pb.constraints.pb.WatchPb
compute the slack of the current constraint slack = poss - degree of the constraint
slackConstraint(BigInteger[], BigInteger) - Method in class org.sat4j.pb.constraints.pb.WatchPb
compute the slack of a described constraint slack = poss - degree of the constraint
slackIsCorrect(int) - Method in class org.sat4j.pb.constraints.pb.ConflictMap
 
slackIsCorrect(int) - Method in interface org.sat4j.pb.constraints.pb.IConflict
 
solver - Variable in class org.sat4j.pb.reader.OPBReader2005
 
SolverFactory - Class in org.sat4j.pb
User friendly access to pre-constructed solvers.
sort() - Method in class org.sat4j.pb.constraints.pb.WatchPb
sort coefficient and literal arrays
sort(int, int) - Method in class org.sat4j.pb.constraints.pb.WatchPb
sort partially coefficient and literal arrays
stopExplanation() - Method in class org.sat4j.pb.tools.DependencyHelper
Stop the explanation computation.
stopSolver() - Method in class org.sat4j.pb.tools.DependencyHelper
Stop the SAT solver that is looking for a solution.
StringNegator - Class in org.sat4j.pb.tools
 

T

thing - Variable in class org.sat4j.pb.tools.WeightedObject
 
toBigInt(int) - Static method in class org.sat4j.pb.constraints.pb.Pseudos
 
toString() - Method in class org.sat4j.pb.constraints.pb.ConflictMap
 
toString() - Method in class org.sat4j.pb.constraints.pb.MapPb
 
toString() - Method in class org.sat4j.pb.constraints.pb.WatchPb
 
toString(String) - Method in class org.sat4j.pb.core.PBSolverClause
 
toString(String) - Method in class org.sat4j.pb.core.PBSolverCP
 
toString(String) - Method in class org.sat4j.pb.core.PBSolverMerging
 
toString(String) - Method in class org.sat4j.pb.core.PBSolverWithImpliedClause
 
toString() - Method in class org.sat4j.pb.ObjectiveFunction
 
toString() - Method in class org.sat4j.pb.OPBStringSolver
 
toString(String) - Method in class org.sat4j.pb.OPBStringSolver
 
toString(String) - Method in class org.sat4j.pb.OptToPBSATAdapter
 
toString() - Method in class org.sat4j.pb.orders.VarOrderHeapObjective
 
toString(String) - Method in class org.sat4j.pb.PseudoOptDecorator
 
toString() - Method in class org.sat4j.pb.UserFriendlyPBStringSolver
 
toString(String) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver
 
toVecBigInt(IVecInt) - Static method in class org.sat4j.pb.constraints.pb.Pseudos
 
translateVarToId(String) - Method in class org.sat4j.pb.reader.OPBReader2005
 
translateVarToId(String) - Method in class org.sat4j.pb.reader.OPBReader2007
 

U

undo(int) - Method in class org.sat4j.pb.constraints.pb.MaxWatchPb
M?
undo(int) - Method in class org.sat4j.pb.constraints.pb.MinWatchPb
M???
UnitClausePB - Class in org.sat4j.pb.constraints.pb
 
UnitClausePB(int, ILits) - Constructor for class org.sat4j.pb.constraints.pb.UnitClausePB
 
unNegate(T) - Method in interface org.sat4j.pb.tools.INegator
 
unNegate(String) - Method in class org.sat4j.pb.tools.StringNegator
 
updateSlack(int) - Method in class org.sat4j.pb.constraints.pb.ConflictMap
 
updateSlack(int) - Method in interface org.sat4j.pb.constraints.pb.IConflict
 
updateWatched(BigInteger, int) - Method in class org.sat4j.pb.constraints.pb.MinWatchPb
 
updateWatched(BigInteger, int) - Method in class org.sat4j.pb.constraints.pb.PuebloMinWatchPb
 
usage() - Method in class org.sat4j.pb.LanceurPseudo2005
 
UserFriendlyPBStringSolver<T> - Class in org.sat4j.pb
Solver to display SAT instances using domain objects names instead of Dimacs numbers.
UserFriendlyPBStringSolver() - Constructor for class org.sat4j.pb.UserFriendlyPBStringSolver
 
UserFriendlyPBStringSolver(int) - Constructor for class org.sat4j.pb.UserFriendlyPBStringSolver
 

V

VarOrderHeapObjective - Class in org.sat4j.pb.orders
 
VarOrderHeapObjective() - Constructor for class org.sat4j.pb.orders.VarOrderHeapObjective
 
VarOrderHeapObjective(IPhaseSelectionStrategy) - Constructor for class org.sat4j.pb.orders.VarOrderHeapObjective
 
voc - Variable in class org.sat4j.pb.constraints.pb.WatchPb
constraint's vocabulary

W

watchCumul - Variable in class org.sat4j.pb.constraints.pb.WatchPb
sum of the coefficients of the literals satisfied or unvalued
watched - Variable in class org.sat4j.pb.constraints.pb.MinWatchPb
Liste des indices des litt???
watching - Variable in class org.sat4j.pb.constraints.pb.MinWatchPb
Sert ???
watchingCount - Variable in class org.sat4j.pb.constraints.pb.MinWatchPb
Liste des indices des litt???
WatchPb - Class in org.sat4j.pb.constraints.pb
 
weightedLits - Variable in class org.sat4j.pb.constraints.pb.MapPb
 
WeightedObject<T> - Class in org.sat4j.pb.tools
 
why() - Method in class org.sat4j.pb.tools.DependencyHelper
Explain the reason of the inconsistency of the set of constraints.
why(T) - Method in class org.sat4j.pb.tools.DependencyHelper
Explain a domain object has been set to true in a solution.
whyNot(T) - Method in class org.sat4j.pb.tools.DependencyHelper
Explain a domain object has been set to false in a solution.

X

XplainPB - Class in org.sat4j.pb.tools
 
XplainPB(IPBSolver) - Constructor for class org.sat4j.pb.tools.XplainPB
 

A B C D E F G H I L M N O P R S T U V W X

Copyright © 2009 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.