A B C D E F G H I 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
 
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
 
AbstractOptimizationLauncher - Class in org.sat4j
This class is intended to be used by launchers to solve optimization problems, i.e. problems for which a loop is needed to find the optimal solution.
AbstractOptimizationLauncher() - Constructor for class org.sat4j.AbstractOptimizationLauncher
 
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.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
 
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.Binary
 
addAtLeast(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Binomial
 
addAtLeast(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Commander
 
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(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Product
 
addAtLeast(IVecInt, int) - Method in class org.sat4j.tools.ManyCore
 
addAtLeast(IVecInt, int) - Method in class org.sat4j.tools.SolverDecorator
 
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.Binomial
 
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.SolverDecorator
 
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
 
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
 
addClause(IVecInt) - Method in class org.sat4j.minisat.core.Solver
 
addClause(int[]) - Method in class org.sat4j.minisat.core.Solver
 
addClause(IVecInt) - Method in class org.sat4j.opt.MaxSatDecorator
 
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(int[]) - Method in interface org.sat4j.specs.ISolverService
Add a new clause in the SAT solver.
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.ManyCore
 
addClause(IVecInt) - Method in class org.sat4j.tools.SolverDecorator
 
addClause(IVecInt, int) - Method in class org.sat4j.tools.xplain.HighLevelXplain
 
addClause(IVecInt) - Method in class org.sat4j.tools.xplain.Xplain
 
addConstr(Constr) - Method in class org.sat4j.minisat.core.Solver
 
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(IVecInt, int) - Method in class org.sat4j.tools.ManyCore
 
addExactly(IVecInt, int) - Method in class org.sat4j.tools.SolverDecorator
 
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
 
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
 
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.
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 class org.sat4j.AbstractLauncher
 
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.
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
 
assump - Variable in class org.sat4j.tools.xplain.HighLevelXplain
 
assump - Variable in class org.sat4j.tools.xplain.Xplain
 
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(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.
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.
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
 
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
 
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
 
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
 
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.minisat.core.ICDCLLogger
 
Constr - Interface in org.sat4j.minisat.core
Basic constraint abstraction used in Solver.
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.
constrs - Variable in class org.sat4j.tools.xplain.HighLevelXplain
 
constrs - Variable in class org.sat4j.tools.xplain.Xplain
 
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.xplain.HighLevelXplain
 
createNewVar(IVecInt) - Method in class org.sat4j.tools.xplain.Xplain
 
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.
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
 
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
 
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.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.xplain.HighLevelXplain
 
discardLastestVar() - Method in class org.sat4j.tools.xplain.Xplain
 
discardSolutionsForOptimizing() - Method in class org.sat4j.tools.LexicoDecorator
 
displayAnswer() - Method in class org.sat4j.AbstractOptimizationLauncher
 
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
 
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.SearchEnumeratorListener
 
end(Lbool) - Method in class org.sat4j.tools.SearchListenerAdapter
 
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.minisat.core.UnitPropagationListener
satisfies a literal
enqueue(int, Constr) - Method in interface org.sat4j.minisat.core.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.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
 
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
 
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
 
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
 

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.SolverDecorator
 
findModel(IVecInt) - Method in class org.sat4j.tools.SolverDecorator
 
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
 
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
 
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. 
fullAdderCarry(int, int, int, int) - Method in class org.sat4j.tools.GateTranslator
 
fullAdderSum(int, int, int, int) - Method in class org.sat4j.tools.GateTranslator
 

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
 
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.xplain.Xplain
 
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.
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
 
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 class org.sat4j.tools.AbstractOutputSolver
 
getLogPrefix() - Method in class org.sat4j.tools.ManyCore
 
getLogPrefix() - Method in class org.sat4j.tools.SolverDecorator
 
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
 
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
 
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
 
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
 
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
 
getSearchParams() - Method in interface org.sat4j.minisat.core.RestartStrategy
 
getSearchParams() - Method in class org.sat4j.minisat.restarts.ArminRestarts
 
getSearchParams() - Method in class org.sat4j.minisat.restarts.LubyRestarts
 
getSearchParams() - Method in class org.sat4j.minisat.restarts.MiniSATRestarts
 
getSearchParams() - Method in class org.sat4j.minisat.restarts.NoRestarts
 
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
 
getSolvers() - Method in class org.sat4j.tools.ManyCore
 
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
 
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
 
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
 
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.
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
 
GroupedCNFReader - Class in org.sat4j.reader
 
GroupedCNFReader(HighLevelXplain<ISolver>) - 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.
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).
handleLine() - Method in class org.sat4j.reader.DimacsReader
 
handleLine() - Method in class org.sat4j.reader.GroupedCNFReader
 
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.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.
ICDCLLogger - Interface in org.sat4j.minisat.core
 
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
 
ILits - Interface in org.sat4j.minisat.core
That interface manages the solver's internal vocabulary.
IMPLIES - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader
 
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) - 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) - Method in class org.sat4j.minisat.restarts.ArminRestarts
 
init(SearchParams) - Method in class org.sat4j.minisat.restarts.LubyRestarts
 
init(SearchParams) - Method in class org.sat4j.minisat.restarts.MiniSATRestarts
 
init(SearchParams) - 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(ISolverService) - Method in class org.sat4j.tools.MultiTracing
 
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.SpeedTracing
 
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
 
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
 
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(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.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.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.
isSolutionOptimal - Variable in class org.sat4j.opt.AbstractSelectorVariablesDecorator
 
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
 
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
 
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
 

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.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
 
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.minisat.core.ICDCLLogger
 
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
 
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
 
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
 
Minimal4InclusionModel - Class in org.sat4j.tools
Computes models with a minimal subset (with respect to set inclusion) of negative literals.
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
 
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.IProblem
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.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.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.xplain.HighLevelXplain
 
model() - Method in class org.sat4j.tools.xplain.Xplain
 
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.
modelWithInternalVariables() - Method in class org.sat4j.minisat.core.Solver
 
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.ManyCore
 
modelWithInternalVariables() - Method in class org.sat4j.tools.SolverDecorator
 
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 - Class in org.sat4j.tools
Allow to feed the solver with several SearchListener.
MultiTracing(SearchListener...) - Constructor for class org.sat4j.tools.MultiTracing
 
MultiTracing(List<SearchListener>) - 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
 
neg(int) - Static method in class org.sat4j.core.LiteralsUtils
Returns the opposite literal.
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
 
newBestSingleWL() - 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.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
 
newGreedySolver() - Static method in class org.sat4j.minisat.SolverFactory
 
newLearnedClause(Constr, int) - Method in interface org.sat4j.minisat.core.RestartStrategy
 
newLearnedClause(Constr, int) - Method in class org.sat4j.minisat.restarts.ArminRestarts
 
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
 
newMiniLearningPure() - 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
 
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
 
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
 
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.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
 

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.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.LubyRestarts
 
onRestart() - Method in class org.sat4j.minisat.restarts.MiniSATRestarts
 
onRestart() - Method in class org.sat4j.minisat.restarts.NoRestarts
 
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.
OPTIMUM_FOUND - Static variable in class org.sat4j.ExitCode
 
OptToSatAdapter - Class in org.sat4j.tools
 
OptToSatAdapter(IOptimizationProblem) - 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.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
 
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
 
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.
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.opt.AbstractSelectorVariablesDecorator
 
prevboolmodel - Variable in class org.sat4j.tools.LexicoDecorator
 
prevfullmodel - Variable in class org.sat4j.opt.AbstractSelectorVariablesDecorator
 
prevfullmodel - Variable in class org.sat4j.tools.LexicoDecorator
 
prevmodel - Variable in class org.sat4j.opt.AbstractSelectorVariablesDecorator
 
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
 
printInfos(PrintWriter, String) - Method in class org.sat4j.minisat.core.Solver
 
printInfos(PrintWriter, String) - 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, String) - Method in class org.sat4j.tools.ManyCore
 
printInfos(PrintWriter, String) - Method in class org.sat4j.tools.SolverDecorator
 
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, 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
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(PrintStream, String) - Method in class org.sat4j.tools.ManyCore
Deprecated. 
printStat(PrintWriter, String) - 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
 
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
 
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
 
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
 
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
 
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.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 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.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.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
 
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
S?
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
 

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() - 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
 
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
 
setDisplaySolutionLine(boolean) - Method in class org.sat4j.AbstractOptimizationLauncher
 
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
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
 
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.AbstractOptimizationLauncher
 
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
 
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
 
setLearner(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(ICDCLLogger) - Method in interface org.sat4j.minisat.core.ICDCL
 
setLogger(ICDCLLogger) - 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
 
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
 
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
 
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.
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
 
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
 
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
 
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
 
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
 
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
 
setVerbosity(boolean) - Method in class org.sat4j.reader.Reader
 
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.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 class org.sat4j.AbstractLauncher
 
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[]) - Method in interface org.sat4j.specs.SearchListener
a solution is found.
solutionFound(int[]) - Method in class org.sat4j.tools.DotSearchTracing
 
solutionFound(int[]) - Method in class org.sat4j.tools.HeuristicsTracing
 
solutionFound(int[]) - Method in class org.sat4j.tools.LearnedTracing
 
solutionFound(int[]) - Method in class org.sat4j.tools.MultiTracing
 
solutionFound(int[]) - Method in class org.sat4j.tools.SearchEnumeratorListener
 
solutionFound(int[]) - Method in class org.sat4j.tools.SearchListenerAdapter
 
solutionFound(int[]) - Method in class org.sat4j.tools.TextOutputTracing
 
solve(IProblem) - Method in class org.sat4j.AbstractLauncher
 
solve(IProblem) - Method in class org.sat4j.AbstractOptimizationLauncher
 
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, ICDCLLogger) - Constructor for class org.sat4j.minisat.core.Solver
 
solver - Variable in class org.sat4j.reader.DimacsReader
 
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
 
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.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 class org.sat4j.tools.encoding.EncodingStrategyAdapter
 
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() - 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
affectation en ordre chronologique
trailLim - Variable in class org.sat4j.minisat.core.Solver
indice des s?
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
 
UnitClauses - Class in org.sat4j.minisat.constraints.cnf
 
UnitClauses(IVecInt) - Constructor for class org.sat4j.minisat.constraints.cnf.UnitClauses
 
UnitPropagationListener - Interface in org.sat4j.minisat.core
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
 
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.minisat.core.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
 

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

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