Index (SAT4J core 2.3.4 API)

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

A

AAGReader - Class in org.sat4j.reader: Reader for the ASCII And Inverter Graph format defined by Armin Biere.
AbstractCardinalityDataStructure - Class in org.sat4j.minisat.constraints
AbstractCardinalityDataStructure() - Constructor for class org.sat4j.minisat.constraints.AbstractCardinalityDataStructure
AbstractClauseSelectorSolver<T extends ISolver> - Class in org.sat4j.tools
AbstractClauseSelectorSolver(T) - Constructor for class org.sat4j.tools.AbstractClauseSelectorSolver
AbstractDataStructureFactory - Class in org.sat4j.minisat.constraints
AbstractDataStructureFactory() - Constructor for class org.sat4j.minisat.constraints.AbstractDataStructureFactory
AbstractLauncher - Class in org.sat4j: That class is used by launchers used to solve decision problems, i.e.
AbstractLauncher() - Constructor for class org.sat4j.AbstractLauncher
AbstractMinimalModel - Class in org.sat4j.tools
AbstractMinimalModel(ISolver) - Constructor for class org.sat4j.tools.AbstractMinimalModel
AbstractMinimalModel(ISolver, IVecInt) - Constructor for class org.sat4j.tools.AbstractMinimalModel
AbstractMinimalModel(ISolver, SolutionFoundListener) - Constructor for class org.sat4j.tools.AbstractMinimalModel
AbstractMinimalModel(ISolver, IVecInt, SolutionFoundListener) - Constructor for class org.sat4j.tools.AbstractMinimalModel
AbstractOptimizationLauncher - Class in org.sat4j: Deprecated.
AbstractOptimizationLauncher() - Constructor for class org.sat4j.AbstractOptimizationLauncher: Deprecated.
AbstractOutputSolver - Class in org.sat4j.tools
AbstractOutputSolver() - Constructor for class org.sat4j.tools.AbstractOutputSolver
AbstractSelectorVariablesDecorator - Class in org.sat4j.opt: Abstract class which adds a new "selector" variable for each clause entered in the solver.
AbstractSelectorVariablesDecorator(ISolver) - Constructor for class org.sat4j.opt.AbstractSelectorVariablesDecorator
ActiveLearning<D extends DataStructureFactory> - Class in org.sat4j.minisat.learning: Learn clauses with a great number of active variables.
ActiveLearning() - Constructor for class org.sat4j.minisat.learning.ActiveLearning
ActiveLearning(double) - Constructor for class org.sat4j.minisat.learning.ActiveLearning
activity - Variable in class org.sat4j.minisat.constraints.cnf.BinaryClause
activity - Variable in class org.sat4j.minisat.constraints.cnf.HTClause
activity - Variable in class org.sat4j.minisat.constraints.cnf.UnitClause
activity - Variable in class org.sat4j.minisat.constraints.cnf.WLClause
activity - Variable in class org.sat4j.minisat.orders.VarOrderHeap: mesure heuristique de l'activite d'une variable.
ActivityComparator - Class in org.sat4j.minisat.core: Utility class to sort the constraints according to their activity.
ActivityComparator() - Constructor for class org.sat4j.minisat.core.ActivityComparator
add(IConstr) - Method in class org.sat4j.core.ConstrGroup
addAllClauses(IVec<IVecInt>) - Method in class org.sat4j.minisat.core.Solver
addAllClauses(IVec<IVecInt>) - Method in interface org.sat4j.specs.ISolver: Create clauses from a set of set of literals.
addAllClauses(IVec<IVecInt>) - Method in class org.sat4j.tools.AbstractOutputSolver
addAllClauses(IVec<IVecInt>) - Method in class org.sat4j.tools.ManyCore
addAllClauses(IVec<IVecInt>) - Method in class org.sat4j.tools.SolverDecorator
addAllClauses(IVec<IVecInt>) - Method in class org.sat4j.tools.StatisticsSolver
addAtLeast(IVecInt, int) - Method in class org.sat4j.minisat.core.Solver
addAtLeast(IVecInt, int) - Method in interface org.sat4j.specs.ISolver: Create a cardinality constraint of the type "at least n of those literals must be satisfied"
addAtLeast(IVecInt, int) - Method in class org.sat4j.tools.ClausalCardinalitiesDecorator
addAtLeast(IVecInt, int) - Method in class org.sat4j.tools.DimacsOutputSolver
addAtLeast(IVecInt, int) - Method in class org.sat4j.tools.DimacsStringSolver
addAtLeast(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.EncodingStrategyAdapter
addAtLeast(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Policy
addAtLeast(IVecInt, int) - Method in class org.sat4j.tools.ManyCore
addAtLeast(IVecInt, int) - Method in class org.sat4j.tools.NegationDecorator
addAtLeast(IVecInt, int) - Method in class org.sat4j.tools.SolverDecorator
addAtLeast(IVecInt, int) - Method in class org.sat4j.tools.StatisticsSolver
addAtLeast(IVecInt, int) - Method in class org.sat4j.tools.xplain.HighLevelXplain
addAtLeast(IVecInt, int) - Method in class org.sat4j.tools.xplain.Xplain
addAtLeastOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.EncodingStrategyAdapter
addAtMost(IVecInt, int) - Method in class org.sat4j.minisat.core.Solver
addAtMost(IVecInt, int) - Method in interface org.sat4j.specs.ISolver: Create a cardinality constraint of the type "at most n of those literals must be satisfied"
addAtMost(IVecInt, int) - Method in class org.sat4j.tools.ClausalCardinalitiesDecorator
addAtMost(IVecInt, int) - Method in class org.sat4j.tools.DimacsOutputSolver
addAtMost(IVecInt, int) - Method in class org.sat4j.tools.DimacsStringSolver
addAtMost(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Binary
addAtMost(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Binomial
addAtMost(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Commander
addAtMost(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.EncodingStrategyAdapter
addAtMost(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Policy
addAtMost(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Product
addAtMost(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Sequential: This encoding adds (n-1)*k variables (n is the number of variables in the at most constraint and k is the degree of the constraint) and 2nk+n-3k-1 clauses.
addAtMost(IVecInt, int) - Method in class org.sat4j.tools.ManyCore
addAtMost(IVecInt, int) - Method in class org.sat4j.tools.NegationDecorator
addAtMost(IVecInt, int) - Method in class org.sat4j.tools.SolverDecorator
addAtMost(IVecInt, int) - Method in class org.sat4j.tools.StatisticsSolver
addAtMost(IVecInt, int) - Method in class org.sat4j.tools.xplain.HighLevelXplain
addAtMost(IVecInt, int) - Method in class org.sat4j.tools.xplain.Xplain
addAtMostNonOpt(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Product
addAtMostOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Binary: p being the smaller integer greater than log_2(n), this encoding adds p variables and n*p clauses.
addAtMostOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Binomial
addAtMostOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Commander: In this encoding, variables are partitioned in groups.
addAtMostOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.EncodingStrategyAdapter
addAtMostOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Ladder
addAtMostOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Product
addAtMostOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Sequential
addAtMostOnTheFly(int[], int) - Method in class org.sat4j.minisat.core.Solver
addAtMostOnTheFly(int[], int) - Method in interface org.sat4j.specs.ISolverService: Add a new pseudo cardinality constraint sum literals <= degree in the solver.
addBlockingClause(IVecInt) - Method in class org.sat4j.minisat.core.Solver
addBlockingClause(IVecInt) - Method in interface org.sat4j.specs.ISolver: Add a clause in order to prevent an assignment to occur.
addBlockingClause(IVecInt) - Method in class org.sat4j.tools.AbstractOutputSolver
addBlockingClause(IVecInt) - Method in class org.sat4j.tools.ManyCore
addBlockingClause(IVecInt) - Method in class org.sat4j.tools.SolverDecorator
addBlockingClause(IVecInt) - Method in class org.sat4j.tools.StatisticsSolver
addClause(IVecInt) - Method in class org.sat4j.minisat.core.Solver
addClause(IVecInt) - Method in class org.sat4j.opt.MaxSatDecorator
addClause(IVecInt, int) - Method in interface org.sat4j.specs.IGroupSolver
addClause(IVecInt) - Method in interface org.sat4j.specs.ISolver: Create a clause from a set of literals The literals are represented by non null integers such that opposite literals a represented by opposite values.
addClause(IVecInt) - Method in class org.sat4j.tools.DimacsOutputSolver
addClause(IVecInt) - Method in class org.sat4j.tools.DimacsStringSolver
addClause(IVecInt) - Method in class org.sat4j.tools.FullClauseSelectorSolver
addClause(IVecInt, int) - Method in class org.sat4j.tools.GroupClauseSelectorSolver
addClause(IVecInt) - Method in class org.sat4j.tools.ManyCore
addClause(IVecInt) - Method in class org.sat4j.tools.NegationDecorator
addClause(IVecInt) - Method in class org.sat4j.tools.SolverDecorator
addClause(IVecInt) - Method in class org.sat4j.tools.StatisticsSolver
addClauseOnTheFly(int[]) - Method in class org.sat4j.minisat.core.Solver
addClauseOnTheFly(int[]) - Method in interface org.sat4j.specs.ISolverService: Add a new clause in the SAT solver.
addConstr(Constr) - Method in class org.sat4j.minisat.core.Solver
addControlableClause(IVecInt) - Method in class org.sat4j.tools.FullClauseSelectorSolver
addControlableClause(IVecInt, int) - Method in class org.sat4j.tools.GroupClauseSelectorSolver
addCriterion(IVecInt) - Method in class org.sat4j.tools.LexicoDecorator
addExactly(IVecInt, int) - Method in class org.sat4j.minisat.core.Solver
addExactly(IVecInt, int) - Method in interface org.sat4j.specs.ISolver: Create a cardinality constraint of the type "exactly n of those literals must be satisfied".
addExactly(IVecInt, int) - Method in class org.sat4j.tools.ClausalCardinalitiesDecorator
addExactly(IVecInt, int) - Method in class org.sat4j.tools.DimacsOutputSolver
addExactly(IVecInt, int) - Method in class org.sat4j.tools.DimacsStringSolver
addExactly(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Binary
addExactly(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Binomial
addExactly(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Commander
addExactly(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.EncodingStrategyAdapter
addExactly(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Policy
addExactly(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Product
addExactly(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Sequential
addExactly(IVecInt, int) - Method in class org.sat4j.tools.ManyCore
addExactly(IVecInt, int) - Method in class org.sat4j.tools.NegationDecorator
addExactly(IVecInt, int) - Method in class org.sat4j.tools.SolverDecorator
addExactly(IVecInt, int) - Method in class org.sat4j.tools.StatisticsSolver
addExactly(IVecInt, int) - Method in class org.sat4j.tools.xplain.Xplain
addExactlyOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Binary
addExactlyOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Binomial
addExactlyOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Commander
addExactlyOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.EncodingStrategyAdapter
addExactlyOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Ladder
addExactlyOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Product
addExactlyOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Sequential
adding(int) - Method in interface org.sat4j.specs.SearchListener: adding forced variable (conflict driven assignment)
adding(int) - Method in class org.sat4j.tools.DotSearchTracing
adding(int) - Method in class org.sat4j.tools.MultiTracing
adding(int) - Method in class org.sat4j.tools.SearchListenerAdapter
adding(int) - Method in class org.sat4j.tools.TextOutputTracing
addInvisiblePoint(double, double) - Method in class org.sat4j.tools.FileBasedVisualizationTool
addInvisiblePoint(double, double) - Method in interface org.sat4j.tools.IVisualizationTool
additionalFullAdderConstraints(int, int, int, int, int) - Method in class org.sat4j.tools.GateTranslator
addNonControlableClause(IVecInt) - Method in class org.sat4j.tools.FullClauseSelectorSolver
addNonControlableClause(IVecInt) - Method in class org.sat4j.tools.GroupClauseSelectorSolver
addOriginalClause(IVecInt) - Method in class org.sat4j.tools.CheckMUSSolutionListener
addPoint(double, double) - Method in class org.sat4j.tools.FileBasedVisualizationTool
addPoint(double, double) - Method in interface org.sat4j.tools.IVisualizationTool
admitABetterSolution() - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
admitABetterSolution(IVecInt) - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
admitABetterSolution(IVecInt) - Method in class org.sat4j.opt.MaxSatDecorator
admitABetterSolution() - Method in class org.sat4j.opt.MinOneDecorator
admitABetterSolution(IVecInt) - Method in class org.sat4j.opt.MinOneDecorator
admitABetterSolution() - Method in interface org.sat4j.specs.IOptimizationProblem: Look for a solution of the optimization problem.
admitABetterSolution(IVecInt) - Method in interface org.sat4j.specs.IOptimizationProblem: Look for a solution of the optimization problem when some literals are satisfied.
admitABetterSolution() - Method in class org.sat4j.tools.LexicoDecorator
admitABetterSolution(IVecInt) - Method in class org.sat4j.tools.LexicoDecorator
AIGReader - Class in org.sat4j.reader: Reader for the Binary And Inverter Graph format defined by Armin Biere.
AllMUSes - Class in org.sat4j.tools: This is a tool for computing all the MUSes (Minimum Unsatisfiable Sets) of a set of clauses.
AllMUSes(boolean, ASolverFactory<? extends ISolver>) - Constructor for class org.sat4j.tools.AllMUSes
AllMUSes(ASolverFactory<? extends ISolver>) - Constructor for class org.sat4j.tools.AllMUSes
analyze(Constr, Pair) - Method in class org.sat4j.minisat.core.Solver
analyzeAtRootLevel(Constr) - Method in class org.sat4j.minisat.core.Solver
analyzeFinalConflictInTermsOfAssumptions(Constr, IVecInt, int) - Method in class org.sat4j.minisat.core.Solver: Derive a subset of the assumptions causing the inconistency.
AND - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader
and(int, IVecInt) - Method in class org.sat4j.tools.GateTranslator: Translate y <=> x1 /\ x2 /\ ... /\ xn into clauses.
and(int, int, int) - Method in class org.sat4j.tools.GateTranslator: Translate y <=> x1 /\ x2
ANSWER_PREFIX - Static variable in interface org.sat4j.ILauncherMode
ArminRestarts - Class in org.sat4j.minisat.restarts: Rapid restart strategy presented by Armin Biere during it's SAT 07 invited talk.
ArminRestarts() - Constructor for class org.sat4j.minisat.restarts.ArminRestarts
ASolverFactory<T extends ISolver> - Class in org.sat4j.core: A solver factory is responsible for providing prebuilt solvers to the end user.
ASolverFactory() - Constructor for class org.sat4j.core.ASolverFactory
assertConstraint(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.card.AtLeast
assertConstraint(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
assertConstraint(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
assertConstraint(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
assertConstraint(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.HTClause
assertConstraint(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
assertConstraint(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
assertConstraint(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.WLClause
assertConstraint(UnitPropagationListener) - Method in interface org.sat4j.minisat.core.Constr: Method called when the constraint is to be asserted.
assertConstraintIfNeeded(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.card.AtLeast
assertConstraintIfNeeded(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
assertConstraintIfNeeded(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
assertConstraintIfNeeded(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
assertConstraintIfNeeded(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.HTClause
assertConstraintIfNeeded(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
assertConstraintIfNeeded(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
assertConstraintIfNeeded(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.WLClause
assertConstraintIfNeeded(UnitPropagationListener) - Method in interface org.sat4j.minisat.core.Constr: Method called when the constraint is added to the solver "on the fly".
assignLiteral(int) - Method in interface org.sat4j.minisat.core.IOrder: indicate that a literal has been satisfied.
assignLiteral(int) - Method in interface org.sat4j.minisat.core.IPhaseSelectionStrategy: indicate that a literal has been satisfied.
assignLiteral(int) - Method in class org.sat4j.minisat.orders.NegativeLiteralSelectionStrategy
assignLiteral(int) - Method in class org.sat4j.minisat.orders.PhaseCachingAutoEraseStrategy
assignLiteral(int) - Method in class org.sat4j.minisat.orders.PhaseInLastLearnedClauseSelectionStrategy
assignLiteral(int) - Method in class org.sat4j.minisat.orders.PositiveLiteralSelectionStrategy
assignLiteral(int) - Method in class org.sat4j.minisat.orders.RandomLiteralSelectionStrategy
assignLiteral(int) - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
assignLiteral(int) - Method in class org.sat4j.minisat.orders.RSATLastLearnedClausesPhaseSelectionStrategy
assignLiteral(int) - Method in class org.sat4j.minisat.orders.RSATPhaseSelectionStrategy
assignLiteral(int) - Method in class org.sat4j.minisat.orders.TabuListDecorator
assignLiteral(int) - Method in class org.sat4j.minisat.orders.UserFixedPhaseSelectionStrategy
assignLiteral(int) - Method in class org.sat4j.minisat.orders.VarOrderHeap
assume(int) - Method in class org.sat4j.minisat.core.Solver
assuming(int) - Method in interface org.sat4j.specs.SearchListener: decision variable
assuming(int) - Method in class org.sat4j.tools.DecisionTracing
assuming(int) - Method in class org.sat4j.tools.DotSearchTracing
assuming(int) - Method in class org.sat4j.tools.MultiTracing
assuming(int) - Method in class org.sat4j.tools.SearchListenerAdapter
assuming(int) - Method in class org.sat4j.tools.TextOutputTracing
AtLeast - Class in org.sat4j.minisat.constraints.card
AtLeast(ILits, IVecInt, int) - Constructor for class org.sat4j.minisat.constraints.card.AtLeast
ATLEAST - Static variable in class org.sat4j.minisat.constraints.card.MinWatchCard
ATLEAST - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader
atLeastNew(UnitPropagationListener, ILits, IVecInt, int) - Static method in class org.sat4j.minisat.constraints.card.AtLeast
ATMOST - Static variable in class org.sat4j.minisat.constraints.card.MinWatchCard
ATMOST - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader
average() - Method in class org.sat4j.minisat.core.CircularBuffer

B

Backbone - Class in org.sat4j.tools: The aim of this class is to compute efficiently the literals implied by the set of constraints (also called backbone or unit implicates).
backbone(ISolver) - Static method in class org.sat4j.tools.RemiUtils: Compute the set of literals common to all models of the formula.
backjump(int) - Method in interface org.sat4j.specs.SearchListener: The solver is asked to backjump to a given decision level.
backjump(int) - Method in class org.sat4j.tools.DecisionLevelTracing
backjump(int) - Method in class org.sat4j.tools.MultiTracing
backjump(int) - Method in class org.sat4j.tools.SearchListenerAdapter
backjump(int) - Method in class org.sat4j.tools.TextOutputTracing
backtrack(int[]) - Method in class org.sat4j.minisat.core.Solver
backtrack(int[]) - Method in interface org.sat4j.specs.ISolverService: Ask the SAT solver to backtrack.
backtracking(int) - Method in interface org.sat4j.specs.SearchListener: backtrack on a decision variable
backtracking(int) - Method in class org.sat4j.tools.DotSearchTracing
backtracking(int) - Method in class org.sat4j.tools.MultiTracing
backtracking(int) - Method in class org.sat4j.tools.SearchListenerAdapter
backtracking(int) - Method in class org.sat4j.tools.TextOutputTracing
backtrackLevel - Variable in class org.sat4j.minisat.core.Pair
BasicLauncher<T extends ISolver> - Class in org.sat4j: Very simple launcher, to be used during the SAT competition or the SAT race for instance.
BasicLauncher(ASolverFactory<T>) - Constructor for class org.sat4j.BasicLauncher
beginLoop() - Method in interface org.sat4j.specs.SearchListener: starts a propagation
beginLoop() - Method in class org.sat4j.tools.DotSearchTracing
beginLoop() - Method in class org.sat4j.tools.MultiTracing
beginLoop() - Method in class org.sat4j.tools.SearchListenerAdapter
beginLoop() - Method in class org.sat4j.tools.TextOutputTracing
beginTime - Variable in class org.sat4j.AbstractLauncher
belongsToPool(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
belongsToPool(int) - Method in interface org.sat4j.minisat.core.ILits: Returns true iff the variable is used in the set of constraints.
Binary - Class in org.sat4j.tools.encoding: Binary encoding for the "at most one" and "at most k" cases.
Binary() - Constructor for class org.sat4j.tools.encoding.Binary
BinaryClause - Class in org.sat4j.minisat.constraints.cnf: Data structure for binary clause.
BinaryClause(IVecInt, ILits) - Constructor for class org.sat4j.minisat.constraints.cnf.BinaryClause: Creates a new basic clause
Binomial - Class in org.sat4j.tools.encoding: Binomial encoding for the "at most one" and "at most k" cases.
Binomial() - Constructor for class org.sat4j.tools.encoding.Binomial
bound() - Method in class org.sat4j.minisat.core.ConflictTimerAdapter
brandNewClause(UnitPropagationListener, ILits, IVecInt) - Static method in class org.sat4j.minisat.constraints.cnf.OriginalBinaryClause: Creates a brand new clause, presumably from external data.
brandNewClause(UnitPropagationListener, ILits, IVecInt) - Static method in class org.sat4j.minisat.constraints.cnf.OriginalHTClause: Creates a brand new clause, presumably from external data.
brandNewClause(UnitPropagationListener, ILits, IVecInt) - Static method in class org.sat4j.minisat.constraints.cnf.OriginalWLClause: Creates a brand new clause, presumably from external data.

C

calcReason(int, IVecInt) - Method in class org.sat4j.minisat.constraints.card.AtLeast
calcReason(int, IVecInt) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard: Calcule la cause de l'affection d'un litt?
calcReason(int, IVecInt) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard: computes the reason for a literal
calcReason(int, IVecInt) - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
calcReason(int, IVecInt) - Method in class org.sat4j.minisat.constraints.cnf.HTClause
calcReason(int, IVecInt) - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
calcReason(int, IVecInt) - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
calcReason(int, IVecInt) - Method in class org.sat4j.minisat.constraints.cnf.WLClause
calcReason(int, IVecInt) - Method in interface org.sat4j.minisat.core.Constr: Compute the reason for a given assignment.
calcReasonOnTheFly(int, IVecInt, IVecInt) - Method in class org.sat4j.minisat.constraints.card.AtLeast
calcReasonOnTheFly(int, IVecInt, IVecInt) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
calcReasonOnTheFly(int, IVecInt, IVecInt) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
calcReasonOnTheFly(int, IVecInt, IVecInt) - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
calcReasonOnTheFly(int, IVecInt, IVecInt) - Method in class org.sat4j.minisat.constraints.cnf.HTClause
calcReasonOnTheFly(int, IVecInt, IVecInt) - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
calcReasonOnTheFly(int, IVecInt, IVecInt) - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
calcReasonOnTheFly(int, IVecInt, IVecInt) - Method in class org.sat4j.minisat.constraints.cnf.WLClause
calcReasonOnTheFly(int, IVecInt, IVecInt) - Method in interface org.sat4j.minisat.core.Constr: Compute the reason for a given assignment in a the constraint created on the fly in the solver.
calculateObjective() - Method in class org.sat4j.opt.MaxSatDecorator
calculateObjective() - Method in class org.sat4j.opt.MinOneDecorator
calculateObjective() - Method in interface org.sat4j.specs.IOptimizationProblem: Deprecated.
calculateObjective() - Method in class org.sat4j.tools.LexicoDecorator
canBePropagatedMultipleTimes() - Method in class org.sat4j.core.ConstrGroup
canBePropagatedMultipleTimes() - Method in class org.sat4j.minisat.constraints.card.AtLeast
canBePropagatedMultipleTimes() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
canBePropagatedMultipleTimes() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
canBePropagatedMultipleTimes() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
canBePropagatedMultipleTimes() - Method in class org.sat4j.minisat.constraints.cnf.HTClause
canBePropagatedMultipleTimes() - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
canBePropagatedMultipleTimes() - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
canBePropagatedMultipleTimes() - Method in class org.sat4j.minisat.constraints.cnf.WLClause
canBePropagatedMultipleTimes() - Method in interface org.sat4j.specs.IConstr: Partition constraints into the ones that can only be found once on the trail (e.g. clauses) and the ones that can be found several times (e.g.
cancelExplanation() - Method in class org.sat4j.tools.xplain.HighLevelXplain
cancelExplanation() - Method in class org.sat4j.tools.xplain.Xplain
cancelExplanationComputation() - Method in class org.sat4j.tools.xplain.DeletionStrategy
cancelExplanationComputation() - Method in class org.sat4j.tools.xplain.InsertionStrategy
cancelExplanationComputation() - Method in interface org.sat4j.tools.xplain.MinimizationStrategy
cancelExplanationComputation() - Method in class org.sat4j.tools.xplain.QuickXplain2001Strategy
cancelExplanationComputation() - Method in class org.sat4j.tools.xplain.QuickXplainStrategy
cancelUntil(int) - Method in class org.sat4j.minisat.core.Solver: Cancel several levels of assumptions
capacity() - Method in class org.sat4j.minisat.constraints.cnf.Lits: To get the capacity of the current vocabulary.
CARD - Static variable in class org.sat4j.reader.JSONReader
CardinalityDataStructure - Class in org.sat4j.minisat.constraints
CardinalityDataStructure() - Constructor for class org.sat4j.minisat.constraints.CardinalityDataStructure
CardinalityDataStructureYanMax - Class in org.sat4j.minisat.constraints
CardinalityDataStructureYanMax() - Constructor for class org.sat4j.minisat.constraints.CardinalityDataStructureYanMax
CardinalityDataStructureYanMin - Class in org.sat4j.minisat.constraints
CardinalityDataStructureYanMin() - Constructor for class org.sat4j.minisat.constraints.CardinalityDataStructureYanMin
changedreason - Variable in class org.sat4j.minisat.core.SolverStats
CheckMUSSolutionListener - Class in org.sat4j.tools
CheckMUSSolutionListener(ASolverFactory<? extends ISolver>) - Constructor for class org.sat4j.tools.CheckMUSSolutionListener
checkThatItIsAMUS(IVecInt) - Method in class org.sat4j.tools.CheckMUSSolutionListener
CircularBuffer - Class in org.sat4j.minisat.core: Create a circular buffer of a given capacity allowing to compute efficiently the mean of the values storied.
CircularBuffer(int) - Constructor for class org.sat4j.minisat.core.CircularBuffer
claBumpActivity(Constr) - Method in class org.sat4j.minisat.core.Solver: Propagate activity to a constraint
ClausalCardinalitiesDecorator<T extends ISolver> - Class in org.sat4j.tools: A decorator for clausal cardinalities constraints.
ClausalCardinalitiesDecorator(T) - Constructor for class org.sat4j.tools.ClausalCardinalitiesDecorator
ClausalCardinalitiesDecorator(T, EncodingStrategyAdapter) - Constructor for class org.sat4j.tools.ClausalCardinalitiesDecorator
ClausalDataStructureWL - Class in org.sat4j.minisat.constraints
ClausalDataStructureWL() - Constructor for class org.sat4j.minisat.constraints.ClausalDataStructureWL
CLAUSE - Static variable in class org.sat4j.reader.JSONReader
ClauseOnlyLearning<D extends DataStructureFactory> - Class in org.sat4j.minisat.learning: The solver only records among all the constraints only the clauses.
ClauseOnlyLearning() - Constructor for class org.sat4j.minisat.learning.ClauseOnlyLearning
Clauses - Class in org.sat4j.minisat.constraints.cnf
Clauses() - Constructor for class org.sat4j.minisat.constraints.cnf.Clauses
cleaning() - Method in interface org.sat4j.specs.SearchListener: The solver is going to delete some learned clauses.
cleaning() - Method in class org.sat4j.tools.ConflictDepthTracing
cleaning() - Method in class org.sat4j.tools.ConflictLevelTracing
cleaning() - Method in class org.sat4j.tools.DecisionTracing
cleaning() - Method in class org.sat4j.tools.LearnedClausesSizeTracing
cleaning() - Method in class org.sat4j.tools.LearnedTracing
cleaning() - Method in class org.sat4j.tools.MultiTracing
cleaning() - Method in class org.sat4j.tools.SearchListenerAdapter
cleaning() - Method in class org.sat4j.tools.SpeedTracing
cleaning() - Method in class org.sat4j.tools.TextOutputTracing
clear() - Method in class org.sat4j.core.ConstrGroup
clear() - Method in class org.sat4j.core.ReadOnlyVec
clear() - Method in class org.sat4j.core.ReadOnlyVecInt
clear() - Method in class org.sat4j.core.Vec
clear() - Method in class org.sat4j.core.VecInt
clear() - Method in class org.sat4j.minisat.core.CircularBuffer
clear() - Method in class org.sat4j.minisat.core.IntQueue: Vide la queue
clear() - Method in interface org.sat4j.specs.IVec
clear() - Method in interface org.sat4j.specs.IVecInt
clearDecorated() - Method in class org.sat4j.tools.SolverDecorator: Method to be called to clear the decorator from its decorated solver.
clearLearntClauses() - Method in class org.sat4j.minisat.core.Solver
clearLearntClauses() - Method in interface org.sat4j.specs.ISolver: Remove clauses learned during the solving process.
clearLearntClauses() - Method in class org.sat4j.tools.AbstractOutputSolver
clearLearntClauses() - Method in class org.sat4j.tools.ManyCore
clearLearntClauses() - Method in class org.sat4j.tools.SolverDecorator
clearLearntClauses() - Method in class org.sat4j.tools.StatisticsSolver
close() - Method in class org.sat4j.reader.EfficientScanner
Commander - Class in org.sat4j.tools.encoding: Commander encoding for "at most one" and "at most k" cases.
Commander() - Constructor for class org.sat4j.tools.encoding.Commander
COMMENT_PREFIX - Static variable in class org.sat4j.AbstractLauncher
compare(A, A) - Method in class org.sat4j.core.DefaultComparator
compare(Constr, Constr) - Method in class org.sat4j.minisat.core.ActivityComparator
compute(ISolver) - Static method in class org.sat4j.tools.Backbone: Computes the backbone of a formula following the algorithm described in João Marques-Silva, Mikolás Janota, Inês Lynce: On Computing Backbones of Propositional Theories.
compute(ISolver, IVecInt) - Static method in class org.sat4j.tools.Backbone: Computes the backbone of a formula following the algorithm described in João Marques-Silva, Mikolás Janota, Inês Lynce: On Computing Backbones of Propositional Theories.
compute(ISolver, int[]) - Static method in class org.sat4j.tools.Backbone
compute(ISolver, int[], IVecInt) - Static method in class org.sat4j.tools.Backbone
computeAllMSS() - Method in class org.sat4j.tools.AllMUSes
computeAllMSS(SolutionFoundListener) - Method in class org.sat4j.tools.AllMUSes
computeAllMSSOrdered(SolutionFoundListener) - Method in class org.sat4j.tools.AllMUSes
computeAllMUSes() - Method in class org.sat4j.tools.AllMUSes
computeAllMUSes(SolutionFoundListener) - Method in class org.sat4j.tools.AllMUSes: Computes all the MUSes associated to the set of constraints added to the solver
computeAllMUSesOrdered(SolutionFoundListener) - Method in class org.sat4j.tools.AllMUSes
computePropagation(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
computeWatches() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
configureSolver(String[]) - Method in class org.sat4j.AbstractLauncher
configureSolver(String[]) - Method in class org.sat4j.BasicLauncher
configureSolver(String[]) - Method in class org.sat4j.MUSLauncher
ConflictDepthTracing - Class in org.sat4j.tools
ConflictDepthTracing(IVisualizationTool, IVisualizationTool, IVisualizationTool) - Constructor for class org.sat4j.tools.ConflictDepthTracing
conflictDetectedInWatchesFor(int, int) - Method in class org.sat4j.minisat.constraints.AbstractDataStructureFactory
conflictDetectedInWatchesFor(int, int) - Method in interface org.sat4j.minisat.core.DataStructureFactory
conflictFound(IConstr, int, int) - Method in interface org.sat4j.specs.SearchListener: a conflict has been found.
conflictFound(int) - Method in interface org.sat4j.specs.SearchListener: a conflict has been found while propagating values.
conflictFound(IConstr, int, int) - Method in class org.sat4j.tools.ConflictDepthTracing
conflictFound(IConstr, int, int) - Method in class org.sat4j.tools.ConflictLevelTracing
conflictFound(IConstr, int, int) - Method in class org.sat4j.tools.DecisionLevelTracing
conflictFound(IConstr, int, int) - Method in class org.sat4j.tools.DotSearchTracing
conflictFound(int) - Method in class org.sat4j.tools.DotSearchTracing
conflictFound(IConstr, int, int) - Method in class org.sat4j.tools.LBDTracing
conflictFound(IConstr, int, int) - Method in class org.sat4j.tools.LearnedClauseSizeTracing
conflictFound(IConstr, int, int) - Method in class org.sat4j.tools.MultiTracing
conflictFound(int) - Method in class org.sat4j.tools.MultiTracing
conflictFound(IConstr, int, int) - Method in class org.sat4j.tools.SearchListenerAdapter
conflictFound(int) - Method in class org.sat4j.tools.SearchListenerAdapter
conflictFound(IConstr, int, int) - Method in class org.sat4j.tools.TextOutputTracing
conflictFound(int) - Method in class org.sat4j.tools.TextOutputTracing
ConflictLevelTracing - Class in org.sat4j.tools
ConflictLevelTracing(IVisualizationTool, IVisualizationTool, IVisualizationTool) - Constructor for class org.sat4j.tools.ConflictLevelTracing
conflicts - Variable in class org.sat4j.minisat.core.SolverStats
ConflictTimer - Interface in org.sat4j.minisat.core: Conflict based timer.
ConflictTimerAdapter - Class in org.sat4j.minisat.core: Perform a task when a given number of conflicts is reached.
ConflictTimerAdapter(int) - Constructor for class org.sat4j.minisat.core.ConflictTimerAdapter
ConflictTimerContainer - Class in org.sat4j.minisat.core: Agregator for conflict timers (composite design pattern).
ConflictTimerContainer() - Constructor for class org.sat4j.minisat.core.ConflictTimerContainer
CONSOLE - Static variable in interface org.sat4j.specs.ILogAble
Constr - Interface in org.sat4j.minisat.core: Basic constraint abstraction used in Solver.
constraint - Variable in class org.sat4j.reader.JSONReader
constraintRegexp() - Method in class org.sat4j.reader.JSONReader
ConstrGroup - Class in org.sat4j.core: A utility class used to manage easily group of clauses to be deleted at some point in the solver.
ConstrGroup() - Constructor for class org.sat4j.core.ConstrGroup: Create a ConstrGroup that cannot contain null constrs.
ConstrGroup(boolean) - Constructor for class org.sat4j.core.ConstrGroup: Create a new constrGroup.
constrs - Variable in class org.sat4j.minisat.core.Solver: Set of original constraints.
contains(T) - Method in class org.sat4j.core.ReadOnlyVec
contains(int) - Method in class org.sat4j.core.ReadOnlyVecInt
contains(T) - Method in class org.sat4j.core.Vec
contains(int) - Method in class org.sat4j.core.VecInt
contains(T) - Method in interface org.sat4j.specs.IVec
contains(int) - Method in interface org.sat4j.specs.IVecInt
containsAt(int) - Method in class org.sat4j.core.ReadOnlyVecInt
containsAt(int, int) - Method in class org.sat4j.core.ReadOnlyVecInt
containsAt(int) - Method in class org.sat4j.core.VecInt
containsAt(int, int) - Method in class org.sat4j.core.VecInt
containsAt(int) - Method in interface org.sat4j.specs.IVecInt: returns the index of the first occurrence of e, else -1.
containsAt(int, int) - Method in interface org.sat4j.specs.IVecInt: returns the index of the first occurence of e occurring after from (excluded), else -1.
ContradictionException - Exception in org.sat4j.specs: That exception is launched whenever a trivial contradiction is found (e.g.
ContradictionException() - Constructor for exception org.sat4j.specs.ContradictionException
ContradictionException(String) - Constructor for exception org.sat4j.specs.ContradictionException
ContradictionException(Throwable) - Constructor for exception org.sat4j.specs.ContradictionException
ContradictionException(String, Throwable) - Constructor for exception org.sat4j.specs.ContradictionException
copyTo(IVec<T>) - Method in class org.sat4j.core.ReadOnlyVec
copyTo(E[]) - Method in class org.sat4j.core.ReadOnlyVec
copyTo(IVecInt) - Method in class org.sat4j.core.ReadOnlyVecInt
copyTo(int[]) - Method in class org.sat4j.core.ReadOnlyVecInt
copyTo(IVec<T>) - Method in class org.sat4j.core.Vec: Ces operations devraient se faire en temps constant.
copyTo(E[]) - Method in class org.sat4j.core.Vec
copyTo(IVecInt) - Method in class org.sat4j.core.VecInt: Copy the content of this vector into another one.
copyTo(int[]) - Method in class org.sat4j.core.VecInt: Copy the content of this vector into an array of integer.
copyTo(IVec<T>) - Method in interface org.sat4j.specs.IVec: Ces operations devraient se faire en temps constant.
copyTo(E[]) - Method in interface org.sat4j.specs.IVec
copyTo(IVecInt) - Method in interface org.sat4j.specs.IVecInt: C'est operations devraient se faire en temps constant.
copyTo(int[]) - Method in interface org.sat4j.specs.IVecInt
COUNT - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader
Counter - Class in org.sat4j.minisat.core
Counter() - Constructor for class org.sat4j.minisat.core.Counter
Counter(int) - Constructor for class org.sat4j.minisat.core.Counter
countSolutions() - Method in class org.sat4j.tools.SolutionCounter: Naive approach to count the solutions available in a boolean formula: each time a solution is found, a new clause is added to prevent it to be found again.
createCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.AbstractDataStructureFactory
createCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructure
createCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructureYanMax
createCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructureYanMin
createCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.MixedDataStructureDanielHT
createCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.MixedDataStructureDanielWL
createCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.MixedDataStructureSingleWL
createCardinalityConstraint(IVecInt, int) - Method in interface org.sat4j.minisat.core.DataStructureFactory: Create a cardinality constraint of the form sum li >= degree.
createClause(IVecInt) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructure
createClause(IVecInt) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructureYanMax
createClause(IVecInt) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructureYanMin
createClause(IVecInt) - Method in class org.sat4j.minisat.constraints.ClausalDataStructureWL
createClause(IVecInt) - Method in class org.sat4j.minisat.constraints.MixedDataStructureDanielHT
createClause(IVecInt) - Method in class org.sat4j.minisat.constraints.MixedDataStructureDanielWL
createClause(IVecInt) - Method in class org.sat4j.minisat.constraints.MixedDataStructureSingleWL
createClause(IVecInt) - Method in interface org.sat4j.minisat.core.DataStructureFactory
createLits() - Method in class org.sat4j.minisat.constraints.AbstractCardinalityDataStructure
createLits() - Method in class org.sat4j.minisat.constraints.AbstractDataStructureFactory
createLits() - Method in class org.sat4j.minisat.constraints.ClausalDataStructureWL
createLits() - Method in class org.sat4j.minisat.constraints.MixedDataStructureDanielHT
createLits() - Method in class org.sat4j.minisat.constraints.MixedDataStructureDanielWL
createLits() - Method in class org.sat4j.minisat.constraints.MixedDataStructureSingleWL
createNewVar(IVecInt) - Method in class org.sat4j.tools.AbstractClauseSelectorSolver
createReader(ISolver, String) - Method in class org.sat4j.AbstractLauncher
createReader(ISolver, String) - Method in class org.sat4j.BasicLauncher
createReader(ISolver, String) - Method in class org.sat4j.MUSLauncher
createSolverByName(String) - Method in class org.sat4j.core.ASolverFactory: create a solver from its String name. the solvername Xxxx must map one of the newXxxx methods.
createUnregisteredCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.AbstractDataStructureFactory
createUnregisteredCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructure
createUnregisteredCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructureYanMax
createUnregisteredCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructureYanMin
createUnregisteredCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.MixedDataStructureDanielHT
createUnregisteredCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.MixedDataStructureDanielWL
createUnregisteredCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.MixedDataStructureSingleWL
createUnregisteredCardinalityConstraint(IVecInt, int) - Method in interface org.sat4j.minisat.core.DataStructureFactory
createUnregisteredClause(IVecInt) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructure
createUnregisteredClause(IVecInt) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructureYanMax
createUnregisteredClause(IVecInt) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructureYanMin
createUnregisteredClause(IVecInt) - Method in class org.sat4j.minisat.constraints.ClausalDataStructureWL
createUnregisteredClause(IVecInt) - Method in class org.sat4j.minisat.constraints.MixedDataStructureDanielHT
createUnregisteredClause(IVecInt) - Method in class org.sat4j.minisat.constraints.MixedDataStructureDanielWL
createUnregisteredClause(IVecInt) - Method in class org.sat4j.minisat.constraints.MixedDataStructureSingleWL
createUnregisteredClause(IVecInt) - Method in interface org.sat4j.minisat.core.DataStructureFactory
criteria - Variable in class org.sat4j.tools.LexicoDecorator
CURRENT_OPTIMUM_VALUE_PREFIX - Static variable in interface org.sat4j.ILauncherMode
currentChar() - Method in class org.sat4j.reader.EfficientScanner
currentCriterion - Variable in class org.sat4j.tools.LexicoDecorator
currentDecisionLevel() - Method in class org.sat4j.minisat.core.Solver
currentDecisionLevel() - Method in interface org.sat4j.specs.ISolverService: To access the current decision level

D

DataStructureFactory - Interface in org.sat4j.minisat.core: The aim of the factory is to provide a concrete implementation of clauses, cardinality constraints and pseudo boolean consraints.
dec() - Method in class org.sat4j.minisat.core.Counter
decayActivities() - Method in class org.sat4j.minisat.core.Solver
DECISION - Static variable in interface org.sat4j.ILauncherMode: The launcher is in decision mode: the answer is either SAT, UNSAT or UNKNOWN
decisionLevel() - Method in class org.sat4j.minisat.core.Solver
DecisionLevelTracing - Class in org.sat4j.tools
DecisionLevelTracing(IVisualizationTool) - Constructor for class org.sat4j.tools.DecisionLevelTracing
decisions - Variable in class org.sat4j.minisat.core.SolverStats
DecisionTracing - Class in org.sat4j.tools
DecisionTracing(IVisualizationTool, IVisualizationTool, IVisualizationTool, IVisualizationTool) - Constructor for class org.sat4j.tools.DecisionTracing
decode(int[]) - Method in class org.sat4j.reader.AAGReader
decode(int[], PrintWriter) - Method in class org.sat4j.reader.AAGReader
decode(int[]) - Method in class org.sat4j.reader.AIGReader
decode(int[], PrintWriter) - Method in class org.sat4j.reader.AIGReader
decode(int[]) - Method in class org.sat4j.reader.DimacsReader
decode(int[], PrintWriter) - Method in class org.sat4j.reader.DimacsReader
decode(int[]) - Method in class org.sat4j.reader.InstanceReader: Deprecated.
decode(int[], PrintWriter) - Method in class org.sat4j.reader.InstanceReader
decode(int[]) - Method in class org.sat4j.reader.JSONReader: Deprecated.
decode(int[], PrintWriter) - Method in class org.sat4j.reader.JSONReader
decode(int[]) - Method in class org.sat4j.reader.LecteurDimacs
decode(int[], PrintWriter) - Method in class org.sat4j.reader.LecteurDimacs
decode(int[]) - Method in class org.sat4j.reader.Reader: Deprecated.
decode(int[], PrintWriter) - Method in class org.sat4j.reader.Reader: Produce a model using the reader format on a provided printwriter.
decode(int[]) - Method in class org.sat4j.tools.DimacsArrayReader
decorated() - Method in class org.sat4j.tools.SolverDecorator
DEFAULT_LUBY_FACTOR - Static variable in class org.sat4j.minisat.restarts.LubyRestarts
DefaultComparator<A extends Comparable<A>> - Class in org.sat4j.core: A simple comparator for comparable objects.
DefaultComparator() - Constructor for class org.sat4j.core.DefaultComparator
defaultSolver() - Method in class org.sat4j.core.ASolverFactory: To obtain the default solver of the library.
defaultSolver() - Method in class org.sat4j.LightFactory
defaultSolver() - Method in class org.sat4j.minisat.SolverFactory
degree - Variable in class org.sat4j.minisat.constraints.card.MinWatchCard: degree of the cardinality constraint
delete(int) - Method in class org.sat4j.core.ReadOnlyVec
delete(int) - Method in class org.sat4j.core.ReadOnlyVecInt
delete(int) - Method in class org.sat4j.core.Vec: Delete the ith element of the vector.
delete(int) - Method in class org.sat4j.core.VecInt: Delete the ith element of the vector.
delete(int) - Method in interface org.sat4j.specs.IVec: Delete the ith element of the vector.
delete(int) - Method in interface org.sat4j.specs.IVecInt: Delete the ith element of the vector.
delete(int[]) - Method in interface org.sat4j.specs.SearchListener: delete a clause
delete(int[]) - Method in class org.sat4j.tools.DotSearchTracing
delete(int[]) - Method in class org.sat4j.tools.MultiTracing
delete(int[]) - Method in class org.sat4j.tools.SearchListenerAdapter
delete(int[]) - Method in class org.sat4j.tools.TextOutputTracing
DeletionStrategy - Class in org.sat4j.tools.xplain: An implementation of the deletion based minimization.
DeletionStrategy() - Constructor for class org.sat4j.tools.xplain.DeletionStrategy
dequeue() - Method in class org.sat4j.minisat.core.IntQueue: returns the nexdt element in the queue.
dimacs2internal(IVecInt) - Method in class org.sat4j.minisat.core.Solver
DimacsArrayReader - Class in org.sat4j.tools: Very simple Dimacs array reader.
DimacsArrayReader(ISolver) - Constructor for class org.sat4j.tools.DimacsArrayReader
DimacsOutputSolver - Class in org.sat4j.tools: Solver used to display in a writer the CNF instance in Dimacs format.
DimacsOutputSolver() - Constructor for class org.sat4j.tools.DimacsOutputSolver
DimacsOutputSolver(PrintWriter) - Constructor for class org.sat4j.tools.DimacsOutputSolver
DimacsReader - Class in org.sat4j.reader: Very simple Dimacs file parser.
DimacsReader(ISolver) - Constructor for class org.sat4j.reader.DimacsReader
DimacsReader(ISolver, String) - Constructor for class org.sat4j.reader.DimacsReader
DimacsStringSolver - Class in org.sat4j.tools: Solver used to write down a CNF into a String.
DimacsStringSolver() - Constructor for class org.sat4j.tools.DimacsStringSolver
DimacsStringSolver(int) - Constructor for class org.sat4j.tools.DimacsStringSolver
disableNumberOfConstraintCheck() - Method in class org.sat4j.reader.DimacsReader
discard() - Method in class org.sat4j.opt.MaxSatDecorator
discard() - Method in class org.sat4j.opt.MinOneDecorator
discard() - Method in interface org.sat4j.specs.IOptimizationProblem: Deprecated.
discard() - Method in class org.sat4j.tools.LexicoDecorator
discardCurrentSolution() - Method in class org.sat4j.opt.MaxSatDecorator
discardCurrentSolution() - Method in class org.sat4j.opt.MinOneDecorator
discardCurrentSolution() - Method in interface org.sat4j.specs.IOptimizationProblem: Discard the current solution in the optimization problem.
discardCurrentSolution() - Method in class org.sat4j.tools.LexicoDecorator
discardLastestVar() - Method in class org.sat4j.tools.AbstractClauseSelectorSolver
discardSolutionsForOptimizing() - Method in class org.sat4j.tools.LexicoDecorator
displayAnswer() - Method in class org.sat4j.AbstractOptimizationLauncher: Deprecated.
displayHeader() - Method in class org.sat4j.AbstractLauncher
displayLicense() - Method in class org.sat4j.AbstractLauncher
displayResult() - Method in class org.sat4j.AbstractLauncher
displayResult() - Method in class org.sat4j.AbstractOptimizationLauncher: Deprecated.
displayResult(ISolver, IProblem, ILogAble, PrintWriter, Reader, long, boolean) - Method in interface org.sat4j.ILauncherMode: Output of the launcher when the solver stops
displayResult() - Method in class org.sat4j.MUSLauncher
DotSearchTracing<T> - Class in org.sat4j.tools: Class allowing to express the search as a tree in the dot language.
DotSearchTracing(String, Map<Integer, T>) - Constructor for class org.sat4j.tools.DotSearchTracing
dsfactory - Variable in class org.sat4j.minisat.core.Solver

E

EfficientScanner - Class in org.sat4j.reader: Efficient scanner based on the LecteurDimacs class written by Frederic Laihem.
EfficientScanner(InputStream, char) - Constructor for class org.sat4j.reader.EfficientScanner
EfficientScanner(InputStream) - Constructor for class org.sat4j.reader.EfficientScanner
EMPTY - Static variable in class org.sat4j.core.VecInt
empty() - Method in class org.sat4j.minisat.core.Heap
EncodingStrategy - Enum in org.sat4j.tools.encoding: This Enum describes the different encodings that can be used for the "at most one", "at most k", "exactly one", "exactly k" constraints.
EncodingStrategyAdapter - Class in org.sat4j.tools.encoding: The aim of this class is to use different encodings for specific constraints.
EncodingStrategyAdapter() - Constructor for class org.sat4j.tools.encoding.EncodingStrategyAdapter
end(Lbool) - Method in interface org.sat4j.specs.SearchListener: End the search.
end(Lbool) - Method in class org.sat4j.tools.ConflictDepthTracing
end(Lbool) - Method in class org.sat4j.tools.ConflictLevelTracing
end(Lbool) - Method in class org.sat4j.tools.DecisionLevelTracing
end(Lbool) - Method in class org.sat4j.tools.DecisionTracing
end(Lbool) - Method in class org.sat4j.tools.DotSearchTracing
end() - Method in class org.sat4j.tools.FileBasedVisualizationTool
end() - Method in interface org.sat4j.tools.IVisualizationTool
end(Lbool) - Method in class org.sat4j.tools.LBDTracing
end(Lbool) - Method in class org.sat4j.tools.LearnedClauseSizeTracing
end(Lbool) - Method in class org.sat4j.tools.LearnedClausesSizeTracing
end(Lbool) - Method in class org.sat4j.tools.MultiTracing
end(Lbool) - Method in class org.sat4j.tools.RupSearchListener
end(Lbool) - Method in class org.sat4j.tools.SearchEnumeratorListener
end(Lbool) - Method in class org.sat4j.tools.SearchListenerAdapter
end(Lbool) - Method in class org.sat4j.tools.SearchMinOneListener
end(Lbool) - Method in class org.sat4j.tools.SpeedTracing
end(Lbool) - Method in class org.sat4j.tools.TextOutputTracing
enqueue(int) - Method in class org.sat4j.minisat.core.Solver
enqueue(int, Constr) - Method in class org.sat4j.minisat.core.Solver
enqueue(int) - Method in interface org.sat4j.specs.UnitPropagationListener: satisfies a literal
enqueue(int, Constr) - Method in interface org.sat4j.specs.UnitPropagationListener: satisfies a literal
ensure(int) - Method in class org.sat4j.core.ReadOnlyVec
ensure(int) - Method in class org.sat4j.core.ReadOnlyVecInt
ensure(int) - Method in class org.sat4j.core.Vec
ensure(int) - Method in class org.sat4j.core.VecInt
ensure(int) - Method in class org.sat4j.minisat.core.IntQueue: Utilisee pour accroitre dynamiquement la taille de la queue.
ensure(int) - Method in interface org.sat4j.specs.IVec
ensure(int) - Method in interface org.sat4j.specs.IVecInt
ensurePool(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
ensurePool(int) - Method in interface org.sat4j.minisat.core.ILits: Make sure that all data structures are ready to manage howmany boolean variables.
eof() - Method in class org.sat4j.reader.EfficientScanner
equals(Object) - Method in class org.sat4j.core.ReadOnlyVec
equals(Object) - Method in class org.sat4j.core.ReadOnlyVecInt
equals(Object) - Method in class org.sat4j.core.Vec
equals(Object) - Method in class org.sat4j.core.VecInt: Two vectors are equals iff they have the very same elements in the order.
equals(Object) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
equals(Object) - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
equals(Object) - Method in class org.sat4j.minisat.constraints.cnf.HTClause
equals(Object) - Method in class org.sat4j.minisat.constraints.cnf.WLClause
evaluate() - Method in class org.sat4j.tools.LexicoDecorator
evaluate(int) - Method in class org.sat4j.tools.LexicoDecorator
exitCode - Variable in class org.sat4j.AbstractLauncher
ExitCode - Class in org.sat4j: Enumeration allowing to manage easily exit code for the SAT and PB Competitions.
expectedNbOfConstr - Variable in class org.sat4j.reader.DimacsReader
EXPENSIVE_SIMPLIFICATION - Variable in class org.sat4j.minisat.core.Solver
EXPENSIVE_SIMPLIFICATION_WLONLY - Variable in class org.sat4j.minisat.core.Solver
expireTimeout() - Method in class org.sat4j.minisat.core.Solver
expireTimeout() - Method in interface org.sat4j.specs.ISolver: Expire the timeout of the solver.
expireTimeout() - Method in class org.sat4j.tools.AbstractOutputSolver
expireTimeout() - Method in class org.sat4j.tools.ManyCore
expireTimeout() - Method in class org.sat4j.tools.SolverDecorator
expireTimeout() - Method in class org.sat4j.tools.StatisticsSolver
explain(ISolver, Map<Integer, ?>, IVecInt) - Method in class org.sat4j.tools.xplain.DeletionStrategy
explain() - Method in class org.sat4j.tools.xplain.HighLevelXplain
explain(ISolver, Map<Integer, ?>, IVecInt) - Method in class org.sat4j.tools.xplain.InsertionStrategy
explain(ISolver, Map<Integer, ?>, IVecInt) - Method in interface org.sat4j.tools.xplain.MinimizationStrategy
explain(ISolver, Map<Integer, ?>, IVecInt) - Method in class org.sat4j.tools.xplain.QuickXplain2001Strategy
explain(ISolver, Map<Integer, ?>, IVecInt) - Method in class org.sat4j.tools.xplain.QuickXplainStrategy
explain() - Method in class org.sat4j.tools.xplain.Xplain: Provide an explanation of the inconsistency in term of a subset minimal set of constraints.
Explainer - Interface in org.sat4j.tools.xplain
ExtendedDimacsArrayReader - Class in org.sat4j.tools: Reader for the Extended Dimacs format proposed by Fahiem Bacchus and Toby Walsh in array representation (without the terminating 0).
ExtendedDimacsArrayReader(ISolver) - Constructor for class org.sat4j.tools.ExtendedDimacsArrayReader
externalState() - Method in class org.sat4j.tools.AbstractClauseSelectorSolver: In external state, the solver will prevent the selector variables to be satisfied.

F

FALSE - Static variable in class org.sat4j.specs.Lbool
FALSE - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader
FileBasedVisualizationTool - Class in org.sat4j.tools
FileBasedVisualizationTool(String) - Constructor for class org.sat4j.tools.FileBasedVisualizationTool
findModel() - Method in class org.sat4j.minisat.core.Solver
findModel(IVecInt) - Method in class org.sat4j.minisat.core.Solver
findModel() - Method in interface org.sat4j.specs.IProblem: Look for a model satisfying all the clauses available in the problem.
findModel(IVecInt) - Method in interface org.sat4j.specs.IProblem: Look for a model satisfying all the clauses available in the problem.
findModel() - Method in class org.sat4j.tools.AbstractOutputSolver
findModel(IVecInt) - Method in class org.sat4j.tools.AbstractOutputSolver
findModel() - Method in class org.sat4j.tools.ManyCore
findModel(IVecInt) - Method in class org.sat4j.tools.ManyCore
findModel() - Method in class org.sat4j.tools.OptToSatAdapter
findModel(IVecInt) - Method in class org.sat4j.tools.OptToSatAdapter
findModel() - Method in class org.sat4j.tools.SolverDecorator
findModel(IVecInt) - Method in class org.sat4j.tools.SolverDecorator
findModel() - Method in class org.sat4j.tools.StatisticsSolver
findModel(IVecInt) - Method in class org.sat4j.tools.StatisticsSolver
findModel() - Method in class org.sat4j.tools.xplain.HighLevelXplain
findModel(IVecInt) - Method in class org.sat4j.tools.xplain.HighLevelXplain
findModel() - Method in class org.sat4j.tools.xplain.Xplain
findModel(IVecInt) - Method in class org.sat4j.tools.xplain.Xplain
firstConstr - Variable in class org.sat4j.tools.AbstractOutputSolver
fixCriterionValue() - Method in class org.sat4j.tools.LexicoDecorator
FixedLengthLearning<D extends DataStructureFactory> - Class in org.sat4j.minisat.learning: A learning scheme for learning constraints of size smaller than a given constant.
FixedLengthLearning() - Constructor for class org.sat4j.minisat.learning.FixedLengthLearning
FixedLengthLearning(int) - Constructor for class org.sat4j.minisat.learning.FixedLengthLearning
fixedNbClauses - Variable in class org.sat4j.tools.AbstractOutputSolver
FixedPeriodRestarts - Class in org.sat4j.minisat.restarts
FixedPeriodRestarts() - Constructor for class org.sat4j.minisat.restarts.FixedPeriodRestarts
fixedSize(int) - Method in class org.sat4j.minisat.core.Solver
flushConstraint() - Method in class org.sat4j.reader.DimacsReader
flushConstraint() - Method in class org.sat4j.reader.GroupedCNFReader
forceObjectiveValueTo(Number) - Method in class org.sat4j.opt.MaxSatDecorator
forceObjectiveValueTo(Number) - Method in class org.sat4j.opt.MinOneDecorator
forceObjectiveValueTo(Number) - Method in interface org.sat4j.specs.IOptimizationProblem: Force the value of the objective function.
forceObjectiveValueTo(Number) - Method in class org.sat4j.tools.LexicoDecorator
forgets(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
forgets(int) - Method in interface org.sat4j.minisat.core.ILits: Removes a variable from the formula.
formatString - Variable in class org.sat4j.reader.DimacsReader
formula - Variable in class org.sat4j.reader.JSONReader
forwardActivity(double) - Method in class org.sat4j.minisat.constraints.card.AtLeast
forwardActivity(double) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
forwardActivity(double) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
forwardActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.LearntBinaryClause
forwardActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.LearntHTClause
forwardActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.LearntWLClause
forwardActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.OriginalBinaryClause
forwardActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.OriginalHTClause
forwardActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.OriginalWLClause
forwardActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
forwardActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
forwardActivity(double) - Method in interface org.sat4j.minisat.core.Constr: Deprecated.
fromLastDecisionLevel(IVecInt) - Method in class org.sat4j.minisat.core.Solver
fullAdderCarry(int, int, int, int) - Method in class org.sat4j.tools.GateTranslator
fullAdderSum(int, int, int, int) - Method in class org.sat4j.tools.GateTranslator
FullClauseSelectorSolver<T extends ISolver> - Class in org.sat4j.tools
FullClauseSelectorSolver(T, boolean) - Constructor for class org.sat4j.tools.FullClauseSelectorSolver

G

gateFalse(int) - Method in class org.sat4j.tools.GateTranslator: translate y <=> FALSE into a clause.
GateTranslator - Class in org.sat4j.tools: Utility class to easily feed a SAT solver using logical gates.
GateTranslator(ISolver) - Constructor for class org.sat4j.tools.GateTranslator
gateTrue(int) - Method in class org.sat4j.tools.GateTranslator: translate y <=> TRUE into a clause.
get(int) - Method in class org.sat4j.core.ConstrGroup
get(int) - Method in class org.sat4j.core.ReadOnlyVec
get(int) - Method in class org.sat4j.core.ReadOnlyVecInt
get(int) - Method in class org.sat4j.core.Vec
get(int) - Method in class org.sat4j.core.VecInt
get(int) - Method in class org.sat4j.minisat.constraints.card.AtLeast
get(int) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
get(int) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
get(int) - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause: Retourne le ieme literal de la clause.
get(int) - Method in class org.sat4j.minisat.constraints.cnf.HTClause: Return the ith literal of the clause.
get(int) - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
get(int) - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
get(int) - Method in class org.sat4j.minisat.constraints.cnf.WLClause: Retourne le ieme literal de la clause.
get(int) - Method in class org.sat4j.minisat.core.Heap
get(int) - Method in interface org.sat4j.specs.IConstr: returns the ith literal in the constraint
get(int) - Method in interface org.sat4j.specs.IVec
get(int) - Method in interface org.sat4j.specs.IVecInt
getActivity() - Method in class org.sat4j.core.ConstrGroup
getActivity() - Method in class org.sat4j.minisat.constraints.card.AtLeast
getActivity() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard: Obtenir la valeur de l'activit?
getActivity() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard: Returns the activity of the constraint
getActivity() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
getActivity() - Method in class org.sat4j.minisat.constraints.cnf.HTClause
getActivity() - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
getActivity() - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
getActivity() - Method in class org.sat4j.minisat.constraints.cnf.WLClause
getActivity() - Method in interface org.sat4j.specs.IConstr: To obtain the activity of the constraint.
getActivityPercent() - Method in class org.sat4j.minisat.learning.ActiveLearning
getAddedVars() - Method in class org.sat4j.tools.AbstractClauseSelectorSolver
getAddedVars() - Method in class org.sat4j.tools.FullClauseSelectorSolver
getAddedVars() - Method in class org.sat4j.tools.GroupClauseSelectorSolver
getAddedVars() - Method in class org.sat4j.tools.NegationDecorator
getAtLeastKEncoding() - Method in class org.sat4j.tools.encoding.Policy
getAtLeastOneEncoding() - Method in class org.sat4j.tools.encoding.Policy
getAtMostKEncoding() - Method in class org.sat4j.tools.encoding.Policy
getAtMostOneEncoding() - Method in class org.sat4j.tools.encoding.Policy
getBeginTime() - Method in class org.sat4j.AbstractLauncher: Obtaining the current time spent since the beginning of the solving process.
getClaDecay() - Method in class org.sat4j.minisat.core.SearchParams
getCoef(int) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
getConflictBoundIncFactor() - Method in class org.sat4j.minisat.core.SearchParams
getConstr(int) - Method in class org.sat4j.core.ConstrGroup
getConstraints() - Method in class org.sat4j.tools.FullClauseSelectorSolver
getConstrs() - Method in class org.sat4j.tools.FullClauseSelectorSolver
getCurrentExitCode() - Method in interface org.sat4j.ILauncherMode: Allow the launcher to get the current status of the problem: SAT, UNSAT, UPPER_BOUND, etc.
getDegree() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
getDSFactory() - Method in class org.sat4j.minisat.core.Solver
getExactlyKEncoding() - Method in class org.sat4j.tools.encoding.Policy
getExactlyOneEncoding() - Method in class org.sat4j.tools.encoding.Policy
getExitCode() - Method in class org.sat4j.AbstractLauncher: Get the value of the ExitCode
getExpectedNumberOfClauses() - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
getFactor() - Method in class org.sat4j.minisat.restarts.LubyRestarts
getFilename() - Method in class org.sat4j.tools.FileBasedVisualizationTool
getFromPool(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
getFromPool(int) - Method in interface org.sat4j.minisat.core.ILits: Translates a Dimacs literal into an internal representation literal.
getInitConflictBound() - Method in class org.sat4j.minisat.core.SearchParams
getInstanceName(String[]) - Method in class org.sat4j.AbstractLauncher
getInstanceName(String[]) - Method in class org.sat4j.BasicLauncher
getInstanceName(String[]) - Method in class org.sat4j.MUSLauncher
getIthConstr(int) - Method in class org.sat4j.minisat.core.Solver: returns the ith constraint in the solver.
getLastClause() - Method in class org.sat4j.tools.FullClauseSelectorSolver
getLastConstr() - Method in class org.sat4j.tools.FullClauseSelectorSolver
getLearnedConstraints() - Method in class org.sat4j.minisat.core.Solver
getLearnedConstraints() - Method in interface org.sat4j.specs.ISolverService: Read-Only access to the list of constraints learned and not deleted so far in the solver.
getLevel(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
getLevel(int) - Method in interface org.sat4j.minisat.core.ILits: Returns the level at which that literal has been assigned a value, else -1.
getLimit() - Method in class org.sat4j.minisat.learning.ActiveLearning
getLimit() - Method in class org.sat4j.minisat.learning.PercentLengthLearning
getLiterals(String) - Method in class org.sat4j.reader.JSONReader
getLiteralsPropagatedAt(int) - Method in class org.sat4j.minisat.core.Solver
getLiteralsPropagatedAt(int) - Method in interface org.sat4j.specs.ISolverService: To access the literals propagated at a specific decision level.
getLits() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
getLits() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
getLits() - Method in class org.sat4j.minisat.constraints.cnf.HTClause
getLits() - Method in class org.sat4j.minisat.constraints.cnf.WLClause
getLogger() - Method in interface org.sat4j.minisat.core.ICDCL
getLogger() - Method in class org.sat4j.minisat.core.Solver
getLogPrefix() - Method in class org.sat4j.minisat.core.Solver
getLogPrefix() - Method in interface org.sat4j.specs.ISolver
getLogPrefix() - Method in interface org.sat4j.specs.ISolverService
getLogPrefix() - Method in class org.sat4j.tools.AbstractOutputSolver
getLogPrefix() - Method in class org.sat4j.tools.ManyCore
getLogPrefix() - Method in class org.sat4j.tools.SolverDecorator
getLogPrefix() - Method in class org.sat4j.tools.StatisticsSolver
getLogWriter() - Method in class org.sat4j.AbstractLauncher
getMaxLength() - Method in class org.sat4j.minisat.learning.FixedLengthLearning
getmin() - Method in class org.sat4j.minisat.core.Heap
getMssList() - Method in class org.sat4j.tools.AllMUSes
getNbexpectedclauses() - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
getNumberOfSolutionFound() - Method in class org.sat4j.tools.SearchEnumeratorListener
getObjectiveValue() - Method in class org.sat4j.opt.MaxSatDecorator
getObjectiveValue() - Method in class org.sat4j.opt.MinOneDecorator
getObjectiveValue() - Method in interface org.sat4j.specs.IOptimizationProblem: Read only access to the value of the objective function for the current solution.
getObjectiveValue() - Method in class org.sat4j.tools.LexicoDecorator
getObjectiveValue(int) - Method in class org.sat4j.tools.LexicoDecorator
getOrder() - Method in interface org.sat4j.minisat.core.ICDCL
getOrder() - Method in class org.sat4j.minisat.core.Solver
getOut() - Method in class org.sat4j.tools.DimacsStringSolver
getOutLearnt() - Method in class org.sat4j.minisat.core.Solver
getPeriod() - Method in class org.sat4j.minisat.orders.PureOrder
getPeriod() - Method in class org.sat4j.minisat.restarts.FixedPeriodRestarts
getPhaseSelectionStrategy() - Method in interface org.sat4j.minisat.core.IOrder
getPhaseSelectionStrategy() - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
getPhaseSelectionStrategy() - Method in class org.sat4j.minisat.orders.TabuListDecorator
getPhaseSelectionStrategy() - Method in class org.sat4j.minisat.orders.VarOrderHeap
getPrevboolmodel() - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
getPrevfullmodel() - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
getPrevmodel() - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
getProbability() - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
getReader() - Method in class org.sat4j.AbstractLauncher
getReason(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
getReason(int) - Method in interface org.sat4j.minisat.core.ILits: Returns the reason of the assignment of a literal.
getRestartStrategy() - Method in interface org.sat4j.minisat.core.ICDCL
getRestartStrategy() - Method in class org.sat4j.minisat.core.Solver
getSearchListener() - Method in class org.sat4j.minisat.core.Solver
getSearchListener() - Method in interface org.sat4j.specs.ISolver: Get the current SearchListener.
getSearchListener() - Method in class org.sat4j.tools.AbstractOutputSolver
getSearchListener() - Method in class org.sat4j.tools.ManyCore
getSearchListener() - Method in class org.sat4j.tools.SolverDecorator
getSearchListener() - Method in class org.sat4j.tools.StatisticsSolver
getSearchParams() - Method in interface org.sat4j.minisat.core.ICDCL
getSearchParams() - Method in class org.sat4j.minisat.core.Solver
getSimplifier() - Method in interface org.sat4j.minisat.core.ICDCL
getSimplifier() - Method in class org.sat4j.minisat.core.Solver
getSolver() - Method in class org.sat4j.reader.DimacsReader
getSolver() - Method in class org.sat4j.tools.DimacsArrayReader
getSolverInstance() - Method in class org.sat4j.tools.AllMUSes: Gets an instance of ISolver that can be used to compute all MUSes
getSolvers() - Method in class org.sat4j.tools.ManyCore
getSolvingEngine() - Method in class org.sat4j.minisat.core.Solver
getSolvingEngine() - Method in interface org.sat4j.specs.ISolver: Retrieve the real engine in case the engine is decorated by one or several decorator.
getSolvingEngine() - Method in class org.sat4j.tools.AbstractOutputSolver
getSolvingEngine() - Method in class org.sat4j.tools.ManyCore
getSolvingEngine() - Method in class org.sat4j.tools.SolverDecorator
getSolvingEngine() - Method in class org.sat4j.tools.StatisticsSolver
getStat() - Method in class org.sat4j.minisat.core.Solver
getStat() - Method in interface org.sat4j.specs.ISolver: To obtain a map of the available statistics from the solver.
getStat() - Method in class org.sat4j.tools.AbstractOutputSolver
getStat() - Method in class org.sat4j.tools.ManyCore
getStat() - Method in class org.sat4j.tools.SolverDecorator
getStat() - Method in class org.sat4j.tools.StatisticsSolver
getStats() - Method in interface org.sat4j.minisat.core.ICDCL
getStats() - Method in class org.sat4j.minisat.core.Solver
getString(String) - Static method in class org.sat4j.Messages
getTimeout() - Method in class org.sat4j.minisat.core.Solver
getTimeout() - Method in interface org.sat4j.specs.ISolver: Useful to check the internal timeout of the solver.
getTimeout() - Method in class org.sat4j.tools.AbstractOutputSolver
getTimeout() - Method in class org.sat4j.tools.ManyCore
getTimeout() - Method in class org.sat4j.tools.SolverDecorator
getTimeout() - Method in class org.sat4j.tools.StatisticsSolver
getTimeoutMs() - Method in class org.sat4j.minisat.core.Solver
getTimeoutMs() - Method in interface org.sat4j.specs.ISolver: Useful to check the internal timeout of the solver.
getTimeoutMs() - Method in class org.sat4j.tools.AbstractOutputSolver
getTimeoutMs() - Method in class org.sat4j.tools.ManyCore
getTimeoutMs() - Method in class org.sat4j.tools.SolverDecorator
getTimeoutMs() - Method in class org.sat4j.tools.StatisticsSolver
getTimer() - Method in interface org.sat4j.minisat.core.LearnedConstraintsDeletionStrategy
getValue() - Method in class org.sat4j.minisat.core.Counter
getVarDecay() - Method in class org.sat4j.minisat.core.SearchParams
getVariableHeuristics() - Method in interface org.sat4j.minisat.core.IOrder: Read-Only access to the value of the heuristics for each variable.
getVariableHeuristics() - Method in class org.sat4j.minisat.core.Solver
getVariableHeuristics() - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
getVariableHeuristics() - Method in class org.sat4j.minisat.orders.TabuListDecorator
getVariableHeuristics() - Method in class org.sat4j.minisat.orders.VarOrderHeap
getVariableHeuristics() - Method in interface org.sat4j.specs.ISolverService: Read-Only access to the value of the heuristics for each variable.
getVarToHighLevel() - Method in class org.sat4j.tools.GroupClauseSelectorSolver
getVocabulary() - Method in class org.sat4j.minisat.constraints.AbstractDataStructureFactory
getVocabulary() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
getVocabulary() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
getVocabulary() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
getVocabulary() - Method in class org.sat4j.minisat.constraints.cnf.HTClause
getVocabulary() - Method in class org.sat4j.minisat.constraints.cnf.WLClause
getVocabulary() - Method in interface org.sat4j.minisat.core.DataStructureFactory
getVocabulary() - Method in class org.sat4j.minisat.core.Solver
getVocabulary() - Method in class org.sat4j.minisat.orders.VarOrderHeap
getWatchesFor(int) - Method in class org.sat4j.minisat.constraints.AbstractDataStructureFactory
getWatchesFor(int) - Method in interface org.sat4j.minisat.core.DataStructureFactory
glucose - Variable in class org.sat4j.minisat.core.Solver
Glucose21Restarts - Class in org.sat4j.minisat.restarts: Dynamic restart strategy of Glucose 2.1 as presented in Refining restarts strategies for SAT and UNSAT formulae.
Glucose21Restarts() - Constructor for class org.sat4j.minisat.restarts.Glucose21Restarts
GroupClauseSelectorSolver<T extends ISolver> - Class in org.sat4j.tools
GroupClauseSelectorSolver(T) - Constructor for class org.sat4j.tools.GroupClauseSelectorSolver
GroupedCNFReader - Class in org.sat4j.reader
GroupedCNFReader(IGroupSolver) - Constructor for class org.sat4j.reader.GroupedCNFReader
growTo(int, T) - Method in class org.sat4j.core.ReadOnlyVec
growTo(int, int) - Method in class org.sat4j.core.ReadOnlyVecInt
growTo(int, T) - Method in class org.sat4j.core.Vec
growTo(int, int) - Method in class org.sat4j.core.VecInt
growTo(int, T) - Method in interface org.sat4j.specs.IVec
growTo(int, int) - Method in interface org.sat4j.specs.IVecInt

H

halfAdderCarry(int, int, int) - Method in class org.sat4j.tools.GateTranslator
halfAdderSum(int, int, int) - Method in class org.sat4j.tools.GateTranslator
halfOr(int, IVecInt) - Method in class org.sat4j.tools.GateTranslator: translate y <= x1 \/ x2 \/ ... \/ xn into clauses.
handleCard(String) - Method in class org.sat4j.reader.JSONReader
handleConstr(int, int, int[]) - Method in class org.sat4j.tools.DimacsArrayReader
handleConstr(int, int, int[]) - Method in class org.sat4j.tools.ExtendedDimacsArrayReader: Handles a single constraint (constraint == Extended Dimacs circuit gate).
handleFileName(String, String) - Method in class org.sat4j.reader.InstanceReader
handleLine() - Method in class org.sat4j.reader.DimacsReader
handleLine() - Method in class org.sat4j.reader.GroupedCNFReader
handleNotHandled(String) - Method in class org.sat4j.reader.JSONReader
hasASingleSolution() - Method in class org.sat4j.tools.SingleSolutionDetector: Please use that method only after a positive answer from isSatisfiable() (else a runtime exception will be launched).
hasASingleSolution(IVecInt) - Method in class org.sat4j.tools.SingleSolutionDetector: Please use that method only after a positive answer from isSatisfiable(assumptions) (else a runtime exception will be launched).
hashCode() - Method in class org.sat4j.core.ReadOnlyVec
hashCode() - Method in class org.sat4j.core.ReadOnlyVecInt
hashCode() - Method in class org.sat4j.core.Vec
hashCode() - Method in class org.sat4j.core.VecInt
hashCode() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
hashCode() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
hashCode() - Method in class org.sat4j.minisat.constraints.cnf.HTClause
hashCode() - Method in class org.sat4j.minisat.constraints.cnf.WLClause
hasNext() - Method in interface org.sat4j.specs.IteratorInt
hasNoObjectiveFunction() - Method in class org.sat4j.opt.MaxSatDecorator
hasNoObjectiveFunction() - Method in class org.sat4j.opt.MinOneDecorator
hasNoObjectiveFunction() - Method in interface org.sat4j.specs.IOptimizationProblem: If the optimization problem has no objective function, then it is a simple decision problem.
hasNoObjectiveFunction() - Method in class org.sat4j.tools.LexicoDecorator
head - Variable in class org.sat4j.minisat.constraints.cnf.BinaryClause
head - Variable in class org.sat4j.minisat.constraints.cnf.HTClause
Heap - Class in org.sat4j.minisat.core: Heap implementation used to maintain the variables order in some heuristics.
Heap(double[]) - Constructor for class org.sat4j.minisat.core.Heap
heap - Variable in class org.sat4j.minisat.orders.VarOrderHeap
heapProperty() - Method in class org.sat4j.minisat.core.Heap
heapProperty(int) - Method in class org.sat4j.minisat.core.Heap
HeuristicsTracing - Class in org.sat4j.tools
HeuristicsTracing(IVisualizationTool) - Constructor for class org.sat4j.tools.HeuristicsTracing
HighLevelXplain<T extends ISolver> - Class in org.sat4j.tools.xplain: Computation of MUS in a structured CNF, i.e. the clauses belong to components, the explanation is to be extracted in terms of components.
HighLevelXplain(T) - Constructor for class org.sat4j.tools.xplain.HighLevelXplain
HTClause - Class in org.sat4j.minisat.constraints.cnf: Lazy data structure for clause using the Head Tail data structure from SATO, The original scheme is improved by avoiding moving pointers to literals but moving the literals themselves.
HTClause(IVecInt, ILits) - Constructor for class org.sat4j.minisat.constraints.cnf.HTClause: Creates a new basic clause

I

ICDCL<D extends DataStructureFactory> - Interface in org.sat4j.minisat.core: Abstraction for Conflict Driven Clause Learning Solver.
IConstr - Interface in org.sat4j.specs: The most general abstraction for handling a constraint.
IFF - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader
iff(int, IVecInt) - Method in class org.sat4j.tools.GateTranslator: translate y <=> (x1 <=> x2 <=> ... <=> xn) into clauses.
IFTHENELSE - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader
ignoredclauses - Variable in class org.sat4j.minisat.core.SolverStats
IGroupSolver - Interface in org.sat4j.specs: Represents a CNF in which clauses are grouped into levels.
ILauncherMode - Interface in org.sat4j: Allow to change the behavior of the launcher (either decision or optimization mode)
ILits - Interface in org.sat4j.minisat.core: That interface manages the solver's internal vocabulary.
ILogAble - Interface in org.sat4j.specs: Utility interface to catch objects with logging capability (able to log).
IMPLIES - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader
importedUnits - Variable in class org.sat4j.minisat.core.SolverStats
inc() - Method in class org.sat4j.minisat.core.Counter
incActivity(double) - Method in class org.sat4j.minisat.constraints.card.AtLeast
incActivity(double) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard: Incr?
incActivity(double) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard: Increments activity of the constraint
incActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.LearntBinaryClause
incActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.LearntHTClause
incActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.LearntWLClause
incActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.OriginalBinaryClause
incActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.OriginalHTClause
incActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.OriginalWLClause
incActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
incActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
incActivity(double) - Method in interface org.sat4j.minisat.core.Constr: Increase the constraint activity.
increase(int) - Method in class org.sat4j.minisat.core.Heap
indexOf(T) - Method in class org.sat4j.core.ReadOnlyVec
indexOf(int) - Method in class org.sat4j.core.ReadOnlyVecInt
indexOf(T) - Method in class org.sat4j.core.Vec
indexOf(int) - Method in class org.sat4j.core.VecInt
indexOf(T) - Method in interface org.sat4j.specs.IVec
indexOf(int) - Method in interface org.sat4j.specs.IVecInt
inHeap(int) - Method in class org.sat4j.minisat.core.Heap
init(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
init(int) - Method in interface org.sat4j.minisat.core.ILits
init() - Method in interface org.sat4j.minisat.core.IOrder: that method has the responsibility to initialize all arrays in the heuristics.
init(int) - Method in interface org.sat4j.minisat.core.IPhaseSelectionStrategy: that method has the responsibility to initialize all arrays in the heuristics.
init(int, int) - Method in interface org.sat4j.minisat.core.IPhaseSelectionStrategy: initialize the phase of a given variable to the given value.
init() - Method in interface org.sat4j.minisat.core.LearnedConstraintsDeletionStrategy
init() - Method in interface org.sat4j.minisat.core.LearningStrategy: hook method called just before the search begins.
init(SearchParams, SolverStats) - Method in interface org.sat4j.minisat.core.RestartStrategy: Hook method called just before the search starts.
init() - Method in class org.sat4j.minisat.learning.FixedLengthLearning
init() - Method in class org.sat4j.minisat.learning.LimitedLearning
init() - Method in class org.sat4j.minisat.learning.PercentLengthLearning
init(int) - Method in class org.sat4j.minisat.orders.NegativeLiteralSelectionStrategy
init(int, int) - Method in class org.sat4j.minisat.orders.NegativeLiteralSelectionStrategy
init(int) - Method in class org.sat4j.minisat.orders.PositiveLiteralSelectionStrategy
init(int, int) - Method in class org.sat4j.minisat.orders.PositiveLiteralSelectionStrategy
init(int) - Method in class org.sat4j.minisat.orders.RandomLiteralSelectionStrategy
init(int, int) - Method in class org.sat4j.minisat.orders.RandomLiteralSelectionStrategy
init() - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
init() - Method in class org.sat4j.minisat.orders.SubsetVarOrder
init() - Method in class org.sat4j.minisat.orders.TabuListDecorator
init() - Method in class org.sat4j.minisat.orders.VarOrderHeap: that method has the responsability to initialize all arrays in the heuristics.
init(SearchParams, SolverStats) - Method in class org.sat4j.minisat.restarts.ArminRestarts
init(SearchParams, SolverStats) - Method in class org.sat4j.minisat.restarts.FixedPeriodRestarts
init(SearchParams, SolverStats) - Method in class org.sat4j.minisat.restarts.Glucose21Restarts
init(SearchParams, SolverStats) - Method in class org.sat4j.minisat.restarts.LubyRestarts
init(SearchParams, SolverStats) - Method in class org.sat4j.minisat.restarts.MiniSATRestarts
init(SearchParams, SolverStats) - Method in class org.sat4j.minisat.restarts.NoRestarts
init(S) - Method in interface org.sat4j.specs.SearchListener: Provide access to the solver's controllable interface.
init(ISolverService) - Method in class org.sat4j.tools.ConflictDepthTracing
init(ISolverService) - Method in class org.sat4j.tools.ConflictLevelTracing
init(ISolverService) - Method in class org.sat4j.tools.DecisionTracing
init() - Method in class org.sat4j.tools.FileBasedVisualizationTool
init(ISolverService) - Method in class org.sat4j.tools.HeuristicsTracing
init() - Method in interface org.sat4j.tools.IVisualizationTool
init(ISolverService) - Method in class org.sat4j.tools.LearnedTracing
init(T) - Method in class org.sat4j.tools.MultiTracing
init(S) - Method in class org.sat4j.tools.RupSearchListener
init(ISolverService) - Method in class org.sat4j.tools.SearchEnumeratorListener
init(S) - Method in class org.sat4j.tools.SearchListenerAdapter
init(ISolverService) - Method in class org.sat4j.tools.SearchMinOneListener
init(ISolverService) - Method in class org.sat4j.tools.TextOutputTracing
initStats(SolverStats) - Method in class org.sat4j.minisat.core.Solver
insert(int) - Method in class org.sat4j.minisat.core.Heap
insert(int) - Method in class org.sat4j.minisat.core.IntQueue: Add an element to the queue.
insertFirst(T) - Method in class org.sat4j.core.ReadOnlyVec
insertFirst(int) - Method in class org.sat4j.core.ReadOnlyVecInt
insertFirst(T) - Method in class org.sat4j.core.Vec: Insert an element at the very beginning of the vector.
insertFirst(int) - Method in class org.sat4j.core.VecInt: Insert an element at the very begining of the vector.
insertFirst(T) - Method in interface org.sat4j.specs.IVec: Insert an element at the very begining of the vector.
insertFirst(int) - Method in interface org.sat4j.specs.IVecInt: Insert an element at the very begining of the vector.
insertFirstWithShifting(T) - Method in class org.sat4j.core.ReadOnlyVec
insertFirstWithShifting(T) - Method in class org.sat4j.core.Vec
insertFirstWithShifting(T) - Method in interface org.sat4j.specs.IVec
InsertionStrategy - Class in org.sat4j.tools.xplain: An implementation of the ReplayXplain algorithm as explained by Ulrich Junker in the following paper:
InsertionStrategy() - Constructor for class org.sat4j.tools.xplain.InsertionStrategy
inspects - Variable in class org.sat4j.minisat.core.SolverStats
instance() - Static method in class org.sat4j.LightFactory: Access to the single instance of the factory.
instance() - Static method in class org.sat4j.minisat.SolverFactory: Access to the single instance of the factory.
InstanceReader - Class in org.sat4j.reader: An reader having the responsability to choose the right reader according to the input.
InstanceReader(ISolver) - Constructor for class org.sat4j.reader.InstanceReader
internalState() - Method in class org.sat4j.tools.AbstractClauseSelectorSolver: In the internal state, the solver will allow the selector variables to be satisfied.
IntQueue - Class in org.sat4j.minisat.core: Implementation of a queue.
IntQueue() - Constructor for class org.sat4j.minisat.core.IntQueue
IOptimizationProblem - Interface in org.sat4j.specs: Represents an optimization problem.
IOrder - Interface in org.sat4j.minisat.core: Interface for the variable ordering heuristics.
IPhaseSelectionStrategy - Interface in org.sat4j.minisat.core: The responsibility of that class is to choose the phase (positive or negative) of the variable that was selected by the IOrder.
IProblem - Interface in org.sat4j.specs: Access to the information related to a given problem instance.
isDBSimplificationAllowed() - Method in class org.sat4j.minisat.core.Solver
isDBSimplificationAllowed() - Method in interface org.sat4j.specs.ISolver: Indicate whether the solver is allowed to simplify the formula by propagating the truth value of top level satisfied variables.
isDBSimplificationAllowed() - Method in class org.sat4j.tools.AbstractOutputSolver
isDBSimplificationAllowed() - Method in class org.sat4j.tools.ManyCore
isDBSimplificationAllowed() - Method in class org.sat4j.tools.SolverDecorator
isDBSimplificationAllowed() - Method in class org.sat4j.tools.StatisticsSolver
isEmpty() - Method in class org.sat4j.core.ReadOnlyVec
isEmpty() - Method in class org.sat4j.core.ReadOnlyVecInt
isEmpty() - Method in class org.sat4j.core.Vec
isEmpty() - Method in class org.sat4j.core.VecInt
isEmpty() - Method in interface org.sat4j.specs.IVec: To know if a vector is empty
isEmpty() - Method in interface org.sat4j.specs.IVecInt: To know if a vector is empty
isFalsified(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
isFalsified(int) - Method in interface org.sat4j.minisat.core.ILits: Check if a literal is falsified.
isFull() - Method in class org.sat4j.minisat.core.CircularBuffer
isImplied(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
isImplied(int) - Method in interface org.sat4j.minisat.core.ILits
ISimplifier - Interface in org.sat4j.minisat.core: Strategy for simplifying the conflict clause derived by the solver.
isNeedToReduceDB() - Method in class org.sat4j.minisat.core.Solver
ISolver - Interface in org.sat4j.specs: This interface contains all services provided by a SAT solver.
ISolverService - Interface in org.sat4j.specs: The aim on that interface is to allow power users to communicate with the SAT solver using Dimacs format.
isOptimal() - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
isOptimal() - Method in class org.sat4j.opt.MinOneDecorator
isOptimal() - Method in interface org.sat4j.specs.IOptimizationProblem: Allows to check afterwards if the solution provided by the solver is optimal or not.
isOptimal() - Method in class org.sat4j.tools.LexicoDecorator
isOptimal() - Method in class org.sat4j.tools.OptToSatAdapter: Allow to easily check is the solution returned by isSatisfiable is optimal or not.
isSatisfiable() - Method in class org.sat4j.minisat.core.Solver
isSatisfiable(boolean) - Method in class org.sat4j.minisat.core.Solver
isSatisfiable(IVecInt) - Method in class org.sat4j.minisat.core.Solver
isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.minisat.core.Solver
isSatisfiable() - Method in interface org.sat4j.specs.IProblem: Check the satisfiability of the set of constraints contained inside the solver.
isSatisfiable(IVecInt, boolean) - Method in interface org.sat4j.specs.IProblem: Check the satisfiability of the set of constraints contained inside the solver.
isSatisfiable(boolean) - Method in interface org.sat4j.specs.IProblem: Check the satisfiability of the set of constraints contained inside the solver.
isSatisfiable(IVecInt) - Method in interface org.sat4j.specs.IProblem: Check the satisfiability of the set of constraints contained inside the solver.
isSatisfiable(boolean) - Method in class org.sat4j.tools.AbstractClauseSelectorSolver
isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.tools.AbstractClauseSelectorSolver
isSatisfiable() - Method in class org.sat4j.tools.AbstractClauseSelectorSolver
isSatisfiable(IVecInt) - Method in class org.sat4j.tools.AbstractClauseSelectorSolver
isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.tools.AbstractOutputSolver
isSatisfiable(boolean) - Method in class org.sat4j.tools.AbstractOutputSolver
isSatisfiable() - Method in class org.sat4j.tools.AbstractOutputSolver
isSatisfiable(IVecInt) - Method in class org.sat4j.tools.AbstractOutputSolver
isSatisfiable() - Method in class org.sat4j.tools.ManyCore
isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.tools.ManyCore
isSatisfiable(boolean) - Method in class org.sat4j.tools.ManyCore
isSatisfiable(IVecInt) - Method in class org.sat4j.tools.ManyCore
isSatisfiable() - Method in class org.sat4j.tools.ModelIterator
isSatisfiable(IVecInt) - Method in class org.sat4j.tools.ModelIterator
isSatisfiable() - Method in class org.sat4j.tools.ModelIteratorToSATAdapter
isSatisfiable(IVecInt) - Method in class org.sat4j.tools.ModelIteratorToSATAdapter
isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.tools.NegationDecorator
isSatisfiable() - Method in class org.sat4j.tools.OptToSatAdapter
isSatisfiable(boolean) - Method in class org.sat4j.tools.OptToSatAdapter
isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.tools.OptToSatAdapter
isSatisfiable(IVecInt) - Method in class org.sat4j.tools.OptToSatAdapter
isSatisfiable(boolean) - Method in class org.sat4j.tools.SolverDecorator
isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.tools.SolverDecorator
isSatisfiable() - Method in class org.sat4j.tools.SolverDecorator
isSatisfiable(IVecInt) - Method in class org.sat4j.tools.SolverDecorator
isSatisfiable() - Method in class org.sat4j.tools.StatisticsSolver
isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.tools.StatisticsSolver
isSatisfiable(boolean) - Method in class org.sat4j.tools.StatisticsSolver
isSatisfiable(IVecInt) - Method in class org.sat4j.tools.StatisticsSolver
isSatisfiable() - Method in class org.sat4j.tools.xplain.HighLevelXplain
isSatisfiable(boolean) - Method in class org.sat4j.tools.xplain.HighLevelXplain
isSatisfiable(IVecInt) - Method in class org.sat4j.tools.xplain.HighLevelXplain
isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.tools.xplain.HighLevelXplain
isSatisfiable() - Method in class org.sat4j.tools.xplain.Xplain
isSatisfiable(boolean) - Method in class org.sat4j.tools.xplain.Xplain
isSatisfiable(IVecInt) - Method in class org.sat4j.tools.xplain.Xplain
isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.tools.xplain.Xplain
isSatisfied(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
isSatisfied(int) - Method in interface org.sat4j.minisat.core.ILits: Check if a literal is satisfied.
isSkipDuplicatedEntries() - Method in class org.sat4j.tools.FullClauseSelectorSolver
isSolutionOptimal() - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
isSolutionOptimal - Variable in class org.sat4j.tools.LexicoDecorator
isSolverKeptHot() - Method in class org.sat4j.minisat.core.Solver
isSolverKeptHot() - Method in interface org.sat4j.specs.ISolver: Ask to the solver if it is in "hot" mode, meaning that the heuristics is not reset after call is isSatisfiable().
isSolverKeptHot() - Method in class org.sat4j.tools.AbstractOutputSolver
isSolverKeptHot() - Method in class org.sat4j.tools.ManyCore
isSolverKeptHot() - Method in class org.sat4j.tools.SolverDecorator
isSolverKeptHot() - Method in class org.sat4j.tools.StatisticsSolver
isSubsetOf(VecInt) - Method in class org.sat4j.core.VecInt: to detect that the vector is a subset of another one.
isUnassigned(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
isUnassigned(int) - Method in interface org.sat4j.minisat.core.ILits: Check if a literal is assigned a truth value.
isVerbose() - Method in class org.sat4j.minisat.core.Solver
isVerbose() - Method in class org.sat4j.reader.Reader
isVerbose() - Method in interface org.sat4j.specs.ISolver: To know if the solver is in verbose mode (output allowed) or not.
isVerbose() - Method in class org.sat4j.tools.AbstractOutputSolver
isVerbose() - Method in class org.sat4j.tools.ManyCore
isVerbose() - Method in class org.sat4j.tools.SolverDecorator
isVerbose() - Method in class org.sat4j.tools.StatisticsSolver
ite(int, int, int, int) - Method in class org.sat4j.tools.GateTranslator: translate y <=> if x1 then x2 else x3 into clauses.
iterator() - Method in class org.sat4j.core.ReadOnlyVec
iterator() - Method in class org.sat4j.core.ReadOnlyVecInt
iterator() - Method in class org.sat4j.core.Vec
iterator() - Method in class org.sat4j.core.VecInt
iterator() - Method in interface org.sat4j.specs.IVec
iterator() - Method in interface org.sat4j.specs.IVecInt
IteratorInt - Interface in org.sat4j.specs: Iterator interface to avoid boxing int into Integer.
IVec<T> - Interface in org.sat4j.specs: An abstraction on the type of vector used in the library.
IVecInt - Interface in org.sat4j.specs: An abstraction for the vector of int used on the library.
IVisualizationTool - Interface in org.sat4j.tools

J

JSONReader<S extends ISolver> - Class in org.sat4j.reader: Simple JSON reader for clauses and cardinality constraints.
JSONReader(S) - Constructor for class org.sat4j.reader.JSONReader

L

Ladder - Class in org.sat4j.tools.encoding: Ladder encoding for the "at most one" and "exactly one" cases.
Ladder() - Constructor for class org.sat4j.tools.encoding.Ladder
last() - Method in class org.sat4j.core.ReadOnlyVec
last() - Method in class org.sat4j.core.ReadOnlyVecInt
last() - Method in class org.sat4j.core.Vec: return the latest element on the stack.
last() - Method in class org.sat4j.core.VecInt
last() - Method in interface org.sat4j.specs.IVec: return the latest element on the stack.
last() - Method in interface org.sat4j.specs.IVecInt
LBDTracing - Class in org.sat4j.tools
LBDTracing(IVisualizationTool) - Constructor for class org.sat4j.tools.LBDTracing
Lbool - Class in org.sat4j.specs: That enumeration defines the possible truth value for a variable: satisfied, falsified or unknown/undefined.
learn(Constr) - Method in interface org.sat4j.minisat.core.Learner
learn(Constr) - Method in class org.sat4j.minisat.core.Solver
learn(IConstr) - Method in interface org.sat4j.specs.SearchListener: learning a new clause
learn(IConstr) - Method in class org.sat4j.tools.DotSearchTracing
learn(IConstr) - Method in class org.sat4j.tools.LearnedClausesSizeTracing
learn(IConstr) - Method in class org.sat4j.tools.MultiTracing
learn(IConstr) - Method in class org.sat4j.tools.RupSearchListener
learn(IConstr) - Method in class org.sat4j.tools.SearchListenerAdapter
learn(IConstr) - Method in class org.sat4j.tools.TextOutputTracing
learnConstraint(Constr) - Method in class org.sat4j.minisat.constraints.AbstractDataStructureFactory
learnConstraint(Constr) - Method in interface org.sat4j.minisat.core.DataStructureFactory
learnedbinaryclauses - Variable in class org.sat4j.minisat.core.SolverStats
learnedclauses - Variable in class org.sat4j.minisat.core.SolverStats
LearnedClauseSizeTracing - Class in org.sat4j.tools
LearnedClauseSizeTracing(IVisualizationTool) - Constructor for class org.sat4j.tools.LearnedClauseSizeTracing
LearnedClausesSizeTracing - Class in org.sat4j.tools
LearnedClausesSizeTracing(IVisualizationTool, IVisualizationTool, IVisualizationTool) - Constructor for class org.sat4j.tools.LearnedClausesSizeTracing
LearnedConstraintsDeletionStrategy - Interface in org.sat4j.minisat.core: Strategy for cleaning the database of learned clauses.
learnedConstraintsDeletionStrategy - Variable in class org.sat4j.minisat.core.Solver
LearnedConstraintsEvaluationType - Enum in org.sat4j.minisat.core: List the available strategies to evaluate learned clauses.
learnedliterals - Variable in class org.sat4j.minisat.core.SolverStats
learnedternaryclauses - Variable in class org.sat4j.minisat.core.SolverStats
LearnedTracing - Class in org.sat4j.tools
LearnedTracing(IVisualizationTool) - Constructor for class org.sat4j.tools.LearnedTracing
learner - Variable in class org.sat4j.minisat.constraints.AbstractDataStructureFactory
Learner - Interface in org.sat4j.minisat.core: Provide the learning service.
learningCondition(Constr) - Method in class org.sat4j.minisat.learning.ActiveLearning
learningCondition(Constr) - Method in class org.sat4j.minisat.learning.ClauseOnlyLearning
learningCondition(Constr) - Method in class org.sat4j.minisat.learning.FixedLengthLearning
learningCondition(Constr) - Method in class org.sat4j.minisat.learning.LimitedLearning
learningCondition(Constr) - Method in class org.sat4j.minisat.learning.PercentLengthLearning
LearningStrategy<D extends DataStructureFactory> - Interface in org.sat4j.minisat.core: Implementation of the strategy design pattern for allowing various learning schemes.
learns(Constr) - Method in interface org.sat4j.minisat.core.LearningStrategy
learns(Constr) - Method in class org.sat4j.minisat.learning.LimitedLearning
learns(Constr) - Method in class org.sat4j.minisat.learning.MiniSATLearning
learns(Constr) - Method in class org.sat4j.minisat.learning.NoLearningButHeuristics
learns(Constr) - Method in class org.sat4j.minisat.learning.NoLearningNoHeuristics
learnt() - Method in class org.sat4j.core.ConstrGroup
learnt() - Method in class org.sat4j.minisat.constraints.card.AtLeast
learnt() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard: D?
learnt() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard: Returns wether the constraint is learnt or not.
learnt() - Method in class org.sat4j.minisat.constraints.cnf.LearntBinaryClause
learnt() - Method in class org.sat4j.minisat.constraints.cnf.LearntHTClause
learnt() - Method in class org.sat4j.minisat.constraints.cnf.LearntWLClause
learnt() - Method in class org.sat4j.minisat.constraints.cnf.OriginalBinaryClause
learnt() - Method in class org.sat4j.minisat.constraints.cnf.OriginalHTClause
learnt() - Method in class org.sat4j.minisat.constraints.cnf.OriginalWLClause
learnt() - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
learnt() - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
learnt() - Method in interface org.sat4j.specs.IConstr
LearntBinaryClause - Class in org.sat4j.minisat.constraints.cnf
LearntBinaryClause(IVecInt, ILits) - Constructor for class org.sat4j.minisat.constraints.cnf.LearntBinaryClause
LearntHTClause - Class in org.sat4j.minisat.constraints.cnf
LearntHTClause(IVecInt, ILits) - Constructor for class org.sat4j.minisat.constraints.cnf.LearntHTClause
learnts - Variable in class org.sat4j.minisat.core.Solver: Set of learned constraints.
LearntWLClause - Class in org.sat4j.minisat.constraints.cnf
LearntWLClause(IVecInt, ILits) - Constructor for class org.sat4j.minisat.constraints.cnf.LearntWLClause
learnUnit(int) - Method in interface org.sat4j.specs.SearchListener: learn a new unit clause (a literal)
learnUnit(int) - Method in class org.sat4j.tools.ManyCore
learnUnit(int) - Method in class org.sat4j.tools.MultiTracing
learnUnit(int) - Method in class org.sat4j.tools.RupSearchListener
learnUnit(int) - Method in class org.sat4j.tools.SearchListenerAdapter
learnUnit(int) - Method in class org.sat4j.tools.TextOutputTracing
LecteurDimacs - Class in org.sat4j.reader: Dimacs Reader written by Frederic Laihem.
LecteurDimacs(ISolver) - Constructor for class org.sat4j.reader.LecteurDimacs
LexicoDecorator<T extends ISolver> - Class in org.sat4j.tools
LexicoDecorator(T) - Constructor for class org.sat4j.tools.LexicoDecorator
LightFactory - Class in org.sat4j: That class is the entry point to the default, best performing configuration of SAT4J.
LightFactory() - Constructor for class org.sat4j.LightFactory
lightSolver() - Method in class org.sat4j.core.ASolverFactory: To obtain a solver that is suitable for solving many small instances of SAT problems.
lightSolver() - Method in class org.sat4j.LightFactory
lightSolver() - Method in class org.sat4j.minisat.SolverFactory
LimitedLearning<D extends DataStructureFactory> - Class in org.sat4j.minisat.learning: Learn only clauses which size is smaller than a percentage of the number of variables.
LimitedLearning() - Constructor for class org.sat4j.minisat.learning.LimitedLearning
linearisation(ILits, IVecInt) - Static method in class org.sat4j.minisat.constraints.card.MinWatchCard: Simplifies the constraint w.r.t. the assignments of the literals
literal - Variable in class org.sat4j.minisat.constraints.cnf.UnitClause
literals - Variable in class org.sat4j.minisat.constraints.cnf.UnitClauses
literals - Variable in class org.sat4j.reader.DimacsReader
LiteralsUtils - Class in org.sat4j.core: Utility methods to avoid using bit manipulation inside code.
lits - Variable in class org.sat4j.minisat.constraints.AbstractDataStructureFactory
lits - Variable in class org.sat4j.minisat.constraints.card.AtLeast: constraint literals
Lits - Class in org.sat4j.minisat.constraints.cnf
Lits() - Constructor for class org.sat4j.minisat.constraints.cnf.Lits
lits - Variable in class org.sat4j.minisat.constraints.cnf.WLClause
lits - Variable in class org.sat4j.minisat.learning.LimitedLearning
lits - Variable in class org.sat4j.minisat.orders.VarOrderHeap
locked() - Method in class org.sat4j.minisat.constraints.card.AtLeast
locked() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard: La contrainte est la cause d'une propagation unitaire
locked() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard: Returns if the constraint is the reason for a unit propagation.
locked() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
locked() - Method in class org.sat4j.minisat.constraints.cnf.HTClause
locked() - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
locked() - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
locked() - Method in class org.sat4j.minisat.constraints.cnf.WLClause
locked() - Method in interface org.sat4j.minisat.core.Constr: Indicate wether a constraint is responsible from an assignment.
log(String) - Method in class org.sat4j.AbstractLauncher: Display messages as comments on STDOUT
log(String) - Method in interface org.sat4j.specs.ILogAble
lowerBound() - Method in class org.sat4j.tools.SolutionCounter: Get the number of solutions found before the timeout occurs.
luby() - Method in class org.sat4j.minisat.restarts.LubyRestarts: returns the current value of the luby sequence.
LubyRestarts - Class in org.sat4j.minisat.restarts: Luby series
LubyRestarts() - Constructor for class org.sat4j.minisat.restarts.LubyRestarts
LubyRestarts(int) - Constructor for class org.sat4j.minisat.restarts.LubyRestarts

M

main(String[]) - Static method in class org.sat4j.BasicLauncher: Lance le prouveur sur un fichier Dimacs.
main(String[]) - Static method in class org.sat4j.LightFactory
main(String[]) - Static method in class org.sat4j.MoreThanSAT
main(String[]) - Static method in class org.sat4j.MUSLauncher
manageUnsatCase() - Method in class org.sat4j.tools.LexicoDecorator
ManyCore<S extends ISolver> - Class in org.sat4j.tools: A class allowing to run several solvers in parallel.
ManyCore(ASolverFactory<S>, String...) - Constructor for class org.sat4j.tools.ManyCore
ManyCore(String[], S...) - Constructor for class org.sat4j.tools.ManyCore: Create a parallel solver from a list of solvers and a list of names.
ManyCore(S...) - Constructor for class org.sat4j.tools.ManyCore
MaxSatDecorator - Class in org.sat4j.opt: Computes a solution that satisfies the maximum of clauses.
MaxSatDecorator(ISolver) - Constructor for class org.sat4j.opt.MaxSatDecorator
MaxSatDecorator(ISolver, boolean) - Constructor for class org.sat4j.opt.MaxSatDecorator
maxUnsatisfied - Variable in class org.sat4j.minisat.constraints.card.AtLeast: number of allowed falsified literal
MaxWatchCard - Class in org.sat4j.minisat.constraints.card
MaxWatchCard(ILits, IVecInt, boolean, int) - Constructor for class org.sat4j.minisat.constraints.card.MaxWatchCard: Constructeur de base cr?
maxWatchCardNew(UnitPropagationListener, ILits, IVecInt, boolean, int) - Static method in class org.sat4j.minisat.constraints.card.MaxWatchCard: Permet la cr?
memory_based - Variable in class org.sat4j.minisat.core.Solver
Messages - Class in org.sat4j: That class is intented to manage internationalisation within the application.
middleLits - Variable in class org.sat4j.minisat.constraints.cnf.HTClause
Minimal4CardinalityModel - Class in org.sat4j.tools: Computes models with a minimal number (with respect to cardinality) of negative literals.
Minimal4CardinalityModel(ISolver) - Constructor for class org.sat4j.tools.Minimal4CardinalityModel
Minimal4CardinalityModel(ISolver, IVecInt, SolutionFoundListener) - Constructor for class org.sat4j.tools.Minimal4CardinalityModel
Minimal4CardinalityModel(ISolver, IVecInt) - Constructor for class org.sat4j.tools.Minimal4CardinalityModel
Minimal4CardinalityModel(ISolver, SolutionFoundListener) - Constructor for class org.sat4j.tools.Minimal4CardinalityModel
Minimal4InclusionModel - Class in org.sat4j.tools: Computes models with a minimal subset (with respect to set inclusion) of negative literals.
Minimal4InclusionModel(ISolver, IVecInt, SolutionFoundListener) - Constructor for class org.sat4j.tools.Minimal4InclusionModel
Minimal4InclusionModel(ISolver, IVecInt) - Constructor for class org.sat4j.tools.Minimal4InclusionModel
Minimal4InclusionModel(ISolver) - Constructor for class org.sat4j.tools.Minimal4InclusionModel
minimalExplanation() - Method in interface org.sat4j.tools.xplain.Explainer
minimalExplanation() - Method in class org.sat4j.tools.xplain.HighLevelXplain
minimalExplanation() - Method in class org.sat4j.tools.xplain.Xplain: Provide an explanation of the inconsistency in terms of a subset minimal set of constraints, each constraint being referred to as its index (order) in the solver: first constraint is numbered 1, the second 2, etc.
MinimizationStrategy - Interface in org.sat4j.tools.xplain: Minimization technique used to reduce an unsatisfiable set of constraints into a minimally unsatisfiable subformula (MUS).
MiniSATLearning<D extends DataStructureFactory> - Class in org.sat4j.minisat.learning: MiniSAT learning scheme.
MiniSATLearning() - Constructor for class org.sat4j.minisat.learning.MiniSATLearning
MiniSATRestarts - Class in org.sat4j.minisat.restarts: Minisat original restart strategy.
MiniSATRestarts() - Constructor for class org.sat4j.minisat.restarts.MiniSATRestarts
MinOneDecorator - Class in org.sat4j.opt: Computes a solution with the smallest number of satisfied literals.
MinOneDecorator(ISolver) - Constructor for class org.sat4j.opt.MinOneDecorator
MinWatchCard - Class in org.sat4j.minisat.constraints.card
MinWatchCard(ILits, IVecInt, boolean, int) - Constructor for class org.sat4j.minisat.constraints.card.MinWatchCard: Constructs and normalizes a cardinality constraint. used by minWatchCardNew in the non-normalized case.
MinWatchCard(ILits, IVecInt, int) - Constructor for class org.sat4j.minisat.constraints.card.MinWatchCard: Constructs and normalizes a cardinality constraint. used by MinWatchCardPB.normalizedMinWatchCardNew() in the normalized case.
minWatchCardNew(UnitPropagationListener, ILits, IVecInt, boolean, int) - Static method in class org.sat4j.minisat.constraints.card.MinWatchCard: Constructs a cardinality constraint with a minimal set of watched literals Permet la cr?
MixedDataStructureDanielHT - Class in org.sat4j.minisat.constraints: Uses specific data structure for cardinality constraints.
MixedDataStructureDanielHT() - Constructor for class org.sat4j.minisat.constraints.MixedDataStructureDanielHT
MixedDataStructureDanielWL - Class in org.sat4j.minisat.constraints
MixedDataStructureDanielWL() - Constructor for class org.sat4j.minisat.constraints.MixedDataStructureDanielWL
MixedDataStructureSingleWL - Class in org.sat4j.minisat.constraints
MixedDataStructureSingleWL() - Constructor for class org.sat4j.minisat.constraints.MixedDataStructureSingleWL
model() - Method in class org.sat4j.minisat.core.Solver: Si un mod?
model(int) - Method in class org.sat4j.minisat.core.Solver
model() - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
model(int) - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
model() - Method in class org.sat4j.opt.MinOneDecorator
model() - Method in interface org.sat4j.specs.IProblem: Provide a model (if any) for a satisfiable formula.
model(int) - Method in interface org.sat4j.specs.RandomAccessModel: Provide the truth value of a specific variable in the model.
model() - Method in class org.sat4j.tools.AbstractOutputSolver
model(int) - Method in class org.sat4j.tools.AbstractOutputSolver
model() - Method in class org.sat4j.tools.FullClauseSelectorSolver
model() - Method in class org.sat4j.tools.GroupClauseSelectorSolver
model() - Method in class org.sat4j.tools.LexicoDecorator
model(int) - Method in class org.sat4j.tools.LexicoDecorator
model() - Method in class org.sat4j.tools.ManyCore
model(int) - Method in class org.sat4j.tools.ManyCore
model() - Method in class org.sat4j.tools.Minimal4CardinalityModel
model() - Method in class org.sat4j.tools.Minimal4InclusionModel
model() - Method in class org.sat4j.tools.ModelIterator
model() - Method in class org.sat4j.tools.ModelIteratorToSATAdapter
model() - Method in class org.sat4j.tools.OptToSatAdapter
model(int) - Method in class org.sat4j.tools.OptToSatAdapter
model(int) - Method in class org.sat4j.tools.SolverDecorator
model() - Method in class org.sat4j.tools.SolverDecorator
model() - Method in class org.sat4j.tools.StatisticsSolver
model(int) - Method in class org.sat4j.tools.StatisticsSolver
ModelIterator - Class in org.sat4j.tools: That class allows to iterate through all the models (implicants) of a formula.
ModelIterator(ISolver) - Constructor for class org.sat4j.tools.ModelIterator: Create an iterator over the solutions available in solver.
ModelIterator(ISolver, long) - Constructor for class org.sat4j.tools.ModelIterator: Create an iterator over a limited number of solutions available in solver.
ModelIteratorToSATAdapter - Class in org.sat4j.tools: This class allow to use the ModelIterator class as a solver.
ModelIteratorToSATAdapter(ISolver, SolutionFoundListener) - Constructor for class org.sat4j.tools.ModelIteratorToSATAdapter
ModelIteratorToSATAdapter(ISolver, long, SolutionFoundListener) - Constructor for class org.sat4j.tools.ModelIteratorToSATAdapter
modelListener - Variable in class org.sat4j.tools.AbstractMinimalModel
modelWithInternalVariables() - Method in class org.sat4j.minisat.core.Solver
modelWithInternalVariables() - Method in class org.sat4j.opt.MinOneDecorator
modelWithInternalVariables() - Method in interface org.sat4j.specs.ISolver: That method is designed to be used to retrieve the real model of the current set of constraints, i.e. to provide the truth value of boolean variables used internally in the solver (for encoding purposes for instance).
modelWithInternalVariables() - Method in class org.sat4j.tools.DimacsOutputSolver
modelWithInternalVariables() - Method in class org.sat4j.tools.DimacsStringSolver
modelWithInternalVariables() - Method in class org.sat4j.tools.LexicoDecorator
modelWithInternalVariables() - Method in class org.sat4j.tools.ManyCore
modelWithInternalVariables() - Method in class org.sat4j.tools.Minimal4CardinalityModel
modelWithInternalVariables() - Method in class org.sat4j.tools.Minimal4InclusionModel
modelWithInternalVariables() - Method in class org.sat4j.tools.OptToSatAdapter
modelWithInternalVariables() - Method in class org.sat4j.tools.SolverDecorator
modelWithInternalVariables() - Method in class org.sat4j.tools.StatisticsSolver
MoreThanSAT - Class in org.sat4j: This is an example of use of the SAT4J library for computing the backbone of a CNF or to compute the number of solutions of a CNF.
moveTo(IVec<T>) - Method in class org.sat4j.core.ReadOnlyVec
moveTo(int, int) - Method in class org.sat4j.core.ReadOnlyVec
moveTo(IVecInt) - Method in class org.sat4j.core.ReadOnlyVecInt
moveTo(int[]) - Method in class org.sat4j.core.ReadOnlyVecInt
moveTo(int, int) - Method in class org.sat4j.core.ReadOnlyVecInt
moveTo(int, int[]) - Method in class org.sat4j.core.ReadOnlyVecInt
moveTo(IVec<T>) - Method in class org.sat4j.core.Vec
moveTo(int, int) - Method in class org.sat4j.core.Vec
moveTo(IVecInt) - Method in class org.sat4j.core.VecInt
moveTo(int, int) - Method in class org.sat4j.core.VecInt
moveTo(int[]) - Method in class org.sat4j.core.VecInt
moveTo(int, int[]) - Method in class org.sat4j.core.VecInt
moveTo(IVec<T>) - Method in interface org.sat4j.specs.IVec: Move the content of the vector into dest.
moveTo(int, int) - Method in interface org.sat4j.specs.IVec: Move elements inside the vector.
moveTo(IVecInt) - Method in interface org.sat4j.specs.IVecInt
moveTo(int, int[]) - Method in interface org.sat4j.specs.IVecInt
moveTo(int[]) - Method in interface org.sat4j.specs.IVecInt
moveTo(int, int) - Method in interface org.sat4j.specs.IVecInt: Move elements inside the vector.
moveTo2(IVecInt) - Method in class org.sat4j.core.ReadOnlyVecInt
moveTo2(IVecInt) - Method in class org.sat4j.core.VecInt
moveTo2(IVecInt) - Method in interface org.sat4j.specs.IVecInt
MultiTracing<T extends ISolverService> - Class in org.sat4j.tools: Allow to feed the solver with several SearchListener.
MultiTracing(SearchListener<T>...) - Constructor for class org.sat4j.tools.MultiTracing
MultiTracing(List<SearchListener<T>>) - Constructor for class org.sat4j.tools.MultiTracing
MUSLauncher - Class in org.sat4j
MUSLauncher() - Constructor for class org.sat4j.MUSLauncher

N

NAND - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader
nAssigns() - Method in class org.sat4j.minisat.core.Solver
nbclauses - Variable in class org.sat4j.tools.AbstractOutputSolver
nbvars - Variable in class org.sat4j.tools.AbstractOutputSolver
nConstraints() - Method in class org.sat4j.minisat.core.Solver
nConstraints() - Method in interface org.sat4j.specs.IProblem: To know the number of constraints currently available in the solver.
nConstraints() - Method in class org.sat4j.tools.AbstractOutputSolver
nConstraints() - Method in class org.sat4j.tools.DimacsOutputSolver
nConstraints() - Method in class org.sat4j.tools.DimacsStringSolver
nConstraints() - Method in class org.sat4j.tools.ManyCore
nConstraints() - Method in class org.sat4j.tools.SolverDecorator
nConstraints() - Method in class org.sat4j.tools.StatisticsSolver
neg(int) - Static method in class org.sat4j.core.LiteralsUtils: Returns the opposite literal.
NegationDecorator<T extends ISolver> - Class in org.sat4j.tools: Negates the formula inside a solver.
NegationDecorator(T) - Constructor for class org.sat4j.tools.NegationDecorator
negativeLiterals(ISolver) - Static method in class org.sat4j.tools.AbstractMinimalModel
NegativeLiteralSelectionStrategy - Class in org.sat4j.minisat.orders
NegativeLiteralSelectionStrategy() - Constructor for class org.sat4j.minisat.orders.NegativeLiteralSelectionStrategy
negLit(int) - Static method in class org.sat4j.core.LiteralsUtils: Returns the negative literal associated with a variable.
newBackjumping() - Static method in class org.sat4j.minisat.SolverFactory
newBest17() - Static method in class org.sat4j.minisat.SolverFactory
newBestHT() - Static method in class org.sat4j.minisat.SolverFactory
newBestWL() - Static method in class org.sat4j.minisat.SolverFactory
newConflict() - Method in interface org.sat4j.minisat.core.ConflictTimer
newConflict() - Method in class org.sat4j.minisat.core.ConflictTimerAdapter
newConflict() - Method in class org.sat4j.minisat.core.ConflictTimerContainer
newConflict() - Method in class org.sat4j.minisat.restarts.ArminRestarts
newConflict() - Method in class org.sat4j.minisat.restarts.FixedPeriodRestarts
newConflict() - Method in class org.sat4j.minisat.restarts.Glucose21Restarts
newConflict() - Method in class org.sat4j.minisat.restarts.LubyRestarts
newConflict() - Method in class org.sat4j.minisat.restarts.MiniSATRestarts
newConflict() - Method in class org.sat4j.minisat.restarts.NoRestarts
newDefault() - Static method in class org.sat4j.minisat.SolverFactory: Default solver of the SolverFactory.
newDefaultAutoErasePhaseSaving() - Static method in class org.sat4j.minisat.SolverFactory
newDefaultMS21PhaseSaving() - Static method in class org.sat4j.minisat.SolverFactory
newDimacsOutput() - Static method in class org.sat4j.minisat.SolverFactory
newGlucose() - Static method in class org.sat4j.minisat.SolverFactory
newGlucose21() - Static method in class org.sat4j.minisat.SolverFactory
newGreedySolver() - Static method in class org.sat4j.minisat.SolverFactory
newLearnedClause(Constr, int) - Method in interface org.sat4j.minisat.core.RestartStrategy: Callback method called when a new clause is learned by the solver, after conflict analysis.
newLearnedClause(Constr, int) - Method in class org.sat4j.minisat.restarts.ArminRestarts
newLearnedClause(Constr, int) - Method in class org.sat4j.minisat.restarts.FixedPeriodRestarts
newLearnedClause(Constr, int) - Method in class org.sat4j.minisat.restarts.Glucose21Restarts
newLearnedClause(Constr, int) - Method in class org.sat4j.minisat.restarts.LubyRestarts
newLearnedClause(Constr, int) - Method in class org.sat4j.minisat.restarts.MiniSATRestarts
newLearnedClause(Constr, int) - Method in class org.sat4j.minisat.restarts.NoRestarts
newLight() - Static method in class org.sat4j.minisat.SolverFactory: Small footprint SAT solver.
newMiniLearning(DataStructureFactory, IOrder) - Static method in class org.sat4j.minisat.SolverFactory
newMiniLearningHeap() - Static method in class org.sat4j.minisat.SolverFactory
newMiniLearningHeap(DataStructureFactory) - Static method in class org.sat4j.minisat.SolverFactory
newMiniLearningHeapExpSimp() - Static method in class org.sat4j.minisat.SolverFactory
newMiniLearningHeapEZSimp() - Static method in class org.sat4j.minisat.SolverFactory
newMiniLearningHeapEZSimpLongRestarts() - Static method in class org.sat4j.minisat.SolverFactory
newMiniLearningHeapEZSimpNoRestarts() - Static method in class org.sat4j.minisat.SolverFactory
newMiniLearningHeapRsatExpSimp() - Static method in class org.sat4j.minisat.SolverFactory
newMiniLearningHeapRsatExpSimpBiere() - Static method in class org.sat4j.minisat.SolverFactory
newMiniLearningHeapRsatExpSimpLuby() - Static method in class org.sat4j.minisat.SolverFactory
newMiniSATHeap() - Static method in class org.sat4j.minisat.SolverFactory
newMiniSATHeap(DataStructureFactory) - Static method in class org.sat4j.minisat.SolverFactory
newMiniSATHeapExpSimp() - Static method in class org.sat4j.minisat.SolverFactory
newMiniSATHeapEZSimp() - Static method in class org.sat4j.minisat.SolverFactory
newMinOneSolver() - Static method in class org.sat4j.minisat.SolverFactory
newParallel() - Static method in class org.sat4j.minisat.SolverFactory
newSAT() - Static method in class org.sat4j.minisat.SolverFactory: That solver is expected to perform better on satisfiable benchmarks.
newSATUNSAT() - Static method in class org.sat4j.minisat.SolverFactory: Two solvers are running in //: one for solving SAT instances, the other one for solving unsat instances.
newStatistics() - Static method in class org.sat4j.minisat.SolverFactory
newUNSAT() - Static method in class org.sat4j.minisat.SolverFactory: That solver is expected to perform better on unsatisfiable benchmarks.
newVar() - Method in class org.sat4j.minisat.core.Solver: Deprecated.
newVar(int) - Method in class org.sat4j.minisat.core.Solver
newVar(int) - Method in interface org.sat4j.specs.IProblem: Declare howmany variables in the problem (and thus in the vocabulary), that will be represented using the Dimacs format by integers ranging from 1 to howmany.
newVar() - Method in interface org.sat4j.specs.ISolver: Deprecated.
newVar(int) - Method in class org.sat4j.tools.AbstractOutputSolver
newVar() - Method in class org.sat4j.tools.DimacsOutputSolver
newVar(int) - Method in class org.sat4j.tools.DimacsOutputSolver
newVar() - Method in class org.sat4j.tools.DimacsStringSolver
newVar(int) - Method in class org.sat4j.tools.DimacsStringSolver
newVar() - Method in class org.sat4j.tools.ManyCore
newVar(int) - Method in class org.sat4j.tools.ManyCore
newVar() - Method in class org.sat4j.tools.SolverDecorator: Deprecated.
newVar(int) - Method in class org.sat4j.tools.SolverDecorator
newVar(int) - Method in class org.sat4j.tools.StatisticsSolver
newVar() - Method in class org.sat4j.tools.StatisticsSolver: Deprecated.
next() - Method in class org.sat4j.reader.EfficientScanner
next() - Method in interface org.sat4j.specs.IteratorInt
nextBigInteger() - Method in class org.sat4j.reader.EfficientScanner
nextFreeVarId(boolean) - Method in class org.sat4j.minisat.constraints.cnf.Lits
nextFreeVarId(boolean) - Method in interface org.sat4j.minisat.core.ILits: Ask the solver for a free variable identifier, in Dimacs format (i.e. a positive number).
nextFreeVarId(boolean) - Method in class org.sat4j.minisat.core.Solver
nextFreeVarId(boolean) - Method in interface org.sat4j.specs.ISolver: Ask the solver for a free variable identifier, in Dimacs format (i.e. a positive number).
nextFreeVarId(boolean) - Method in class org.sat4j.tools.DimacsOutputSolver
nextFreeVarId(boolean) - Method in class org.sat4j.tools.DimacsStringSolver
nextFreeVarId(boolean) - Method in class org.sat4j.tools.ManyCore
nextFreeVarId(boolean) - Method in class org.sat4j.tools.SolverDecorator
nextFreeVarId(boolean) - Method in class org.sat4j.tools.StatisticsSolver
nextInt() - Method in class org.sat4j.reader.EfficientScanner: To get the next available integer.
nextLine() - Method in class org.sat4j.reader.EfficientScanner
nextLuby() - Method in class org.sat4j.minisat.restarts.LubyRestarts: Computes and return the next value of the luby sequence.
nextRestartNumberOfConflict() - Method in interface org.sat4j.minisat.core.RestartStrategy: Deprecated.
nextRestartNumberOfConflict() - Method in class org.sat4j.minisat.restarts.ArminRestarts
nextRestartNumberOfConflict() - Method in class org.sat4j.minisat.restarts.FixedPeriodRestarts: Deprecated.
nextRestartNumberOfConflict() - Method in class org.sat4j.minisat.restarts.Glucose21Restarts
nextRestartNumberOfConflict() - Method in class org.sat4j.minisat.restarts.LubyRestarts
nextRestartNumberOfConflict() - Method in class org.sat4j.minisat.restarts.MiniSATRestarts
nextRestartNumberOfConflict() - Method in class org.sat4j.minisat.restarts.NoRestarts
niceParameters(UnitPropagationListener, ILits, IVecInt, int) - Static method in class org.sat4j.minisat.constraints.card.AtLeast
NO_SIMPLIFICATION - Static variable in class org.sat4j.minisat.core.Solver
NoLearningButHeuristics<D extends DataStructureFactory> - Class in org.sat4j.minisat.learning: Allows MiniSAT to do backjumping without learning.
NoLearningButHeuristics() - Constructor for class org.sat4j.minisat.learning.NoLearningButHeuristics
NoLearningNoHeuristics<D extends DataStructureFactory> - Class in org.sat4j.minisat.learning: Allows MiniSAT to do backjumping without learning.
NoLearningNoHeuristics() - Constructor for class org.sat4j.minisat.learning.NoLearningNoHeuristics
nonOptimalMeansSatisfiable() - Method in class org.sat4j.opt.MaxSatDecorator
nonOptimalMeansSatisfiable() - Method in class org.sat4j.opt.MinOneDecorator
nonOptimalMeansSatisfiable() - Method in interface org.sat4j.specs.IOptimizationProblem: A suboptimal solution has different meaning depending of the optimization problem considered.
nonOptimalMeansSatisfiable() - Method in class org.sat4j.tools.LexicoDecorator
NOR - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader
NoRestarts - Class in org.sat4j.minisat.restarts: Disable restarts in the solver.
NoRestarts() - Constructor for class org.sat4j.minisat.restarts.NoRestarts
normalize() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard: On normalise la contrainte au sens de Barth
normalize() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard: normalize the constraint (cf.
not(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
not() - Method in class org.sat4j.specs.Lbool: boolean negation.
NOT - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader
not(int, int) - Method in class org.sat4j.tools.GateTranslator: Translate y <=> not x into clauses.
NOTGOOD - Static variable in interface org.sat4j.tools.IVisualizationTool
numberOfCriteria() - Method in class org.sat4j.tools.LexicoDecorator
numberOfInterestingVariables() - Method in class org.sat4j.minisat.orders.VarOrderHeap
numberOfModelsFoundSoFar() - Method in class org.sat4j.tools.ModelIterator: To know the number of models already found.
numberOfSolvers - Variable in class org.sat4j.tools.ManyCore
nVars() - Method in class org.sat4j.minisat.constraints.cnf.Lits
nVars() - Method in interface org.sat4j.minisat.core.ILits: to obtain the max id of the variable
nVars() - Method in class org.sat4j.minisat.core.Solver
nVars() - Method in interface org.sat4j.specs.IProblem: To know the number of variables used in the solver as declared by newVar() In case the method newVar() has not been used, the method returns the number of variables used in the solver.
nVars() - Method in interface org.sat4j.specs.ISolverService: Read-Only access to the number of variables declared in the solver.
nVars() - Method in class org.sat4j.tools.AbstractOutputSolver
nVars() - Method in class org.sat4j.tools.DimacsOutputSolver
nVars() - Method in class org.sat4j.tools.DimacsStringSolver
nVars() - Method in class org.sat4j.tools.ManyCore
nVars() - Method in class org.sat4j.tools.SolverDecorator
nVars() - Method in class org.sat4j.tools.StatisticsSolver

O

onBackjumpToRootLevel() - Method in interface org.sat4j.minisat.core.RestartStrategy: Called when the solver backjumps to the root level.
onBackjumpToRootLevel() - Method in class org.sat4j.minisat.restarts.ArminRestarts
onBackjumpToRootLevel() - Method in class org.sat4j.minisat.restarts.FixedPeriodRestarts
onBackjumpToRootLevel() - Method in class org.sat4j.minisat.restarts.Glucose21Restarts
onBackjumpToRootLevel() - Method in class org.sat4j.minisat.restarts.LubyRestarts
onBackjumpToRootLevel() - Method in class org.sat4j.minisat.restarts.MiniSATRestarts
onBackjumpToRootLevel() - Method in class org.sat4j.minisat.restarts.NoRestarts
onClauseLearning(Constr) - Method in interface org.sat4j.minisat.core.LearnedConstraintsDeletionStrategy: Hook method called when a new clause has just been derived during conflict analysis.
onConflictAnalysis(Constr) - Method in interface org.sat4j.minisat.core.LearnedConstraintsDeletionStrategy: Hook method called on constraints participating to the conflict analysis.
onFinishWithAnswer(boolean, boolean, int) - Method in class org.sat4j.tools.ManyCore
onFinishWithAnswer(boolean, boolean, int) - Method in interface org.sat4j.tools.OutcomeListener
onPropagation(Constr) - Method in interface org.sat4j.minisat.core.LearnedConstraintsDeletionStrategy: Hook method called when a unit clause is propagated thanks to from.
onRestart() - Method in interface org.sat4j.minisat.core.RestartStrategy: Hook method called when a restart occurs (once the solver has backtracked to top decision level).
onRestart() - Method in class org.sat4j.minisat.restarts.ArminRestarts
onRestart() - Method in class org.sat4j.minisat.restarts.FixedPeriodRestarts
onRestart() - Method in class org.sat4j.minisat.restarts.Glucose21Restarts
onRestart() - Method in class org.sat4j.minisat.restarts.LubyRestarts
onRestart() - Method in class org.sat4j.minisat.restarts.MiniSATRestarts
onRestart() - Method in class org.sat4j.minisat.restarts.NoRestarts
onSolutionFound(int[]) - Method in class org.sat4j.tools.CheckMUSSolutionListener
onSolutionFound(IVecInt) - Method in class org.sat4j.tools.CheckMUSSolutionListener
onSolutionFound(int[]) - Method in interface org.sat4j.tools.SolutionFoundListener: Callback method called when a new solution is found.
onSolutionFound(IVecInt) - Method in interface org.sat4j.tools.SolutionFoundListener: Callback method called when a new solution is found.
onUnsatTermination() - Method in class org.sat4j.tools.CheckMUSSolutionListener
onUnsatTermination() - Method in interface org.sat4j.tools.SolutionFoundListener: Callback method called when the search is finished (either unsat problem or no more solutions found)
optimisationFunction(IVecInt, IVec<BigInteger>, IVecInt) - Method in class org.sat4j.tools.GateTranslator: Translate an optimization function into constraints and provides the binary literals in results.
OPTIMIZATION - Static variable in interface org.sat4j.ILauncherMode: The launcher is in optimization mode: the answer is either SAT, UPPER_BOUND, OPTIMUM_FOUND, UNSAT or UNKNOWN.
OPTIMUM_FOUND - Static variable in class org.sat4j.ExitCode
OptToSatAdapter - Class in org.sat4j.tools
OptToSatAdapter(IOptimizationProblem) - Constructor for class org.sat4j.tools.OptToSatAdapter
OptToSatAdapter(IOptimizationProblem, SolutionFoundListener) - Constructor for class org.sat4j.tools.OptToSatAdapter
OR - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader
or(int, IVecInt) - Method in class org.sat4j.tools.GateTranslator: translate y <=> x1 \/ x2 \/ ... \/ xn into clauses.
org.sat4j - package org.sat4j: Contains a command line launcher for the SAT solvers.
org.sat4j.core - package org.sat4j.core: Implementation of the data structures available in org.sat4j.specs.
org.sat4j.minisat - package org.sat4j.minisat: Implementation of the MiniSAT specification in Java.
org.sat4j.minisat.constraints - package org.sat4j.minisat.constraints: Implementations of various constraints for MiniSAT.
org.sat4j.minisat.constraints.card - package org.sat4j.minisat.constraints.card: Implementations of cardinality constraints.
org.sat4j.minisat.constraints.cnf - package org.sat4j.minisat.constraints.cnf: Implementations of clausal constraints.
org.sat4j.minisat.core - package org.sat4j.minisat.core: Implementation of the MiniSAT solver skeleton.
org.sat4j.minisat.learning - package org.sat4j.minisat.learning: Various learning strategies.
org.sat4j.minisat.orders - package org.sat4j.minisat.orders: Various heuristics to select the next variable to branch on.
org.sat4j.minisat.restarts - package org.sat4j.minisat.restarts: Various restart strategies.
org.sat4j.opt - package org.sat4j.opt: Built-in optimization framework.
org.sat4j.reader - package org.sat4j.reader: Some utility classes to read problems from plain text files.
org.sat4j.specs - package org.sat4j.specs: Those classes are intended for users dealing with SAT solvers as black boxes.
org.sat4j.tools - package org.sat4j.tools: Tools to be used on top of an ISolver.
org.sat4j.tools.encoding - package org.sat4j.tools.encoding: Implementation of different encodings.
org.sat4j.tools.xplain - package org.sat4j.tools.xplain: Implementation of an explanation engine in case of unsatisfiability.
OriginalBinaryClause - Class in org.sat4j.minisat.constraints.cnf
OriginalBinaryClause(IVecInt, ILits) - Constructor for class org.sat4j.minisat.constraints.cnf.OriginalBinaryClause
OriginalHTClause - Class in org.sat4j.minisat.constraints.cnf
OriginalHTClause(IVecInt, ILits) - Constructor for class org.sat4j.minisat.constraints.cnf.OriginalHTClause
OriginalWLClause - Class in org.sat4j.minisat.constraints.cnf
OriginalWLClause(IVecInt, ILits) - Constructor for class org.sat4j.minisat.constraints.cnf.OriginalWLClause
out - Variable in class org.sat4j.AbstractLauncher
out - Variable in class org.sat4j.minisat.core.Solver
OutcomeListener - Interface in org.sat4j.tools: Simple interface to check the outcome of running a solver in parallel.

P

Pair - Class in org.sat4j.minisat.core: Utility class to be used to return the two results of a conflict analysis.
Pair() - Constructor for class org.sat4j.minisat.core.Pair
ParseFormatException - Exception in org.sat4j.reader: Exception launched when there is a problem during parsing.
ParseFormatException() - Constructor for exception org.sat4j.reader.ParseFormatException: Constructor for ParseFormatException.
ParseFormatException(String) - Constructor for exception org.sat4j.reader.ParseFormatException: Constructor for ParseFormatException.
ParseFormatException(String, Throwable) - Constructor for exception org.sat4j.reader.ParseFormatException: Constructor for ParseFormatException.
ParseFormatException(Throwable) - Constructor for exception org.sat4j.reader.ParseFormatException: Constructor for ParseFormatException.
parseInstance(InputStream) - Method in class org.sat4j.reader.AAGReader
parseInstance(InputStream) - Method in class org.sat4j.reader.AIGReader
parseInstance(InputStream) - Method in class org.sat4j.reader.DimacsReader
parseInstance(String) - Method in class org.sat4j.reader.InstanceReader
parseInstance(InputStream) - Method in class org.sat4j.reader.InstanceReader
parseInstance(InputStream) - Method in class org.sat4j.reader.JSONReader
parseInstance(InputStream) - Method in class org.sat4j.reader.LecteurDimacs
parseInstance(String) - Method in class org.sat4j.reader.Reader: This is the usual method to feed a solver with a benchmark.
parseInstance(InputStream) - Method in class org.sat4j.reader.Reader: Read a file from a stream.
parseInstance(Reader) - Method in class org.sat4j.reader.Reader: Deprecated.
parseInstance(int[], int[], int[][], int) - Method in class org.sat4j.tools.DimacsArrayReader
parseString(String) - Method in class org.sat4j.reader.JSONReader
PARSING_ERROR - Static variable in exception org.sat4j.reader.ParseFormatException
PercentLengthLearning<D extends DataStructureFactory> - Class in org.sat4j.minisat.learning: Selects the constraints to learn according to its length as a percentage of the total number of variables in the solver universe.
PercentLengthLearning() - Constructor for class org.sat4j.minisat.learning.PercentLengthLearning
PercentLengthLearning(int) - Constructor for class org.sat4j.minisat.learning.PercentLengthLearning
PhaseCachingAutoEraseStrategy - Class in org.sat4j.minisat.orders
PhaseCachingAutoEraseStrategy() - Constructor for class org.sat4j.minisat.orders.PhaseCachingAutoEraseStrategy
PhaseInLastLearnedClauseSelectionStrategy - Class in org.sat4j.minisat.orders: Keeps record of the phase of a variable in the lastest recorded clause.
PhaseInLastLearnedClauseSelectionStrategy() - Constructor for class org.sat4j.minisat.orders.PhaseInLastLearnedClauseSelectionStrategy
phaseStrategy - Variable in class org.sat4j.minisat.orders.VarOrderHeap
pLiterals - Variable in class org.sat4j.tools.AbstractMinimalModel
Policy - Class in org.sat4j.tools.encoding: This class allows the use of different encodings for different cardinality constraints.
Policy() - Constructor for class org.sat4j.tools.encoding.Policy
pop() - Method in class org.sat4j.core.ReadOnlyVec
pop() - Method in class org.sat4j.core.ReadOnlyVecInt
pop() - Method in class org.sat4j.core.Vec: Pop the last element on the stack.
pop() - Method in class org.sat4j.core.VecInt: depile le dernier element du vecteur.
pop() - Method in interface org.sat4j.specs.IVec: Pop the last element on the stack.
pop() - Method in interface org.sat4j.specs.IVecInt: depile le dernier element du vecteur.
positiveLiterals(ISolver) - Static method in class org.sat4j.tools.AbstractMinimalModel
PositiveLiteralSelectionStrategy - Class in org.sat4j.minisat.orders
PositiveLiteralSelectionStrategy() - Constructor for class org.sat4j.minisat.orders.PositiveLiteralSelectionStrategy
posLit(int) - Static method in class org.sat4j.core.LiteralsUtils: Returns the positive literal associated with a variable.
prevboolmodel - Variable in class org.sat4j.tools.LexicoDecorator
prevConstr - Variable in class org.sat4j.tools.LexicoDecorator
prevfullmodel - Variable in class org.sat4j.tools.LexicoDecorator
prevmodelwithinternalvars - Variable in class org.sat4j.tools.LexicoDecorator
prime - Variable in class org.sat4j.AbstractLauncher
primeImplicant() - Method in class org.sat4j.minisat.core.Solver
primeImplicant(int) - Method in class org.sat4j.minisat.core.Solver
primeImplicant() - Method in interface org.sat4j.specs.IProblem: Provide a prime implicant, i.e. a set of literal that is sufficient to satisfy all constraints of the problem.
primeImplicant(int) - Method in interface org.sat4j.specs.IProblem: Check if a given literal is part of the prime implicant computed by the IProblem.primeImplicant() method.
primeImplicant() - Method in class org.sat4j.tools.AbstractOutputSolver
primeImplicant(int) - Method in class org.sat4j.tools.DimacsOutputSolver
primeImplicant(int) - Method in class org.sat4j.tools.DimacsStringSolver
primeImplicant() - Method in class org.sat4j.tools.ManyCore
primeImplicant(int) - Method in class org.sat4j.tools.ManyCore
primeImplicant() - Method in class org.sat4j.tools.ModelIterator
primeImplicant() - Method in class org.sat4j.tools.SolverDecorator
primeImplicant(int) - Method in class org.sat4j.tools.SolverDecorator
primeImplicant() - Method in class org.sat4j.tools.StatisticsSolver
primeImplicant(int) - Method in class org.sat4j.tools.StatisticsSolver
printInfos(PrintWriter) - Method in class org.sat4j.minisat.core.Solver
printInfos(PrintWriter, String) - Method in class org.sat4j.minisat.core.Solver
printInfos(PrintWriter, String) - Method in interface org.sat4j.specs.IProblem: Deprecated.
printInfos(PrintWriter) - Method in interface org.sat4j.specs.IProblem: To print additional informations regarding the problem.
printInfos(PrintWriter, String) - Method in class org.sat4j.tools.AbstractOutputSolver
printInfos(PrintWriter) - Method in class org.sat4j.tools.DimacsOutputSolver
printInfos(PrintWriter) - Method in class org.sat4j.tools.DimacsStringSolver
printInfos(PrintWriter, String) - Method in class org.sat4j.tools.ManyCore
printInfos(PrintWriter) - Method in class org.sat4j.tools.ManyCore
printInfos(PrintWriter, String) - Method in class org.sat4j.tools.SolverDecorator
printInfos(PrintWriter) - Method in class org.sat4j.tools.SolverDecorator
printInfos(PrintWriter, String) - Method in class org.sat4j.tools.StatisticsSolver: Deprecated.
printInfos(PrintWriter) - Method in class org.sat4j.tools.StatisticsSolver
printLearntClausesInfos(PrintWriter, String) - Method in class org.sat4j.minisat.core.Solver
printStat(PrintWriter, String) - Method in interface org.sat4j.minisat.core.IOrder: Display statistics regarding the heuristics.
printStat(PrintStream, String) - Method in class org.sat4j.minisat.core.Solver
printStat(PrintWriter) - Method in class org.sat4j.minisat.core.Solver
printStat(PrintWriter, String) - Method in class org.sat4j.minisat.core.Solver
printStat(PrintWriter, String) - Method in class org.sat4j.minisat.core.SolverStats
printStat(PrintWriter, String) - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
printStat(PrintWriter, String) - Method in class org.sat4j.minisat.orders.TabuListDecorator
printStat(PrintWriter, String) - Method in class org.sat4j.minisat.orders.VarOrderHeap
printStat(PrintStream, String) - Method in interface org.sat4j.specs.ISolver: Deprecated.
printStat(PrintWriter, String) - Method in interface org.sat4j.specs.ISolver: Deprecated.
using the prefix does no longer makes sense because the solver owns it.
printStat(PrintWriter) - Method in interface org.sat4j.specs.ISolver: Display statistics to the given output writer
printStat(PrintStream, String) - Method in class org.sat4j.tools.AbstractOutputSolver
printStat(PrintWriter, String) - Method in class org.sat4j.tools.AbstractOutputSolver
printStat(PrintWriter) - Method in class org.sat4j.tools.DimacsOutputSolver
printStat(PrintWriter) - Method in class org.sat4j.tools.DimacsStringSolver
printStat(PrintStream, String) - Method in class org.sat4j.tools.ManyCore: Deprecated.
printStat(PrintWriter, String) - Method in class org.sat4j.tools.ManyCore
printStat(PrintWriter) - Method in class org.sat4j.tools.ManyCore
printStat(PrintStream, String) - Method in class org.sat4j.tools.SolverDecorator: Deprecated.
printStat(PrintWriter, String) - Method in class org.sat4j.tools.SolverDecorator
printStat(PrintWriter) - Method in class org.sat4j.tools.SolverDecorator
printStat(PrintStream, String) - Method in class org.sat4j.tools.StatisticsSolver: Deprecated.
printStat(PrintWriter, String) - Method in class org.sat4j.tools.StatisticsSolver: Deprecated.
printStat(PrintWriter) - Method in class org.sat4j.tools.StatisticsSolver
problem - Variable in class org.sat4j.AbstractLauncher
Product - Class in org.sat4j.tools.encoding: Implementation of product encoding for at most one and at most k constraints.
Product() - Constructor for class org.sat4j.tools.encoding.Product
Propagatable - Interface in org.sat4j.minisat.core: This interface is to be implemented by the classes wanted to be notified of the falsification of a literal.
propagate(UnitPropagationListener, int) - Method in class org.sat4j.minisat.constraints.card.AtLeast
propagate(UnitPropagationListener, int) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard: Propagation de la valeur de v?
propagate(UnitPropagationListener, int) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard: propagates the value of a falsified literal
propagate(UnitPropagationListener, int) - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
propagate(UnitPropagationListener, int) - Method in class org.sat4j.minisat.constraints.cnf.HTClause
propagate(UnitPropagationListener, int) - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
propagate(UnitPropagationListener, int) - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
propagate(UnitPropagationListener, int) - Method in class org.sat4j.minisat.constraints.cnf.WLClause
propagate(UnitPropagationListener, int) - Method in interface org.sat4j.minisat.core.Propagatable: Propagate the truth value of a literal in constraints in which that literal is falsified.
propagate() - Method in class org.sat4j.minisat.core.Solver
propagating(int, IConstr) - Method in interface org.sat4j.specs.SearchListener: Unit propagation
propagating(int, IConstr) - Method in class org.sat4j.tools.DotSearchTracing
propagating(int, IConstr) - Method in class org.sat4j.tools.MultiTracing
propagating(int, IConstr) - Method in class org.sat4j.tools.SearchListenerAdapter
propagating(int, IConstr) - Method in class org.sat4j.tools.SpeedTracing
propagating(int, IConstr) - Method in class org.sat4j.tools.TextOutputTracing
propagations - Variable in class org.sat4j.minisat.core.SolverStats
provideUnitClauses(UnitPropagationListener) - Method in interface org.sat4j.specs.UnitClauseProvider
provideUnitClauses(UnitPropagationListener) - Method in class org.sat4j.tools.ManyCore
PureOrder - Class in org.sat4j.minisat.orders
PureOrder() - Constructor for class org.sat4j.minisat.orders.PureOrder
PureOrder(int) - Constructor for class org.sat4j.minisat.orders.PureOrder
push(T) - Method in class org.sat4j.core.ReadOnlyVec
push(int) - Method in class org.sat4j.core.ReadOnlyVecInt
push(T) - Method in class org.sat4j.core.Vec
push(int) - Method in class org.sat4j.core.VecInt
push(int) - Method in class org.sat4j.minisat.core.CircularBuffer
push(T) - Method in interface org.sat4j.specs.IVec
push(int) - Method in interface org.sat4j.specs.IVecInt
pushAll(IVecInt) - Method in class org.sat4j.core.VecInt

Q

QuickXplain2001Strategy - Class in org.sat4j.tools.xplain: An implementation of the QuickXplain algorithm as explained by Ulrich Junker in the following paper:
QuickXplain2001Strategy() - Constructor for class org.sat4j.tools.xplain.QuickXplain2001Strategy
QuickXplainStrategy - Class in org.sat4j.tools.xplain: An implementation of the QuickXplain algorithm as explained by Ulrich Junker in the following paper:
QuickXplainStrategy() - Constructor for class org.sat4j.tools.xplain.QuickXplainStrategy

R

RAND - Static variable in class org.sat4j.minisat.orders.RandomLiteralSelectionStrategy
RandomAccessModel - Interface in org.sat4j.specs: That interface allows to efficiently retrieve the truth value of a given variable in the solver.
RandomLiteralSelectionStrategy - Class in org.sat4j.minisat.orders: The variable selection strategy randomly picks one phase, either positive or negative.
RandomLiteralSelectionStrategy() - Constructor for class org.sat4j.minisat.orders.RandomLiteralSelectionStrategy
RandomWalkDecorator - Class in org.sat4j.minisat.orders
RandomWalkDecorator(VarOrderHeap) - Constructor for class org.sat4j.minisat.orders.RandomWalkDecorator
RandomWalkDecorator(VarOrderHeap, double) - Constructor for class org.sat4j.minisat.orders.RandomWalkDecorator
readConstrs() - Method in class org.sat4j.reader.DimacsReader
reader - Variable in class org.sat4j.AbstractLauncher
Reader - Class in org.sat4j.reader: A reader is responsible to feed an ISolver from a text file and to convert the model found by the solver to a textual representation.
Reader() - Constructor for class org.sat4j.reader.Reader
ReadOnlyVec<T> - Class in org.sat4j.core: Utility class to allow Read Only access to an IVec.
ReadOnlyVec(IVec<T>) - Constructor for class org.sat4j.core.ReadOnlyVec
ReadOnlyVecInt - Class in org.sat4j.core: Utility class to allow Read Only access only to an IVecInt.
ReadOnlyVecInt(IVecInt) - Constructor for class org.sat4j.core.ReadOnlyVecInt
readProblem(String) - Method in class org.sat4j.AbstractLauncher: Reads a problem file from the command line.
readProblemLine() - Method in class org.sat4j.reader.DimacsReader
readProblemLine() - Method in class org.sat4j.reader.GroupedCNFReader
realNumberOfVariables() - Method in class org.sat4j.minisat.core.Solver
realNumberOfVariables() - Method in interface org.sat4j.specs.ISolver: Retrieve the real number of variables used in the solver.
realNumberOfVariables() - Method in class org.sat4j.tools.DimacsOutputSolver
realNumberOfVariables() - Method in class org.sat4j.tools.DimacsStringSolver
realNumberOfVariables() - Method in class org.sat4j.tools.ManyCore
realNumberOfVariables() - Method in class org.sat4j.tools.SolverDecorator
realNumberOfVariables() - Method in class org.sat4j.tools.StatisticsSolver
realnVars() - Method in class org.sat4j.minisat.constraints.cnf.Lits
realnVars() - Method in interface org.sat4j.minisat.core.ILits: to obtain the real number of variables appearing in the formula
reason - Variable in class org.sat4j.minisat.core.Pair
reduce(IVec<Constr>) - Method in interface org.sat4j.minisat.core.LearnedConstraintsDeletionStrategy: Hook method called when the solver wants to reduce the set of learned clauses.
reduceDB() - Method in class org.sat4j.minisat.core.Solver
reduceddb - Variable in class org.sat4j.minisat.core.SolverStats
reducedliterals - Variable in class org.sat4j.minisat.core.SolverStats
register() - Method in class org.sat4j.minisat.constraints.card.AtLeast
register() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
register() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
register() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
register() - Method in class org.sat4j.minisat.constraints.cnf.LearntHTClause
register() - Method in class org.sat4j.minisat.constraints.cnf.LearntWLClause
register() - Method in class org.sat4j.minisat.constraints.cnf.OriginalHTClause
register() - Method in class org.sat4j.minisat.constraints.cnf.OriginalWLClause
register() - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
register() - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
register() - Method in interface org.sat4j.minisat.core.Constr: Register the constraint to the solver.
registerLiteral(int) - Method in class org.sat4j.minisat.core.Solver
registerLiteral(int) - Method in interface org.sat4j.specs.ISolver: Tell the solver to consider that the literal is in the CNF.
registerLiteral(int) - Method in class org.sat4j.tools.DimacsOutputSolver
registerLiteral(int) - Method in class org.sat4j.tools.DimacsStringSolver
registerLiteral(int) - Method in class org.sat4j.tools.ManyCore
registerLiteral(int) - Method in class org.sat4j.tools.SolverDecorator
registerLiteral(int) - Method in class org.sat4j.tools.StatisticsSolver
RemiUtils - Class in org.sat4j.tools: Class dedicated to Remi Coletta utility methods :-)
remove(T) - Method in class org.sat4j.core.ReadOnlyVec
remove(int) - Method in class org.sat4j.core.ReadOnlyVecInt
remove(T) - Method in class org.sat4j.core.Vec: Remove an element that belongs to the Vector.
remove(int) - Method in class org.sat4j.core.VecInt: Enleve un element qui se trouve dans le vecteur!!!
remove(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.card.AtLeast
remove(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
remove(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard: Removes a constraint from the solver
remove(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
remove(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.HTClause
remove(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
remove(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
remove(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.WLClause
remove(UnitPropagationListener) - Method in interface org.sat4j.minisat.core.Constr: Remove a constraint from the solver.
remove(T) - Method in interface org.sat4j.specs.IVec: Enleve un element qui se trouve dans le vecteur!!!
remove(int) - Method in interface org.sat4j.specs.IVecInt: Enleve un element qui se trouve dans le vecteur!!!
removeConstr(IConstr) - Method in class org.sat4j.minisat.core.Solver
removeConstr(IConstr) - Method in interface org.sat4j.specs.ISolver: Remove a constraint returned by one of the add method from the solver.
removeConstr(IConstr) - Method in class org.sat4j.tools.AbstractOutputSolver
removeConstr(IConstr) - Method in class org.sat4j.tools.ManyCore
removeConstr(IConstr) - Method in class org.sat4j.tools.SolverDecorator
removeConstr(IConstr) - Method in class org.sat4j.tools.StatisticsSolver
removeConstr(IConstr) - Method in class org.sat4j.tools.xplain.Xplain
removeFrom(ISolver) - Method in class org.sat4j.core.ConstrGroup
removeSubsumedConstr(IConstr) - Method in class org.sat4j.minisat.core.Solver
removeSubsumedConstr(IConstr) - Method in interface org.sat4j.specs.ISolver: Remove a constraint returned by one of the add method from the solver that is subsumed by a constraint already in the solver or to be added to the solver.
removeSubsumedConstr(IConstr) - Method in interface org.sat4j.specs.ISolverService: Remove a constraint returned by one of the add method from the solver that is subsumed by a constraint already in the solver or to be added to the solver.
removeSubsumedConstr(IConstr) - Method in class org.sat4j.tools.AbstractOutputSolver
removeSubsumedConstr(IConstr) - Method in class org.sat4j.tools.ManyCore
removeSubsumedConstr(IConstr) - Method in class org.sat4j.tools.SolverDecorator
removeSubsumedConstr(IConstr) - Method in class org.sat4j.tools.StatisticsSolver
removeSubsumedConstr(IConstr) - Method in class org.sat4j.tools.xplain.Xplain
rescaleBy(double) - Method in class org.sat4j.minisat.constraints.card.AtLeast
rescaleBy(double) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard: Permet le r??
rescaleBy(double) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard: Rescales the activity value of the constraint
rescaleBy(double) - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
rescaleBy(double) - Method in class org.sat4j.minisat.constraints.cnf.HTClause
rescaleBy(double) - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
rescaleBy(double) - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
rescaleBy(double) - Method in class org.sat4j.minisat.constraints.cnf.WLClause
rescaleBy(double) - Method in interface org.sat4j.minisat.core.Constr: Rescale the clause activity by a value.
reset() - Method in class org.sat4j.minisat.constraints.AbstractDataStructureFactory
reset(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
reset() - Method in interface org.sat4j.minisat.core.ConflictTimer
reset() - Method in class org.sat4j.minisat.core.ConflictTimerAdapter
reset() - Method in class org.sat4j.minisat.core.ConflictTimerContainer
reset() - Method in interface org.sat4j.minisat.core.DataStructureFactory
reset(int) - Method in interface org.sat4j.minisat.core.ILits: Reset a literal in the vocabulary.
reset() - Method in class org.sat4j.minisat.core.Solver
reset() - Method in class org.sat4j.minisat.core.SolverStats
reset() - Method in class org.sat4j.minisat.restarts.ArminRestarts
reset() - Method in class org.sat4j.minisat.restarts.FixedPeriodRestarts
reset() - Method in class org.sat4j.minisat.restarts.Glucose21Restarts
reset() - Method in class org.sat4j.minisat.restarts.LubyRestarts
reset() - Method in class org.sat4j.minisat.restarts.MiniSATRestarts
reset() - Method in class org.sat4j.minisat.restarts.NoRestarts
reset() - Method in class org.sat4j.opt.MaxSatDecorator
reset() - Method in class org.sat4j.opt.MinOneDecorator
reset() - Method in interface org.sat4j.specs.ISolver: Clean up the internal state of the solver.
reset() - Method in class org.sat4j.tools.DimacsOutputSolver
reset() - Method in class org.sat4j.tools.DimacsStringSolver
reset() - Method in class org.sat4j.tools.ManyCore
reset() - Method in class org.sat4j.tools.ModelIterator
reset() - Method in class org.sat4j.tools.OptToSatAdapter
reset() - Method in class org.sat4j.tools.SolverDecorator
reset() - Method in class org.sat4j.tools.StatisticsSolver
resetPool() - Method in class org.sat4j.minisat.constraints.cnf.Lits
resetPool() - Method in interface org.sat4j.minisat.core.ILits: reset the vocabulary.
restarting() - Method in interface org.sat4j.specs.SearchListener: The solver restarts the search.
restarting() - Method in class org.sat4j.tools.ConflictDepthTracing
restarting() - Method in class org.sat4j.tools.ConflictLevelTracing
restarting() - Method in class org.sat4j.tools.DecisionTracing
restarting() - Method in class org.sat4j.tools.HeuristicsTracing
restarting() - Method in class org.sat4j.tools.LearnedClausesSizeTracing
restarting() - Method in class org.sat4j.tools.LearnedTracing
restarting() - Method in class org.sat4j.tools.MultiTracing
restarting() - Method in class org.sat4j.tools.SearchListenerAdapter
restarting() - Method in class org.sat4j.tools.SpeedTracing
restarting() - Method in class org.sat4j.tools.TextOutputTracing
RestartStrategy - Interface in org.sat4j.minisat.core: Abstraction allowing to choose various restarts strategies.
rootLevel - Variable in class org.sat4j.minisat.core.Solver: position of assumptions before starting the search.
rootSimplifications - Variable in class org.sat4j.minisat.core.SolverStats
RSATLastLearnedClausesPhaseSelectionStrategy - Class in org.sat4j.minisat.orders: Keeps track of the phase of the latest assignment.
RSATLastLearnedClausesPhaseSelectionStrategy() - Constructor for class org.sat4j.minisat.orders.RSATLastLearnedClausesPhaseSelectionStrategy
RSATPhaseSelectionStrategy - Class in org.sat4j.minisat.orders: Keeps track of the phase of the latest assignment.
RSATPhaseSelectionStrategy() - Constructor for class org.sat4j.minisat.orders.RSATPhaseSelectionStrategy
run(String[]) - Method in class org.sat4j.AbstractLauncher
run() - Method in class org.sat4j.minisat.core.ConflictTimerAdapter
run(String[]) - Method in class org.sat4j.MUSLauncher
RupSearchListener<S extends ISolverService> - Class in org.sat4j.tools: Output an unsat proof using the reverse unit propagation (RUP) format.
RupSearchListener(String) - Constructor for class org.sat4j.tools.RupSearchListener

S

sanityCheck(IVecInt, ILits, UnitPropagationListener) - Static method in class org.sat4j.minisat.constraints.cnf.Clauses: Perform some sanity check before constructing a clause a) if a literal is assigned true, return null (the clause is satisfied) b) if a literal is assigned false, remove it c) if a clause contains a literal and its opposite (tautology) return null d) remove duplicate literals e) if the clause is empty, return null f) if the clause if unit, transmit it to the object responsible for unit propagation
SATISFIABLE - Static variable in class org.sat4j.ExitCode
satisfies(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
satisfies(int) - Method in interface org.sat4j.minisat.core.ILits: Satisfies a boolean variable (truth value is TRUE).
scanner - Variable in class org.sat4j.reader.DimacsReader
SearchEnumeratorListener - Class in org.sat4j.tools: That class allows to iterate over the models from the inside: conflicts are created to ask the solver to backtrack.
SearchEnumeratorListener(SolutionFoundListener) - Constructor for class org.sat4j.tools.SearchEnumeratorListener
SearchListener<S extends ISolverService> - Interface in org.sat4j.specs: Interface to the solver main steps.
SearchListenerAdapter<S extends ISolverService> - Class in org.sat4j.tools
SearchListenerAdapter() - Constructor for class org.sat4j.tools.SearchListenerAdapter
SearchMinOneListener - Class in org.sat4j.tools: That class allows to iterate over the models from the inside: conflicts are created to ask the solver to backtrack.
SearchMinOneListener(SolutionFoundListener) - Constructor for class org.sat4j.tools.SearchMinOneListener
SearchParams - Class in org.sat4j.minisat.core: Some parameters used during the search.
SearchParams() - Constructor for class org.sat4j.minisat.core.SearchParams: Default search parameters.
SearchParams(int) - Constructor for class org.sat4j.minisat.core.SearchParams
SearchParams(double, int) - Constructor for class org.sat4j.minisat.core.SearchParams
SearchParams(double, double, double, int) - Constructor for class org.sat4j.minisat.core.SearchParams
select() - Method in interface org.sat4j.minisat.core.IOrder: Selects the next "best" unassigned literal.
select(int) - Method in interface org.sat4j.minisat.core.IPhaseSelectionStrategy: selects the phase of the variable according to a phase selection strategy.
select(int) - Method in class org.sat4j.minisat.orders.NegativeLiteralSelectionStrategy
select(int) - Method in class org.sat4j.minisat.orders.PositiveLiteralSelectionStrategy
select() - Method in class org.sat4j.minisat.orders.PureOrder
select(int) - Method in class org.sat4j.minisat.orders.RandomLiteralSelectionStrategy
select() - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
select() - Method in class org.sat4j.minisat.orders.TabuListDecorator
select() - Method in class org.sat4j.minisat.orders.VarOrderHeap: Selectionne une nouvelle variable, non affectee, ayant l'activite la plus elevee.
Sequential - Class in org.sat4j.tools.encoding: Implementation of the sequential encoding for the at most k constraint.
Sequential() - Constructor for class org.sat4j.tools.encoding.Sequential
set(int, T) - Method in class org.sat4j.core.ReadOnlyVec
set(int, int) - Method in class org.sat4j.core.ReadOnlyVecInt
set(int, T) - Method in class org.sat4j.core.Vec
set(int, int) - Method in class org.sat4j.core.VecInt
set(int, T) - Method in interface org.sat4j.specs.IVec
set(int, int) - Method in interface org.sat4j.specs.IVecInt
setActivity(double) - Method in class org.sat4j.minisat.constraints.card.AtLeast
setActivity(double) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
setActivity(double) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
setActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.LearntBinaryClause
setActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.LearntHTClause
setActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.OriginalBinaryClause
setActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.OriginalHTClause
setActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
setActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
setActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.WLClause
setActivity(double) - Method in interface org.sat4j.minisat.core.Constr: Set the activity at a specific value
setActivityPercent(double) - Method in class org.sat4j.minisat.learning.ActiveLearning
setAtLeastKEncoding(EncodingStrategyAdapter) - Method in class org.sat4j.tools.encoding.Policy
setAtLeastKEncoding(EncodingStrategy) - Method in class org.sat4j.tools.encoding.Policy
setAtLeastOneEncoding(EncodingStrategyAdapter) - Method in class org.sat4j.tools.encoding.Policy
setAtLeastOneEncoding(EncodingStrategy) - Method in class org.sat4j.tools.encoding.Policy
setAtMostKEncoding(EncodingStrategyAdapter) - Method in class org.sat4j.tools.encoding.Policy
setAtMostKEncoding(EncodingStrategy) - Method in class org.sat4j.tools.encoding.Policy
setAtMostOneEncoding(EncodingStrategyAdapter) - Method in class org.sat4j.tools.encoding.Policy
setAtMostOneEncoding(EncodingStrategy) - Method in class org.sat4j.tools.encoding.Policy
setBound(int) - Method in class org.sat4j.minisat.learning.FixedLengthLearning
setBound(int) - Method in class org.sat4j.minisat.learning.PercentLengthLearning
setBounds(int) - Method in class org.sat4j.minisat.core.Heap
setClaDecay(double) - Method in class org.sat4j.minisat.core.SearchParams
setConflictBoundIncFactor(double) - Method in class org.sat4j.minisat.core.SearchParams
setDataStructureFactory(D) - Method in interface org.sat4j.minisat.core.ICDCL: Change the internal representation of the constraints.
setDataStructureFactory(D) - Method in class org.sat4j.minisat.core.Solver
setDataStructureFactory(DataStructureFactory) - Method in class org.sat4j.minisat.learning.MiniSATLearning
setDBSimplificationAllowed(boolean) - Method in class org.sat4j.minisat.core.Solver
setDBSimplificationAllowed(boolean) - Method in interface org.sat4j.specs.ISolver: Set whether the solver is allowed to simplify the formula by propagating the truth value of top level satisfied variables.
setDBSimplificationAllowed(boolean) - Method in class org.sat4j.tools.AbstractOutputSolver
setDBSimplificationAllowed(boolean) - Method in class org.sat4j.tools.ManyCore
setDBSimplificationAllowed(boolean) - Method in class org.sat4j.tools.SolverDecorator
setDBSimplificationAllowed(boolean) - Method in class org.sat4j.tools.StatisticsSolver
setDisplaySolutionLine(boolean) - Method in class org.sat4j.AbstractLauncher: To change the display so that solution line appears or not.
setDisplaySolutionLine(boolean) - Method in class org.sat4j.AbstractOptimizationLauncher: Deprecated.
setExactlyKEncoding(EncodingStrategyAdapter) - Method in class org.sat4j.tools.encoding.Policy
setExactlyKEncoding(EncodingStrategy) - Method in class org.sat4j.tools.encoding.Policy
setExactlyOneEncoding(EncodingStrategyAdapter) - Method in class org.sat4j.tools.encoding.Policy
setExactlyOneEncoding(EncodingStrategy) - Method in class org.sat4j.tools.encoding.Policy
setExitCode(ExitCode) - Method in class org.sat4j.AbstractLauncher: Change the value of the exit code in the Launcher
setExitCode(ExitCode) - Method in interface org.sat4j.ILauncherMode: Allow to set a specific exit code to the launcher (in case of trivial unsatisfiability for instance).
setExpectedNumberOfClauses(int) - Method in class org.sat4j.minisat.core.Solver
setExpectedNumberOfClauses(int) - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
setExpectedNumberOfClauses(int) - Method in class org.sat4j.opt.MaxSatDecorator
setExpectedNumberOfClauses(int) - Method in interface org.sat4j.specs.ISolver: To inform the solver of the expected number of clauses to read.
setExpectedNumberOfClauses(int) - Method in class org.sat4j.tools.DimacsOutputSolver
setExpectedNumberOfClauses(int) - Method in class org.sat4j.tools.DimacsStringSolver
setExpectedNumberOfClauses(int) - Method in class org.sat4j.tools.ManyCore
setExpectedNumberOfClauses(int) - Method in class org.sat4j.tools.SolverDecorator
setExpectedNumberOfClauses(int) - Method in class org.sat4j.tools.StatisticsSolver
setFactor(int) - Method in class org.sat4j.minisat.restarts.LubyRestarts
setFilename(String) - Method in class org.sat4j.tools.FileBasedVisualizationTool
setIncomplete(boolean) - Method in class org.sat4j.AbstractLauncher
setIncomplete(boolean) - Method in class org.sat4j.AbstractOptimizationLauncher: Deprecated.
setIncomplete(boolean) - Method in interface org.sat4j.ILauncherMode: Allows the launcher to specifically return an upper bound of the optimal solution in case of a time out (for maxsat competitions for instance).
setInitConflictBound(int) - Method in class org.sat4j.minisat.core.SearchParams
setKeepSolverHot(boolean) - Method in class org.sat4j.minisat.core.Solver
setKeepSolverHot(boolean) - Method in interface org.sat4j.specs.ISolver: Changed the behavior of the SAT solver heuristics between successive calls.
setKeepSolverHot(boolean) - Method in class org.sat4j.tools.AbstractOutputSolver
setKeepSolverHot(boolean) - Method in class org.sat4j.tools.ManyCore
setKeepSolverHot(boolean) - Method in class org.sat4j.tools.SolverDecorator
setKeepSolverHot(boolean) - Method in class org.sat4j.tools.StatisticsSolver
setLastConstr(IConstr) - Method in class org.sat4j.tools.FullClauseSelectorSolver
setLauncherMode(ILauncherMode) - Method in class org.sat4j.AbstractLauncher
setLearnedConstraintsDeletionStrategy(LearnedConstraintsDeletionStrategy) - Method in interface org.sat4j.minisat.core.ICDCL
setLearnedConstraintsDeletionStrategy(ConflictTimer, LearnedConstraintsEvaluationType) - Method in interface org.sat4j.minisat.core.ICDCL
setLearnedConstraintsDeletionStrategy(LearnedConstraintsEvaluationType) - Method in interface org.sat4j.minisat.core.ICDCL
setLearnedConstraintsDeletionStrategy(LearnedConstraintsDeletionStrategy) - Method in class org.sat4j.minisat.core.Solver
setLearnedConstraintsDeletionStrategy(ConflictTimer, LearnedConstraintsEvaluationType) - Method in class org.sat4j.minisat.core.Solver
setLearnedConstraintsDeletionStrategy(LearnedConstraintsEvaluationType) - Method in class org.sat4j.minisat.core.Solver
setLearner(Learner) - Method in class org.sat4j.minisat.constraints.AbstractDataStructureFactory
setLearner(Learner) - Method in interface org.sat4j.minisat.core.DataStructureFactory
setLearner(LearningStrategy<D>) - Method in interface org.sat4j.minisat.core.ICDCL: Deprecated.
renamed into setLearningStrategy()
setLearner(LearningStrategy<D>) - Method in class org.sat4j.minisat.core.Solver
setLearningStrategy(LearningStrategy<D>) - Method in interface org.sat4j.minisat.core.ICDCL: Allow to change the learning strategy, i.e. to decide which clauses/constraints should be learned by the solver after conflict analysis.
setLearningStrategy(LearningStrategy<D>) - Method in class org.sat4j.minisat.core.Solver
setLearnt() - Method in class org.sat4j.minisat.constraints.card.AtLeast
setLearnt() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
setLearnt() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
setLearnt() - Method in class org.sat4j.minisat.constraints.cnf.LearntBinaryClause
setLearnt() - Method in class org.sat4j.minisat.constraints.cnf.LearntHTClause
setLearnt() - Method in class org.sat4j.minisat.constraints.cnf.LearntWLClause
setLearnt() - Method in class org.sat4j.minisat.constraints.cnf.OriginalBinaryClause
setLearnt() - Method in class org.sat4j.minisat.constraints.cnf.OriginalHTClause
setLearnt() - Method in class org.sat4j.minisat.constraints.cnf.OriginalWLClause
setLearnt() - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
setLearnt() - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
setLearnt() - Method in interface org.sat4j.minisat.core.Constr: Mark a constraint as learnt.
setLevel(int, int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
setLevel(int, int) - Method in interface org.sat4j.minisat.core.ILits: Sets the decision level of a literal.
setLimit(int) - Method in class org.sat4j.minisat.learning.ActiveLearning
setLimit(int) - Method in class org.sat4j.minisat.learning.PercentLengthLearning
setLits(ILits) - Method in interface org.sat4j.minisat.core.IOrder: Method used to provide an easy access the the solver vocabulary.
setLits(ILits) - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
setLits(ILits) - Method in class org.sat4j.minisat.orders.TabuListDecorator
setLits(ILits) - Method in class org.sat4j.minisat.orders.VarOrderHeap
setLogger(ILogAble) - Method in interface org.sat4j.minisat.core.ICDCL
setLogger(ILogAble) - Method in class org.sat4j.minisat.core.Solver
setLogPrefix(String) - Method in class org.sat4j.minisat.core.Solver
setLogPrefix(String) - Method in interface org.sat4j.specs.ISolver: Set the prefix used to display information.
setLogPrefix(String) - Method in class org.sat4j.tools.AbstractOutputSolver
setLogPrefix(String) - Method in class org.sat4j.tools.ManyCore
setLogPrefix(String) - Method in class org.sat4j.tools.SolverDecorator
setLogPrefix(String) - Method in class org.sat4j.tools.StatisticsSolver
setLogWriter(PrintWriter) - Method in class org.sat4j.AbstractLauncher: To change the output stream on which statistics are displayed.
setMaxLength(int) - Method in class org.sat4j.minisat.learning.FixedLengthLearning
setMinimizationStrategy(MinimizationStrategy) - Method in interface org.sat4j.tools.xplain.Explainer
setMinimizationStrategy(MinimizationStrategy) - Method in class org.sat4j.tools.xplain.HighLevelXplain
setMinimizationStrategy(MinimizationStrategy) - Method in class org.sat4j.tools.xplain.Xplain
setNbexpectedclauses(int) - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
setNbVars(int) - Method in class org.sat4j.tools.DimacsStringSolver
setNeedToReduceDB(boolean) - Method in interface org.sat4j.minisat.core.ICDCL
setNeedToReduceDB(boolean) - Method in class org.sat4j.minisat.core.Solver
setOrder(IOrder) - Method in interface org.sat4j.minisat.core.ICDCL
setOrder(IOrder) - Method in class org.sat4j.minisat.core.Solver
setOrder(IOrder) - Method in class org.sat4j.minisat.learning.ActiveLearning
setPeriod(int) - Method in class org.sat4j.minisat.orders.PureOrder
setPeriod(long) - Method in class org.sat4j.minisat.restarts.FixedPeriodRestarts
setPhaseSelectionStrategy(IPhaseSelectionStrategy) - Method in interface org.sat4j.minisat.core.IOrder
setPhaseSelectionStrategy(IPhaseSelectionStrategy) - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
setPhaseSelectionStrategy(IPhaseSelectionStrategy) - Method in class org.sat4j.minisat.orders.TabuListDecorator
setPhaseSelectionStrategy(IPhaseSelectionStrategy) - Method in class org.sat4j.minisat.orders.VarOrderHeap: Change the selection strategy.
setPrevboolmodel(boolean[]) - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
setPrevfullmodel(int[]) - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
setPrevmodel(int[]) - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
setProbability(double) - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
setReason(int, Constr) - Method in class org.sat4j.minisat.constraints.cnf.Lits
setReason(int, Constr) - Method in interface org.sat4j.minisat.core.ILits: Sets the reason of the assignment of a literal.
setRestartStrategy(RestartStrategy) - Method in interface org.sat4j.minisat.core.ICDCL
setRestartStrategy(RestartStrategy) - Method in class org.sat4j.minisat.core.Solver
setSearchListener(SearchListener<S>) - Method in class org.sat4j.minisat.core.Solver
setSearchListener(SearchListener<S>) - Method in interface org.sat4j.specs.ISolver: Allow the user to hook a listener to the solver to be notified of the main steps of the search process.
setSearchListener(SearchListener<S>) - Method in class org.sat4j.tools.AbstractOutputSolver
setSearchListener(SearchListener<I>) - Method in class org.sat4j.tools.ManyCore
setSearchListener(SearchListener<S>) - Method in class org.sat4j.tools.SolverDecorator
setSearchListener(SearchListener<S>) - Method in class org.sat4j.tools.StatisticsSolver
setSearchParams(SearchParams) - Method in interface org.sat4j.minisat.core.ICDCL
setSearchParams(SearchParams) - Method in class org.sat4j.minisat.core.Solver
setSilent(boolean) - Method in class org.sat4j.AbstractLauncher
setSimplifier(SimplificationType) - Method in interface org.sat4j.minisat.core.ICDCL: Setup the reason simplification strategy.
setSimplifier(ISimplifier) - Method in interface org.sat4j.minisat.core.ICDCL: Setup the reason simplification strategy.
setSimplifier(SimplificationType) - Method in class org.sat4j.minisat.core.Solver
setSimplifier(ISimplifier) - Method in class org.sat4j.minisat.core.Solver
setSolutionOptimal(boolean) - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
setSolver(Solver<D>) - Method in interface org.sat4j.minisat.core.LearningStrategy
setSolver(Solver<D>) - Method in class org.sat4j.minisat.learning.ActiveLearning
setSolver(Solver<D>) - Method in class org.sat4j.minisat.learning.LimitedLearning
setSolver(Solver<D>) - Method in class org.sat4j.minisat.learning.MiniSATLearning
setTimeout(int) - Method in class org.sat4j.minisat.core.Solver
setTimeout(int) - Method in interface org.sat4j.specs.ISolver: To set the internal timeout of the solver.
setTimeout(int) - Method in class org.sat4j.tools.AbstractOutputSolver
setTimeout(int) - Method in class org.sat4j.tools.ManyCore
setTimeout(int) - Method in class org.sat4j.tools.SolverDecorator
setTimeout(int) - Method in class org.sat4j.tools.StatisticsSolver
setTimeoutForFindingBetterSolution(int) - Method in class org.sat4j.opt.MaxSatDecorator
setTimeoutForFindingBetterSolution(int) - Method in class org.sat4j.opt.MinOneDecorator
setTimeoutForFindingBetterSolution(int) - Method in interface org.sat4j.specs.IOptimizationProblem: Allow to set a specific timeout when the solver is in optimization mode.
setTimeoutForFindingBetterSolution(int) - Method in class org.sat4j.tools.LexicoDecorator
setTimeoutMs(long) - Method in class org.sat4j.minisat.core.Solver
setTimeoutMs(long) - Method in interface org.sat4j.specs.ISolver: To set the internal timeout of the solver.
setTimeoutMs(long) - Method in class org.sat4j.tools.AbstractOutputSolver
setTimeoutMs(long) - Method in class org.sat4j.tools.ManyCore
setTimeoutMs(long) - Method in class org.sat4j.tools.SolverDecorator
setTimeoutMs(long) - Method in class org.sat4j.tools.StatisticsSolver
setTimeoutOnConflicts(int) - Method in class org.sat4j.minisat.core.Solver
setTimeoutOnConflicts(int) - Method in interface org.sat4j.specs.ISolver: To set the internal timeout of the solver.
setTimeoutOnConflicts(int) - Method in class org.sat4j.tools.AbstractOutputSolver
setTimeoutOnConflicts(int) - Method in class org.sat4j.tools.ManyCore
setTimeoutOnConflicts(int) - Method in class org.sat4j.tools.SolverDecorator
setTimeoutOnConflicts(int) - Method in class org.sat4j.tools.StatisticsSolver
setUnitClauseProvider(UnitClauseProvider) - Method in class org.sat4j.minisat.core.Solver
setUnitClauseProvider(UnitClauseProvider) - Method in interface org.sat4j.specs.ISolver: Allow the solver to ask for unit clauses before each restarts.
setUnitClauseProvider(UnitClauseProvider) - Method in class org.sat4j.tools.AbstractOutputSolver
setUnitClauseProvider(UnitClauseProvider) - Method in class org.sat4j.tools.ManyCore
setUnitClauseProvider(UnitClauseProvider) - Method in class org.sat4j.tools.SolverDecorator
setUnitClauseProvider(UnitClauseProvider) - Method in class org.sat4j.tools.StatisticsSolver
setUnitPropagationListener(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.AbstractDataStructureFactory
setUnitPropagationListener(UnitPropagationListener) - Method in interface org.sat4j.minisat.core.DataStructureFactory
setVarActivityListener(VarActivityListener) - Method in interface org.sat4j.minisat.core.LearningStrategy
setVarActivityListener(VarActivityListener) - Method in class org.sat4j.minisat.learning.LimitedLearning
setVarDecay(double) - Method in interface org.sat4j.minisat.core.IOrder: Sets the variable activity decay as a growing factor for the next variable activity.
setVarDecay(double) - Method in class org.sat4j.minisat.core.SearchParams
setVarDecay(double) - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
setVarDecay(double) - Method in class org.sat4j.minisat.orders.TabuListDecorator
setVarDecay(double) - Method in class org.sat4j.minisat.orders.VarOrderHeap: Change la valeur de varDecay.
setVerbose(boolean) - Method in class org.sat4j.minisat.core.Solver
setVerbose(boolean) - Method in interface org.sat4j.specs.ISolver: Set the verbosity of the solver
setVerbose(boolean) - Method in class org.sat4j.tools.AbstractOutputSolver
setVerbose(boolean) - Method in class org.sat4j.tools.ManyCore
setVerbose(boolean) - Method in class org.sat4j.tools.SolverDecorator
setVerbose(boolean) - Method in class org.sat4j.tools.StatisticsSolver
setVerbosity(boolean) - Method in class org.sat4j.reader.Reader
sharedConflict - Variable in class org.sat4j.minisat.core.Solver
shortcuts - Variable in class org.sat4j.minisat.core.SolverStats
shouldRestart() - Method in interface org.sat4j.minisat.core.RestartStrategy: Ask the strategy if the solver should restart.
shouldRestart() - Method in class org.sat4j.minisat.restarts.ArminRestarts
shouldRestart() - Method in class org.sat4j.minisat.restarts.FixedPeriodRestarts
shouldRestart() - Method in class org.sat4j.minisat.restarts.Glucose21Restarts
shouldRestart() - Method in class org.sat4j.minisat.restarts.LubyRestarts
shouldRestart() - Method in class org.sat4j.minisat.restarts.MiniSATRestarts
shouldRestart() - Method in class org.sat4j.minisat.restarts.NoRestarts
showAvailableSolvers(ASolverFactory<T>) - Method in class org.sat4j.AbstractLauncher
showAvailableSolvers(ASolverFactory<T>, String) - Method in class org.sat4j.AbstractLauncher
shrink(int) - Method in class org.sat4j.core.ReadOnlyVec
shrink(int) - Method in class org.sat4j.core.ReadOnlyVecInt
shrink(int) - Method in class org.sat4j.core.Vec: Remove nofelems from the Vector.
shrink(int) - Method in class org.sat4j.core.VecInt: Remove the latest nofelems elements from the vector
shrink(int) - Method in interface org.sat4j.specs.IVec: Remove nofelems from the Vector.
shrink(int) - Method in interface org.sat4j.specs.IVecInt: Remove the latest nofelems elements from the vector
shrinkTo(int) - Method in class org.sat4j.core.ReadOnlyVec
shrinkTo(int) - Method in class org.sat4j.core.ReadOnlyVecInt
shrinkTo(int) - Method in class org.sat4j.core.Vec: reduce the Vector to exactly newsize elements
shrinkTo(int) - Method in class org.sat4j.core.VecInt
shrinkTo(int) - Method in interface org.sat4j.specs.IVec: reduce the Vector to exactly newsize elements
shrinkTo(int) - Method in interface org.sat4j.specs.IVecInt
shutdownHook - Variable in class org.sat4j.AbstractLauncher
silent - Variable in class org.sat4j.AbstractLauncher
SIMPLE_SIMPLIFICATION - Variable in class org.sat4j.minisat.core.Solver
SimplificationType - Enum in org.sat4j.minisat.core: List the available simplification techniques available.
simplify() - Method in class org.sat4j.minisat.constraints.card.AtLeast
simplify() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard: Simplifie la contrainte(l'all?
simplify() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard: simplifies the constraint
simplify() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
simplify() - Method in class org.sat4j.minisat.constraints.cnf.HTClause
simplify() - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
simplify() - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
simplify() - Method in class org.sat4j.minisat.constraints.cnf.WLClause
simplify() - Method in interface org.sat4j.minisat.core.Constr: Simplifies a constraint, by removing top level falsified literals for instance.
simplify(IVecInt) - Method in interface org.sat4j.minisat.core.ISimplifier
simplifyDB() - Method in class org.sat4j.minisat.core.Solver
SingleSolutionDetector - Class in org.sat4j.tools: This solver decorator allows to detect whether or not the set of constraints available in the solver has only one solution or not.
SingleSolutionDetector(ISolver) - Constructor for class org.sat4j.tools.SingleSolutionDetector
size() - Method in class org.sat4j.core.ConstrGroup
size() - Method in class org.sat4j.core.ReadOnlyVec
size() - Method in class org.sat4j.core.ReadOnlyVecInt
size() - Method in class org.sat4j.core.Vec
size() - Method in class org.sat4j.core.VecInt
size() - Method in class org.sat4j.minisat.constraints.card.AtLeast
size() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
size() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
size() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
size() - Method in class org.sat4j.minisat.constraints.cnf.HTClause
size() - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
size() - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
size() - Method in class org.sat4j.minisat.constraints.cnf.WLClause
size() - Method in class org.sat4j.minisat.core.Heap
size() - Method in class org.sat4j.minisat.core.IntQueue: Pour connaitre la taille de la queue.
size() - Method in interface org.sat4j.specs.IConstr
size() - Method in interface org.sat4j.specs.IVec
size() - Method in interface org.sat4j.specs.IVecInt
skipComments() - Method in class org.sat4j.reader.DimacsReader: Skip comments at the beginning of the input stream.
skipComments() - Method in class org.sat4j.reader.EfficientScanner: Skip commented lines.
skipRestOfLine() - Method in class org.sat4j.reader.EfficientScanner
skipSpaces() - Method in class org.sat4j.reader.EfficientScanner
slistener - Variable in class org.sat4j.minisat.core.Solver
SOLUTION_PREFIX - Static variable in interface org.sat4j.ILauncherMode
SolutionCounter - Class in org.sat4j.tools: Another solver decorator that counts the number of solutions.
SolutionCounter(ISolver) - Constructor for class org.sat4j.tools.SolutionCounter
solutionFound(int[], RandomAccessModel) - Method in interface org.sat4j.specs.SearchListener: a solution is found.
solutionFound(int[], RandomAccessModel) - Method in class org.sat4j.tools.DotSearchTracing
solutionFound(int[], RandomAccessModel) - Method in class org.sat4j.tools.HeuristicsTracing
solutionFound(int[], RandomAccessModel) - Method in class org.sat4j.tools.LearnedTracing
solutionFound(int[], RandomAccessModel) - Method in class org.sat4j.tools.MultiTracing
solutionFound(int[], RandomAccessModel) - Method in class org.sat4j.tools.SearchEnumeratorListener
solutionFound(int[], RandomAccessModel) - Method in class org.sat4j.tools.SearchListenerAdapter
solutionFound(int[], RandomAccessModel) - Method in class org.sat4j.tools.SearchMinOneListener
solutionFound(int[], RandomAccessModel) - Method in class org.sat4j.tools.TextOutputTracing
SolutionFoundListener - Interface in org.sat4j.tools: Allows the end user to react when a new solution is found.
solve(IProblem) - Method in class org.sat4j.AbstractLauncher
solve(IProblem) - Method in class org.sat4j.AbstractOptimizationLauncher: Deprecated.
solve(IProblem, Reader, ILogAble, PrintWriter, long) - Method in interface org.sat4j.ILauncherMode: Main solver call: one call for a decision problem, a loop for an optimization problem.
solver - Variable in class org.sat4j.AbstractLauncher
solver - Variable in class org.sat4j.minisat.constraints.AbstractDataStructureFactory
Solver<D extends DataStructureFactory> - Class in org.sat4j.minisat.core: The backbone of the library providing the modular implementation of a MiniSAT (Chaff) like solver.
Solver(LearningStrategy<D>, D, IOrder, RestartStrategy) - Constructor for class org.sat4j.minisat.core.Solver: creates a Solver without LearningListener.
Solver(LearningStrategy<D>, D, SearchParams, IOrder, RestartStrategy) - Constructor for class org.sat4j.minisat.core.Solver
Solver(LearningStrategy<D>, D, SearchParams, IOrder, RestartStrategy, ILogAble) - Constructor for class org.sat4j.minisat.core.Solver
solver - Variable in class org.sat4j.reader.DimacsReader
solver - Variable in class org.sat4j.reader.JSONReader
solver - Variable in class org.sat4j.tools.DimacsArrayReader
SolverDecorator<T extends ISolver> - Class in org.sat4j.tools: The aim of that class is to allow adding dynamic responsibilities to SAT solvers using the Decorator design pattern.
SolverDecorator(T) - Constructor for class org.sat4j.tools.SolverDecorator
SolverFactory - Class in org.sat4j.minisat: User friendly access to pre-constructed solvers.
solverNames() - Method in class org.sat4j.core.ASolverFactory: This methods returns names of solvers to be used with the method getSolverByName().
solvers - Variable in class org.sat4j.tools.ManyCore
SolverStats - Class in org.sat4j.minisat.core: Contains some statistics regarding the search.
SolverStats() - Constructor for class org.sat4j.minisat.core.SolverStats
sort(Comparator<T>) - Method in class org.sat4j.core.ReadOnlyVec
sort() - Method in class org.sat4j.core.ReadOnlyVecInt
sort(Comparator<T>) - Method in class org.sat4j.core.Vec
sort() - Method in class org.sat4j.core.VecInt: sort the vector using a custom quicksort.
sort(Comparator<T>) - Method in interface org.sat4j.specs.IVec
sort() - Method in interface org.sat4j.specs.IVecInt
sortOnActivity() - Method in class org.sat4j.minisat.core.Solver
sortUnique(Comparator<T>) - Method in class org.sat4j.core.ReadOnlyVec
sortUnique() - Method in class org.sat4j.core.ReadOnlyVecInt
sortUnique(Comparator<T>) - Method in class org.sat4j.core.Vec
sortUnique() - Method in class org.sat4j.core.VecInt
sortUnique(Comparator<T>) - Method in interface org.sat4j.specs.IVec
sortUnique() - Method in interface org.sat4j.specs.IVecInt
SpeedTracing - Class in org.sat4j.tools
SpeedTracing(IVisualizationTool, IVisualizationTool, IVisualizationTool) - Constructor for class org.sat4j.tools.SpeedTracing
start() - Method in interface org.sat4j.specs.SearchListener: Start the search.
start() - Method in class org.sat4j.tools.ConflictDepthTracing
start() - Method in class org.sat4j.tools.ConflictLevelTracing
start() - Method in class org.sat4j.tools.DecisionLevelTracing
start() - Method in class org.sat4j.tools.DecisionTracing
start() - Method in class org.sat4j.tools.DotSearchTracing
start() - Method in class org.sat4j.tools.LBDTracing
start() - Method in class org.sat4j.tools.LearnedClausesSizeTracing
start() - Method in class org.sat4j.tools.MultiTracing
start() - Method in class org.sat4j.tools.SearchListenerAdapter
start() - Method in class org.sat4j.tools.SpeedTracing
start() - Method in class org.sat4j.tools.TextOutputTracing
starts - Variable in class org.sat4j.minisat.core.SolverStats
StatisticsSolver - Class in org.sat4j.tools
StatisticsSolver() - Constructor for class org.sat4j.tools.StatisticsSolver
stop() - Method in class org.sat4j.minisat.core.Solver
stop() - Method in interface org.sat4j.specs.ISolverService: Ask the SAT solver to stop the search.
subset(int) - Method in class org.sat4j.core.ReadOnlyVecInt
subset(int) - Method in class org.sat4j.core.VecInt
subset(int) - Method in interface org.sat4j.specs.IVecInt: Compute all subsets of cardinal k of the vector.
SubsetVarOrder - Class in org.sat4j.minisat.orders
SubsetVarOrder(int[]) - Constructor for class org.sat4j.minisat.orders.SubsetVarOrder
suggestNextLiteralToBranchOn(int) - Method in class org.sat4j.minisat.core.Solver
suggestNextLiteralToBranchOn(int) - Method in interface org.sat4j.specs.ISolverService: Suggests to the SAT solver to branch next on the given literal.

T

TabuListDecorator - Class in org.sat4j.minisat.orders: Uses a tabu list to prevent the solver to
TabuListDecorator(VarOrderHeap) - Constructor for class org.sat4j.minisat.orders.TabuListDecorator
TabuListDecorator(VarOrderHeap, int) - Constructor for class org.sat4j.minisat.orders.TabuListDecorator
tail - Variable in class org.sat4j.minisat.constraints.cnf.BinaryClause
tail - Variable in class org.sat4j.minisat.constraints.cnf.HTClause
TextOutputTracing<T> - Class in org.sat4j.tools: Debugging Search Listener allowing to follow the search in a textual way.
TextOutputTracing(Map<Integer, T>) - Constructor for class org.sat4j.tools.TextOutputTracing
TimeoutException - Exception in org.sat4j.specs: Exception launched when the solver cannot solve a problem within its allowed time.
TimeoutException() - Constructor for exception org.sat4j.specs.TimeoutException: Constructor for TimeoutException.
TimeoutException(String) - Constructor for exception org.sat4j.specs.TimeoutException: Constructor for TimeoutException.
TimeoutException(String, Throwable) - Constructor for exception org.sat4j.specs.TimeoutException: Constructor for TimeoutException.
TimeoutException(Throwable) - Constructor for exception org.sat4j.specs.TimeoutException: Constructor for TimeoutException.
toArray() - Method in class org.sat4j.core.ReadOnlyVec
toArray() - Method in class org.sat4j.core.ReadOnlyVecInt
toArray() - Method in class org.sat4j.core.Vec
toArray() - Method in class org.sat4j.core.VecInt
toArray() - Method in interface org.sat4j.specs.IVec: Allow to access the internal representation of the vector as an array.
toArray() - Method in interface org.sat4j.specs.IVecInt: Allow to access the internal representation of the vector as an array.
toConstraint() - Method in class org.sat4j.minisat.constraints.card.AtLeast
toConstraint() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
toConstraint() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
toConstraint() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
toConstraint() - Method in class org.sat4j.minisat.constraints.cnf.HTClause
toConstraint() - Method in class org.sat4j.minisat.constraints.cnf.WLClause
toConstraint() - Method in interface org.sat4j.minisat.core.Propagatable: Allow to access a constraint view of the propagatable to avoid casting.
toDimacs(int) - Static method in class org.sat4j.core.LiteralsUtils: decode the internal representation of a literal in internal representation into Dimacs format.
toInternal(int) - Static method in class org.sat4j.core.LiteralsUtils: encode the classical Dimacs representation (negated integers for negated literals) into the internal format.
toMap() - Method in class org.sat4j.minisat.core.SolverStats
toString() - Method in class org.sat4j.core.ConstrGroup
toString() - Method in class org.sat4j.core.ReadOnlyVec
toString() - Method in class org.sat4j.core.ReadOnlyVecInt
toString() - Method in class org.sat4j.core.Vec
toString() - Method in class org.sat4j.core.VecInt
toString() - Method in class org.sat4j.ExitCode
toString() - Method in class org.sat4j.minisat.constraints.card.AtLeast: Textual representation of the constraint
toString() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard: Cha?
toString() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard: Returns a string representation of the constraint.
toString() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
toString() - Method in class org.sat4j.minisat.constraints.cnf.HTClause
toString(int) - Static method in class org.sat4j.minisat.constraints.cnf.Lits
toString() - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
toString() - Method in class org.sat4j.minisat.constraints.cnf.WLClause
toString() - Method in class org.sat4j.minisat.core.Counter
toString() - Method in class org.sat4j.minisat.core.IntQueue
toString() - Method in class org.sat4j.minisat.core.SearchParams
toString(String) - Method in class org.sat4j.minisat.core.Solver
toString() - Method in class org.sat4j.minisat.core.Solver
toString() - Method in class org.sat4j.minisat.learning.ActiveLearning
toString() - Method in class org.sat4j.minisat.learning.ClauseOnlyLearning
toString() - Method in class org.sat4j.minisat.learning.FixedLengthLearning
toString() - Method in class org.sat4j.minisat.learning.MiniSATLearning
toString() - Method in class org.sat4j.minisat.learning.PercentLengthLearning
toString() - Method in class org.sat4j.minisat.orders.NegativeLiteralSelectionStrategy
toString() - Method in class org.sat4j.minisat.orders.PhaseCachingAutoEraseStrategy
toString() - Method in class org.sat4j.minisat.orders.PhaseInLastLearnedClauseSelectionStrategy
toString() - Method in class org.sat4j.minisat.orders.PositiveLiteralSelectionStrategy
toString() - Method in class org.sat4j.minisat.orders.PureOrder
toString() - Method in class org.sat4j.minisat.orders.RandomLiteralSelectionStrategy
toString() - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
toString() - Method in class org.sat4j.minisat.orders.RSATLastLearnedClausesPhaseSelectionStrategy
toString() - Method in class org.sat4j.minisat.orders.RSATPhaseSelectionStrategy
toString() - Method in class org.sat4j.minisat.orders.TabuListDecorator
toString() - Method in class org.sat4j.minisat.orders.UserFixedPhaseSelectionStrategy
toString() - Method in class org.sat4j.minisat.orders.VarOrderHeap
toString() - Method in class org.sat4j.minisat.restarts.ArminRestarts
toString() - Method in class org.sat4j.minisat.restarts.FixedPeriodRestarts
toString() - Method in class org.sat4j.minisat.restarts.Glucose21Restarts
toString() - Method in class org.sat4j.minisat.restarts.LubyRestarts
toString() - Method in class org.sat4j.minisat.restarts.MiniSATRestarts
toString() - Method in class org.sat4j.minisat.restarts.NoRestarts
toString(String) - Method in interface org.sat4j.specs.ISolver: Display a textual representation of the solver configuration.
toString() - Method in class org.sat4j.specs.Lbool: Textual representation for the truth value.
toString() - Method in class org.sat4j.tools.ClausalCardinalitiesDecorator
toString(String) - Method in class org.sat4j.tools.ClausalCardinalitiesDecorator
toString(String) - Method in class org.sat4j.tools.DimacsOutputSolver
toString(String) - Method in class org.sat4j.tools.DimacsStringSolver
toString() - Method in class org.sat4j.tools.DimacsStringSolver
toString() - Method in enum org.sat4j.tools.encoding.EncodingStrategy
toString() - Method in class org.sat4j.tools.encoding.EncodingStrategyAdapter
toString() - Method in class org.sat4j.tools.encoding.Policy
toString(String) - Method in class org.sat4j.tools.ManyCore
toString(String) - Method in class org.sat4j.tools.OptToSatAdapter
toString(String) - Method in class org.sat4j.tools.SolverDecorator
toString() - Method in class org.sat4j.tools.SolverDecorator
toString(String) - Method in class org.sat4j.tools.StatisticsSolver
toString() - Method in class org.sat4j.tools.xplain.DeletionStrategy
toString(String) - Method in class org.sat4j.tools.xplain.HighLevelXplain
toString() - Method in class org.sat4j.tools.xplain.InsertionStrategy
toString() - Method in class org.sat4j.tools.xplain.QuickXplain2001Strategy
toString() - Method in class org.sat4j.tools.xplain.QuickXplainStrategy
toString(String) - Method in class org.sat4j.tools.xplain.Xplain
trail - Variable in class org.sat4j.minisat.core.Solver: variable assignments (literals) in chronological order.
trailLim - Variable in class org.sat4j.minisat.core.Solver: position of the decision levels on the trail.
TRUE - Static variable in class org.sat4j.specs.Lbool
TRUE - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader
truthValue(int) - Method in class org.sat4j.minisat.core.Solver
truthValue(int) - Method in interface org.sat4j.specs.ISolverService: To access the truth value of a specific literal under current assignment.

U

unassign(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
unassign(int) - Method in interface org.sat4j.minisat.core.ILits: Unassigns a boolean variable (truth value if UNDEF).
UNDEFINED - Static variable in interface org.sat4j.minisat.core.ILits
UNDEFINED - Static variable in class org.sat4j.specs.Lbool
undertimeout - Variable in class org.sat4j.minisat.core.Solver
undo(int) - Method in class org.sat4j.minisat.constraints.card.AtLeast
undo(int) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard: M?
undo(int) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard: Updates information on the constraint in case of a backtrack
undo(int) - Method in interface org.sat4j.minisat.core.IOrder: Method called when a variable is unassigned.
undo(int) - Method in interface org.sat4j.minisat.core.Undoable: Method called when backtracking
undo(int) - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
undo(int) - Method in class org.sat4j.minisat.orders.TabuListDecorator
undo(int) - Method in class org.sat4j.minisat.orders.VarOrderHeap: Methode appelee quand la variable x est desaffectee.
Undoable - Interface in org.sat4j.minisat.core: Interface providing the undoable service.
undoOne() - Method in class org.sat4j.minisat.core.Solver
undos(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
undos(int) - Method in interface org.sat4j.minisat.core.ILits: Retrieve the methods to call when the solver backtracks.
UnitClause - Class in org.sat4j.minisat.constraints.cnf
UnitClause(int) - Constructor for class org.sat4j.minisat.constraints.cnf.UnitClause
UnitClauseProvider - Interface in org.sat4j.specs: Interface for engines able to derive unit clauses for the current problem.
UnitClauses - Class in org.sat4j.minisat.constraints.cnf
UnitClauses(IVecInt) - Constructor for class org.sat4j.minisat.constraints.cnf.UnitClauses
UnitPropagationListener - Interface in org.sat4j.specs: Interface providing the unit propagation capability.
UNKNOWN - Static variable in class org.sat4j.ExitCode
unsafeGet(int) - Method in class org.sat4j.core.ReadOnlyVecInt
unsafeGet(int) - Method in class org.sat4j.core.VecInt
unsafeGet(int) - Method in interface org.sat4j.specs.IVecInt
unsafePush(T) - Method in class org.sat4j.core.ReadOnlyVec
unsafePush(int) - Method in class org.sat4j.core.ReadOnlyVecInt
unsafePush(T) - Method in class org.sat4j.core.Vec
unsafePush(int) - Method in class org.sat4j.core.VecInt
unsafePush(T) - Method in interface org.sat4j.specs.IVec: To push an element in the vector when you know you have space for it.
unsafePush(int) - Method in interface org.sat4j.specs.IVecInt: Push the element in the Vector without verifying if there is room for it.
unsatExplanation() - Method in class org.sat4j.minisat.core.Solver
unsatExplanation() - Method in interface org.sat4j.specs.ISolver: Retrieve an explanation of the inconsistency in terms of assumption literals.
unsatExplanation() - Method in class org.sat4j.tools.AbstractOutputSolver
unsatExplanation() - Method in class org.sat4j.tools.ManyCore
unsatExplanation() - Method in class org.sat4j.tools.SolverDecorator
unsatExplanation() - Method in class org.sat4j.tools.StatisticsSolver
UNSATISFIABLE - Static variable in class org.sat4j.ExitCode
unset(int) - Method in class org.sat4j.minisat.core.Solver
unset(int) - Method in interface org.sat4j.specs.UnitPropagationListener: Unset a unit clause.
updateActivity(int) - Method in class org.sat4j.minisat.orders.VarOrderHeap
updateLBD - Variable in class org.sat4j.minisat.core.SolverStats
updateVar(int) - Method in interface org.sat4j.minisat.core.IOrder: To be called when the activity of a literal changed.
updateVar(int) - Method in interface org.sat4j.minisat.core.IPhaseSelectionStrategy: To be called when the activity of a literal changed.
updateVar(int) - Method in class org.sat4j.minisat.orders.NegativeLiteralSelectionStrategy
updateVar(int) - Method in class org.sat4j.minisat.orders.PhaseCachingAutoEraseStrategy
updateVar(int) - Method in class org.sat4j.minisat.orders.PhaseInLastLearnedClauseSelectionStrategy
updateVar(int) - Method in class org.sat4j.minisat.orders.PositiveLiteralSelectionStrategy
updateVar(int) - Method in class org.sat4j.minisat.orders.RandomLiteralSelectionStrategy
updateVar(int) - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
updateVar(int) - Method in class org.sat4j.minisat.orders.RSATLastLearnedClausesPhaseSelectionStrategy
updateVar(int) - Method in class org.sat4j.minisat.orders.RSATPhaseSelectionStrategy
updateVar(int) - Method in class org.sat4j.minisat.orders.TabuListDecorator
updateVar(int) - Method in class org.sat4j.minisat.orders.UserFixedPhaseSelectionStrategy
updateVar(int) - Method in class org.sat4j.minisat.orders.VarOrderHeap: Appelee lorsque l'activite de la variable x a change.
updateVarAtDecisionLevel(int) - Method in interface org.sat4j.minisat.core.IOrder: Allow to perform a specific action when a literal of the current decision level is updated.
updateVarAtDecisionLevel(int) - Method in interface org.sat4j.minisat.core.IPhaseSelectionStrategy: Allow to perform a specific action when a literal of the current decision level is updated.
updateVarAtDecisionLevel(int) - Method in class org.sat4j.minisat.orders.NegativeLiteralSelectionStrategy
updateVarAtDecisionLevel(int) - Method in class org.sat4j.minisat.orders.PhaseCachingAutoEraseStrategy
updateVarAtDecisionLevel(int) - Method in class org.sat4j.minisat.orders.PhaseInLastLearnedClauseSelectionStrategy
updateVarAtDecisionLevel(int) - Method in class org.sat4j.minisat.orders.PositiveLiteralSelectionStrategy
updateVarAtDecisionLevel(int) - Method in class org.sat4j.minisat.orders.RandomLiteralSelectionStrategy
updateVarAtDecisionLevel(int) - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
updateVarAtDecisionLevel(int) - Method in class org.sat4j.minisat.orders.RSATLastLearnedClausesPhaseSelectionStrategy
updateVarAtDecisionLevel(int) - Method in class org.sat4j.minisat.orders.RSATPhaseSelectionStrategy
updateVarAtDecisionLevel(int) - Method in class org.sat4j.minisat.orders.TabuListDecorator
updateVarAtDecisionLevel(int) - Method in class org.sat4j.minisat.orders.UserFixedPhaseSelectionStrategy
updateVarAtDecisionLevel(int) - Method in class org.sat4j.minisat.orders.VarOrderHeap
updateWriter() - Method in class org.sat4j.tools.FileBasedVisualizationTool
UPPER_BOUND - Static variable in class org.sat4j.ExitCode
usage() - Method in class org.sat4j.AbstractLauncher
usage() - Method in class org.sat4j.BasicLauncher
usage() - Method in class org.sat4j.MUSLauncher
UserFixedPhaseSelectionStrategy - Class in org.sat4j.minisat.orders: Selection strategy where the phase selection is decided at init time and is not updated during the search.
UserFixedPhaseSelectionStrategy() - Constructor for class org.sat4j.minisat.orders.UserFixedPhaseSelectionStrategy

V

value() - Method in class org.sat4j.ExitCode
valueOf(String) - Static method in enum org.sat4j.minisat.core.LearnedConstraintsEvaluationType: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum org.sat4j.minisat.core.SimplificationType: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum org.sat4j.tools.encoding.EncodingStrategy: Returns the enum constant of this type with the specified name.
values() - Static method in enum org.sat4j.minisat.core.LearnedConstraintsEvaluationType: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum org.sat4j.minisat.core.SimplificationType: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum org.sat4j.tools.encoding.EncodingStrategy: Returns an array containing the constants of this enum type, in the order they are declared.
valueToString(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
valueToString(int) - Method in interface org.sat4j.minisat.core.ILits: Returns a textual representation of the truth value of that literal.
var(int) - Static method in class org.sat4j.core.LiteralsUtils: Returns the variable associated to the literal
varActivity(int) - Method in interface org.sat4j.minisat.core.IOrder: To obtain the current activity of a variable.
varActivity(int) - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
varActivity(int) - Method in class org.sat4j.minisat.orders.TabuListDecorator
varActivity(int) - Method in class org.sat4j.minisat.orders.VarOrderHeap
VarActivityListener - Interface in org.sat4j.minisat.core: Interface providing the capability to increase the activity of a given variable.
varBumpActivity(int) - Method in class org.sat4j.minisat.core.Solver
varBumpActivity(int) - Method in interface org.sat4j.minisat.core.VarActivityListener: Update the activity of a variable v.
varDecayActivity() - Method in interface org.sat4j.minisat.core.IOrder: Decay the variables activities.
varDecayActivity() - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
varDecayActivity() - Method in class org.sat4j.minisat.orders.TabuListDecorator
varDecayActivity() - Method in class org.sat4j.minisat.orders.VarOrderHeap
VarOrderHeap - Class in org.sat4j.minisat.orders
VarOrderHeap() - Constructor for class org.sat4j.minisat.orders.VarOrderHeap
VarOrderHeap(IPhaseSelectionStrategy) - Constructor for class org.sat4j.minisat.orders.VarOrderHeap
Vec<T> - Class in org.sat4j.core: Simple but efficient vector implementation, based on the vector implementation available in MiniSAT.
Vec() - Constructor for class org.sat4j.core.Vec: Create a Vector with an initial capacity of 5 elements.
Vec(T[]) - Constructor for class org.sat4j.core.Vec: Adapter method to translate an array of int into an IVec.
Vec(int) - Constructor for class org.sat4j.core.Vec: Create a Vector with a given capacity.
Vec(int, T) - Constructor for class org.sat4j.core.Vec: Construit un vecteur contenant de taille size rempli a l'aide de size pad.
VecInt - Class in org.sat4j.core: A vector specific for primitive integers, widely used in the solver.
VecInt() - Constructor for class org.sat4j.core.VecInt
VecInt(int) - Constructor for class org.sat4j.core.VecInt
VecInt(int[]) - Constructor for class org.sat4j.core.VecInt: Adapter method to translate an array of int into an IVecInt.
VecInt(int, int) - Constructor for class org.sat4j.core.VecInt: Build a vector of a given initial size filled with an integer.
voc - Variable in class org.sat4j.minisat.constraints.card.AtLeast
voc - Variable in class org.sat4j.minisat.constraints.cnf.HTClause
voc - Variable in class org.sat4j.minisat.constraints.cnf.WLClause
voc - Variable in class org.sat4j.minisat.core.Solver
VOID - Static variable in interface org.sat4j.specs.UnitClauseProvider
VOID - Static variable in interface org.sat4j.tools.SolutionFoundListener

W

watch(int, Propagatable) - Method in class org.sat4j.minisat.constraints.cnf.Lits
watch(int, Propagatable) - Method in interface org.sat4j.minisat.core.ILits: Record a new constraint to watch when a literal is satisfied.
watchCumul - Variable in class org.sat4j.minisat.constraints.card.MinWatchCard: contains the sum of the coefficients of the watched literals
watches(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
watches(int) - Method in interface org.sat4j.minisat.core.ILits
WLClause - Class in org.sat4j.minisat.constraints.cnf: Lazy data structure for clause using Watched Literals.
WLClause(IVecInt, ILits) - Constructor for class org.sat4j.minisat.constraints.cnf.WLClause: Creates a new basic clause

X

XNOR - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader
XOR - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader
xor(int, IVecInt) - Method in class org.sat4j.tools.GateTranslator: translate y <=> x1 xor x2 xor ... xor xn into clauses.
xor(int, int, int) - Method in class org.sat4j.tools.GateTranslator
Xplain<T extends ISolver> - Class in org.sat4j.tools.xplain: Explanation framework for SAT4J.
Xplain(T, boolean) - Constructor for class org.sat4j.tools.xplain.Xplain
Xplain(T) - Constructor for class org.sat4j.tools.xplain.Xplain

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