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

A

AbstractPBClauseCardConstrDataStructure - Class in org.sat4j.pb.constraints

AbstractPBClauseCardConstrDataStructure() - Constructor for class org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure

AbstractPBDataStructureFactory - Class in org.sat4j.pb.constraints

AbstractPBDataStructureFactory() - Constructor for class org.sat4j.pb.constraints.AbstractPBDataStructureFactory

activity - Variable in class org.sat4j.pb.constraints.pb.WatchPb

constraint activity

addAtLeast(IVecInt, int) - Method in class org.sat4j.pb.OPBStringSolver

addAtLeast(IVecInt, int) - Method in class org.sat4j.pb.tools.XplainPB

addAtLeast(IVecInt, int) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver

addAtMost(IVecInt, int) - Method in class org.sat4j.pb.OPBStringSolver

addAtMost(IVecInt, int) - Method in class org.sat4j.pb.tools.XplainPB

addAtMost(IVecInt, int) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver

addClause(IVecInt) - Method in class org.sat4j.pb.OPBStringSolver

addClause(IVecInt) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver

adding(int) - Method in class org.sat4j.pb.tools.ConflictTracing

addPseudoBoolean(IVecInt, IVec<BigInteger>, boolean, BigInteger) - Method in class org.sat4j.pb.core.PBSolver

addPseudoBoolean(IVecInt, IVec<BigInteger>, boolean, BigInteger) - Method in class org.sat4j.pb.core.PBSolverWithImpliedClause

addPseudoBoolean(IVecInt, IVec<BigInteger>, boolean, BigInteger) - Method in interface org.sat4j.pb.IPBSolver

Create a Pseudo-Boolean constraint of the type "at least n of those literals must be satisfied"

addPseudoBoolean(IVecInt, IVec<BigInteger>, boolean, BigInteger) - Method in class org.sat4j.pb.OPBStringSolver

addPseudoBoolean(IVecInt, IVec<BigInteger>, boolean, BigInteger) - Method in class org.sat4j.pb.PBSolverDecorator

addPseudoBoolean(IVecInt, IVec<BigInteger>, boolean, BigInteger) - Method in class org.sat4j.pb.tools.XplainPB

addPseudoBoolean(IVecInt, IVec<BigInteger>, boolean, BigInteger) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver

addToObjectiveFunction(T, int) - Method in class org.sat4j.pb.tools.DependencyHelper

Add a weighted literal to the objective function.

addToObjectiveFunction(T, BigInteger) - Method in class org.sat4j.pb.tools.DependencyHelper

Add a weighted literal to the objective function.

admitABetterSolution() - Method in class org.sat4j.pb.PseudoOptDecorator

admitABetterSolution(IVecInt) - Method in class org.sat4j.pb.PseudoOptDecorator

analyze(Constr, Pair) - Method in class org.sat4j.pb.core.PBSolverCP

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

assertConstraint(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.WatchPb

assertiveLiteral - Variable in class org.sat4j.pb.constraints.pb.MapPb

assuming(int) - Method in class org.sat4j.pb.tools.ConflictTracing

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.

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

backjump(int) - Method in class org.sat4j.pb.tools.ConflictTracing

backtracking(int) - Method in class org.sat4j.pb.tools.ConflictTracing

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

beginLoop() - Method in class org.sat4j.pb.tools.ConflictTracing

beginObjective() - Method in class org.sat4j.pb.reader.OPBReader2005

callback called before we read the objective function

BOUND - Static variable in class org.sat4j.pb.core.PBSolverCautious

brandNewClause(UnitPropagationListener, ILits, IVecInt) - Static method in class org.sat4j.pb.constraints.pb.MixableCBClausePB

brandNewClause(UnitPropagationListener, ILits, IVecInt) - Static method in class org.sat4j.pb.constraints.pb.OriginalBinaryClausePB

Creates a brand new clause, presumably from external data.

brandNewClause(UnitPropagationListener, ILits, IVecInt) - Static method in class org.sat4j.pb.constraints.pb.OriginalHTClausePB

Creates a brand new clause, presumably from external data.

buildConstraintFromConflict(IVecInt, IVec<BigInteger>) - Method in interface org.sat4j.pb.constraints.pb.IDataStructurePB

buildConstraintFromConflict(IVecInt, IVec<BigInteger>) - Method in class org.sat4j.pb.constraints.pb.MapPb

buildConstraintFromMapPb(int[], BigInteger[]) - Method in interface org.sat4j.pb.constraints.pb.IDataStructurePB

buildConstraintFromMapPb(int[], BigInteger[]) - Method in class org.sat4j.pb.constraints.pb.MapPb

byLevel - Variable in class org.sat4j.pb.constraints.pb.ConflictMap

allows to access directly to all variables belonging to a particular level At index 0, unassigned literals are stored (usually level -1); so there is always a step between index and levels.

C

calcReason(int, IVecInt) - Method in class org.sat4j.pb.constraints.pb.WatchPb

compute the reason for the assignment of a literal

calculateDegree(int[]) - Method in class org.sat4j.pb.ObjectiveFunction

calculateObjective() - Method in class org.sat4j.pb.PseudoOptDecorator

canonicalOptFunction - Variable in class org.sat4j.pb.tools.DependencyHelper

checkId(StringBuffer) - Method in class org.sat4j.pb.reader.OPBReader2005

checkId(StringBuffer) - Method in class org.sat4j.pb.reader.OPBReader2007

clause(C, T...) - Method in class org.sat4j.pb.tools.DependencyHelper

Create a clause (thing1 or thing 2 ... or thingn)

coefficientsEqualToOne() - Method in class org.sat4j.pb.constraints.pb.WatchPb

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

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

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

computeAnImpliedClause() - Method in class org.sat4j.pb.constraints.pb.OriginalBinaryClausePB

computeAnImpliedClause() - Method in class org.sat4j.pb.constraints.pb.OriginalHTClausePB

computeAnImpliedClause() - Method in interface org.sat4j.pb.constraints.pb.PBConstr

computeAnImpliedClause() - Method in class org.sat4j.pb.constraints.pb.UnitClausePB

computeAnImpliedClause() - Method in class org.sat4j.pb.constraints.pb.WatchPb

compute an implied clause on the literals with the greater coefficients.

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)

