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

A

AbstractPBClauseCardConstrDataStructure - Class in org.sat4j.pb.constraints
 
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
activity - Variable in class org.sat4j.pb.constraints.pb.WatchPbLong
constraint activity
activity - Variable in class org.sat4j.pb.constraints.pb.WatchPbLongCP
constraint activity
addAllClauses(IVec<IVecInt>) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
addAtLeast(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
addAtLeast(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
addAtLeast(IVecInt, int) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
addAtLeast(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.core.PBSolver
 
addAtLeast(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.core.PBSolver
 
addAtLeast(IVecInt, IVecInt, int) - Method in interface org.sat4j.pb.IPBSolver
Create a pseudo-boolean constraint of the type "at least".
addAtLeast(IVecInt, IVec<BigInteger>, BigInteger) - Method in interface org.sat4j.pb.IPBSolver
Create a pseudo-boolean constraint of the type "at least".
addAtLeast(IVecInt, int) - Method in class org.sat4j.pb.LPStringSolver
 
addAtLeast(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.LPStringSolver
 
addAtLeast(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.LPStringSolver
 
addAtLeast(IVecInt, int) - Method in class org.sat4j.pb.OPBStringSolver
 
addAtLeast(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.OPBStringSolver
 
addAtLeast(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.OPBStringSolver
 
addAtLeast(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.PBSolverDecorator
 
addAtLeast(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.PBSolverDecorator
 
addAtLeast(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.PseudoBitsAdderDecorator
 
addAtLeast(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.PseudoBitsAdderDecorator
 
addAtLeast(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.tools.ClausalConstraintsDecorator
 
addAtLeast(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.tools.ClausalConstraintsDecorator
 
addAtLeast(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.tools.LexicoDecoratorPB
 
addAtLeast(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.tools.LexicoDecoratorPB
 
addAtLeast(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.tools.ManyCorePB
 
addAtLeast(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.tools.ManyCorePB
 
addAtLeast(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.tools.PBAdapter
 
addAtLeast(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.tools.PBAdapter
 
addAtLeast(IVecInt, int) - Method in class org.sat4j.pb.tools.XplainPB
 
addAtLeast(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.tools.XplainPB
 
addAtLeast(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.tools.XplainPB
 
addAtLeast(IVecInt, int) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver
 
addAtLeast(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver
 
addAtLeast(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver
 
addAtMost(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
addAtMost(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
addAtMost(IVecInt, int) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
addAtMost(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.core.PBSolver
 
addAtMost(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.core.PBSolver
 
addAtMost(IVecInt, IVecInt, int) - Method in interface org.sat4j.pb.IPBSolver
Create a pseudo boolean constraint of the type "at most".
addAtMost(IVecInt, IVec<BigInteger>, BigInteger) - Method in interface org.sat4j.pb.IPBSolver
Create a pseudo boolean constraint of the type "at most".
addAtMost(IVecInt, int) - Method in class org.sat4j.pb.LPStringSolver
 
addAtMost(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.LPStringSolver
 
addAtMost(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.LPStringSolver
 
addAtMost(IVecInt, int) - Method in class org.sat4j.pb.OPBStringSolver
 
addAtMost(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.OPBStringSolver
 
addAtMost(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.OPBStringSolver
 
addAtMost(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.PBSolverDecorator
 
addAtMost(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.PBSolverDecorator
 
addAtMost(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.PseudoBitsAdderDecorator
 
addAtMost(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.PseudoBitsAdderDecorator
 
addAtMost(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.tools.ClausalConstraintsDecorator
 
addAtMost(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.tools.ClausalConstraintsDecorator
 
addAtMost(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.tools.LexicoDecoratorPB
 
addAtMost(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.tools.LexicoDecoratorPB
 
addAtMost(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.tools.ManyCorePB
 
addAtMost(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.tools.ManyCorePB
 
addAtMost(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.tools.PBAdapter
 
addAtMost(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.tools.PBAdapter
 
addAtMost(IVecInt, int) - Method in class org.sat4j.pb.tools.XplainPB
 
addAtMost(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.tools.XplainPB
 
addAtMost(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.tools.XplainPB
 
addAtMost(IVecInt, int) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver
 
addAtMost(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver
 
addAtMost(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver
 
addAtMostOnTheFly(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.core.PBSolver
 
addAtMostOnTheFly(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.core.PBSolver
 
addAtMostOnTheFly(IVecInt, IVec<BigInteger>, BigInteger) - Method in interface org.sat4j.pb.IPBSolverService
 
addAtMostOnTheFly(IVecInt, IVecInt, int) - Method in interface org.sat4j.pb.IPBSolverService
 
addBlockingClause(IVecInt) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
addClause(IVecInt) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
addClause(IVecInt) - Method in class org.sat4j.pb.LPStringSolver
 
addClause(IVecInt) - Method in class org.sat4j.pb.OPBStringSolver
 
addClause(IVecInt) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver
 
addCriterion(IVecInt) - Method in class org.sat4j.pb.tools.LexicoDecoratorPB
 
addCriterion(IVecInt, IVec<BigInteger>) - Method in class org.sat4j.pb.tools.LexicoDecoratorPB
 
addCriterion(Collection<T>) - Method in class org.sat4j.pb.tools.LexicoHelper
 
addExactly(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
addExactly(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
addExactly(IVecInt, int) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
addExactly(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.core.PBSolver
 
addExactly(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.core.PBSolver
 
addExactly(IVecInt, IVecInt, int) - Method in interface org.sat4j.pb.IPBSolver
Create a pseudo-boolean constraint of the type "subset sum".
addExactly(IVecInt, IVec<BigInteger>, BigInteger) - Method in interface org.sat4j.pb.IPBSolver
Create a pseudo-boolean constraint of the type "subset sum".
addExactly(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.LPStringSolver
 
addExactly(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.LPStringSolver
 
addExactly(IVecInt, int) - Method in class org.sat4j.pb.OPBStringSolver
 
addExactly(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.OPBStringSolver
 
addExactly(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.OPBStringSolver
 
addExactly(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.PBSolverDecorator
 
addExactly(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.PBSolverDecorator
 
addExactly(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.PseudoBitsAdderDecorator
 
addExactly(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.PseudoBitsAdderDecorator
 
addExactly(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.tools.ClausalConstraintsDecorator
 
addExactly(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.tools.ClausalConstraintsDecorator
 
addExactly(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.tools.LexicoDecoratorPB
 
addExactly(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.tools.LexicoDecoratorPB
 
addExactly(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.tools.ManyCorePB
 
addExactly(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.tools.ManyCorePB
 
addExactly(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.tools.PBAdapter
 
addExactly(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.tools.PBAdapter
 
addExactly(IVecInt, int) - Method in class org.sat4j.pb.tools.XplainPB
 
addExactly(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.tools.XplainPB
 
addExactly(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.tools.XplainPB
 
addExactly(IVecInt, IVecInt, int) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver
 
addExactly(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver
 
addPseudoBoolean(IVecInt, IVec<BigInteger>, boolean, BigInteger) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
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 or at most n of those literals must be satisfied"
addPseudoBoolean(IVecInt, IVec<BigInteger>, boolean, BigInteger) - Method in class org.sat4j.pb.LPStringSolver
 
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.PseudoBitsAdderDecorator
 
addPseudoBoolean(IVecInt, IVec<BigInteger>, boolean, BigInteger) - Method in class org.sat4j.pb.tools.ClausalConstraintsDecorator
 
addPseudoBoolean(IVecInt, IVec<BigInteger>, boolean, BigInteger) - Method in class org.sat4j.pb.tools.LexicoDecoratorPB
 
addPseudoBoolean(IVecInt, IVec<BigInteger>, boolean, BigInteger) - Method in class org.sat4j.pb.tools.ManyCorePB
 
addPseudoBoolean(IVecInt, IVec<BigInteger>, boolean, BigInteger) - Method in class org.sat4j.pb.tools.PBAdapter
 
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.
addWeightedCriterion(Collection<WeightedObject<T>>) - Method in class org.sat4j.pb.tools.LexicoHelper
 
admitABetterSolution() - Method in class org.sat4j.pb.ConstraintRelaxingPseudoOptDecorator
 
admitABetterSolution(IVecInt) - Method in class org.sat4j.pb.ConstraintRelaxingPseudoOptDecorator
 
admitABetterSolution() - Method in class org.sat4j.pb.PseudoOptDecorator
 
admitABetterSolution(IVecInt) - Method in class org.sat4j.pb.PseudoOptDecorator
 
admitABetterSolution(IVecInt) - Method in class org.sat4j.pb.tools.LexicoDecoratorPB
 
analyze(Constr, Pair) - Method in class org.sat4j.pb.core.PBSolverCP
 
analyzeCP(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.WatchPb
 
assertConstraint(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
 
assertConstraint(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
 
assertiveLiteral - Variable in class org.sat4j.pb.constraints.pb.MapPb
 
atLeast(C, 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.
atLeast(C, BigInteger, WeightedObject<T>...) - Method in class org.sat4j.pb.tools.DependencyHelper
Create a PB constraint of the form w1.l1 + w2.l2 + ... wn.ln >= degree where wi are position integers and li are domain objects.
AtLeastCardConstructor - Class in org.sat4j.pb.constraints
 
AtLeastCardConstructor() - Constructor for class org.sat4j.pb.constraints.AtLeastCardConstructor
 
AtLeastCardPBConstructor - Class in org.sat4j.pb.constraints
 
AtLeastCardPBConstructor() - Constructor for class org.sat4j.pb.constraints.AtLeastCardPBConstructor
 
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(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.
atMost(C, 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.
atMost(C, BigInteger, WeightedObject<T>...) - Method in class org.sat4j.pb.tools.DependencyHelper
Create a PB constraint of the form w1.l1 + w2.l2 + ... wn.ln <= degree where wi are position integers and li are domain objects.
atMost(C, int, WeightedObject<T>...) - Method in class org.sat4j.pb.tools.DependencyHelper
 

B

BASIC_NEGATION - Static variable in class org.sat4j.pb.tools.DependencyHelper
 
beginConstraint() - Method in class org.sat4j.pb.reader.OPBReader2005
callback called before we read a constraint
beginConstraint() - Method in class org.sat4j.pb.reader.OPBReader2010
 
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
bigCoefs - Variable in class org.sat4j.pb.constraints.pb.WatchPbLongCP
coefficients of the literals of the constraint
bigDegree - Variable in class org.sat4j.pb.constraints.pb.WatchPbLongCP
degree of the pseudo-boolean constraint
BOUND - Static variable in class org.sat4j.pb.core.PBSolverCautious
 
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
calcReason(int, IVecInt) - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
compute the reason for the assignment of a literal
calcReason(int, IVecInt) - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
compute the reason for the assignment of a literal
calcReasonOnTheFly(int, IVecInt, IVecInt) - Method in class org.sat4j.pb.constraints.pb.WatchPb
 
calcReasonOnTheFly(int, IVecInt, IVecInt) - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
 
calcReasonOnTheFly(int, IVecInt, IVecInt) - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
 
calculateDegree(RandomAccessModel) - Method in class org.sat4j.pb.ObjectiveFunction
Compute the degree of the objective function using a full model.
calculateDegreeImplicant(ISolver) - Method in class org.sat4j.pb.ObjectiveFunction
Compute the degree of the objective function using a prime implicant.
calculateObjective() - Method in class org.sat4j.pb.ConstraintRelaxingPseudoOptDecorator
Deprecated.
calculateObjective() - Method in class org.sat4j.pb.PseudoOptDecorator
 
canBePropagatedMultipleTimes() - Method in class org.sat4j.pb.constraints.pb.WatchPb
 
canBePropagatedMultipleTimes() - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
 
canBePropagatedMultipleTimes() - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
 
checkId(StringBuffer) - Method in class org.sat4j.pb.reader.OPBReader2005
 
checkId(StringBuffer) - Method in class org.sat4j.pb.reader.OPBReader2007
 
ClausalConstraintsDecorator - Class in org.sat4j.pb.tools
 
ClausalConstraintsDecorator(IPBSolver, EncodingStrategyAdapter) - Constructor for class org.sat4j.pb.tools.ClausalConstraintsDecorator
 
ClausalConstraintsDecorator(IPBSolver) - Constructor for class org.sat4j.pb.tools.ClausalConstraintsDecorator
 
clause(C, T...) - Method in class org.sat4j.pb.tools.DependencyHelper
Create a clause (thing1 or thing 2 ... or thingn)
clearLearntClauses() - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
coefficientsEqualToOne() - Method in class org.sat4j.pb.constraints.pb.WatchPb
 
coefficientsEqualToOne() - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
 
coefficientsEqualToOne() - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
 
coeffs - Variable in class org.sat4j.pb.reader.OPBReader2005
 
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
coefs - Variable in class org.sat4j.pb.constraints.pb.WatchPbLong
coefficients of the literals of the constraint
coefs - Variable in class org.sat4j.pb.constraints.pb.WatchPbLongCP
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
 
CompetResolutionMinPBLongMixedWLClauseCardConstrDataStructure - Class in org.sat4j.pb.constraints
 
CompetResolutionMinPBLongMixedWLClauseCardConstrDataStructure() - Constructor for class org.sat4j.pb.constraints.CompetResolutionMinPBLongMixedWLClauseCardConstrDataStructure
 
CompetResolutionPBLongMixedHTClauseCardConstrDataStructure - Class in org.sat4j.pb.constraints
 
CompetResolutionPBLongMixedHTClauseCardConstrDataStructure() - Constructor for class org.sat4j.pb.constraints.CompetResolutionPBLongMixedHTClauseCardConstrDataStructure
 
CompetResolutionPBLongMixedWLClauseCardConstrDataStructure - Class in org.sat4j.pb.constraints
 
CompetResolutionPBLongMixedWLClauseCardConstrDataStructure() - Constructor for class org.sat4j.pb.constraints.CompetResolutionPBLongMixedWLClauseCardConstrDataStructure
 
CompetResolutionPBMixedHTClauseCardConstrDataStructure - Class in org.sat4j.pb.constraints
 
CompetResolutionPBMixedHTClauseCardConstrDataStructure() - Constructor for class org.sat4j.pb.constraints.CompetResolutionPBMixedHTClauseCardConstrDataStructure
 
CompetResolutionPBMixedWLClauseCardConstrDataStructure - Class in org.sat4j.pb.constraints
 
CompetResolutionPBMixedWLClauseCardConstrDataStructure() - Constructor for class org.sat4j.pb.constraints.CompetResolutionPBMixedWLClauseCardConstrDataStructure
 
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.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.UnitClausesPB
 
computeAnImpliedClause() - Method in class org.sat4j.pb.constraints.pb.WatchPb
compute an implied clause on the literals with the greater coefficients.
computeAnImpliedClause() - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
compute an implied clause on the literals with the greater coefficients.
computeAnImpliedClause() - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
compute an implied clause on the literals with the greater coefficients.
computeLeftSide(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)
computeLeftSide() - 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)
computeLeftSide(long[]) - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
compute the sum of the coefficients of the satisfied or non-assigned literals of a described constraint (usually called poss)
computeLeftSide() - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
compute the sum of the coefficients of the satisfied or non-assigned literals of the current constraint (usually called poss)
computeLeftSide(long[]) - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
compute the sum of the coefficients of the satisfied or non-assigned literals of a described constraint (usually called poss)
computeLeftSide(BigInteger[]) - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
compute the sum of the coefficients of the satisfied or non-assigned literals of a described constraint (usually called poss)
computeLeftSide() - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
compute the sum of the coefficients of the satisfied or non-assigned literals of the current constraint (usually called poss)
computePropagation(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.MaxWatchPb
 
computePropagation(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.MaxWatchPbLong
 
computePropagation(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.MaxWatchPbLongCP
 
computePropagation(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.MinWatchPb
 
computePropagation(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.MinWatchPbLong
 
computePropagation(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.MinWatchPbLongCP
 
computePropagation(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.WatchPb
 
computePropagation(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
 
computePropagation(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
 
computeWatches() - Method in class org.sat4j.pb.constraints.pb.MaxWatchPb
All the literals are watched.
computeWatches() - Method in class org.sat4j.pb.constraints.pb.MaxWatchPbLong
All the literals are watched.
computeWatches() - Method in class org.sat4j.pb.constraints.pb.MaxWatchPbLongCP
All the literals are watched.
computeWatches() - Method in class org.sat4j.pb.constraints.pb.MinWatchPb
 
computeWatches() - Method in class org.sat4j.pb.constraints.pb.MinWatchPbLong
 
computeWatches() - Method in class org.sat4j.pb.constraints.pb.MinWatchPbLongCP
 
computeWatches() - Method in class org.sat4j.pb.constraints.pb.WatchPb
 
computeWatches() - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
 
computeWatches() - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
 
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
 
ConflictMapSwitchToClause - Class in org.sat4j.pb.constraints.pb
 
ConflictMapSwitchToClause(PBConstr, int) - Constructor for class org.sat4j.pb.constraints.pb.ConflictMapSwitchToClause
 
ConflictTracing - Class in org.sat4j.pb.tools
 
ConflictTracing(String) - Constructor for class org.sat4j.pb.tools.ConflictTracing
 
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
 
constraintRegexp() - Method in class org.sat4j.pb.reader.JSONPBReader
 
ConstraintRelaxingPseudoOptDecorator - Class in org.sat4j.pb
 
ConstraintRelaxingPseudoOptDecorator(IPBSolver) - Constructor for class org.sat4j.pb.ConstraintRelaxingPseudoOptDecorator
 
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(UnitPropagationListener, ILits, IVecInt, int) - Method in class org.sat4j.pb.constraints.AtLeastCardConstructor
 
constructCard(UnitPropagationListener, ILits, IVecInt, int) - Method in class org.sat4j.pb.constraints.AtLeastCardPBConstructor
 
constructCard(UnitPropagationListener, ILits, IVecInt, int) - Method in interface org.sat4j.pb.constraints.ICardConstructor
 
constructCard(UnitPropagationListener, ILits, IVecInt, int) - Method in class org.sat4j.pb.constraints.MinCardConstructor
 
constructCard(UnitPropagationListener, ILits, IVecInt, int) - Method in class org.sat4j.pb.constraints.MinCardPBConstructor
 
constructClause(IVecInt) - Method in class org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure
 
constructClause(UnitPropagationListener, ILits, IVecInt) - Method in interface org.sat4j.pb.constraints.IClauseConstructor
 
constructClause(UnitPropagationListener, ILits, IVecInt) - Method in class org.sat4j.pb.constraints.UnitBinaryHTClauseConstructor
 
constructClause(UnitPropagationListener, ILits, IVecInt) - Method in class org.sat4j.pb.constraints.UnitBinaryHTClausePBConstructor
 
constructClause(UnitPropagationListener, ILits, IVecInt) - Method in class org.sat4j.pb.constraints.UnitBinaryWLClauseConstructor
 
constructLearntCard(IDataStructurePB) - Method in class org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure
 
constructLearntCard(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure
 
constructLearntCard(ILits, IDataStructurePB) - Method in class org.sat4j.pb.constraints.AtLeastCardConstructor
 
constructLearntCard(ILits, IDataStructurePB) - Method in class org.sat4j.pb.constraints.AtLeastCardPBConstructor
 
constructLearntCard(ILits, IDataStructurePB) - Method in interface org.sat4j.pb.constraints.ICardConstructor
 
constructLearntCard(ILits, IDataStructurePB) - Method in class org.sat4j.pb.constraints.MinCardConstructor
 
constructLearntCard(ILits, IDataStructurePB) - Method in class org.sat4j.pb.constraints.MinCardPBConstructor
 
constructLearntClause(IVecInt) - Method in class org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure
 
constructLearntClause(ILits, IVecInt) - Method in interface org.sat4j.pb.constraints.IClauseConstructor
 
constructLearntClause(ILits, IVecInt) - Method in class org.sat4j.pb.constraints.UnitBinaryHTClauseConstructor
 
constructLearntClause(ILits, IVecInt) - Method in class org.sat4j.pb.constraints.UnitBinaryHTClausePBConstructor
 
constructLearntClause(ILits, IVecInt) - Method in class org.sat4j.pb.constraints.UnitBinaryWLClauseConstructor
 
constructLearntPB(IDataStructurePB) - Method in class org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure
 
constructLearntPB(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure
 
constructLearntPB(ILits, IDataStructurePB) - Method in interface org.sat4j.pb.constraints.IPBConstructor
 
constructLearntPB(ILits, IDataStructurePB) - Method in class org.sat4j.pb.constraints.MaxLongWatchPBConstructor
 
constructLearntPB(ILits, IDataStructurePB) - Method in class org.sat4j.pb.constraints.MaxLongWatchPBCPConstructor
 
constructLearntPB(ILits, IDataStructurePB) - Method in class org.sat4j.pb.constraints.MaxWatchPBConstructor
 
constructLearntPB(ILits, IDataStructurePB) - Method in class org.sat4j.pb.constraints.MinLongWatchPBConstructor
 
constructLearntPB(ILits, IDataStructurePB) - Method in class org.sat4j.pb.constraints.MinLongWatchPBCPConstructor
 
constructLearntPB(ILits, IDataStructurePB) - Method in class org.sat4j.pb.constraints.MinWatchPBConstructor
 
constructLearntPB(ILits, IDataStructurePB) - Method in class org.sat4j.pb.constraints.PuebloMinWatchPBConstructor
 
constructPB(int[], BigInteger[], BigInteger) - Method in class org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure
 
constructPB(UnitPropagationListener, ILits, int[], BigInteger[], BigInteger, BigInteger) - Method in interface org.sat4j.pb.constraints.IPBConstructor
 
constructPB(UnitPropagationListener, ILits, int[], BigInteger[], BigInteger, BigInteger) - Method in class org.sat4j.pb.constraints.MaxLongWatchPBConstructor
 
constructPB(UnitPropagationListener, ILits, int[], BigInteger[], BigInteger, BigInteger) - Method in class org.sat4j.pb.constraints.MaxLongWatchPBCPConstructor
 
constructPB(UnitPropagationListener, ILits, int[], BigInteger[], BigInteger, BigInteger) - Method in class org.sat4j.pb.constraints.MaxWatchPBConstructor
 
constructPB(UnitPropagationListener, ILits, int[], BigInteger[], BigInteger, BigInteger) - Method in class org.sat4j.pb.constraints.MinLongWatchPBConstructor
 
constructPB(UnitPropagationListener, ILits, int[], BigInteger[], BigInteger, BigInteger) - Method in class org.sat4j.pb.constraints.MinLongWatchPBCPConstructor
 
constructPB(UnitPropagationListener, ILits, int[], BigInteger[], BigInteger, BigInteger) - Method in class org.sat4j.pb.constraints.MinWatchPBConstructor
 
constructPB(UnitPropagationListener, ILits, int[], BigInteger[], BigInteger, BigInteger) - Method in class org.sat4j.pb.constraints.PuebloMinWatchPBConstructor
 
createAtLeastPBConstraint(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory
 
createAtLeastPBConstraint(IVecInt, IVec<BigInteger>, BigInteger) - Method in interface org.sat4j.pb.core.PBDataStructureFactory
 
createAtMostPBConstraint(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory
 
createAtMostPBConstraint(IVecInt, IVec<BigInteger>, BigInteger) - Method in interface org.sat4j.pb.core.PBDataStructureFactory
 
createCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory
 
createClause(IVecInt) - Method in class org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure
 
createClause(IVecInt) - Method in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory
 
createClause(IVecInt) - Method in class org.sat4j.pb.constraints.PuebloPBMinClauseCardConstrDataStructure
 
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.ConflictMapSwitchToClause
 
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
 
createUnregisteredAtLeastConstraint(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory
 
createUnregisteredAtLeastConstraint(IVecInt, IVec<BigInteger>, BigInteger) - Method in interface org.sat4j.pb.core.PBDataStructureFactory
 
createUnregisteredAtMostConstraint(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory
 
createUnregisteredAtMostConstraint(IVecInt, IVec<BigInteger>, BigInteger) - Method in interface org.sat4j.pb.core.PBDataStructureFactory
 
createUnregisteredCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory
 
createUnregisteredClause(IVecInt) - Method in class org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure
 
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

d - Variable in class org.sat4j.pb.reader.OPBReader2005
 
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.OPBReader2007
 
decode(int[], PrintWriter) - Method in class org.sat4j.pb.reader.OPBReader2007
 
defaultSolver() - Method in class org.sat4j.pb.SolverFactory
Provides the best available PB solver of the library ready to solve satisfaction problems.
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
degree - Variable in class org.sat4j.pb.constraints.pb.WatchPbLong
degree of the pseudo-boolean constraint
degree - Variable in class org.sat4j.pb.constraints.pb.WatchPbLongCP
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
 
DependencyHelper(IPBSolver, boolean, boolean) - Constructor for class org.sat4j.pb.tools.DependencyHelper
 
discard() - Method in class org.sat4j.pb.ConstraintRelaxingPseudoOptDecorator
Deprecated.
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.ConstraintRelaxingPseudoOptDecorator
 
discardCurrentSolution() - Method in class org.sat4j.pb.PseudoIteratorDecorator
 
discardCurrentSolution() - Method in class org.sat4j.pb.PseudoOptDecorator
 
discardSolutionsForOptimizing() - Method in class org.sat4j.pb.tools.LexicoDecoratorPB
 
discardSolutionsWithObjectiveValueGreaterThan(long) - Method in class org.sat4j.pb.tools.DependencyHelper
 
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
 
displayResult() - Method in class org.sat4j.pb.LanceurPseudo2007Eclipse
 

E

end(Lbool) - Method in class org.sat4j.pb.tools.SearchOptimizerListener
 
endConstraint() - Method in class org.sat4j.pb.reader.OPBReader2005
 
endConstraint() - Method in class org.sat4j.pb.reader.OPBReader2010
 
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.constraints.pb.WatchPbLong
 
equals(Object) - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
 
equals(Object) - Method in class org.sat4j.pb.ObjectiveFunction
 
equals(Object) - Method in class org.sat4j.pb.tools.WeightedObject
 
evaluate() - Method in class org.sat4j.pb.tools.LexicoDecoratorPB
 
evaluate(int) - Method in class org.sat4j.pb.tools.LexicoDecoratorPB
 
expireTimeout() - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 

F

findModel() - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
findModel(IVecInt) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
fixCriterionValue() - Method in class org.sat4j.pb.tools.LexicoDecoratorPB
 
FOR_COMPETITION - Static variable in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory
 
forceObjectiveValueTo(Number) - Method in class org.sat4j.pb.ConstraintRelaxingPseudoOptDecorator
 
forceObjectiveValueTo(Number) - Method in class org.sat4j.pb.PseudoOptDecorator
 
forwardActivity(double) - Method in class org.sat4j.pb.constraints.pb.WatchPb
 
forwardActivity(double) - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
 
forwardActivity(double) - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
 

G

get(int) - Method in class org.sat4j.pb.constraints.pb.WatchPb
to obtain the i-th literal of the constraint
get(int) - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
to obtain the i-th literal of the constraint
get(int) - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
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
getActivity() - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
to obtain the activity value of the constraint
getActivity() - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
to obtain the activity value of the constraint
getASolution() - Method in class org.sat4j.pb.tools.DependencyHelper
Retrieve a collection of objects satisfying the constraints.
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.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.UnitClausesPB
 
getCoef(int) - Method in class org.sat4j.pb.constraints.pb.WatchPb
to obtain the coefficient of the i-th literal of the constraint
getCoef(int) - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
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.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.UnitClausesPB
 
getCoefs() - Method in class org.sat4j.pb.constraints.pb.WatchPb
to obtain the coefficients of the constraint.
getCoefs() - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
to obtain the coefficients of the constraint.
getCorrection() - Method in class org.sat4j.pb.ObjectiveFunction
 
getCurrentObjectiveValue() - Method in class org.sat4j.pb.OptToPBSATAdapter
Return the value of the objective function in the last model found.
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.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.UnitClausesPB
 
getDegree() - Method in class org.sat4j.pb.constraints.pb.WatchPb
 
getDegree() - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
 
getExplanation() - Method in class org.sat4j.pb.LPStringSolver
 
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
 
getIntValue(T) - Method in class org.sat4j.pb.tools.DependencyHelper
Translate a domain object into a dimacs variable.
getIntValue(T, boolean) - Method in class org.sat4j.pb.tools.DependencyHelper
Translate a domain object into a dimacs variable.
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 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.UnitClausesPB
 
getLits() - Method in class org.sat4j.pb.constraints.pb.WatchPb
to obtain the literals of the constraint.
getLits() - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
to obtain the literals of the constraint.
getLits() - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
to obtain the literals of the constraint.
getLogPrefix() - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
getLongCoefs() - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
 
getMappingToDomain() - Method in class org.sat4j.pb.tools.DependencyHelper
 
getNormalizer() - Method in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory
 
getNumberOfConstraints() - Method in class org.sat4j.pb.tools.DependencyHelper
 
getNumberOfReductions() - Method in class org.sat4j.pb.constraints.pb.ConflictMap
 
getNumberOfVariables() - Method in class org.sat4j.pb.tools.DependencyHelper
 
getObjectiveFunction() - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
getObjectiveFunction() - Method in class org.sat4j.pb.core.PBSolver
 
getObjectiveFunction() - Method in interface org.sat4j.pb.IPBSolver
Retrieve the objective function from the solver.
getObjectiveFunction() - Method in interface org.sat4j.pb.IPBSolverService
 
getObjectiveFunction() - Method in class org.sat4j.pb.LPStringSolver
 
getObjectiveFunction() - Method in class org.sat4j.pb.OPBStringSolver
 
getObjectiveFunction() - Method in class org.sat4j.pb.PBSolverDecorator
 
getObjectiveFunction() - Method in class org.sat4j.pb.PseudoBitsAdderDecorator
 
getObjectiveFunction() - Method in class org.sat4j.pb.reader.OPBReader2005
 
getObjectiveFunction() - Method in class org.sat4j.pb.tools.ClausalConstraintsDecorator
 
getObjectiveFunction() - Method in class org.sat4j.pb.tools.DependencyHelper
 
getObjectiveFunction() - Method in class org.sat4j.pb.tools.LexicoDecoratorPB
 
getObjectiveFunction() - Method in class org.sat4j.pb.tools.ManyCorePB
 
getObjectiveFunction() - Method in class org.sat4j.pb.tools.PBAdapter
 
getObjectiveFunction() - Method in class org.sat4j.pb.tools.XplainPB
 
getObjectiveFunction() - Method in class org.sat4j.pb.UserFriendlyPBStringSolver
 
getObjectiveValue() - Method in class org.sat4j.pb.ConstraintRelaxingPseudoOptDecorator
 
getObjectiveValue() - Method in class org.sat4j.pb.PseudoOptDecorator
 
getSearchListener() - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
getSolution() - Method in class org.sat4j.pb.tools.DependencyHelper
Retrieve the solution found.
getSolutionCost() - Method in class org.sat4j.pb.tools.DependencyHelper
 
getSolver() - Method in class org.sat4j.pb.tools.DependencyHelper
 
getSolvingEngine() - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
getStat() - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
getTimeout() - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
getTimeoutMs() - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
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 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.UnitClausesPB
 
getVocabulary() - Method in class org.sat4j.pb.constraints.pb.WatchPb
 
getVocabulary() - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
 
getVocabulary() - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
 
getWeight() - Method in class org.sat4j.pb.tools.WeightedObject
 

H

halfOr(C, T, T...) - Method in class org.sat4j.pb.tools.DependencyHelper
Create a constraint of the form thing <= (thing1 or thing 2 ... or thingn)
handleFileName(String, String) - Method in class org.sat4j.pb.reader.PBInstanceReader
 
handleNotHandled(String) - Method in class org.sat4j.pb.reader.JSONPBReader
 
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
 
hasBeenReduced - Variable in class org.sat4j.pb.constraints.pb.ConflictMap
 
hasBeenReduced() - Method in class org.sat4j.pb.constraints.pb.ConflictMap
 
hashCode() - Method in class org.sat4j.pb.constraints.pb.WatchPb
 
hashCode() - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
 
hashCode() - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
 
hashCode() - Method in class org.sat4j.pb.ObjectiveFunction
 
hashCode() - Method in class org.sat4j.pb.tools.WeightedObject
 
hasNoObjectiveFunction() - Method in class org.sat4j.pb.ConstraintRelaxingPseudoOptDecorator
 
hasNoObjectiveFunction() - Method in class org.sat4j.pb.PseudoOptDecorator
 
hasObjectiveFunction() - Method in class org.sat4j.pb.reader.PBInstanceReader
 
hasObjFunc - Variable in class org.sat4j.pb.reader.OPBReader2005
 
hasVariablesExplanation - Variable in class org.sat4j.pb.reader.OPBReader2005
 

I

ICardConstructor - Interface in org.sat4j.pb.constraints
 
IClauseConstructor - Interface in org.sat4j.pb.constraints
 
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
 
impliedBy(Collection<T>, Collection<T>, Collection<T>) - Method in class org.sat4j.pb.tools.DependencyHelper
Compute the objects implied by the assumptions.
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
incActivity(double) - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
increase activity value of the constraint
incActivity(double) - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
increase activity value of the constraint
increaseWeight(BigInteger) - Method in class org.sat4j.pb.tools.WeightedObject
 
INegator - Interface in org.sat4j.pb.tools
 
init() - Method in class org.sat4j.pb.orders.VarOrderHeapObjective
 
init(IPBSolverService) - Method in class org.sat4j.pb.tools.SearchOptimizerListener
 
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
 
IOrderObjective - Interface in org.sat4j.pb.orders
 
IPBCDCLSolver<D extends PBDataStructureFactory> - Interface in org.sat4j.pb.core
Abstraction for Conflict Driven Clause Learning PBSolver.
IPBConstructor - Interface in org.sat4j.pb.constraints
 
IPBSolver - Interface in org.sat4j.pb
A solver able to deal with pseudo boolean constraints.
IPBSolverService - Interface in org.sat4j.pb
 
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
isAssertive(int) - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
This predicate tests wether the constraint is assertive at decision level dl
isAssertive(int) - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
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
 
isCardinality(IVecInt) - Static method in class org.sat4j.pb.tools.ClausalConstraintsDecorator
 
isCardinality(IVec<BigInteger>) - Static method in class org.sat4j.pb.tools.ClausalConstraintsDecorator
 
isDBSimplificationAllowed() - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
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
 
isLongSufficient() - Method in interface org.sat4j.pb.constraints.pb.IDataStructurePB
 
isLongSufficient() - Method in class org.sat4j.pb.constraints.pb.MapPb
 
isNegated(Object) - Method in interface org.sat4j.pb.tools.INegator
 
isNegated(Object) - Method in class org.sat4j.pb.tools.StringNegator
 
isOptimal() - Method in class org.sat4j.pb.ConstraintRelaxingPseudoOptDecorator
 
isOptimal() - Method in class org.sat4j.pb.OptToPBSATAdapter
 
isOptimal() - Method in class org.sat4j.pb.PseudoOptDecorator
 
isOptimal() - Method in class org.sat4j.pb.tools.LexicoHelper
 
isSatisfiable() - Method in class org.sat4j.pb.ConstraintRelaxingPseudoOptDecorator
 
isSatisfiable(boolean) - Method in class org.sat4j.pb.ConstraintRelaxingPseudoOptDecorator
 
isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.pb.ConstraintRelaxingPseudoOptDecorator
 
isSatisfiable(IVecInt) - Method in class org.sat4j.pb.ConstraintRelaxingPseudoOptDecorator
 
isSatisfiable() - Method in class org.sat4j.pb.constraints.pb.WatchPb
tests if the constraint is still satisfiable.
isSatisfiable() - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
tests if the constraint is still satisfiable.
isSatisfiable() - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
tests if the constraint is still satisfiable.
isSatisfiable() - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
isSatisfiable(boolean) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
isSatisfiable(IVecInt) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
isSatisfiable(IVecInt) - Method in class org.sat4j.pb.LPStringSolver
 
isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.pb.LPStringSolver
 
isSatisfiable(IVecInt) - Method in class org.sat4j.pb.OPBStringSolver
 
isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.pb.OPBStringSolver
 
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.PseudoBitsAdderDecorator
 
isSatisfiable(IVecInt) - Method in class org.sat4j.pb.PseudoBitsAdderDecorator
 
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
 
isSolverKeptHot() - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
isVerbose() - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
IWatchPb - Interface in org.sat4j.pb.constraints.pb
 

J

JSONPBReader - Class in org.sat4j.pb.reader
Simple JSON reader for boolean optimization problems.
JSONPBReader(IPBSolver) - Constructor for class org.sat4j.pb.reader.JSONPBReader
 

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
 
LanceurPseudo2007(ASolverFactory<IPBSolver>) - Constructor for class org.sat4j.pb.LanceurPseudo2007
 
LanceurPseudo2007Eclipse - Class in org.sat4j.pb
 
LanceurPseudo2007Eclipse() - Constructor for class org.sat4j.pb.LanceurPseudo2007Eclipse
 
learn(IConstr) - Method in class org.sat4j.pb.tools.ConflictTracing
 
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 constraint ?
learnt - Variable in class org.sat4j.pb.constraints.pb.WatchPbLong
true if the constraint is a learned constraint
learnt() - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
is the constraint a learnt constraint ?
learnt - Variable in class org.sat4j.pb.constraints.pb.WatchPbLongCP
true if the constraint is a learned constraint
learnt() - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
is the constraint a learnt constraint ?
learntAtLeastConstraintFactory(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure
 
learntAtLeastConstraintFactory(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory
 
learntAtLeastConstraintFactory(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.constraints.PBMaxDataStructure
 
learntAtLeastConstraintFactory(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.constraints.PBMinDataStructure
 
learntAtLeastConstraintFactory(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.constraints.PuebloPBMinDataStructure
 
learntAtMostConstraintFactory(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure
 
learntAtMostConstraintFactory(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory
 
learntAtMostConstraintFactory(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.constraints.PBMaxDataStructure
 
learntAtMostConstraintFactory(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.constraints.PBMinDataStructure
 
learntAtMostConstraintFactory(IVecInt, IVec<BigInteger>, BigInteger) - Method in class org.sat4j.pb.constraints.PuebloPBMinDataStructure
 
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
 
LexicoDecoratorPB - Class in org.sat4j.pb.tools
 
LexicoDecoratorPB(IPBSolver) - Constructor for class org.sat4j.pb.tools.LexicoDecoratorPB
 
LexicoHelper<T,C> - Class in org.sat4j.pb.tools
 
LexicoHelper(IPBSolver) - Constructor for class org.sat4j.pb.tools.LexicoHelper
 
LexicoHelper(IPBSolver, boolean, boolean) - Constructor for class org.sat4j.pb.tools.LexicoHelper
 
LexicoHelper(IPBSolver, boolean) - Constructor for class org.sat4j.pb.tools.LexicoHelper
 
lightSolver() - Method in class org.sat4j.pb.SolverFactory
 
LIMIT_FOR_MAP - Static variable in class org.sat4j.pb.constraints.pb.MaxWatchPb
 
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
lits - Variable in class org.sat4j.pb.constraints.pb.WatchPbLong
literals of the constraint
lits - Variable in class org.sat4j.pb.constraints.pb.WatchPbLongCP
literals of the constraint
lits - Variable in class org.sat4j.pb.reader.OPBReader2005
 
locked() - Method in class org.sat4j.pb.constraints.pb.WatchPb
The constraint is the reason of a unit propagation.
locked() - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
The constraint is the reason of a unit propagation.
locked() - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
The constraint is the reason of a unit propagation.
LPStringSolver - Class in org.sat4j.pb
Solver used to display in a string the pb-instance in OPB format.
LPStringSolver() - Constructor for class org.sat4j.pb.LPStringSolver
 
LPStringSolver(int) - Constructor for class org.sat4j.pb.LPStringSolver
 

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
main(String[]) - Static method in class org.sat4j.pb.PseudoBitsAdderDecorator
 
ManyCorePB - Class in org.sat4j.pb.tools
 
ManyCorePB(ASolverFactory<IPBSolver>, String...) - Constructor for class org.sat4j.pb.tools.ManyCorePB
 
ManyCorePB(IPBSolver...) - Constructor for class org.sat4j.pb.tools.ManyCorePB
 
MapPb - Class in org.sat4j.pb.constraints.pb
 
MapPb(IVecInt, IVec<BigInteger>, BigInteger) - Constructor for class org.sat4j.pb.constraints.pb.MapPb
 
MAXCONFLICTS - Static variable in class org.sat4j.pb.core.PBSolverResCP
 
maximalCoefficient(int) - Method in class org.sat4j.pb.constraints.pb.MinWatchPb
the maximal coefficient for the watched literals
maximalCoefficient(int) - Method in class org.sat4j.pb.constraints.pb.MinWatchPbLong
the maximal coefficient for the watched literals
maximalCoefficient(int) - Method in class org.sat4j.pb.constraints.pb.MinWatchPbLongCP
the maximal coefficient for the watched literals
maximalCoefficient(int) - Method in class org.sat4j.pb.constraints.pb.PuebloMinWatchPb
 
MaxLongWatchPBConstructor - Class in org.sat4j.pb.constraints
 
MaxLongWatchPBConstructor() - Constructor for class org.sat4j.pb.constraints.MaxLongWatchPBConstructor
 
MaxLongWatchPBCPConstructor - Class in org.sat4j.pb.constraints
 
MaxLongWatchPBCPConstructor() - Constructor for class org.sat4j.pb.constraints.MaxLongWatchPBCPConstructor
 
MaxWatchPb - Class in org.sat4j.pb.constraints.pb
Data structure for pseudo-boolean constraint with watched literals.
MaxWatchPBConstructor - Class in org.sat4j.pb.constraints
 
MaxWatchPBConstructor() - Constructor for class org.sat4j.pb.constraints.MaxWatchPBConstructor
 
MaxWatchPbLong - Class in org.sat4j.pb.constraints.pb
Data structure for pseudo-boolean constraint with watched literals.
MaxWatchPbLongCP - Class in org.sat4j.pb.constraints.pb
Data structure for pseudo-boolean constraint with watched literals.
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
MinCardConstructor - Class in org.sat4j.pb.constraints
 
MinCardConstructor() - Constructor for class org.sat4j.pb.constraints.MinCardConstructor
 
MinCardPBConstructor - Class in org.sat4j.pb.constraints
 
MinCardPBConstructor() - Constructor for class org.sat4j.pb.constraints.MinCardPBConstructor
 
MinLongWatchPBConstructor - Class in org.sat4j.pb.constraints
 
MinLongWatchPBConstructor() - Constructor for class org.sat4j.pb.constraints.MinLongWatchPBConstructor
 
MinLongWatchPBCPConstructor - Class in org.sat4j.pb.constraints
 
MinLongWatchPBCPConstructor() - Constructor for class org.sat4j.pb.constraints.MinLongWatchPBCPConstructor
 
minValue() - Method in class org.sat4j.pb.ObjectiveFunction
 
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
Data structure for pseudo-boolean constraint with watched literals.
MinWatchPb(ILits, IDataStructurePB) - Constructor for class org.sat4j.pb.constraints.pb.MinWatchPb
Basic constructor for pb constraint a0.x0 + a1.x1 + ... + an.xn >= k This constructor is called for learnt pseudo boolean constraints.
MinWatchPb(ILits, int[], BigInteger[], BigInteger, BigInteger) - Constructor for class org.sat4j.pb.constraints.pb.MinWatchPb
Basic constructor for PB constraint a0.x0 + a1.x1 + ... + an.xn >= k
MinWatchPBConstructor - Class in org.sat4j.pb.constraints
 
MinWatchPBConstructor() - Constructor for class org.sat4j.pb.constraints.MinWatchPBConstructor
 
MinWatchPbLong - Class in org.sat4j.pb.constraints.pb
Data structure for pseudo-boolean constraint with watched literals.
MinWatchPbLong(ILits, IDataStructurePB) - Constructor for class org.sat4j.pb.constraints.pb.MinWatchPbLong
Basic constructor for pb constraint a0.x0 + a1.x1 + ... + an.xn >= k This constructor is called for learnt pseudo boolean constraints.
MinWatchPbLong(ILits, int[], BigInteger[], BigInteger, BigInteger) - Constructor for class org.sat4j.pb.constraints.pb.MinWatchPbLong
Basic constructor for PB constraint a0.x0 + a1.x1 + ... + an.xn >= k
MinWatchPbLongCP - Class in org.sat4j.pb.constraints.pb
Data structure for pseudo-boolean constraint with watched literals.
MinWatchPbLongCP(ILits, IDataStructurePB) - Constructor for class org.sat4j.pb.constraints.pb.MinWatchPbLongCP
Basic constructor for pb constraint a0.x0 + a1.x1 + ... + an.xn >= k This constructor is called for learnt pseudo boolean constraints.
MinWatchPbLongCP(ILits, int[], BigInteger[], BigInteger, BigInteger) - Constructor for class org.sat4j.pb.constraints.pb.MinWatchPbLongCP
Basic constructor for PB constraint a0.x0 + a1.x1 + ... + an.xn >= k
model() - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
model(int) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
model() - Method in class org.sat4j.pb.OptToPBSATAdapter
 
model(PrintWriter) - Method in class org.sat4j.pb.OptToPBSATAdapter
Compute a minimal model according to the objective function of the IPBProblem decorated.
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
 
modelWithInternalVariables() - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
modelWithInternalVariables() - 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
 
nbNewSymbols - Variable in class org.sat4j.pb.reader.OPBReader2007
contains the number of new symbols generated to linearize products
nbOfWatched() - Method in class org.sat4j.pb.constraints.pb.MinWatchPb
Number of really watched literals.
nbOfWatched() - Method in class org.sat4j.pb.constraints.pb.MinWatchPbLong
Number of really watched literals.
nbOfWatched() - Method in class org.sat4j.pb.constraints.pb.MinWatchPbLongCP
Number of really watched literals.
nbVars - Variable in class org.sat4j.pb.reader.OPBReader2005
 
nConstraints() - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
nConstraints() - Method in class org.sat4j.pb.LPStringSolver
 
nConstraints() - Method in class org.sat4j.pb.OPBStringSolver
 
negateLiteralInAProduct(String, IVecInt) - Method in class org.sat4j.pb.reader.OPBReader2007
callback called when we read a term of a constraint
newBoth() - Static method in class org.sat4j.pb.SolverFactory
Resolution and CuttingPlanes based solvers running in parallel.
newCompetMinPBResLongWLMixedConstraintsObjectiveExpSimp() - Static method in class org.sat4j.pb.SolverFactory
 
newCompetPBCPMixedConstraintsLongMaxObjective() - Static method in class org.sat4j.pb.SolverFactory
 
newCompetPBCPMixedConstraintsLongMinObjective() - Static method in class org.sat4j.pb.SolverFactory
 
newCompetPBCPMixedConstraintsMinObjective() - Static method in class org.sat4j.pb.SolverFactory
 
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
 
newCompetPBResHTMixedConstraintsObjectiveExpSimp() - Static method in class org.sat4j.pb.SolverFactory
 
newCompetPBResLongHTMixedConstraintsObjectiveExpSimp() - Static method in class org.sat4j.pb.SolverFactory
 
newCompetPBResLongWLMixedConstraintsObjectiveExpSimp() - 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(PBDataStructureFactory) - Static method in class org.sat4j.pb.SolverFactory
 
newCompetPBResMixedConstraintsObjectiveExpSimp() - Static method in class org.sat4j.pb.SolverFactory
 
newCompetPBResWLMixedConstraintsObjectiveExpSimp() - Static method in class org.sat4j.pb.SolverFactory
 
newCuttingPlanes() - Static method in class org.sat4j.pb.SolverFactory
Cutting Planes based solver.
newCuttingPlanesAggressiveCleanup() - 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.
newDefaultOptimizer() - Static method in class org.sat4j.pb.SolverFactory
Provides the best available PB solver of the library ready to solve optimization problems.
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
 
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
 
newPBCPMixedConstraintsCautious(int) - Static method in class org.sat4j.pb.SolverFactory
 
newPBCPMixedConstraintsCautious() - 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
 
newPBCPMixedConstraintsResCP(long) - Static method in class org.sat4j.pb.SolverFactory
 
newPBCPMixedConstraintsResCP() - 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.
newResolutionGlucose() - Static method in class org.sat4j.pb.SolverFactory
Resolution based solver (i.e. classic SAT solver able to handle generic constraints.
newResolutionGlucose21() - Static method in class org.sat4j.pb.SolverFactory
Resolution based solver (i.e. classic SAT solver able to handle generic constraints.
newResolutionGlucoseExpSimp() - Static method in class org.sat4j.pb.SolverFactory
Resolution based solver (i.e. classic SAT solver able to handle generic constraints.
newResolutionGlucoseSimpleSimp() - Static method in class org.sat4j.pb.SolverFactory
Resolution based solver (i.e. classic SAT solver able to handle generic constraints.
newResolutionMaxMemory() - Static method in class org.sat4j.pb.SolverFactory
Resolution based solver (i.e. classic SAT solver able to handle generic constraints.
newResolutionSimpleRestarts() - Static method in class org.sat4j.pb.SolverFactory
Resolution based solver (i.e. classic SAT solver able to handle generic constraints.
newSAT() - Static method in class org.sat4j.pb.SolverFactory
That solver is expected to perform better on satisfiable benchmarks.
newSATUNSAT() - Static method in class org.sat4j.pb.SolverFactory
Two solvers are running in //: one for solving SAT instances, the other one for solving unsat instances.
newSimpleSimplification() - Static method in class org.sat4j.pb.SolverFactory
Resolution based solver (i.e. classic SAT solver able to handle generic constraints.
newUNSAT() - Static method in class org.sat4j.pb.SolverFactory
That solver is expected to perform better on unsatisfiable benchmarks.
newVar() - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
newVar(int) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
newVar(int) - Method in class org.sat4j.pb.LPStringSolver
 
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, long) - Static method in class org.sat4j.pb.tools.WeightedObject
 
newWO(E, BigInteger) - Static method in class org.sat4j.pb.tools.WeightedObject
 
nextFreeVarId(boolean) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
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 - Static variable in class org.sat4j.pb.tools.DependencyHelper
 
nonOptimalMeansSatisfiable() - Method in class org.sat4j.pb.ConstraintRelaxingPseudoOptDecorator
 
nonOptimalMeansSatisfiable() - Method in class org.sat4j.pb.PseudoOptDecorator
 
normalizedMaxWatchPbNew(UnitPropagationListener, ILits, int[], BigInteger[], BigInteger, BigInteger) - Static method in class org.sat4j.pb.constraints.pb.MaxWatchPb
build a pseudo boolean constraint.
normalizedMaxWatchPbNew(UnitPropagationListener, ILits, int[], BigInteger[], BigInteger, BigInteger) - Static method in class org.sat4j.pb.constraints.pb.MaxWatchPbLong
build a pseudo boolean constraint.
normalizedMaxWatchPbNew(UnitPropagationListener, ILits, int[], BigInteger[], BigInteger, BigInteger) - Static method in class org.sat4j.pb.constraints.pb.MaxWatchPbLongCP
build a pseudo boolean constraint.
normalizedMinWatchCardPBNew(UnitPropagationListener, ILits, IVecInt, int) - Static method in class org.sat4j.pb.constraints.pb.MinWatchCardPB
Permet la cr?
normalizedMinWatchPbNew(UnitPropagationListener, ILits, int[], BigInteger[], BigInteger, BigInteger) - Static method in class org.sat4j.pb.constraints.pb.MinWatchPb
build a pseudo boolean constraint.
normalizedMinWatchPbNew(UnitPropagationListener, ILits, int[], BigInteger[], BigInteger, BigInteger) - Static method in class org.sat4j.pb.constraints.pb.MinWatchPbLong
build a pseudo boolean constraint.
normalizedMinWatchPbNew(UnitPropagationListener, ILits, int[], BigInteger[], BigInteger, BigInteger) - Static method in class org.sat4j.pb.constraints.pb.MinWatchPbLongCP
build a pseudo boolean constraint.
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
build a pseudo boolean constraint from a specific data structure.
normalizedWatchPbNew(ILits, IDataStructurePB) - Static method in class org.sat4j.pb.constraints.pb.MaxWatchPbLong
build a pseudo boolean constraint from a specific data structure.
normalizedWatchPbNew(ILits, IDataStructurePB) - Static method in class org.sat4j.pb.constraints.pb.MaxWatchPbLongCP
build a pseudo boolean constraint from a specific data structure.
normalizedWatchPbNew(ILits, IDataStructurePB) - Static method in class org.sat4j.pb.constraints.pb.MinWatchPb
build a pseudo boolean constraint from a specific data structure.
normalizedWatchPbNew(ILits, IDataStructurePB) - Static method in class org.sat4j.pb.constraints.pb.MinWatchPbLong
build a pseudo boolean constraint from a specific data structure.
normalizedWatchPbNew(ILits, IDataStructurePB) - Static method in class org.sat4j.pb.constraints.pb.MinWatchPbLongCP
build a pseudo boolean constraint from a specific data structure.
normalizedWatchPbNew(ILits, IDataStructurePB) - Static method in class org.sat4j.pb.constraints.pb.PuebloMinWatchPb
 
normalizeObjective(ObjectiveFunction) - Static method in class org.sat4j.pb.constraints.pb.Pseudos
 
not(T) - Method in class org.sat4j.pb.tools.DependencyHelper
 
numberOfCP - Variable in class org.sat4j.pb.core.PBSolverStats
 
numberOfCriteria() - Method in class org.sat4j.pb.tools.LexicoDecoratorPB
 
numberOfLearnedConstraintsReduced - Variable in class org.sat4j.pb.core.PBSolverStats
 
numberOfReductions - Variable in class org.sat4j.pb.constraints.pb.ConflictMap
 
numberOfReductions - Variable in class org.sat4j.pb.core.PBSolverStats
 
numberOfResolution - Variable in class org.sat4j.pb.core.PBSolverStats
 
nVars() - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 

O

obfct - Variable in class org.sat4j.pb.LanceurPseudo2005
 
OBJECTIVE_FUNCTION - Static variable in class org.sat4j.pb.reader.JSONPBReader
 
OBJECTIVE_FUNCTION_PATTERN - Static variable in class org.sat4j.pb.reader.JSONPBReader
 
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
 
objectiveFunctionBased - Variable in class org.sat4j.pb.core.PBSolver
 
objectiveFunctionToLP(ObjectiveFunction, StringBuffer) - Method in class org.sat4j.pb.LPStringSolver
 
ObjectiveReducerPBSolverDecorator - Class in org.sat4j.pb.core
 
ObjectiveReducerPBSolverDecorator(IPBSolver) - Constructor for class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
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
 
OPBReader2010 - Class in org.sat4j.pb.reader
 
OPBReader2010(IPBSolver) - Constructor for class org.sat4j.pb.reader.OPBReader2010
 
OPBReader2012 - Class in org.sat4j.pb.reader
OPBReader allowing to read several objective functions in an OPB file.
OPBReader2012(IPBSolver) - Constructor for class org.sat4j.pb.reader.OPBReader2012
 
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
 
operator - Variable in class org.sat4j.pb.reader.OPBReader2005
 
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
Implementations of pseudo boolean solvers
org.sat4j.pb.constraints - package org.sat4j.pb.constraints
Implementation of data structures for pseudo boolean constraints.
org.sat4j.pb.constraints.pb - package org.sat4j.pb.constraints.pb
Implementations of pseudo boolean constraints.
org.sat4j.pb.core - package org.sat4j.pb.core
Implementations of pseudo boolean solvers
org.sat4j.pb.orders - package org.sat4j.pb.orders
Various heuristics for the next variable to branch on.
org.sat4j.pb.reader - package org.sat4j.pb.reader
Readers for opb instances.
org.sat4j.pb.tools - package org.sat4j.pb.tools
Implementation of different tools for pseudo boolean solvers
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(LineNumberReader) - Method in class org.sat4j.pb.reader.OPBReader2005
 
parseInstance(InputStream) - Method in class org.sat4j.pb.reader.OPBReader2005
 
parseInstance(Reader) - Method in class org.sat4j.pb.reader.OPBReader2010
 
parseInstance(Reader) - Method in class org.sat4j.pb.reader.OPBReader2012
 
PB - Static variable in class org.sat4j.pb.reader.JSONPBReader
 
PBAdapter - Class in org.sat4j.pb.tools
Allow to put a ISolver when an IPBSolver is required.
PBAdapter(ISolver) - Constructor for class org.sat4j.pb.tools.PBAdapter
 
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
 
PBLongMaxClauseCardConstrDataStructure - Class in org.sat4j.pb.constraints
 
PBLongMaxClauseCardConstrDataStructure() - Constructor for class org.sat4j.pb.constraints.PBLongMaxClauseCardConstrDataStructure
 
PBLongMinClauseCardConstrDataStructure - Class in org.sat4j.pb.constraints
 
PBLongMinClauseCardConstrDataStructure() - Constructor for class org.sat4j.pb.constraints.PBLongMinClauseCardConstrDataStructure
 
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(LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, IOrder, RestartStrategy) - Constructor for class org.sat4j.pb.core.PBSolver
 
PBSolver(LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, SearchParams, IOrder, RestartStrategy) - Constructor for class org.sat4j.pb.core.PBSolver
 
PBSolverCautious - Class in org.sat4j.pb.core
 
PBSolverCautious(LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, IOrder) - Constructor for class org.sat4j.pb.core.PBSolverCautious
 
PBSolverCautious(LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, IOrder, int) - Constructor for class org.sat4j.pb.core.PBSolverCautious
 
PBSolverClause - Class in org.sat4j.pb.core
 
PBSolverClause(LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, IOrder) - Constructor for class org.sat4j.pb.core.PBSolverClause
 
PBSolverCP - Class in org.sat4j.pb.core
 
PBSolverCP(LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, IOrder) - Constructor for class org.sat4j.pb.core.PBSolverCP
 
PBSolverCP(LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, SearchParams, IOrder, RestartStrategy) - Constructor for class org.sat4j.pb.core.PBSolverCP
 
PBSolverCP(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
 
PBSolverResCP - Class in org.sat4j.pb.core
 
PBSolverResCP(LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, IOrder) - Constructor for class org.sat4j.pb.core.PBSolverResCP
 
PBSolverResCP(LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, IOrder, long) - Constructor for class org.sat4j.pb.core.PBSolverResCP
 
PBSolverResCP(LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, SearchParams, IOrder, RestartStrategy) - Constructor for class org.sat4j.pb.core.PBSolverResCP
 
PBSolverResCP(LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, SearchParams, IOrder) - Constructor for class org.sat4j.pb.core.PBSolverResCP
 
PBSolverResolution - Class in org.sat4j.pb.core
 
PBSolverResolution(LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, SearchParams, IOrder, RestartStrategy) - Constructor for class org.sat4j.pb.core.PBSolverResolution
 
PBSolverResolution(LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, IOrder, RestartStrategy) - Constructor for class org.sat4j.pb.core.PBSolverResolution
 
PBSolverStats - Class in org.sat4j.pb.core
 
PBSolverStats() - Constructor for class org.sat4j.pb.core.PBSolverStats
 
PBSolverWithImpliedClause - Class in org.sat4j.pb.core
 
PBSolverWithImpliedClause(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
ppcm : least common multiple for two integers (plus petit commun multiple)
ppcm(BigInteger, BigInteger) - Static method in class org.sat4j.pb.constraints.pb.WatchPbLong
ppcm : least common multiple for two integers (plus petit commun multiple)
ppcm(BigInteger, BigInteger) - Static method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
ppcm : least common multiple for two integers (plus petit commun multiple)
primeImplicant() - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
primeImplicant(int) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
printInfos(PrintWriter, String) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
printInfos(PrintWriter) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
printStat(PrintStream, String) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
printStat(PrintWriter, String) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
printStat(PrintWriter) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
printStat(PrintWriter, String) - Method in class org.sat4j.pb.core.PBSolverStats
 
propagate(UnitPropagationListener, int) - Method in class org.sat4j.pb.constraints.pb.MaxWatchPb
Propagation of a falsified literal
propagate(UnitPropagationListener, int) - Method in class org.sat4j.pb.constraints.pb.MaxWatchPbLong
Propagation of a falsified literal
propagate(UnitPropagationListener, int) - Method in class org.sat4j.pb.constraints.pb.MaxWatchPbLongCP
Propagation of a falsified literal
propagate(UnitPropagationListener, int) - Method in class org.sat4j.pb.constraints.pb.MinWatchPb
Propagation of a falsified literal
propagate(UnitPropagationListener, int) - Method in class org.sat4j.pb.constraints.pb.MinWatchPbLong
Propagation of a falsified literal
propagate(UnitPropagationListener, int) - Method in class org.sat4j.pb.constraints.pb.MinWatchPbLongCP
Propagation of a falsified literal
propagate(UnitPropagationListener, int) - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
 
PSEUDO_PATTERN - Static variable in class org.sat4j.pb.reader.JSONPBReader
 
PseudoBitsAdderDecorator - Class in org.sat4j.pb
A decorator that computes minimal pseudo boolean models.
PseudoBitsAdderDecorator(IPBSolver) - Constructor for class org.sat4j.pb.PseudoBitsAdderDecorator
 
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
Create a PB decorator for which a non optimal solution means that the problem is satisfiable.
PseudoOptDecorator(IPBSolver, boolean) - Constructor for class org.sat4j.pb.PseudoOptDecorator
Create a PB decorator with a specific semantic of non optimal solution.
PseudoOptDecorator(IPBSolver, boolean, boolean) - Constructor for class org.sat4j.pb.PseudoOptDecorator
Create a PB decorator with a specific semantic of non optimal solution.
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
 
PuebloMinWatchPBConstructor - Class in org.sat4j.pb.constraints
 
PuebloMinWatchPBConstructor() - Constructor for class org.sat4j.pb.constraints.PuebloMinWatchPBConstructor
 
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

RandomWalkDecoratorObjective - Class in org.sat4j.pb.orders
 
RandomWalkDecoratorObjective(VarOrderHeapObjective, double) - Constructor for class org.sat4j.pb.orders.RandomWalkDecoratorObjective
 
readConstraint() - Method in class org.sat4j.pb.reader.OPBReader2005
read a constraint calls beginConstraint, constraintTerm and endConstraint
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
readMetaData() - Method in class org.sat4j.pb.reader.OPBReader2010
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.OPBReader2012
 
readObjective() - Method in class org.sat4j.pb.reader.OPBReader2005
read the objective line (if any) calls beginObjective, objectiveTerm and endObjective
readObjective() - Method in class org.sat4j.pb.reader.OPBReader2010
 
readObjective() - Method in class org.sat4j.pb.reader.OPBReader2012
 
readProblem(String) - Method in class org.sat4j.pb.LanceurPseudo2005
 
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
realNumberOfVariables() - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
reduceInConstraint(IWatchPb, BigInteger[], int, BigInteger) - Method in class org.sat4j.pb.constraints.pb.ConflictMap
constraint reduction : removes a literal of the constraint.
reduceInConstraint(IWatchPb, 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[], IWatchPb) - Method in class org.sat4j.pb.constraints.pb.ConflictMap
 
reduceUntilConflict(int, int, BigInteger[], IWatchPb) - 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[], IWatchPb) - Method in class org.sat4j.pb.constraints.pb.ConflictMapSwitchToClause
reduces the constraint defined by wpb until the result of the cutting plane is a conflict. this reduction returns either a clause if .
register() - Method in class org.sat4j.pb.constraints.pb.MinWatchCardPB
 
register() - Method in class org.sat4j.pb.constraints.pb.WatchPb
 
register() - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
 
register() - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
 
registerLiteral(int) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
remove(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.MaxWatchPb
Remove a constraint from the solver
remove(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.MaxWatchPbLong
Remove a constraint from the solver
remove(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.MaxWatchPbLongCP
Remove a constraint from the solver
remove(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.MinWatchPb
Remove the constraint from the solver
remove(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.MinWatchPbLong
Remove the constraint from the solver
remove(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.MinWatchPbLongCP
Remove the constraint from the solver
remove(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
 
removeConstr(IConstr) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
removeSubsumedConstr(IConstr) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
rescaleBy(double) - Method in class org.sat4j.pb.constraints.pb.WatchPb
to re-scale the activity of the constraint
rescaleBy(double) - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
to re-scale the activity of the constraint
rescaleBy(double) - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
to re-scale the activity of the constraint
reset() - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
reset() - Method in class org.sat4j.pb.core.PBSolverStats
 
reset() - Method in class org.sat4j.pb.PseudoOptDecorator
 
reset() - Method in class org.sat4j.pb.tools.DependencyHelper
Reset the state of the helper (mapping, objective function, etc).
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

SAT4J_MAX_BIG_INTEGER - Static variable in class org.sat4j.pb.reader.OPBReader2010
 
saturation() - Method in interface org.sat4j.pb.constraints.pb.IDataStructurePB
 
saturation() - Method in class org.sat4j.pb.constraints.pb.MapPb
 
SearchOptimizerListener - Class in org.sat4j.pb.tools
 
SearchOptimizerListener(SolutionFoundListener) - Constructor for class org.sat4j.pb.tools.SearchOptimizerListener
 
setActivity(double) - Method in class org.sat4j.pb.constraints.pb.WatchPb
 
setActivity(double) - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
 
setActivity(double) - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
 
setCorrection(BigInteger) - Method in class org.sat4j.pb.ObjectiveFunction
 
setDBSimplificationAllowed(boolean) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
setExpectedNumberOfClauses(int) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
setExpectedNumberOfClauses(int) - Method in class org.sat4j.pb.LPStringSolver
 
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.
setKeepSolverHot(boolean) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
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
the constraint is learnt
setLearnt() - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
the constraint is learnt
setLearnt() - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
the constraint is learnt
setListOfVariablesForExplanation(IVecInt) - Method in class org.sat4j.pb.LPStringSolver
 
setListOfVariablesForExplanation(IVecInt) - Method in class org.sat4j.pb.OPBStringSolver
 
setListOfVariablesForExplanation(IVecInt) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver
 
setLogPrefix(String) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
setMapping(Map<Integer, T>) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver
 
setNegator(INegator) - 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.ObjectiveReducerPBSolverDecorator
 
setObjectiveFunction(ObjectiveFunction) - Method in class org.sat4j.pb.core.PBSolver
 
setObjectiveFunction(ObjectiveFunction) - Method in interface org.sat4j.pb.IPBSolver
Provide an objective function to the solver.
setObjectiveFunction(ObjectiveFunction) - Method in class org.sat4j.pb.LPStringSolver
 
setObjectiveFunction(ObjectiveFunction) - Method in class org.sat4j.pb.OPBStringSolver
 
setObjectiveFunction(ObjectiveFunction) - Method in interface org.sat4j.pb.orders.IOrderObjective
 
setObjectiveFunction(ObjectiveFunction) - Method in class org.sat4j.pb.orders.RandomWalkDecoratorObjective
 
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.PseudoBitsAdderDecorator
 
setObjectiveFunction(ObjectiveFunction) - Method in class org.sat4j.pb.PseudoOptDecorator
 
setObjectiveFunction(ObjectiveFunction) - Method in class org.sat4j.pb.tools.ClausalConstraintsDecorator
 
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.LexicoDecoratorPB
 
setObjectiveFunction(ObjectiveFunction) - Method in class org.sat4j.pb.tools.ManyCorePB
 
setObjectiveFunction(ObjectiveFunction) - Method in class org.sat4j.pb.tools.PBAdapter
 
setObjectiveFunction(ObjectiveFunction) - Method in class org.sat4j.pb.tools.XplainPB
 
setObjectiveFunction(ObjectiveFunction) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver
 
setSearchListener(SearchListener<S>) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
setTimeout(int) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
setTimeout(int) - Method in class org.sat4j.pb.PseudoOptDecorator
 
setTimeoutForFindingBetterSolution(int) - Method in class org.sat4j.pb.ConstraintRelaxingPseudoOptDecorator
 
setTimeoutForFindingBetterSolution(int) - Method in class org.sat4j.pb.OptToPBSATAdapter
Allow to set a specific timeout when the solver is in optimization mode.
setTimeoutForFindingBetterSolution(int) - Method in class org.sat4j.pb.PseudoOptDecorator
 
setTimeoutMs(long) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
setTimeoutOnConflicts(int) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
setTrue(T, C) - Method in class org.sat4j.pb.tools.DependencyHelper
Add a constraint to set the value of a domain object to true.
setVerbose(boolean) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
simplify() - Method in class org.sat4j.pb.constraints.pb.WatchPb
simplify the constraint (if it is satisfied)
simplify() - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
simplify the constraint (if it is satisfied)
simplify() - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
simplify the constraint (if it is satisfied)
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
 
size() - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
 
size() - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
 
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(BigInteger[], BigInteger) - Method in interface org.sat4j.pb.constraints.pb.IWatchPb
 
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
slackConstraint() - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
compute the slack of the current constraint slack = poss - degree of the constraint
slackConstraint(long[], long) - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
compute the slack of a described constraint slack = poss - degree of the constraint
slackConstraint() - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
compute the slack of the current constraint slack = poss - degree of the constraint
slackConstraint(long[], long) - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
compute the slack of a described constraint slack = poss - degree of the constraint
slackConstraint(BigInteger[], BigInteger) - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
 
slackIsCorrect(int) - Method in class org.sat4j.pb.constraints.pb.ConflictMap
 
slackIsCorrect(int) - Method in interface org.sat4j.pb.constraints.pb.IConflict
 
solutionFound(int[], RandomAccessModel) - Method in class org.sat4j.pb.tools.SearchOptimizerListener
 
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
sort() - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
sort coefficient and literal arrays
sort(int, int) - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
sort partially coefficient and literal arrays
sort() - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
sort coefficient and literal arrays
sort(int, int) - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
sort partially coefficient and literal arrays
stats - Variable in class org.sat4j.pb.core.PBSolver
 
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
 
sumcoefs - Variable in class org.sat4j.pb.constraints.pb.WatchPb
 
sumcoefs - Variable in class org.sat4j.pb.constraints.pb.WatchPbLong
 
sumcoefs - Variable in class org.sat4j.pb.constraints.pb.WatchPbLongCP
 
sumOfCoefficients(BigInteger[]) - Static method in class org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure
 

T

thing - Variable in class org.sat4j.pb.tools.WeightedObject
 
toBigInt(int) - Static method in class org.sat4j.pb.constraints.pb.Pseudos
 
toConstraint() - Method in class org.sat4j.pb.constraints.pb.WatchPb
 
toConstraint() - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
 
toConstraint() - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
 
toLong(BigInteger[]) - Static method in class org.sat4j.pb.constraints.pb.WatchPbLong
 
toLong(BigInteger[]) - Static method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
 
toString(String) - Method in class org.sat4j.pb.ConstraintRelaxingPseudoOptDecorator
 
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() - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
 
toString() - Method in class org.sat4j.pb.constraints.pb.WatchPbLongCP
 
toString(String) - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
toString(String) - Method in class org.sat4j.pb.core.PBSolverCautious
 
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.PBSolverWithImpliedClause
 
toString() - Method in class org.sat4j.pb.LPStringSolver
 
toString(String) - Method in class org.sat4j.pb.LPStringSolver
 
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.tools.SearchOptimizerListener
 
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
this method is called during backtrack
undo(int) - Method in class org.sat4j.pb.constraints.pb.MaxWatchPbLong
this method is called during backtrack
undo(int) - Method in class org.sat4j.pb.constraints.pb.MaxWatchPbLongCP
this method is called during backtrack
undo(int) - Method in class org.sat4j.pb.constraints.pb.MinWatchPb
this method is called during backtrack
undo(int) - Method in class org.sat4j.pb.constraints.pb.MinWatchPbLong
this method is called during backtrack
undo(int) - Method in class org.sat4j.pb.constraints.pb.MinWatchPbLongCP
this method is called during backtrack
undo(int) - Method in class org.sat4j.pb.constraints.pb.WatchPbLong
 
UnitBinaryHTClauseConstructor - Class in org.sat4j.pb.constraints
 
UnitBinaryHTClauseConstructor() - Constructor for class org.sat4j.pb.constraints.UnitBinaryHTClauseConstructor
 
UnitBinaryHTClausePBConstructor - Class in org.sat4j.pb.constraints
 
UnitBinaryHTClausePBConstructor() - Constructor for class org.sat4j.pb.constraints.UnitBinaryHTClausePBConstructor
 
UnitBinaryWLClauseConstructor - Class in org.sat4j.pb.constraints
 
UnitBinaryWLClauseConstructor() - Constructor for class org.sat4j.pb.constraints.UnitBinaryWLClauseConstructor
 
UnitClausePB - Class in org.sat4j.pb.constraints.pb
 
UnitClausePB(int, ILits) - Constructor for class org.sat4j.pb.constraints.pb.UnitClausePB
 
UnitClausesPB - Class in org.sat4j.pb.constraints.pb
 
UnitClausesPB(IVecInt) - Constructor for class org.sat4j.pb.constraints.pb.UnitClausesPB
 
unNegate(Object) - Method in interface org.sat4j.pb.tools.INegator
 
unNegate(Object) - Method in class org.sat4j.pb.tools.StringNegator
 
unsatExplanation() - Method in class org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator
 
updateNumberOfReducedLearnedConstraints(IConflict) - Method in class org.sat4j.pb.core.PBSolverCautious
 
updateNumberOfReducedLearnedConstraints(IConflict) - Method in class org.sat4j.pb.core.PBSolverCP
 
updateNumberOfReductions(IConflict) - Method in class org.sat4j.pb.core.PBSolverCautious
 
updateNumberOfReductions(IConflict) - Method in class org.sat4j.pb.core.PBSolverCP
 
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
update arrays watched and watching w.r.t. the propagation of a literal.
updateWatched(long, int) - Method in class org.sat4j.pb.constraints.pb.MinWatchPbLong
update arrays watched and watching w.r.t. the propagation of a literal.
updateWatched(long, int) - Method in class org.sat4j.pb.constraints.pb.MinWatchPbLongCP
update arrays watched and watching w.r.t. the propagation of a literal.
updateWatched(BigInteger, int) - Method in class org.sat4j.pb.constraints.pb.PuebloMinWatchPb
 
UpperBound - Static variable in class org.sat4j.pb.constraints.pb.ConflictMapSwitchToClause
 
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
voc - Variable in class org.sat4j.pb.constraints.pb.WatchPbLong
constraint's vocabulary
voc - Variable in class org.sat4j.pb.constraints.pb.WatchPbLongCP
constraint's vocabulary

W

watchCumul - Variable in class org.sat4j.pb.constraints.pb.MinWatchPb
sum of the coefficients of the literals satisfied or unvalued
watchCumul - Variable in class org.sat4j.pb.constraints.pb.MinWatchPbLong
sum of the coefficients of the literals satisfied or unvalued
watchCumul - Variable in class org.sat4j.pb.constraints.pb.MinWatchPbLongCP
sum of the coefficients of the literals satisfied or unvalued
watched - Variable in class org.sat4j.pb.constraints.pb.MinWatchPb
is the literal of index i watching the constraint ?
watched - Variable in class org.sat4j.pb.constraints.pb.MinWatchPbLong
is the literal of index i watching the constraint ?
watched - Variable in class org.sat4j.pb.constraints.pb.MinWatchPbLongCP
is the literal of index i watching the constraint ?
watching - Variable in class org.sat4j.pb.constraints.pb.MinWatchPb
indexes of literals watching the constraint
watching - Variable in class org.sat4j.pb.constraints.pb.MinWatchPbLong
indexes of literals watching the constraint
watching - Variable in class org.sat4j.pb.constraints.pb.MinWatchPbLongCP
indexes of literals watching the constraint
watchingCount - Variable in class org.sat4j.pb.constraints.pb.MinWatchPb
number of literals watching the constraint.
watchingCount - Variable in class org.sat4j.pb.constraints.pb.MinWatchPbLong
number of literals watching the constraint.
watchingCount - Variable in class org.sat4j.pb.constraints.pb.MinWatchPbLongCP
number of literals watching the constraint.
WatchPb - Class in org.sat4j.pb.constraints.pb
Abstract data structure for pseudo-boolean constraint with watched literals.
WatchPbLong - Class in org.sat4j.pb.constraints.pb
 
WatchPbLongCP - Class in org.sat4j.pb.constraints.pb
 
WCLAUSE - Static variable in class org.sat4j.pb.reader.JSONPBReader
 
WCLAUSE_PATTERN - Static variable in class org.sat4j.pb.reader.JSONPBReader
 
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.
WLITERAL - Static variable in class org.sat4j.pb.reader.JSONPBReader
 
WLITERAL_PATTERN - Static variable in class org.sat4j.pb.reader.JSONPBReader
 

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 J L M N O P R S T U V W X 

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