computePropagation(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.MaxWatchPb

computePropagation(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.MinWatchPb

computePropagation(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.WatchPb

computeWatches() - Method in class org.sat4j.pb.constraints.pb.MaxWatchPb

All the literals are watched.

computeWatches() - Method in class org.sat4j.pb.constraints.pb.MinWatchPb

computeWatches() - Method in class org.sat4j.pb.constraints.pb.WatchPb

configureSolver(String[]) - Method in class org.sat4j.pb.LanceurPseudo2005

configureSolver(String[]) - Method in class org.sat4j.pb.LanceurPseudo2007Eclipse

conflictFound(IConstr, int, int) - Method in class org.sat4j.pb.tools.ConflictTracing

conflictFound(int) - Method in class org.sat4j.pb.tools.ConflictTracing

ConflictMap - Class in org.sat4j.pb.constraints.pb

ConflictMapCardinality - Class in org.sat4j.pb.constraints.pb

ConflictMapCardinality(PBConstr, int) - Constructor for class org.sat4j.pb.constraints.pb.ConflictMapCardinality

ConflictMapClause - Class in org.sat4j.pb.constraints.pb

ConflictMapClause(PBConstr, int) - Constructor for class org.sat4j.pb.constraints.pb.ConflictMapClause

ConflictMapMerging - Class in org.sat4j.pb.constraints.pb

ConflictMapMerging(PBConstr, int) - Constructor for class org.sat4j.pb.constraints.pb.ConflictMapMerging

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

constraintRelOp(String) - Method in class org.sat4j.pb.reader.OPBReader2005

callback called when we read the relational operator of a constraint

constraintRightTerm(BigInteger) - Method in class org.sat4j.pb.reader.OPBReader2005

callback called when we read the right term of a constraint (also known as the degree)

constructCard(IVecInt, int) - Method in class org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure

constructCard(IVecInt, int) - Method in class org.sat4j.pb.constraints.CompetMinHTmixedClauseCardConstrDataStructureFactory

constructCard(IVecInt, int) - Method in class org.sat4j.pb.constraints.CompetResolutionPBMixedHTClauseCardConstrDataStructure

constructCard(IVecInt, int) - Method in class org.sat4j.pb.constraints.CompetResolutionPBMixedWLClauseCardConstrDataStructure

constructCard(IVecInt, int) - Method in class org.sat4j.pb.constraints.PBMaxClauseAtLeastConstrDataStructure

constructCard(IVecInt, int) - Method in class org.sat4j.pb.constraints.PuebloPBMinClauseAtLeastConstrDataStructure

constructCard(IVecInt, int) - Method in class org.sat4j.pb.constraints.PuebloPBMinClauseCardConstrDataStructure

constructClause(IVecInt) - Method in class org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure

constructClause(IVecInt) - Method in class org.sat4j.pb.constraints.CompetMinHTmixedClauseCardConstrDataStructureFactory

constructClause(IVecInt) - Method in class org.sat4j.pb.constraints.CompetResolutionPBMixedHTClauseCardConstrDataStructure

constructClause(IVecInt) - Method in class org.sat4j.pb.constraints.CompetResolutionPBMixedWLClauseCardConstrDataStructure

constructClause(IVecInt) - Method in class org.sat4j.pb.constraints.PBMaxCBClauseCardConstrDataStructure

constructClause(IVecInt) - Method in class org.sat4j.pb.constraints.PuebloPBMinClauseCardConstrDataStructure

constructLearntCard(IDataStructurePB) - Method in class org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure

constructLearntCard(IDataStructurePB) - Method in class org.sat4j.pb.constraints.CompetMinHTmixedClauseCardConstrDataStructureFactory

constructLearntCard(IDataStructurePB) - Method in class org.sat4j.pb.constraints.CompetResolutionPBMixedHTClauseCardConstrDataStructure

constructLearntCard(IDataStructurePB) - Method in class org.sat4j.pb.constraints.CompetResolutionPBMixedWLClauseCardConstrDataStructure

constructLearntCard(IDataStructurePB) - Method in class org.sat4j.pb.constraints.PBMaxClauseAtLeastConstrDataStructure

constructLearntCard(IDataStructurePB) - Method in class org.sat4j.pb.constraints.PuebloPBMinClauseAtLeastConstrDataStructure

constructLearntCard(IDataStructurePB) - Method in class org.sat4j.pb.constraints.PuebloPBMinClauseCardConstrDataStructure

constructLearntClause(IVecInt) - Method in class org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure

constructLearntClause(IVecInt) - Method in class org.sat4j.pb.constraints.CompetMinHTmixedClauseCardConstrDataStructureFactory

constructLearntClause(IVecInt) - Method in class org.sat4j.pb.constraints.CompetResolutionPBMixedHTClauseCardConstrDataStructure

constructLearntClause(IVecInt) - Method in class org.sat4j.pb.constraints.CompetResolutionPBMixedWLClauseCardConstrDataStructure

constructLearntClause(IVecInt) - Method in class org.sat4j.pb.constraints.PuebloPBMinClauseCardConstrDataStructure

constructLearntPB(IDataStructurePB) - Method in class org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure

constructLearntPB(IDataStructurePB) - Method in class org.sat4j.pb.constraints.PBMaxClauseCardConstrDataStructure

constructLearntPB(IDataStructurePB) - Method in class org.sat4j.pb.constraints.PBMinClauseCardConstrDataStructure

constructLearntPB(IDataStructurePB) - Method in class org.sat4j.pb.constraints.PuebloPBMinClauseCardConstrDataStructure

constructPB(int[], BigInteger[], BigInteger) - Method in class org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure

constructPB(int[], BigInteger[], BigInteger) - Method in class org.sat4j.pb.constraints.PBMaxClauseCardConstrDataStructure

constructPB(int[], BigInteger[], BigInteger) - Method in class org.sat4j.pb.constraints.PBMinClauseCardConstrDataStructure

constructPB(int[], BigInteger[], BigInteger) - Method in class org.sat4j.pb.constraints.PuebloPBMinClauseCardConstrDataStructure

createCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory

createClause(IVecInt) - Method in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory

createClause(IVecInt) - Method in class org.sat4j.pb.constraints.CompetResolutionPBMixedHTClauseCardConstrDataStructure

createClause(IVecInt) - Method in class org.sat4j.pb.constraints.CompetResolutionPBMixedWLClauseCardConstrDataStructure

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

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

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

decode(int[]) - Method in class org.sat4j.pb.reader.PBInstanceReader

Deprecated.

decode(int[], PrintWriter) - Method in class org.sat4j.pb.reader.PBInstanceReader

defaultSolver() - Method in class org.sat4j.pb.SolverFactory

degree - Variable in class org.sat4j.pb.constraints.pb.MapPb

degree - Variable in class org.sat4j.pb.constraints.pb.WatchPb

degree of the pseudo-boolean constraint

delete(int[]) - Method in class org.sat4j.pb.tools.ConflictTracing

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

discard(IVec<T>) - Method in class org.sat4j.pb.tools.DependencyHelper

discardCurrentSolution() - Method in class org.sat4j.pb.PseudoIteratorDecorator

discardCurrentSolution() - Method in class org.sat4j.pb.PseudoOptDecorator

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

displayAnswer() - Method in class org.sat4j.pb.LanceurPseudo2007Eclipse

E

end(Lbool) - Method in class org.sat4j.pb.tools.ConflictTracing

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.tools.WeightedObject

explanationEnabled - Variable in class org.sat4j.pb.tools.DependencyHelper

F

FOR_COMPETITION - Static variable in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory

forceObjectiveValueTo(Number) - Method in class org.sat4j.pb.PseudoOptDecorator

forwardActivity(double) - Method in class org.sat4j.pb.constraints.pb.WatchPb

G

get(int) - Method in class org.sat4j.pb.constraints.pb.WatchPb

to obtain the i-th literal of the constraint

get() - Method in class org.sat4j.pb.reader.OPBReader2005

get the next character from the stream

getActivity() - Method in class org.sat4j.pb.constraints.pb.WatchPb

to obtain the activity value of the constraint

getAssertiveLiteral() - Method in interface org.sat4j.pb.constraints.pb.IDataStructurePB

getAssertiveLiteral() - Method in class org.sat4j.pb.constraints.pb.MapPb

getBacktrackLevel(int) - Method in class org.sat4j.pb.constraints.pb.ConflictMap

computes the level for the backtrack : the highest decision level for which the conflict is assertive.

getBacktrackLevel(int) - Method in interface org.sat4j.pb.constraints.pb.IConflict

retourne le niveau de backtrack : c'est-?

getBooleanValueFor(T) - Method in class org.sat4j.pb.tools.DependencyHelper

Retrieve the boolean value associated with a domain object in the solution found by the solver.

getCoef(int) - Method in class org.sat4j.pb.constraints.pb.AtLeastPB

getCoef(int) - Method in class org.sat4j.pb.constraints.pb.LearntBinaryClausePB

getCoef(int) - Method in class org.sat4j.pb.constraints.pb.LearntHTClausePB

getCoef(int) - Method in class org.sat4j.pb.constraints.pb.MinWatchCardPB

getCoef(int) - Method in class org.sat4j.pb.constraints.pb.MixableCBClausePB

getCoef(int) - Method in class org.sat4j.pb.constraints.pb.OriginalBinaryClausePB

getCoef(int) - Method in class org.sat4j.pb.constraints.pb.OriginalHTClausePB

getCoef(int) - Method in interface org.sat4j.pb.constraints.pb.PBConstr

getCoef(int) - Method in class org.sat4j.pb.constraints.pb.UnitClausePB

getCoef(int) - Method in class org.sat4j.pb.constraints.pb.WatchPb

to obtain the coefficient of the i-th literal of the constraint

getCoeffs() - Method in class org.sat4j.pb.ObjectiveFunction

getCoeffs() - Method in class org.sat4j.pb.reader.OPBReader2005

getCoefs() - Method in class org.sat4j.pb.constraints.pb.AtLeastPB

getCoefs() - Method in class org.sat4j.pb.constraints.pb.LearntBinaryClausePB

getCoefs() - Method in class org.sat4j.pb.constraints.pb.LearntHTClausePB

getCoefs() - Method in class org.sat4j.pb.constraints.pb.MinWatchCardPB

getCoefs() - Method in class org.sat4j.pb.constraints.pb.MixableCBClausePB

getCoefs() - Method in class org.sat4j.pb.constraints.pb.OriginalBinaryClausePB

getCoefs() - Method in class org.sat4j.pb.constraints.pb.OriginalHTClausePB

getCoefs() - Method in interface org.sat4j.pb.constraints.pb.PBConstr

getCoefs() - Method in class org.sat4j.pb.constraints.pb.UnitClausePB

getCoefs() - Method in class org.sat4j.pb.constraints.pb.WatchPb

to obtain the coefficients of the constraint.

getDegree() - Method in class org.sat4j.pb.constraints.pb.AtLeastPB

getDegree() - Method in interface org.sat4j.pb.constraints.pb.IDataStructurePB

getDegree() - Method in class org.sat4j.pb.constraints.pb.LearntBinaryClausePB

getDegree() - Method in class org.sat4j.pb.constraints.pb.LearntHTClausePB

getDegree() - Method in class org.sat4j.pb.constraints.pb.MapPb

getDegree() - Method in class org.sat4j.pb.constraints.pb.MinWatchCardPB

getDegree() - Method in class org.sat4j.pb.constraints.pb.MixableCBClausePB

getDegree() - Method in class org.sat4j.pb.constraints.pb.OriginalBinaryClausePB

getDegree() - Method in class org.sat4j.pb.constraints.pb.OriginalHTClausePB

getDegree() - Method in interface org.sat4j.pb.constraints.pb.PBConstr

getDegree() - Method in class org.sat4j.pb.constraints.pb.UnitClausePB

getDegree() - Method in class org.sat4j.pb.constraints.pb.WatchPb

getExplanation() - Method in class org.sat4j.pb.OPBStringSolver

getExplanation() - Method in class org.sat4j.pb.UserFriendlyPBStringSolver

getInstanceName(String[]) - Method in class org.sat4j.pb.LanceurPseudo2005

getListOfVariables() - Method in class org.sat4j.pb.reader.OPBEclipseReader2007

getListOfVariables() - Method in class org.sat4j.pb.reader.OPBReader2005

getLits() - Method in class org.sat4j.pb.constraints.pb.AtLeastPB

getLits() - Method in class org.sat4j.pb.constraints.pb.MixableCBClausePB

getLits() - Method in interface org.sat4j.pb.constraints.pb.PBConstr

getLits() - Method in class org.sat4j.pb.constraints.pb.UnitClausePB

getLits() - Method in class org.sat4j.pb.constraints.pb.WatchPb

to obtain the literals of the constraint.

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

getObjectiveFunction() - Method in interface org.sat4j.pb.IPBSolver

getObjectiveFunction() - Method in class org.sat4j.pb.OPBStringSolver

getObjectiveFunction() - Method in class org.sat4j.pb.PBSolverDecorator

getObjectiveFunction() - Method in class org.sat4j.pb.reader.OPBReader2005

getObjectiveFunction() - Method in class org.sat4j.pb.tools.DependencyHelper

getObjectiveFunction() - Method in class org.sat4j.pb.tools.XplainPB

getObjectiveFunction() - Method in class org.sat4j.pb.UserFriendlyPBStringSolver

getObjectiveValue() - Method in class org.sat4j.pb.PseudoOptDecorator

getSolution() - Method in class org.sat4j.pb.tools.DependencyHelper

Retrieve the solution found.

getSolutionCost() - Method in class org.sat4j.pb.tools.DependencyHelper

getSolver() - Method in class org.sat4j.pb.tools.DependencyHelper

getVars() - Method in class org.sat4j.pb.ObjectiveFunction

getVars() - Method in class org.sat4j.pb.reader.OPBReader2005

getVocabulary() - Method in class org.sat4j.pb.constraints.pb.AtLeastPB

getVocabulary() - Method in class org.sat4j.pb.constraints.pb.MixableCBClausePB

getVocabulary() - Method in interface org.sat4j.pb.constraints.pb.PBConstr

getVocabulary() - Method in class org.sat4j.pb.constraints.pb.UnitClausePB

getVocabulary() - Method in class org.sat4j.pb.constraints.pb.WatchPb

getWeight() - Method in class org.sat4j.pb.tools.WeightedObject

H

hasASolution() - Method in class org.sat4j.pb.tools.DependencyHelper

hasASolution(IVec<T>) - Method in class org.sat4j.pb.tools.DependencyHelper

hasASolution(Collection<T>) - Method in class org.sat4j.pb.tools.DependencyHelper

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.tools.WeightedObject

hasNoObjectiveFunction() - Method in class org.sat4j.pb.PseudoOptDecorator

hasObjFunc - Variable in class org.sat4j.pb.reader.OPBReader2005

hasVariablesExplanation - Variable in class org.sat4j.pb.reader.OPBReader2005

I

IConflict - Interface in org.sat4j.pb.constraints.pb

IDataStructurePB - Interface in org.sat4j.pb.constraints.pb

iff(C, T, T...) - Method in class org.sat4j.pb.tools.DependencyHelper

Create a constraint using equivalency chains thing <=> (thing1 <=> thing2 <=> ... <=> thingn)

ifThenElse(C, T, T, T, T) - Method in class org.sat4j.pb.tools.DependencyHelper

Create a constraint of the form thing <=> (if conditionThing then thenThing else elseThing)

implication(T...) - Method in class org.sat4j.pb.tools.DependencyHelper

Create a logical implication of the form lhs -> rhs

ImplicationAnd<T,C> - Class in org.sat4j.pb.tools

That class is used to represent a conjunction of literals in the RHS of an implication.

ImplicationAnd(DependencyHelper<T, C>, IVecInt) - Constructor for class org.sat4j.pb.tools.ImplicationAnd

ImplicationNamer<T,C> - Class in org.sat4j.pb.tools

That class is used to associate each constraint with another object that must be used to represent it in an explanation.

ImplicationNamer(DependencyHelper<T, C>, IVec<IConstr>) - Constructor for class org.sat4j.pb.tools.ImplicationNamer

ImplicationRHS<T,C> - Class in org.sat4j.pb.tools

That class represents the RHS of an implication.

ImplicationRHS(DependencyHelper<T, C>, IVecInt) - Constructor for class org.sat4j.pb.tools.ImplicationRHS

implies(T...) - Method in class org.sat4j.pb.tools.DisjunctionRHS

implies(T) - Method in class org.sat4j.pb.tools.ImplicationRHS

Build an implication with a conjunction of literals in the RHS.

implies(T...) - Method in class org.sat4j.pb.tools.ImplicationRHS

Build an implication with a disjunction of literals in the RHS.

impliesNot(T) - Method in class org.sat4j.pb.tools.ImplicationRHS

Build an implication with a conjunction of literals in the RHS.

incActivity(double) - Method in class org.sat4j.pb.constraints.pb.WatchPb

increase activity value of the constraint

increaseWeight(BigInteger) - Method in class org.sat4j.pb.tools.WeightedObject

INegator - Interface in org.sat4j.pb.tools

init() - Method in class org.sat4j.pb.orders.VarOrderHeapObjective

instance() - Static method in class org.sat4j.pb.SolverFactory

Access to the single instance of the factory.

instance - Static variable in class org.sat4j.pb.tools.StringNegator

InternalMapPBStructure - Class in org.sat4j.pb.constraints.pb

IPBSolver - Interface in org.sat4j.pb

A solver able to deal with pseudo boolean constraints.

isAssertive(int) - Method in class org.sat4j.pb.constraints.pb.ConflictMap

tests if the conflict is assertive (allows to imply a literal) at a particular decision level

isAssertive(int) - Method in interface org.sat4j.pb.constraints.pb.IConflict

isAssertive(int) - Method in class org.sat4j.pb.constraints.pb.WatchPb

This predicate tests wether the constraint is assertive at decision level dl

isCardinality() - Method in interface org.sat4j.pb.constraints.pb.IDataStructurePB

isCardinality() - Method in class org.sat4j.pb.constraints.pb.MapPb

isGoodFirstCharacter(char) - Method in class org.sat4j.pb.reader.OPBReader2005

isGoodFirstCharacter(char) - Method in class org.sat4j.pb.reader.OPBReader2007

isGoodFollowingCharacter(char) - Method in class org.sat4j.pb.reader.OPBReader2005

isNegated(Object) - Method in interface org.sat4j.pb.tools.INegator

isNegated(Object) - Method in class org.sat4j.pb.tools.StringNegator

isSatisfiable() - Method in class org.sat4j.pb.constraints.pb.WatchPb

tests if the constraint is still satisfiable.

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

isSatisfiable(boolean) - Method in class org.sat4j.pb.PseudoOptDecorator

isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.pb.PseudoOptDecorator

isSatisfiable(IVecInt) - Method in class org.sat4j.pb.PseudoOptDecorator

L

LanceurPseudo2005 - Class in org.sat4j.pb

Launcher especially dedicated to the pseudo boolean 05 evaluation (@link http://www.cril.univ-artois.fr/PB05/).

LanceurPseudo2005() - Constructor for class org.sat4j.pb.LanceurPseudo2005

LanceurPseudo2007 - Class in org.sat4j.pb

Launcher for the Pseudo Boolean 2007 competition.

LanceurPseudo2007() - Constructor for class org.sat4j.pb.LanceurPseudo2007

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 ?

LearntBinaryClausePB - Class in org.sat4j.pb.constraints.pb

LearntBinaryClausePB(IVecInt, ILits) - Constructor for class org.sat4j.pb.constraints.pb.LearntBinaryClausePB

learntConstraintFactory(IDataStructurePB) - Method in class org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure

learntConstraintFactory(IDataStructurePB) - Method in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory

learntConstraintFactory(IDataStructurePB) - Method in class org.sat4j.pb.constraints.PBMaxDataStructure

learntConstraintFactory(IDataStructurePB) - Method in class org.sat4j.pb.constraints.PBMinDataStructure

learntConstraintFactory(IDataStructurePB) - Method in class org.sat4j.pb.constraints.PuebloPBMinDataStructure

LearntHTClausePB - Class in org.sat4j.pb.constraints.pb

LearntHTClausePB(IVecInt, ILits) - Constructor for class org.sat4j.pb.constraints.pb.LearntHTClausePB

lightSolver() - Method in class org.sat4j.pb.SolverFactory

literalInAProduct(String, IVecInt) - Method in class org.sat4j.pb.reader.OPBReader2007

callback called when we read a term of a constraint

lits - Variable in class org.sat4j.pb.constraints.pb.WatchPb

literals of the constraint

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.

M

main(String[]) - Static method in class org.sat4j.pb.LanceurPseudo2005

Lance le prouveur sur un fichier Dimacs

main(String[]) - Static method in class org.sat4j.pb.LanceurPseudo2007

Lance le prouveur sur un fichier Dimacs

main(String[]) - Static method in class org.sat4j.pb.LanceurPseudo2007Eclipse

Lance le prouveur sur un fichier Dimacs

MapPb - Class in org.sat4j.pb.constraints.pb

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

MaxWatchPb - 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

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) - Constructor for class org.sat4j.pb.constraints.pb.MinWatchPb

Basic constructor for PB constraint a0.x0 + a1.x1 + ... + an.xn >= k

MixableCBClausePB - Class in org.sat4j.pb.constraints.pb

MixableCBClausePB(IVecInt, ILits, boolean) - Constructor for class org.sat4j.pb.constraints.pb.MixableCBClausePB

MixableCBClausePB(IVecInt, ILits) - Constructor for class org.sat4j.pb.constraints.pb.MixableCBClausePB

model() - Method in class org.sat4j.pb.OptToPBSATAdapter

model(int) - Method in class org.sat4j.pb.OptToPBSATAdapter

model() - Method in class org.sat4j.pb.PseudoOptDecorator

model(int) - Method in class org.sat4j.pb.PseudoOptDecorator

N

named(C) - Method in class org.sat4j.pb.tools.ImplicationAnd

"name" the constraint for the explanation.

named(C) - Method in class org.sat4j.pb.tools.ImplicationNamer

Associate the current constraint with a specific object that will be used to represent it in an explanation.

nbConstr - Variable in class org.sat4j.pb.reader.OPBReader2005

nbConstraintsRead - Variable in class org.sat4j.pb.reader.OPBReader2005

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.

nbVars - Variable in class org.sat4j.pb.reader.OPBReader2005

negateLiteralInAProduct(String, IVecInt) - Method in class org.sat4j.pb.reader.OPBReader2007

callback called when we read a term of a constraint

newCompetPBCPMixedConstraintsObjective() - Static method in class org.sat4j.pb.SolverFactory

newCompetPBCPMixedConstraintsObjectiveLearnJustClauses() - Static method in class org.sat4j.pb.SolverFactory

newCompetPBKillerClassic() - Static method in class org.sat4j.pb.SolverFactory

newCompetPBKillerFixed() - Static method in class org.sat4j.pb.SolverFactory

newCompetPBKillerRSAT() - Static method in class org.sat4j.pb.SolverFactory

newCompetPBResHTMixedConstraintsObjective() - Static method in class org.sat4j.pb.SolverFactory

newCompetPBResMinHTMixedConstraintsObjective() - Static method in class org.sat4j.pb.SolverFactory

newCompetPBResMinHTMixedConstraintsObjectiveExpSimp() - Static method in class org.sat4j.pb.SolverFactory

newCompetPBResMixedConstraintsObjective(PBDataStructureFactory) - Static method in class org.sat4j.pb.SolverFactory

newCompetPBResMixedConstraintsObjectiveExpSimp() - Static method in class org.sat4j.pb.SolverFactory

newCompetPBResWLMixedConstraintsObjective() - 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.

newDefault() - Static method in class org.sat4j.pb.SolverFactory

Default solver of the SolverFactory.

newDefaultNonNormalized() - Static method in class org.sat4j.pb.SolverFactory

Default solver of the SolverFactory for instances not normalized.

newDimacsOutput() - Static method in class org.sat4j.pb.SolverFactory

newEclipseP2() - Static method in class org.sat4j.pb.SolverFactory

newLight() - Static method in class org.sat4j.pb.SolverFactory

Small footprint SAT solver.

newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalReductionToClause() - Static method in class org.sat4j.pb.SolverFactory

newMiniOPBClauseAtLeastConstrMax() - Static method in class org.sat4j.pb.SolverFactory

newMiniOPBClauseAtLeastMinPueblo() - Static method in class org.sat4j.pb.SolverFactory

newMiniOPBClauseCardMin() - Static method in class org.sat4j.pb.SolverFactory

newMiniOPBClauseCardMinPueblo() - Static method in class org.sat4j.pb.SolverFactory

newMiniOPBCounterBasedClauseCardConstrMax() - Static method in class org.sat4j.pb.SolverFactory

newOPBStringSolver() - Static method in class org.sat4j.pb.SolverFactory

newPBCPAllPB() - Static method in class org.sat4j.pb.SolverFactory

newPBCPAllPBWL() - Static method in class org.sat4j.pb.SolverFactory

newPBCPAllPBWLPueblo() - Static method in class org.sat4j.pb.SolverFactory

newPBCPMixedConstrainsImplied() - Static method in class org.sat4j.pb.SolverFactory

newPBCPMixedConstraints() - Static method in class org.sat4j.pb.SolverFactory

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.

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.

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

niceCheckedParameters(IVecInt, IVec<BigInteger>, boolean, BigInteger, ILits) - Static method in class org.sat4j.pb.constraints.pb.Pseudos

niceCheckedParametersForCompetition(int[], BigInteger[], boolean, BigInteger) - Static method in class org.sat4j.pb.constraints.pb.Pseudos

niceParameters(IVecInt, IVec<BigInteger>, boolean, BigInteger, ILits) - Static method in class org.sat4j.pb.constraints.pb.Pseudos

niceParametersForCompetition(int[], BigInteger[], boolean, BigInteger) - Static method in class org.sat4j.pb.constraints.pb.Pseudos

NO_COMPETITION - Static variable in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory

NO_NEGATION - Variable in class org.sat4j.pb.tools.DependencyHelper

nonOptimalMeansSatisfiable() - Method in class org.sat4j.pb.PseudoOptDecorator

normalizedMaxWatchPbNew(UnitPropagationListener, ILits, int[], BigInteger[], BigInteger) - Static method in class org.sat4j.pb.constraints.pb.MaxWatchPb

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) - Static method in class org.sat4j.pb.constraints.pb.MinWatchPb

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

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

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

O

obfct - Variable in class org.sat4j.pb.LanceurPseudo2005

ObjectiveFunction - Class in org.sat4j.pb

Abstraction for an Objective Function for Pseudo Boolean Optimization.

ObjectiveFunction(IVecInt, IVec<BigInteger>) - Constructor for class org.sat4j.pb.ObjectiveFunction

oldGetBacktrackLevel(int) - Method in class org.sat4j.pb.constraints.pb.ConflictMap

oldIsAssertive(int) - Method in class org.sat4j.pb.constraints.pb.ConflictMap

OPBEclipseReader2007 - Class in org.sat4j.pb.reader

OPBEclipseReader2007(IPBSolver) - Constructor for class org.sat4j.pb.reader.OPBEclipseReader2007

OPBReader2005 - Class in org.sat4j.pb.reader

Based on the "Official" reader for the Pseudo Boolean evaluation 2005.

OPBReader2005(IPBSolver) - Constructor for class org.sat4j.pb.reader.OPBReader2005

OPBReader2006 - Class in org.sat4j.pb.reader

Reader complying to the PB06 input format.

OPBReader2006(IPBSolver) - Constructor for class org.sat4j.pb.reader.OPBReader2006

OPBReader2007 - Class in org.sat4j.pb.reader

Reader complying with the PB07 input format.

OPBReader2007(IPBSolver) - Constructor for class org.sat4j.pb.reader.OPBReader2007

OPBReader2010 - Class in org.sat4j.pb.reader

OPBReader2010(IPBSolver) - Constructor for class org.sat4j.pb.reader.OPBReader2010

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

org.sat4j.pb.constraints - package org.sat4j.pb.constraints

org.sat4j.pb.constraints.pb - package org.sat4j.pb.constraints.pb

Implementations of pseudo boolean contraints.

org.sat4j.pb.core - package org.sat4j.pb.core

org.sat4j.pb.orders - package org.sat4j.pb.orders

org.sat4j.pb.reader - package org.sat4j.pb.reader

org.sat4j.pb.tools - package org.sat4j.pb.tools

OriginalBinaryClausePB - Class in org.sat4j.pb.constraints.pb

OriginalBinaryClausePB(IVecInt, ILits) - Constructor for class org.sat4j.pb.constraints.pb.OriginalBinaryClausePB

OriginalHTClausePB - Class in org.sat4j.pb.constraints.pb

OriginalHTClausePB(IVecInt, ILits) - Constructor for class org.sat4j.pb.constraints.pb.OriginalHTClausePB

P

parse() - Method in class org.sat4j.pb.reader.OPBReader2005

parses the file and uses the callbacks to send to send the data back to the program

parseInstance(Reader) - Method in class org.sat4j.pb.reader.OPBReader2005

parseInstance(Reader) - Method in class org.sat4j.pb.reader.OPBReader2010

parseInstance(String) - Method in class org.sat4j.pb.reader.PBInstanceReader

parseInstance(Reader) - Method in class org.sat4j.pb.reader.PBInstanceReader

PBConstr - Interface in org.sat4j.pb.constraints.pb

PBDataStructureFactory - Interface in org.sat4j.pb.core

PBInstanceReader - Class in org.sat4j.pb.reader

An reader having the responsibility to choose the right reader according to the input.

PBInstanceReader(IPBSolver) - Constructor for class org.sat4j.pb.reader.PBInstanceReader

PBMaxCBClauseCardConstrDataStructure - Class in org.sat4j.pb.constraints

PBMaxCBClauseCardConstrDataStructure() - Constructor for class org.sat4j.pb.constraints.PBMaxCBClauseCardConstrDataStructure

PBMaxClauseAtLeastConstrDataStructure - Class in org.sat4j.pb.constraints

PBMaxClauseAtLeastConstrDataStructure() - Constructor for class org.sat4j.pb.constraints.PBMaxClauseAtLeastConstrDataStructure

PBMaxClauseCardConstrDataStructure - Class in org.sat4j.pb.constraints

PBMaxClauseCardConstrDataStructure() - Constructor for class org.sat4j.pb.constraints.PBMaxClauseCardConstrDataStructure

PBMaxDataStructure - Class in org.sat4j.pb.constraints

PBMaxDataStructure() - Constructor for class org.sat4j.pb.constraints.PBMaxDataStructure

PBMinClauseCardConstrDataStructure - Class in org.sat4j.pb.constraints

PBMinClauseCardConstrDataStructure() - Constructor for class org.sat4j.pb.constraints.PBMinClauseCardConstrDataStructure

PBMinDataStructure - Class in org.sat4j.pb.constraints

PBMinDataStructure() - Constructor for class org.sat4j.pb.constraints.PBMinDataStructure

PBSolver - Class in org.sat4j.pb.core

PBSolver(AssertingClauseGenerator, LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, IOrder, RestartStrategy) - Constructor for class org.sat4j.pb.core.PBSolver

PBSolver(AssertingClauseGenerator, LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, SearchParams, IOrder, RestartStrategy) - Constructor for class org.sat4j.pb.core.PBSolver

PBSolverCautious - Class in org.sat4j.pb.core

PBSolverCautious(AssertingClauseGenerator, LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, IOrder) - Constructor for class org.sat4j.pb.core.PBSolverCautious

PBSolverCautious(AssertingClauseGenerator, LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, IOrder, int) - Constructor for class org.sat4j.pb.core.PBSolverCautious

PBSolverClause - Class in org.sat4j.pb.core

PBSolverClause(AssertingClauseGenerator, LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, IOrder) - Constructor for class org.sat4j.pb.core.PBSolverClause

PBSolverCP - Class in org.sat4j.pb.core

PBSolverCP(AssertingClauseGenerator, LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, IOrder) - Constructor for class org.sat4j.pb.core.PBSolverCP

PBSolverCP(AssertingClauseGenerator, LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, SearchParams, IOrder, RestartStrategy) - Constructor for class org.sat4j.pb.core.PBSolverCP

PBSolverCP(AssertingClauseGenerator, LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, SearchParams, IOrder) - Constructor for class org.sat4j.pb.core.PBSolverCP

PBSolverDecorator - Class in org.sat4j.pb

A decorator for the PB solvers.

PBSolverDecorator(IPBSolver) - Constructor for class org.sat4j.pb.PBSolverDecorator

PBSolverMerging - Class in org.sat4j.pb.core

PBSolverMerging(AssertingClauseGenerator, LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, IOrder) - Constructor for class org.sat4j.pb.core.PBSolverMerging

PBSolverResCP - Class in org.sat4j.pb.core

PBSolverResCP(AssertingClauseGenerator, LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, IOrder) - Constructor for class org.sat4j.pb.core.PBSolverResCP

PBSolverResCP(AssertingClauseGenerator, LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, IOrder, long) - Constructor for class org.sat4j.pb.core.PBSolverResCP

PBSolverResCP(AssertingClauseGenerator, LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, SearchParams, IOrder, RestartStrategy) - Constructor for class org.sat4j.pb.core.PBSolverResCP

PBSolverResCP(AssertingClauseGenerator, LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, SearchParams, IOrder) - Constructor for class org.sat4j.pb.core.PBSolverResCP

PBSolverResolution - Class in org.sat4j.pb.core

PBSolverResolution(AssertingClauseGenerator, LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, SearchParams, IOrder, RestartStrategy) - Constructor for class org.sat4j.pb.core.PBSolverResolution

PBSolverResolution(AssertingClauseGenerator, LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, IOrder, RestartStrategy) - Constructor for class org.sat4j.pb.core.PBSolverResolution

PBSolverStats - Class in org.sat4j.pb.core

PBSolverStats() - Constructor for class org.sat4j.pb.core.PBSolverStats

PBSolverWithImpliedClause - Class in org.sat4j.pb.core

PBSolverWithImpliedClause(AssertingClauseGenerator, LearningStrategy<PBDataStructureFactory>, PBDataStructureFactory, IOrder) - Constructor for class org.sat4j.pb.core.PBSolverWithImpliedClause

ppcm(BigInteger, BigInteger) - Static method in class org.sat4j.pb.constraints.pb.ConflictMap

computes the least common factor of two integers (Plus Petit Commun Multiple in french)

ppcm(BigInteger, BigInteger) - Static method in class org.sat4j.pb.constraints.pb.WatchPb

ppcm : least common multiple for two integers (plus petit commun multiple)

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

Propagation of a falsified literal

propagating(int, IConstr) - Method in class org.sat4j.pb.tools.ConflictTracing

PseudoIteratorDecorator - Class in org.sat4j.pb

A decorator that computes all pseudo boolean models.

PseudoIteratorDecorator(IPBSolver) - Constructor for class org.sat4j.pb.PseudoIteratorDecorator

PseudoOptDecorator - Class in org.sat4j.pb

A decorator that computes minimal pseudo boolean models.

PseudoOptDecorator(IPBSolver) - Constructor for class org.sat4j.pb.PseudoOptDecorator

Pseudos - Class in org.sat4j.pb.constraints.pb

Pseudos() - Constructor for class org.sat4j.pb.constraints.pb.Pseudos

PuebloMinWatchPb - Class in org.sat4j.pb.constraints.pb

PuebloPBMinClauseAtLeastConstrDataStructure - Class in org.sat4j.pb.constraints

PuebloPBMinClauseAtLeastConstrDataStructure() - Constructor for class org.sat4j.pb.constraints.PuebloPBMinClauseAtLeastConstrDataStructure

PuebloPBMinClauseCardConstrDataStructure - Class in org.sat4j.pb.constraints

PuebloPBMinClauseCardConstrDataStructure() - Constructor for class org.sat4j.pb.constraints.PuebloPBMinClauseCardConstrDataStructure

PuebloPBMinDataStructure - Class in org.sat4j.pb.constraints

PuebloPBMinDataStructure() - Constructor for class org.sat4j.pb.constraints.PuebloPBMinDataStructure

putback(char) - Method in class org.sat4j.pb.reader.OPBReader2005

put back a character into the stream (only one chr can be put back)

R

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

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

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

reduceInConstraint(WatchPb, BigInteger[], int, BigInteger) - Method in class org.sat4j.pb.constraints.pb.ConflictMap

constraint reduction : removes a literal of the constraint.

reduceInConstraint(WatchPb, BigInteger[], int, BigInteger) - Method in interface org.sat4j.pb.constraints.pb.IConflict

Reduction d'une contrainte On supprime un litteral non assigne prioritairement, vrai sinon.

reduceUntilConflict(int, int, BigInteger[], WatchPb) - Method in class org.sat4j.pb.constraints.pb.ConflictMap

reduceUntilConflict(int, int, BigInteger[], WatchPb) - Method in class org.sat4j.pb.constraints.pb.ConflictMapClause

reduces the constraint defined by wpb until the result of the cutting plane is a conflict. this reduction returns a clause.

reduceUntilConflict(int, int, BigInteger[], WatchPb) - Method in class org.sat4j.pb.constraints.pb.ConflictMapMerging

reduces the constraint defined by wpb until the result of the cutting plane is a conflict. this reduction returns a PB constraint.

reduceUntilConflict(int, int, BigInteger[], WatchPb) - 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.AtLeastPB

register() - Method in class org.sat4j.pb.constraints.pb.MinWatchCardPB

register() - Method in class org.sat4j.pb.constraints.pb.WatchPb

remove(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.MaxWatchPb

Remove a constraint from the solver

remove(UnitPropagationListener) - Method in class org.sat4j.pb.constraints.pb.MinWatchPb

Remove the constraint from the solver

rescaleBy(double) - Method in class org.sat4j.pb.constraints.pb.WatchPb

to re-scale the activity of the constraint

reset() - Method in class org.sat4j.pb.core.PBSolverStats

reset() - Method in class org.sat4j.pb.PseudoOptDecorator

resolve(PBConstr, int, VarActivityListener) - Method in class org.sat4j.pb.constraints.pb.ConflictMap

computes a cutting plane with a pseudo-boolean constraint. this method updates the current instance (of ConflictMap).

resolve(PBConstr, int, VarActivityListener) - Method in interface org.sat4j.pb.constraints.pb.IConflict

Effectue une resolution avec une contrainte PB.

restarting() - Method in class org.sat4j.pb.tools.ConflictTracing

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

setExpectedNumberOfClauses(int) - Method in class org.sat4j.pb.OPBStringSolver

setExpectedNumberOfClauses(int) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver

setFalse(T, C) - Method in class org.sat4j.pb.tools.DependencyHelper

Add a constraint to set the value of a domain object to false.

setLearnt() - Method in class org.sat4j.pb.constraints.pb.AtLeastPB

setLearnt() - Method in class org.sat4j.pb.constraints.pb.MinWatchCardPB

setLearnt() - Method in class org.sat4j.pb.constraints.pb.WatchPb

the constraint is learnt

setListOfVariablesForExplanation(IVecInt) - Method in class org.sat4j.pb.OPBStringSolver

setListOfVariablesForExplanation(IVecInt) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver

setMapping(Map<Integer, T>) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver

setNegator(INegator) - Method in class org.sat4j.pb.tools.DependencyHelper

setNormalizer(String) - Method in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory

setNormalizer(AbstractPBDataStructureFactory.INormalizer) - Method in class org.sat4j.pb.constraints.AbstractPBDataStructureFactory

setObjectiveFunction(ObjectiveFunction) - Method in class org.sat4j.pb.core.PBSolver

setObjectiveFunction(ObjectiveFunction) - Method in interface org.sat4j.pb.IPBSolver

setObjectiveFunction(ObjectiveFunction) - Method in class org.sat4j.pb.OPBStringSolver

setObjectiveFunction(ObjectiveFunction) - Method in class org.sat4j.pb.orders.VarOrderHeapObjective

setObjectiveFunction(ObjectiveFunction) - Method in class org.sat4j.pb.PBSolverDecorator

setObjectiveFunction(ObjectiveFunction) - Method in class org.sat4j.pb.PseudoOptDecorator

setObjectiveFunction(WeightedObject<T>...) - Method in class org.sat4j.pb.tools.DependencyHelper

Add an objective function to ask for a solution that minimize the objective function.

setObjectiveFunction(ObjectiveFunction) - Method in class org.sat4j.pb.tools.XplainPB

setObjectiveFunction(ObjectiveFunction) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver

setTrue(T, C) - Method in class org.sat4j.pb.tools.DependencyHelper

Add a constraint to set the value of a domain object to true.

simplify() - Method in class org.sat4j.pb.constraints.pb.WatchPb

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

skipSpaces() - Method in class org.sat4j.pb.reader.OPBReader2005

skip white spaces

slackConflict() - Method in class org.sat4j.pb.constraints.pb.ConflictMap

computes the slack of the current instance

slackConflict() - Method in interface org.sat4j.pb.constraints.pb.IConflict

slackConstraint() - Method in class org.sat4j.pb.constraints.pb.WatchPb

compute the slack of the current constraint slack = poss - degree of the constraint

slackConstraint(BigInteger[], BigInteger) - Method in class org.sat4j.pb.constraints.pb.WatchPb

compute the slack of a described constraint slack = poss - degree of the constraint

slackIsCorrect(int) - Method in class org.sat4j.pb.constraints.pb.ConflictMap

slackIsCorrect(int) - Method in interface org.sat4j.pb.constraints.pb.IConflict

solutionFound() - Method in class org.sat4j.pb.tools.ConflictTracing

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

start() - Method in class org.sat4j.pb.tools.ConflictTracing

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

T

thing - Variable in class org.sat4j.pb.tools.WeightedObject

toBigInt(int) - Static method in class org.sat4j.pb.constraints.pb.Pseudos

toString() - Method in class org.sat4j.pb.constraints.pb.ConflictMap

toString() - Method in class org.sat4j.pb.constraints.pb.MapPb

toString() - Method in class org.sat4j.pb.constraints.pb.WatchPb

toString(String) - Method in class org.sat4j.pb.core.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.PBSolverMerging

toString(String) - Method in class org.sat4j.pb.core.PBSolverWithImpliedClause

toString() - Method in class org.sat4j.pb.ObjectiveFunction

toString() - Method in class org.sat4j.pb.OPBStringSolver

toString(String) - Method in class org.sat4j.pb.OPBStringSolver

toString(String) - Method in class org.sat4j.pb.OptToPBSATAdapter

toString() - Method in class org.sat4j.pb.orders.VarOrderHeapObjective

toString(String) - Method in class org.sat4j.pb.PseudoOptDecorator

toString() - Method in class org.sat4j.pb.UserFriendlyPBStringSolver

toString(String) - Method in class org.sat4j.pb.UserFriendlyPBStringSolver

toVecBigInt(IVecInt) - Static method in class org.sat4j.pb.constraints.pb.Pseudos

translateVarToId(String) - Method in class org.sat4j.pb.reader.OPBReader2005

translateVarToId(String) - Method in class org.sat4j.pb.reader.OPBReader2007

U

undo(int) - Method in class org.sat4j.pb.constraints.pb.MaxWatchPb

this method is called during backtrack

undo(int) - Method in class org.sat4j.pb.constraints.pb.MinWatchPb

this method is called during backtrack

UnitClausePB - Class in org.sat4j.pb.constraints.pb

UnitClausePB(int, ILits) - Constructor for class org.sat4j.pb.constraints.pb.UnitClausePB

unNegate(Object) - Method in interface org.sat4j.pb.tools.INegator

unNegate(Object) - Method in class org.sat4j.pb.tools.StringNegator

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(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

W

watchCumul - Variable in class org.sat4j.pb.constraints.pb.MinWatchPb

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 ?

watching - Variable in class org.sat4j.pb.constraints.pb.MinWatchPb

indexes of literals watching the constraint

watchingCount - Variable in class org.sat4j.pb.constraints.pb.MinWatchPb

number of literals watching the constraint.

WatchPb - Class in org.sat4j.pb.constraints.pb

Abstract data structure for pseudo-boolean constraint with watched literals.

weightedLits - Variable in class org.sat4j.pb.constraints.pb.MapPb

WeightedObject<T> - Class in org.sat4j.pb.tools

why() - Method in class org.sat4j.pb.tools.DependencyHelper

Explain the reason of the inconsistency of the set of constraints.

why(T) - Method in class org.sat4j.pb.tools.DependencyHelper

Explain a domain object has been set to true in a solution.

whyNot(T) - Method in class org.sat4j.pb.tools.DependencyHelper

Explain a domain object has been set to false in a solution.

X

XplainPB - Class in org.sat4j.pb.tools

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

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