- AAGReader - Class in org.sat4j.reader
-
Reader for the ASCII And Inverter Graph format defined by Armin Biere.
- AbstractCardinalityDataStructure - Class in org.sat4j.minisat.constraints
-
- AbstractCardinalityDataStructure() - Constructor for class org.sat4j.minisat.constraints.AbstractCardinalityDataStructure
-
- AbstractClauseSelectorSolver<T extends ISolver> - Class in org.sat4j.tools
-
- AbstractClauseSelectorSolver(T) - Constructor for class org.sat4j.tools.AbstractClauseSelectorSolver
-
- AbstractDataStructureFactory - Class in org.sat4j.minisat.constraints
-
- AbstractDataStructureFactory() - Constructor for class org.sat4j.minisat.constraints.AbstractDataStructureFactory
-
- AbstractLauncher - Class in org.sat4j
-
That class is used by launchers used to solve decision problems, i.e.
- AbstractLauncher() - Constructor for class org.sat4j.AbstractLauncher
-
- AbstractMinimalModel - Class in org.sat4j.tools
-
- AbstractMinimalModel(ISolver) - Constructor for class org.sat4j.tools.AbstractMinimalModel
-
- AbstractMinimalModel(ISolver, IVecInt) - Constructor for class org.sat4j.tools.AbstractMinimalModel
-
- AbstractMinimalModel(ISolver, SolutionFoundListener) - Constructor for class org.sat4j.tools.AbstractMinimalModel
-
- AbstractMinimalModel(ISolver, IVecInt, SolutionFoundListener) - Constructor for class org.sat4j.tools.AbstractMinimalModel
-
- AbstractOptimizationLauncher - Class in org.sat4j
-
Deprecated.
- AbstractOptimizationLauncher() - Constructor for class org.sat4j.AbstractOptimizationLauncher
-
Deprecated.
- AbstractOutputSolver - Class in org.sat4j.tools
-
- AbstractOutputSolver() - Constructor for class org.sat4j.tools.AbstractOutputSolver
-
- AbstractSelectorVariablesDecorator - Class in org.sat4j.opt
-
Abstract class which adds a new "selector" variable for each clause entered
in the solver.
- AbstractSelectorVariablesDecorator(ISolver) - Constructor for class org.sat4j.opt.AbstractSelectorVariablesDecorator
-
- ActiveLearning<D extends DataStructureFactory> - Class in org.sat4j.minisat.learning
-
Learn clauses with a great number of active variables.
- ActiveLearning() - Constructor for class org.sat4j.minisat.learning.ActiveLearning
-
- ActiveLearning(double) - Constructor for class org.sat4j.minisat.learning.ActiveLearning
-
- activity - Variable in class org.sat4j.minisat.constraints.cnf.BinaryClause
-
- activity - Variable in class org.sat4j.minisat.constraints.cnf.HTClause
-
- activity - Variable in class org.sat4j.minisat.constraints.cnf.UnitClause
-
- activity - Variable in class org.sat4j.minisat.constraints.cnf.WLClause
-
- activity - Variable in class org.sat4j.minisat.orders.VarOrderHeap
-
mesure heuristique de l'activite d'une variable.
- ActivityComparator - Class in org.sat4j.minisat.core
-
Utility class to sort the constraints according to their activity.
- ActivityComparator() - Constructor for class org.sat4j.minisat.core.ActivityComparator
-
- add(IConstr) - Method in class org.sat4j.core.ConstrGroup
-
- addAllClauses(IVec<IVecInt>) - Method in class org.sat4j.minisat.core.Solver
-
- addAllClauses(IVec<IVecInt>) - Method in interface org.sat4j.specs.ISolver
-
Create clauses from a set of set of literals.
- addAllClauses(IVec<IVecInt>) - Method in class org.sat4j.tools.AbstractOutputSolver
-
- addAllClauses(IVec<IVecInt>) - Method in class org.sat4j.tools.ManyCore
-
- addAllClauses(IVec<IVecInt>) - Method in class org.sat4j.tools.SolverDecorator
-
- addAllClauses(IVec<IVecInt>) - Method in class org.sat4j.tools.StatisticsSolver
-
- addAtLeast(IVecInt, int) - Method in class org.sat4j.minisat.core.Solver
-
- addAtLeast(IVecInt, int) - Method in interface org.sat4j.specs.ISolver
-
Create a cardinality constraint of the type "at least n of those literals
must be satisfied"
- addAtLeast(IVecInt, int) - Method in class org.sat4j.tools.ClausalCardinalitiesDecorator
-
- addAtLeast(IVecInt, int) - Method in class org.sat4j.tools.DimacsOutputSolver
-
- addAtLeast(IVecInt, int) - Method in class org.sat4j.tools.DimacsStringSolver
-
- addAtLeast(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.EncodingStrategyAdapter
-
- addAtLeast(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Policy
-
- addAtLeast(IVecInt, int) - Method in class org.sat4j.tools.ManyCore
-
- addAtLeast(IVecInt, int) - Method in class org.sat4j.tools.NegationDecorator
-
- addAtLeast(IVecInt, int) - Method in class org.sat4j.tools.SolverDecorator
-
- addAtLeast(IVecInt, int) - Method in class org.sat4j.tools.StatisticsSolver
-
- addAtLeast(IVecInt, int) - Method in class org.sat4j.tools.xplain.HighLevelXplain
-
- addAtLeast(IVecInt, int) - Method in class org.sat4j.tools.xplain.Xplain
-
- addAtLeastOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.EncodingStrategyAdapter
-
- addAtMost(IVecInt, int) - Method in class org.sat4j.minisat.core.Solver
-
- addAtMost(IVecInt, int) - Method in interface org.sat4j.specs.ISolver
-
Create a cardinality constraint of the type "at most n of those literals
must be satisfied"
- addAtMost(IVecInt, int) - Method in class org.sat4j.tools.ClausalCardinalitiesDecorator
-
- addAtMost(IVecInt, int) - Method in class org.sat4j.tools.DimacsOutputSolver
-
- addAtMost(IVecInt, int) - Method in class org.sat4j.tools.DimacsStringSolver
-
- addAtMost(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Binary
-
- addAtMost(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Binomial
-
- addAtMost(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Commander
-
- addAtMost(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.EncodingStrategyAdapter
-
- addAtMost(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Policy
-
- addAtMost(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Product
-
- addAtMost(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Sequential
-
This encoding adds (n-1)*k variables (n is the number of variables in the
at most constraint and k is the degree of the constraint) and 2nk+n-3k-1
clauses.
- addAtMost(IVecInt, int) - Method in class org.sat4j.tools.ManyCore
-
- addAtMost(IVecInt, int) - Method in class org.sat4j.tools.NegationDecorator
-
- addAtMost(IVecInt, int) - Method in class org.sat4j.tools.SolverDecorator
-
- addAtMost(IVecInt, int) - Method in class org.sat4j.tools.StatisticsSolver
-
- addAtMost(IVecInt, int) - Method in class org.sat4j.tools.xplain.HighLevelXplain
-
- addAtMost(IVecInt, int) - Method in class org.sat4j.tools.xplain.Xplain
-
- addAtMostNonOpt(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Product
-
- addAtMostOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Binary
-
p being the smaller integer greater than log_2(n), this encoding adds p
variables and n*p clauses.
- addAtMostOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Binomial
-
- addAtMostOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Commander
-
In this encoding, variables are partitioned in groups.
- addAtMostOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.EncodingStrategyAdapter
-
- addAtMostOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Ladder
-
- addAtMostOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Product
-
- addAtMostOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Sequential
-
- addAtMostOnTheFly(int[], int) - Method in class org.sat4j.minisat.core.Solver
-
- addAtMostOnTheFly(int[], int) - Method in interface org.sat4j.specs.ISolverService
-
Add a new pseudo cardinality constraint sum literals <= degree in the
solver.
- addBlockingClause(IVecInt) - Method in class org.sat4j.minisat.core.Solver
-
- addBlockingClause(IVecInt) - Method in interface org.sat4j.specs.ISolver
-
Add a clause in order to prevent an assignment to occur.
- addBlockingClause(IVecInt) - Method in class org.sat4j.tools.AbstractOutputSolver
-
- addBlockingClause(IVecInt) - Method in class org.sat4j.tools.ManyCore
-
- addBlockingClause(IVecInt) - Method in class org.sat4j.tools.SolverDecorator
-
- addBlockingClause(IVecInt) - Method in class org.sat4j.tools.StatisticsSolver
-
- addClause(IVecInt) - Method in class org.sat4j.minisat.core.Solver
-
- addClause(IVecInt) - Method in class org.sat4j.opt.MaxSatDecorator
-
- addClause(IVecInt, int) - Method in interface org.sat4j.specs.IGroupSolver
-
- addClause(IVecInt) - Method in interface org.sat4j.specs.ISolver
-
Create a clause from a set of literals The literals are represented by
non null integers such that opposite literals a represented by opposite
values.
- addClause(IVecInt) - Method in class org.sat4j.tools.DimacsOutputSolver
-
- addClause(IVecInt) - Method in class org.sat4j.tools.DimacsStringSolver
-
- addClause(IVecInt) - Method in class org.sat4j.tools.FullClauseSelectorSolver
-
- addClause(IVecInt, int) - Method in class org.sat4j.tools.GroupClauseSelectorSolver
-
- addClause(IVecInt) - Method in class org.sat4j.tools.ManyCore
-
- addClause(IVecInt) - Method in class org.sat4j.tools.NegationDecorator
-
- addClause(IVecInt) - Method in class org.sat4j.tools.SolverDecorator
-
- addClause(IVecInt) - Method in class org.sat4j.tools.StatisticsSolver
-
- addClauseOnTheFly(int[]) - Method in class org.sat4j.minisat.core.Solver
-
- addClauseOnTheFly(int[]) - Method in interface org.sat4j.specs.ISolverService
-
Add a new clause in the SAT solver.
- addConstr(Constr) - Method in class org.sat4j.minisat.core.Solver
-
- addControlableClause(IVecInt) - Method in class org.sat4j.tools.FullClauseSelectorSolver
-
- addControlableClause(IVecInt, int) - Method in class org.sat4j.tools.GroupClauseSelectorSolver
-
- addCriterion(IVecInt) - Method in class org.sat4j.tools.LexicoDecorator
-
- addExactly(IVecInt, int) - Method in class org.sat4j.minisat.core.Solver
-
- addExactly(IVecInt, int) - Method in interface org.sat4j.specs.ISolver
-
Create a cardinality constraint of the type
"exactly n of those literals must be satisfied".
- addExactly(IVecInt, int) - Method in class org.sat4j.tools.ClausalCardinalitiesDecorator
-
- addExactly(IVecInt, int) - Method in class org.sat4j.tools.DimacsOutputSolver
-
- addExactly(IVecInt, int) - Method in class org.sat4j.tools.DimacsStringSolver
-
- addExactly(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Binary
-
- addExactly(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Binomial
-
- addExactly(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Commander
-
- addExactly(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.EncodingStrategyAdapter
-
- addExactly(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Policy
-
- addExactly(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Product
-
- addExactly(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Sequential
-
- addExactly(IVecInt, int) - Method in class org.sat4j.tools.ManyCore
-
- addExactly(IVecInt, int) - Method in class org.sat4j.tools.NegationDecorator
-
- addExactly(IVecInt, int) - Method in class org.sat4j.tools.SolverDecorator
-
- addExactly(IVecInt, int) - Method in class org.sat4j.tools.StatisticsSolver
-
- addExactly(IVecInt, int) - Method in class org.sat4j.tools.xplain.Xplain
-
- addExactlyOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Binary
-
- addExactlyOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Binomial
-
- addExactlyOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Commander
-
- addExactlyOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.EncodingStrategyAdapter
-
- addExactlyOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Ladder
-
- addExactlyOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Product
-
- addExactlyOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Sequential
-
- adding(int) - Method in interface org.sat4j.specs.SearchListener
-
adding forced variable (conflict driven assignment)
- adding(int) - Method in class org.sat4j.tools.DotSearchTracing
-
- adding(int) - Method in class org.sat4j.tools.MultiTracing
-
- adding(int) - Method in class org.sat4j.tools.SearchListenerAdapter
-
- adding(int) - Method in class org.sat4j.tools.TextOutputTracing
-
- addInvisiblePoint(double, double) - Method in class org.sat4j.tools.FileBasedVisualizationTool
-
- addInvisiblePoint(double, double) - Method in interface org.sat4j.tools.IVisualizationTool
-
- additionalFullAdderConstraints(int, int, int, int, int) - Method in class org.sat4j.tools.GateTranslator
-
- addNonControlableClause(IVecInt) - Method in class org.sat4j.tools.FullClauseSelectorSolver
-
- addNonControlableClause(IVecInt) - Method in class org.sat4j.tools.GroupClauseSelectorSolver
-
- addOriginalClause(IVecInt) - Method in class org.sat4j.tools.CheckMUSSolutionListener
-
- addPoint(double, double) - Method in class org.sat4j.tools.FileBasedVisualizationTool
-
- addPoint(double, double) - Method in interface org.sat4j.tools.IVisualizationTool
-
- admitABetterSolution() - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
-
- admitABetterSolution(IVecInt) - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
-
- admitABetterSolution(IVecInt) - Method in class org.sat4j.opt.MaxSatDecorator
-
- admitABetterSolution() - Method in class org.sat4j.opt.MinOneDecorator
-
- admitABetterSolution(IVecInt) - Method in class org.sat4j.opt.MinOneDecorator
-
- admitABetterSolution() - Method in interface org.sat4j.specs.IOptimizationProblem
-
Look for a solution of the optimization problem.
- admitABetterSolution(IVecInt) - Method in interface org.sat4j.specs.IOptimizationProblem
-
Look for a solution of the optimization problem when some literals are
satisfied.
- admitABetterSolution() - Method in class org.sat4j.tools.LexicoDecorator
-
- admitABetterSolution(IVecInt) - Method in class org.sat4j.tools.LexicoDecorator
-
- AIGReader - Class in org.sat4j.reader
-
Reader for the Binary And Inverter Graph format defined by Armin Biere.
- AllMUSes - Class in org.sat4j.tools
-
This is a tool for computing all the MUSes (Minimum Unsatisfiable Sets) of a
set of clauses.
- AllMUSes(boolean, ASolverFactory<? extends ISolver>) - Constructor for class org.sat4j.tools.AllMUSes
-
- AllMUSes(ASolverFactory<? extends ISolver>) - Constructor for class org.sat4j.tools.AllMUSes
-
- analyze(Constr, Pair) - Method in class org.sat4j.minisat.core.Solver
-
- analyzeAtRootLevel(Constr) - Method in class org.sat4j.minisat.core.Solver
-
- analyzeFinalConflictInTermsOfAssumptions(Constr, IVecInt, int) - Method in class org.sat4j.minisat.core.Solver
-
Derive a subset of the assumptions causing the inconistency.
- AND - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader
-
- and(int, IVecInt) - Method in class org.sat4j.tools.GateTranslator
-
Translate y <=> x1 /\ x2 /\ ... /\ xn into clauses.
- and(int, int, int) - Method in class org.sat4j.tools.GateTranslator
-
Translate y <=> x1 /\ x2
- ANSWER_PREFIX - Static variable in interface org.sat4j.ILauncherMode
-
- ArminRestarts - Class in org.sat4j.minisat.restarts
-
Rapid restart strategy presented by Armin Biere during it's SAT 07 invited
talk.
- ArminRestarts() - Constructor for class org.sat4j.minisat.restarts.ArminRestarts
-
- ASolverFactory<T extends ISolver> - Class in org.sat4j.core
-
A solver factory is responsible for providing prebuilt solvers to the end
user.
- ASolverFactory() - Constructor for class org.sat4j.core.ASolverFactory
-
- assertConstraint(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.card.AtLeast
-
- assertConstraint(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
-
- assertConstraint(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
-
- assertConstraint(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
-
- assertConstraint(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.HTClause
-
- assertConstraint(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
-
- assertConstraint(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
-
- assertConstraint(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.WLClause
-
- assertConstraint(UnitPropagationListener) - Method in interface org.sat4j.minisat.core.Constr
-
Method called when the constraint is to be asserted.
- assignLiteral(int) - Method in interface org.sat4j.minisat.core.IOrder
-
indicate that a literal has been satisfied.
- assignLiteral(int) - Method in interface org.sat4j.minisat.core.IPhaseSelectionStrategy
-
indicate that a literal has been satisfied.
- assignLiteral(int) - Method in class org.sat4j.minisat.orders.NegativeLiteralSelectionStrategy
-
- assignLiteral(int) - Method in class org.sat4j.minisat.orders.PhaseCachingAutoEraseStrategy
-
- assignLiteral(int) - Method in class org.sat4j.minisat.orders.PhaseInLastLearnedClauseSelectionStrategy
-
- assignLiteral(int) - Method in class org.sat4j.minisat.orders.PositiveLiteralSelectionStrategy
-
- assignLiteral(int) - Method in class org.sat4j.minisat.orders.RandomLiteralSelectionStrategy
-
- assignLiteral(int) - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
-
- assignLiteral(int) - Method in class org.sat4j.minisat.orders.RSATLastLearnedClausesPhaseSelectionStrategy
-
- assignLiteral(int) - Method in class org.sat4j.minisat.orders.RSATPhaseSelectionStrategy
-
- assignLiteral(int) - Method in class org.sat4j.minisat.orders.TabuListDecorator
-
- assignLiteral(int) - Method in class org.sat4j.minisat.orders.UserFixedPhaseSelectionStrategy
-
- assignLiteral(int) - Method in class org.sat4j.minisat.orders.VarOrderHeap
-
- assume(int) - Method in class org.sat4j.minisat.core.Solver
-
- assuming(int) - Method in interface org.sat4j.specs.SearchListener
-
decision variable
- assuming(int) - Method in class org.sat4j.tools.DecisionTracing
-
- assuming(int) - Method in class org.sat4j.tools.DotSearchTracing
-
- assuming(int) - Method in class org.sat4j.tools.MultiTracing
-
- assuming(int) - Method in class org.sat4j.tools.SearchListenerAdapter
-
- assuming(int) - Method in class org.sat4j.tools.TextOutputTracing
-
- AtLeast - Class in org.sat4j.minisat.constraints.card
-
- AtLeast(ILits, IVecInt, int) - Constructor for class org.sat4j.minisat.constraints.card.AtLeast
-
- ATLEAST - Static variable in class org.sat4j.minisat.constraints.card.MinWatchCard
-
- ATLEAST - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader
-
- atLeastNew(UnitPropagationListener, ILits, IVecInt, int) - Static method in class org.sat4j.minisat.constraints.card.AtLeast
-
- ATMOST - Static variable in class org.sat4j.minisat.constraints.card.MinWatchCard
-
- ATMOST - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader
-
- average() - Method in class org.sat4j.minisat.core.CircularBuffer
-
- Backbone - Class in org.sat4j.tools
-
The aim of this class is to compute efficiently the literals implied by the
set of constraints (also called backbone or unit implicates).
- backbone(ISolver) - Static method in class org.sat4j.tools.RemiUtils
-
Compute the set of literals common to all models of the formula.
- backjump(int) - Method in interface org.sat4j.specs.SearchListener
-
The solver is asked to backjump to a given decision level.
- backjump(int) - Method in class org.sat4j.tools.DecisionLevelTracing
-
- backjump(int) - Method in class org.sat4j.tools.MultiTracing
-
- backjump(int) - Method in class org.sat4j.tools.SearchListenerAdapter
-
- backjump(int) - Method in class org.sat4j.tools.TextOutputTracing
-
- backtrack(int[]) - Method in class org.sat4j.minisat.core.Solver
-
- backtrack(int[]) - Method in interface org.sat4j.specs.ISolverService
-
Ask the SAT solver to backtrack.
- backtracking(int) - Method in interface org.sat4j.specs.SearchListener
-
backtrack on a decision variable
- backtracking(int) - Method in class org.sat4j.tools.DotSearchTracing
-
- backtracking(int) - Method in class org.sat4j.tools.MultiTracing
-
- backtracking(int) - Method in class org.sat4j.tools.SearchListenerAdapter
-
- backtracking(int) - Method in class org.sat4j.tools.TextOutputTracing
-
- backtrackLevel - Variable in class org.sat4j.minisat.core.Pair
-
- BasicLauncher<T extends ISolver> - Class in org.sat4j
-
Very simple launcher, to be used during the SAT competition or the SAT race
for instance.
- BasicLauncher(ASolverFactory<T>) - Constructor for class org.sat4j.BasicLauncher
-
- beginLoop() - Method in interface org.sat4j.specs.SearchListener
-
starts a propagation
- beginLoop() - Method in class org.sat4j.tools.DotSearchTracing
-
- beginLoop() - Method in class org.sat4j.tools.MultiTracing
-
- beginLoop() - Method in class org.sat4j.tools.SearchListenerAdapter
-
- beginLoop() - Method in class org.sat4j.tools.TextOutputTracing
-
- beginTime - Variable in class org.sat4j.AbstractLauncher
-
- belongsToPool(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
-
- belongsToPool(int) - Method in interface org.sat4j.minisat.core.ILits
-
Returns true iff the variable is used in the set of constraints.
- Binary - Class in org.sat4j.tools.encoding
-
Binary encoding for the "at most one" and "at most k" cases.
- Binary() - Constructor for class org.sat4j.tools.encoding.Binary
-
- BinaryClause - Class in org.sat4j.minisat.constraints.cnf
-
Data structure for binary clause.
- BinaryClause(IVecInt, ILits) - Constructor for class org.sat4j.minisat.constraints.cnf.BinaryClause
-
Creates a new basic clause
- Binomial - Class in org.sat4j.tools.encoding
-
Binomial encoding for the "at most one" and "at most k" cases.
- Binomial() - Constructor for class org.sat4j.tools.encoding.Binomial
-
- bound() - Method in class org.sat4j.minisat.core.ConflictTimerAdapter
-
- brandNewClause(UnitPropagationListener, ILits, IVecInt) - Static method in class org.sat4j.minisat.constraints.cnf.OriginalBinaryClause
-
Creates a brand new clause, presumably from external data.
- brandNewClause(UnitPropagationListener, ILits, IVecInt) - Static method in class org.sat4j.minisat.constraints.cnf.OriginalHTClause
-
Creates a brand new clause, presumably from external data.
- brandNewClause(UnitPropagationListener, ILits, IVecInt) - Static method in class org.sat4j.minisat.constraints.cnf.OriginalWLClause
-
Creates a brand new clause, presumably from external data.
- calcReason(int, IVecInt) - Method in class org.sat4j.minisat.constraints.card.AtLeast
-
- calcReason(int, IVecInt) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
-
Calcule la cause de l'affection d'un litt?
- calcReason(int, IVecInt) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
-
computes the reason for a literal
- calcReason(int, IVecInt) - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
-
- calcReason(int, IVecInt) - Method in class org.sat4j.minisat.constraints.cnf.HTClause
-
- calcReason(int, IVecInt) - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
-
- calcReason(int, IVecInt) - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
-
- calcReason(int, IVecInt) - Method in class org.sat4j.minisat.constraints.cnf.WLClause
-
- calcReason(int, IVecInt) - Method in interface org.sat4j.minisat.core.Constr
-
Compute the reason for a given assignment.
- calcReasonOnTheFly(int, IVecInt, IVecInt) - Method in class org.sat4j.minisat.constraints.card.AtLeast
-
- calcReasonOnTheFly(int, IVecInt, IVecInt) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
-
- calcReasonOnTheFly(int, IVecInt, IVecInt) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
-
- calcReasonOnTheFly(int, IVecInt, IVecInt) - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
-
- calcReasonOnTheFly(int, IVecInt, IVecInt) - Method in class org.sat4j.minisat.constraints.cnf.HTClause
-
- calcReasonOnTheFly(int, IVecInt, IVecInt) - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
-
- calcReasonOnTheFly(int, IVecInt, IVecInt) - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
-
- calcReasonOnTheFly(int, IVecInt, IVecInt) - Method in class org.sat4j.minisat.constraints.cnf.WLClause
-
- calcReasonOnTheFly(int, IVecInt, IVecInt) - Method in interface org.sat4j.minisat.core.Constr
-
Compute the reason for a given assignment in a the constraint created on
the fly in the solver.
- calculateObjective() - Method in class org.sat4j.opt.MaxSatDecorator
-
- calculateObjective() - Method in class org.sat4j.opt.MinOneDecorator
-
- calculateObjective() - Method in interface org.sat4j.specs.IOptimizationProblem
-
Deprecated.
- calculateObjective() - Method in class org.sat4j.tools.LexicoDecorator
-
- canBePropagatedMultipleTimes() - Method in class org.sat4j.core.ConstrGroup
-
- canBePropagatedMultipleTimes() - Method in class org.sat4j.minisat.constraints.card.AtLeast
-
- canBePropagatedMultipleTimes() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
-
- canBePropagatedMultipleTimes() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
-
- canBePropagatedMultipleTimes() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
-
- canBePropagatedMultipleTimes() - Method in class org.sat4j.minisat.constraints.cnf.HTClause
-
- canBePropagatedMultipleTimes() - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
-
- canBePropagatedMultipleTimes() - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
-
- canBePropagatedMultipleTimes() - Method in class org.sat4j.minisat.constraints.cnf.WLClause
-
- canBePropagatedMultipleTimes() - Method in interface org.sat4j.specs.IConstr
-
Partition constraints into the ones that can only be found once on the
trail (e.g. clauses) and the ones that can be found several times (e.g.
- cancelExplanation() - Method in class org.sat4j.tools.xplain.HighLevelXplain
-
- cancelExplanation() - Method in class org.sat4j.tools.xplain.Xplain
-
- cancelExplanationComputation() - Method in class org.sat4j.tools.xplain.DeletionStrategy
-
- cancelExplanationComputation() - Method in class org.sat4j.tools.xplain.InsertionStrategy
-
- cancelExplanationComputation() - Method in interface org.sat4j.tools.xplain.MinimizationStrategy
-
- cancelExplanationComputation() - Method in class org.sat4j.tools.xplain.QuickXplain2001Strategy
-
- cancelExplanationComputation() - Method in class org.sat4j.tools.xplain.QuickXplainStrategy
-
- cancelUntil(int) - Method in class org.sat4j.minisat.core.Solver
-
Cancel several levels of assumptions
- capacity() - Method in class org.sat4j.minisat.constraints.cnf.Lits
-
To get the capacity of the current vocabulary.
- CARD - Static variable in class org.sat4j.reader.JSONReader
-
- CardinalityDataStructure - Class in org.sat4j.minisat.constraints
-
- CardinalityDataStructure() - Constructor for class org.sat4j.minisat.constraints.CardinalityDataStructure
-
- CardinalityDataStructureYanMax - Class in org.sat4j.minisat.constraints
-
- CardinalityDataStructureYanMax() - Constructor for class org.sat4j.minisat.constraints.CardinalityDataStructureYanMax
-
- CardinalityDataStructureYanMin - Class in org.sat4j.minisat.constraints
-
- CardinalityDataStructureYanMin() - Constructor for class org.sat4j.minisat.constraints.CardinalityDataStructureYanMin
-
- changedreason - Variable in class org.sat4j.minisat.core.SolverStats
-
- CheckMUSSolutionListener - Class in org.sat4j.tools
-
- CheckMUSSolutionListener(ASolverFactory<? extends ISolver>) - Constructor for class org.sat4j.tools.CheckMUSSolutionListener
-
- checkThatItIsAMUS(IVecInt) - Method in class org.sat4j.tools.CheckMUSSolutionListener
-
- CircularBuffer - Class in org.sat4j.minisat.core
-
Create a circular buffer of a given capacity allowing to compute efficiently
the mean of the values storied.
- CircularBuffer(int) - Constructor for class org.sat4j.minisat.core.CircularBuffer
-
- claBumpActivity(Constr) - Method in class org.sat4j.minisat.core.Solver
-
Propagate activity to a constraint
- ClausalCardinalitiesDecorator<T extends ISolver> - Class in org.sat4j.tools
-
A decorator for clausal cardinalities constraints.
- ClausalCardinalitiesDecorator(T) - Constructor for class org.sat4j.tools.ClausalCardinalitiesDecorator
-
- ClausalCardinalitiesDecorator(T, EncodingStrategyAdapter) - Constructor for class org.sat4j.tools.ClausalCardinalitiesDecorator
-
- ClausalDataStructureWL - Class in org.sat4j.minisat.constraints
-
- ClausalDataStructureWL() - Constructor for class org.sat4j.minisat.constraints.ClausalDataStructureWL
-
- CLAUSE - Static variable in class org.sat4j.reader.JSONReader
-
- ClauseOnlyLearning<D extends DataStructureFactory> - Class in org.sat4j.minisat.learning
-
The solver only records among all the constraints only the clauses.
- ClauseOnlyLearning() - Constructor for class org.sat4j.minisat.learning.ClauseOnlyLearning
-
- Clauses - Class in org.sat4j.minisat.constraints.cnf
-
- Clauses() - Constructor for class org.sat4j.minisat.constraints.cnf.Clauses
-
- cleaning() - Method in interface org.sat4j.specs.SearchListener
-
The solver is going to delete some learned clauses.
- cleaning() - Method in class org.sat4j.tools.ConflictDepthTracing
-
- cleaning() - Method in class org.sat4j.tools.ConflictLevelTracing
-
- cleaning() - Method in class org.sat4j.tools.DecisionTracing
-
- cleaning() - Method in class org.sat4j.tools.LearnedClausesSizeTracing
-
- cleaning() - Method in class org.sat4j.tools.LearnedTracing
-
- cleaning() - Method in class org.sat4j.tools.MultiTracing
-
- cleaning() - Method in class org.sat4j.tools.SearchListenerAdapter
-
- cleaning() - Method in class org.sat4j.tools.SpeedTracing
-
- cleaning() - Method in class org.sat4j.tools.TextOutputTracing
-
- clear() - Method in class org.sat4j.core.ConstrGroup
-
- clear() - Method in class org.sat4j.core.ReadOnlyVec
-
- clear() - Method in class org.sat4j.core.ReadOnlyVecInt
-
- clear() - Method in class org.sat4j.core.Vec
-
- clear() - Method in class org.sat4j.core.VecInt
-
- clear() - Method in class org.sat4j.minisat.core.CircularBuffer
-
- clear() - Method in class org.sat4j.minisat.core.IntQueue
-
Vide la queue
- clear() - Method in interface org.sat4j.specs.IVec
-
- clear() - Method in interface org.sat4j.specs.IVecInt
-
- clearDecorated() - Method in class org.sat4j.tools.SolverDecorator
-
Method to be called to clear the decorator from its decorated solver.
- clearLearntClauses() - Method in class org.sat4j.minisat.core.Solver
-
- clearLearntClauses() - Method in interface org.sat4j.specs.ISolver
-
Remove clauses learned during the solving process.
- clearLearntClauses() - Method in class org.sat4j.tools.AbstractOutputSolver
-
- clearLearntClauses() - Method in class org.sat4j.tools.ManyCore
-
- clearLearntClauses() - Method in class org.sat4j.tools.SolverDecorator
-
- clearLearntClauses() - Method in class org.sat4j.tools.StatisticsSolver
-
- close() - Method in class org.sat4j.reader.EfficientScanner
-
- Commander - Class in org.sat4j.tools.encoding
-
Commander encoding for "at most one" and "at most k" cases.
- Commander() - Constructor for class org.sat4j.tools.encoding.Commander
-
- COMMENT_PREFIX - Static variable in class org.sat4j.AbstractLauncher
-
- compare(A, A) - Method in class org.sat4j.core.DefaultComparator
-
- compare(Constr, Constr) - Method in class org.sat4j.minisat.core.ActivityComparator
-
- compute(ISolver) - Static method in class org.sat4j.tools.Backbone
-
Computes the backbone of a formula following the algorithm described in
João Marques-Silva, Mikolás Janota, Inês Lynce: On Computing Backbones of
Propositional Theories.
- compute(ISolver, IVecInt) - Static method in class org.sat4j.tools.Backbone
-
Computes the backbone of a formula following the algorithm described in
João Marques-Silva, Mikolás Janota, Inês Lynce: On Computing Backbones of
Propositional Theories.
- compute(ISolver, int[]) - Static method in class org.sat4j.tools.Backbone
-
- compute(ISolver, int[], IVecInt) - Static method in class org.sat4j.tools.Backbone
-
- computeAllMSS() - Method in class org.sat4j.tools.AllMUSes
-
- computeAllMSS(SolutionFoundListener) - Method in class org.sat4j.tools.AllMUSes
-
- computeAllMSSOrdered(SolutionFoundListener) - Method in class org.sat4j.tools.AllMUSes
-
- computeAllMUSes() - Method in class org.sat4j.tools.AllMUSes
-
- computeAllMUSes(SolutionFoundListener) - Method in class org.sat4j.tools.AllMUSes
-
Computes all the MUSes associated to the set of constraints added to the
solver
- computeAllMUSesOrdered(SolutionFoundListener) - Method in class org.sat4j.tools.AllMUSes
-
- computePropagation(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
-
- computeWatches() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
-
- configureSolver(String[]) - Method in class org.sat4j.AbstractLauncher
-
- configureSolver(String[]) - Method in class org.sat4j.BasicLauncher
-
- configureSolver(String[]) - Method in class org.sat4j.MUSLauncher
-
- ConflictDepthTracing - Class in org.sat4j.tools
-
- ConflictDepthTracing(IVisualizationTool, IVisualizationTool, IVisualizationTool) - Constructor for class org.sat4j.tools.ConflictDepthTracing
-
- conflictDetectedInWatchesFor(int, int) - Method in class org.sat4j.minisat.constraints.AbstractDataStructureFactory
-
- conflictDetectedInWatchesFor(int, int) - Method in interface org.sat4j.minisat.core.DataStructureFactory
-
- conflictFound(IConstr, int, int) - Method in interface org.sat4j.specs.SearchListener
-
a conflict has been found.
- conflictFound(int) - Method in interface org.sat4j.specs.SearchListener
-
a conflict has been found while propagating values.
- conflictFound(IConstr, int, int) - Method in class org.sat4j.tools.ConflictDepthTracing
-
- conflictFound(IConstr, int, int) - Method in class org.sat4j.tools.ConflictLevelTracing
-
- conflictFound(IConstr, int, int) - Method in class org.sat4j.tools.DecisionLevelTracing
-
- conflictFound(IConstr, int, int) - Method in class org.sat4j.tools.DotSearchTracing
-
- conflictFound(int) - Method in class org.sat4j.tools.DotSearchTracing
-
- conflictFound(IConstr, int, int) - Method in class org.sat4j.tools.LBDTracing
-
- conflictFound(IConstr, int, int) - Method in class org.sat4j.tools.LearnedClauseSizeTracing
-
- conflictFound(IConstr, int, int) - Method in class org.sat4j.tools.MultiTracing
-
- conflictFound(int) - Method in class org.sat4j.tools.MultiTracing
-
- conflictFound(IConstr, int, int) - Method in class org.sat4j.tools.SearchListenerAdapter
-
- conflictFound(int) - Method in class org.sat4j.tools.SearchListenerAdapter
-
- conflictFound(IConstr, int, int) - Method in class org.sat4j.tools.TextOutputTracing
-
- conflictFound(int) - Method in class org.sat4j.tools.TextOutputTracing
-
- ConflictLevelTracing - Class in org.sat4j.tools
-
- ConflictLevelTracing(IVisualizationTool, IVisualizationTool, IVisualizationTool) - Constructor for class org.sat4j.tools.ConflictLevelTracing
-
- conflicts - Variable in class org.sat4j.minisat.core.SolverStats
-
- ConflictTimer - Interface in org.sat4j.minisat.core
-
Conflict based timer.
- ConflictTimerAdapter - Class in org.sat4j.minisat.core
-
Perform a task when a given number of conflicts is reached.
- ConflictTimerAdapter(int) - Constructor for class org.sat4j.minisat.core.ConflictTimerAdapter
-
- ConflictTimerContainer - Class in org.sat4j.minisat.core
-
Agregator for conflict timers (composite design pattern).
- ConflictTimerContainer() - Constructor for class org.sat4j.minisat.core.ConflictTimerContainer
-
- CONSOLE - Static variable in interface org.sat4j.specs.ILogAble
-
- Constr - Interface in org.sat4j.minisat.core
-
Basic constraint abstraction used in Solver.
- constraint - Variable in class org.sat4j.reader.JSONReader
-
- constraintRegexp() - Method in class org.sat4j.reader.JSONReader
-
- ConstrGroup - Class in org.sat4j.core
-
A utility class used to manage easily group of clauses to be deleted at some
point in the solver.
- ConstrGroup() - Constructor for class org.sat4j.core.ConstrGroup
-
Create a ConstrGroup that cannot contain null constrs.
- ConstrGroup(boolean) - Constructor for class org.sat4j.core.ConstrGroup
-
Create a new constrGroup.
- constrs - Variable in class org.sat4j.minisat.core.Solver
-
Set of original constraints.
- contains(T) - Method in class org.sat4j.core.ReadOnlyVec
-
- contains(int) - Method in class org.sat4j.core.ReadOnlyVecInt
-
- contains(T) - Method in class org.sat4j.core.Vec
-
- contains(int) - Method in class org.sat4j.core.VecInt
-
- contains(T) - Method in interface org.sat4j.specs.IVec
-
- contains(int) - Method in interface org.sat4j.specs.IVecInt
-
- containsAt(int) - Method in class org.sat4j.core.ReadOnlyVecInt
-
- containsAt(int, int) - Method in class org.sat4j.core.ReadOnlyVecInt
-
- containsAt(int) - Method in class org.sat4j.core.VecInt
-
- containsAt(int, int) - Method in class org.sat4j.core.VecInt
-
- containsAt(int) - Method in interface org.sat4j.specs.IVecInt
-
returns the index of the first occurrence of e, else -1.
- containsAt(int, int) - Method in interface org.sat4j.specs.IVecInt
-
returns the index of the first occurence of e occurring after from
(excluded), else -1.
- ContradictionException - Exception in org.sat4j.specs
-
That exception is launched whenever a trivial contradiction is found (e.g.
- ContradictionException() - Constructor for exception org.sat4j.specs.ContradictionException
-
- ContradictionException(String) - Constructor for exception org.sat4j.specs.ContradictionException
-
- ContradictionException(Throwable) - Constructor for exception org.sat4j.specs.ContradictionException
-
- ContradictionException(String, Throwable) - Constructor for exception org.sat4j.specs.ContradictionException
-
- copyTo(IVec<T>) - Method in class org.sat4j.core.ReadOnlyVec
-
- copyTo(E[]) - Method in class org.sat4j.core.ReadOnlyVec
-
- copyTo(IVecInt) - Method in class org.sat4j.core.ReadOnlyVecInt
-
- copyTo(int[]) - Method in class org.sat4j.core.ReadOnlyVecInt
-
- copyTo(IVec<T>) - Method in class org.sat4j.core.Vec
-
Ces operations devraient se faire en temps constant.
- copyTo(E[]) - Method in class org.sat4j.core.Vec
-
- copyTo(IVecInt) - Method in class org.sat4j.core.VecInt
-
Copy the content of this vector into another one.
- copyTo(int[]) - Method in class org.sat4j.core.VecInt
-
Copy the content of this vector into an array of integer.
- copyTo(IVec<T>) - Method in interface org.sat4j.specs.IVec
-
Ces operations devraient se faire en temps constant.
- copyTo(E[]) - Method in interface org.sat4j.specs.IVec
-
- copyTo(IVecInt) - Method in interface org.sat4j.specs.IVecInt
-
C'est operations devraient se faire en temps constant.
- copyTo(int[]) - Method in interface org.sat4j.specs.IVecInt
-
- COUNT - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader
-
- Counter - Class in org.sat4j.minisat.core
-
- Counter() - Constructor for class org.sat4j.minisat.core.Counter
-
- Counter(int) - Constructor for class org.sat4j.minisat.core.Counter
-
- countSolutions() - Method in class org.sat4j.tools.SolutionCounter
-
Naive approach to count the solutions available in a boolean formula:
each time a solution is found, a new clause is added to prevent it to be
found again.
- createCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.AbstractDataStructureFactory
-
- createCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructure
-
- createCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructureYanMax
-
- createCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructureYanMin
-
- createCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.MixedDataStructureDanielHT
-
- createCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.MixedDataStructureDanielWL
-
- createCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.MixedDataStructureSingleWL
-
- createCardinalityConstraint(IVecInt, int) - Method in interface org.sat4j.minisat.core.DataStructureFactory
-
Create a cardinality constraint of the form sum li >= degree.
- createClause(IVecInt) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructure
-
- createClause(IVecInt) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructureYanMax
-
- createClause(IVecInt) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructureYanMin
-
- createClause(IVecInt) - Method in class org.sat4j.minisat.constraints.ClausalDataStructureWL
-
- createClause(IVecInt) - Method in class org.sat4j.minisat.constraints.MixedDataStructureDanielHT
-
- createClause(IVecInt) - Method in class org.sat4j.minisat.constraints.MixedDataStructureDanielWL
-
- createClause(IVecInt) - Method in class org.sat4j.minisat.constraints.MixedDataStructureSingleWL
-
- createClause(IVecInt) - Method in interface org.sat4j.minisat.core.DataStructureFactory
-
- createLits() - Method in class org.sat4j.minisat.constraints.AbstractCardinalityDataStructure
-
- createLits() - Method in class org.sat4j.minisat.constraints.AbstractDataStructureFactory
-
- createLits() - Method in class org.sat4j.minisat.constraints.ClausalDataStructureWL
-
- createLits() - Method in class org.sat4j.minisat.constraints.MixedDataStructureDanielHT
-
- createLits() - Method in class org.sat4j.minisat.constraints.MixedDataStructureDanielWL
-
- createLits() - Method in class org.sat4j.minisat.constraints.MixedDataStructureSingleWL
-
- createNewVar(IVecInt) - Method in class org.sat4j.tools.AbstractClauseSelectorSolver
-
- createReader(ISolver, String) - Method in class org.sat4j.AbstractLauncher
-
- createReader(ISolver, String) - Method in class org.sat4j.BasicLauncher
-
- createReader(ISolver, String) - Method in class org.sat4j.MUSLauncher
-
- createSolverByName(String) - Method in class org.sat4j.core.ASolverFactory
-
create a solver from its String name. the solvername Xxxx must map one of
the newXxxx methods.
- createUnregisteredCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.AbstractDataStructureFactory
-
- createUnregisteredCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructure
-
- createUnregisteredCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructureYanMax
-
- createUnregisteredCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructureYanMin
-
- createUnregisteredCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.MixedDataStructureDanielHT
-
- createUnregisteredCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.MixedDataStructureDanielWL
-
- createUnregisteredCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.MixedDataStructureSingleWL
-
- createUnregisteredCardinalityConstraint(IVecInt, int) - Method in interface org.sat4j.minisat.core.DataStructureFactory
-
- createUnregisteredClause(IVecInt) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructure
-
- createUnregisteredClause(IVecInt) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructureYanMax
-
- createUnregisteredClause(IVecInt) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructureYanMin
-
- createUnregisteredClause(IVecInt) - Method in class org.sat4j.minisat.constraints.ClausalDataStructureWL
-
- createUnregisteredClause(IVecInt) - Method in class org.sat4j.minisat.constraints.MixedDataStructureDanielHT
-
- createUnregisteredClause(IVecInt) - Method in class org.sat4j.minisat.constraints.MixedDataStructureDanielWL
-
- createUnregisteredClause(IVecInt) - Method in class org.sat4j.minisat.constraints.MixedDataStructureSingleWL
-
- createUnregisteredClause(IVecInt) - Method in interface org.sat4j.minisat.core.DataStructureFactory
-
- criteria - Variable in class org.sat4j.tools.LexicoDecorator
-
- CURRENT_OPTIMUM_VALUE_PREFIX - Static variable in interface org.sat4j.ILauncherMode
-
- currentChar() - Method in class org.sat4j.reader.EfficientScanner
-
- currentCriterion - Variable in class org.sat4j.tools.LexicoDecorator
-
- currentDecisionLevel() - Method in class org.sat4j.minisat.core.Solver
-
- currentDecisionLevel() - Method in interface org.sat4j.specs.ISolverService
-
To access the current decision level
- DataStructureFactory - Interface in org.sat4j.minisat.core
-
The aim of the factory is to provide a concrete implementation of clauses,
cardinality constraints and pseudo boolean consraints.
- dec() - Method in class org.sat4j.minisat.core.Counter
-
- decayActivities() - Method in class org.sat4j.minisat.core.Solver
-
- DECISION - Static variable in interface org.sat4j.ILauncherMode
-
The launcher is in decision mode: the answer is either SAT, UNSAT or
UNKNOWN
- decisionLevel() - Method in class org.sat4j.minisat.core.Solver
-
- DecisionLevelTracing - Class in org.sat4j.tools
-
- DecisionLevelTracing(IVisualizationTool) - Constructor for class org.sat4j.tools.DecisionLevelTracing
-
- decisions - Variable in class org.sat4j.minisat.core.SolverStats
-
- DecisionTracing - Class in org.sat4j.tools
-
- DecisionTracing(IVisualizationTool, IVisualizationTool, IVisualizationTool, IVisualizationTool) - Constructor for class org.sat4j.tools.DecisionTracing
-
- decode(int[]) - Method in class org.sat4j.reader.AAGReader
-
- decode(int[], PrintWriter) - Method in class org.sat4j.reader.AAGReader
-
- decode(int[]) - Method in class org.sat4j.reader.AIGReader
-
- decode(int[], PrintWriter) - Method in class org.sat4j.reader.AIGReader
-
- decode(int[]) - Method in class org.sat4j.reader.DimacsReader
-
- decode(int[], PrintWriter) - Method in class org.sat4j.reader.DimacsReader
-
- decode(int[]) - Method in class org.sat4j.reader.InstanceReader
-
Deprecated.
- decode(int[], PrintWriter) - Method in class org.sat4j.reader.InstanceReader
-
- decode(int[]) - Method in class org.sat4j.reader.JSONReader
-
Deprecated.
- decode(int[], PrintWriter) - Method in class org.sat4j.reader.JSONReader
-
- decode(int[]) - Method in class org.sat4j.reader.LecteurDimacs
-
- decode(int[], PrintWriter) - Method in class org.sat4j.reader.LecteurDimacs
-
- decode(int[]) - Method in class org.sat4j.reader.Reader
-
Deprecated.
- decode(int[], PrintWriter) - Method in class org.sat4j.reader.Reader
-
Produce a model using the reader format on a provided printwriter.
- decode(int[]) - Method in class org.sat4j.tools.DimacsArrayReader
-
- decorated() - Method in class org.sat4j.tools.SolverDecorator
-
- DEFAULT_LUBY_FACTOR - Static variable in class org.sat4j.minisat.restarts.LubyRestarts
-
- DefaultComparator<A extends Comparable<A>> - Class in org.sat4j.core
-
A simple comparator for comparable objects.
- DefaultComparator() - Constructor for class org.sat4j.core.DefaultComparator
-
- defaultSolver() - Method in class org.sat4j.core.ASolverFactory
-
To obtain the default solver of the library.
- defaultSolver() - Method in class org.sat4j.LightFactory
-
- defaultSolver() - Method in class org.sat4j.minisat.SolverFactory
-
- degree - Variable in class org.sat4j.minisat.constraints.card.MinWatchCard
-
degree of the cardinality constraint
- delete(int) - Method in class org.sat4j.core.ReadOnlyVec
-
- delete(int) - Method in class org.sat4j.core.ReadOnlyVecInt
-
- delete(int) - Method in class org.sat4j.core.Vec
-
Delete the ith element of the vector.
- delete(int) - Method in class org.sat4j.core.VecInt
-
Delete the ith element of the vector.
- delete(int) - Method in interface org.sat4j.specs.IVec
-
Delete the ith element of the vector.
- delete(int) - Method in interface org.sat4j.specs.IVecInt
-
Delete the ith element of the vector.
- delete(int[]) - Method in interface org.sat4j.specs.SearchListener
-
delete a clause
- delete(int[]) - Method in class org.sat4j.tools.DotSearchTracing
-
- delete(int[]) - Method in class org.sat4j.tools.MultiTracing
-
- delete(int[]) - Method in class org.sat4j.tools.SearchListenerAdapter
-
- delete(int[]) - Method in class org.sat4j.tools.TextOutputTracing
-
- DeletionStrategy - Class in org.sat4j.tools.xplain
-
An implementation of the deletion based minimization.
- DeletionStrategy() - Constructor for class org.sat4j.tools.xplain.DeletionStrategy
-
- dequeue() - Method in class org.sat4j.minisat.core.IntQueue
-
returns the nexdt element in the queue.
- dimacs2internal(IVecInt) - Method in class org.sat4j.minisat.core.Solver
-
- DimacsArrayReader - Class in org.sat4j.tools
-
Very simple Dimacs array reader.
- DimacsArrayReader(ISolver) - Constructor for class org.sat4j.tools.DimacsArrayReader
-
- DimacsOutputSolver - Class in org.sat4j.tools
-
Solver used to display in a writer the CNF instance in Dimacs format.
- DimacsOutputSolver() - Constructor for class org.sat4j.tools.DimacsOutputSolver
-
- DimacsOutputSolver(PrintWriter) - Constructor for class org.sat4j.tools.DimacsOutputSolver
-
- DimacsReader - Class in org.sat4j.reader
-
Very simple Dimacs file parser.
- DimacsReader(ISolver) - Constructor for class org.sat4j.reader.DimacsReader
-
- DimacsReader(ISolver, String) - Constructor for class org.sat4j.reader.DimacsReader
-
- DimacsStringSolver - Class in org.sat4j.tools
-
Solver used to write down a CNF into a String.
- DimacsStringSolver() - Constructor for class org.sat4j.tools.DimacsStringSolver
-
- DimacsStringSolver(int) - Constructor for class org.sat4j.tools.DimacsStringSolver
-
- disableNumberOfConstraintCheck() - Method in class org.sat4j.reader.DimacsReader
-
- discard() - Method in class org.sat4j.opt.MaxSatDecorator
-
- discard() - Method in class org.sat4j.opt.MinOneDecorator
-
- discard() - Method in interface org.sat4j.specs.IOptimizationProblem
-
Deprecated.
- discard() - Method in class org.sat4j.tools.LexicoDecorator
-
- discardCurrentSolution() - Method in class org.sat4j.opt.MaxSatDecorator
-
- discardCurrentSolution() - Method in class org.sat4j.opt.MinOneDecorator
-
- discardCurrentSolution() - Method in interface org.sat4j.specs.IOptimizationProblem
-
Discard the current solution in the optimization problem.
- discardCurrentSolution() - Method in class org.sat4j.tools.LexicoDecorator
-
- discardLastestVar() - Method in class org.sat4j.tools.AbstractClauseSelectorSolver
-
- discardSolutionsForOptimizing() - Method in class org.sat4j.tools.LexicoDecorator
-
- displayAnswer() - Method in class org.sat4j.AbstractOptimizationLauncher
-
Deprecated.
- displayHeader() - Method in class org.sat4j.AbstractLauncher
-
- displayLicense() - Method in class org.sat4j.AbstractLauncher
-
- displayResult() - Method in class org.sat4j.AbstractLauncher
-
- displayResult() - Method in class org.sat4j.AbstractOptimizationLauncher
-
Deprecated.
- displayResult(ISolver, IProblem, ILogAble, PrintWriter, Reader, long, boolean) - Method in interface org.sat4j.ILauncherMode
-
Output of the launcher when the solver stops
- displayResult() - Method in class org.sat4j.MUSLauncher
-
- DotSearchTracing<T> - Class in org.sat4j.tools
-
Class allowing to express the search as a tree in the dot language.
- DotSearchTracing(String, Map<Integer, T>) - Constructor for class org.sat4j.tools.DotSearchTracing
-
- dsfactory - Variable in class org.sat4j.minisat.core.Solver
-
- gateFalse(int) - Method in class org.sat4j.tools.GateTranslator
-
translate y <=> FALSE into a clause.
- GateTranslator - Class in org.sat4j.tools
-
Utility class to easily feed a SAT solver using logical gates.
- GateTranslator(ISolver) - Constructor for class org.sat4j.tools.GateTranslator
-
- gateTrue(int) - Method in class org.sat4j.tools.GateTranslator
-
translate y <=> TRUE into a clause.
- get(int) - Method in class org.sat4j.core.ConstrGroup
-
- get(int) - Method in class org.sat4j.core.ReadOnlyVec
-
- get(int) - Method in class org.sat4j.core.ReadOnlyVecInt
-
- get(int) - Method in class org.sat4j.core.Vec
-
- get(int) - Method in class org.sat4j.core.VecInt
-
- get(int) - Method in class org.sat4j.minisat.constraints.card.AtLeast
-
- get(int) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
-
- get(int) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
-
- get(int) - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
-
Retourne le ieme literal de la clause.
- get(int) - Method in class org.sat4j.minisat.constraints.cnf.HTClause
-
Return the ith literal of the clause.
- get(int) - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
-
- get(int) - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
-
- get(int) - Method in class org.sat4j.minisat.constraints.cnf.WLClause
-
Retourne le ieme literal de la clause.
- get(int) - Method in class org.sat4j.minisat.core.Heap
-
- get(int) - Method in interface org.sat4j.specs.IConstr
-
returns the ith literal in the constraint
- get(int) - Method in interface org.sat4j.specs.IVec
-
- get(int) - Method in interface org.sat4j.specs.IVecInt
-
- getActivity() - Method in class org.sat4j.core.ConstrGroup
-
- getActivity() - Method in class org.sat4j.minisat.constraints.card.AtLeast
-
- getActivity() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
-
Obtenir la valeur de l'activit?
- getActivity() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
-
Returns the activity of the constraint
- getActivity() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
-
- getActivity() - Method in class org.sat4j.minisat.constraints.cnf.HTClause
-
- getActivity() - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
-
- getActivity() - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
-
- getActivity() - Method in class org.sat4j.minisat.constraints.cnf.WLClause
-
- getActivity() - Method in interface org.sat4j.specs.IConstr
-
To obtain the activity of the constraint.
- getActivityPercent() - Method in class org.sat4j.minisat.learning.ActiveLearning
-
- getAddedVars() - Method in class org.sat4j.tools.AbstractClauseSelectorSolver
-
- getAddedVars() - Method in class org.sat4j.tools.FullClauseSelectorSolver
-
- getAddedVars() - Method in class org.sat4j.tools.GroupClauseSelectorSolver
-
- getAddedVars() - Method in class org.sat4j.tools.NegationDecorator
-
- getAtLeastKEncoding() - Method in class org.sat4j.tools.encoding.Policy
-
- getAtLeastOneEncoding() - Method in class org.sat4j.tools.encoding.Policy
-
- getAtMostKEncoding() - Method in class org.sat4j.tools.encoding.Policy
-
- getAtMostOneEncoding() - Method in class org.sat4j.tools.encoding.Policy
-
- getBeginTime() - Method in class org.sat4j.AbstractLauncher
-
Obtaining the current time spent since the beginning of the solving
process.
- getClaDecay() - Method in class org.sat4j.minisat.core.SearchParams
-
- getCoef(int) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
-
- getConflictBoundIncFactor() - Method in class org.sat4j.minisat.core.SearchParams
-
- getConstr(int) - Method in class org.sat4j.core.ConstrGroup
-
- getConstraints() - Method in class org.sat4j.tools.FullClauseSelectorSolver
-
- getConstrs() - Method in class org.sat4j.tools.FullClauseSelectorSolver
-
- getCurrentExitCode() - Method in interface org.sat4j.ILauncherMode
-
Allow the launcher to get the current status of the problem: SAT, UNSAT,
UPPER_BOUND, etc.
- getDegree() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
-
- getDSFactory() - Method in class org.sat4j.minisat.core.Solver
-
- getExactlyKEncoding() - Method in class org.sat4j.tools.encoding.Policy
-
- getExactlyOneEncoding() - Method in class org.sat4j.tools.encoding.Policy
-
- getExitCode() - Method in class org.sat4j.AbstractLauncher
-
Get the value of the ExitCode
- getExpectedNumberOfClauses() - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
-
- getFactor() - Method in class org.sat4j.minisat.restarts.LubyRestarts
-
- getFilename() - Method in class org.sat4j.tools.FileBasedVisualizationTool
-
- getFromPool(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
-
- getFromPool(int) - Method in interface org.sat4j.minisat.core.ILits
-
Translates a Dimacs literal into an internal representation literal.
- getInitConflictBound() - Method in class org.sat4j.minisat.core.SearchParams
-
- getInstanceName(String[]) - Method in class org.sat4j.AbstractLauncher
-
- getInstanceName(String[]) - Method in class org.sat4j.BasicLauncher
-
- getInstanceName(String[]) - Method in class org.sat4j.MUSLauncher
-
- getIthConstr(int) - Method in class org.sat4j.minisat.core.Solver
-
returns the ith constraint in the solver.
- getLastClause() - Method in class org.sat4j.tools.FullClauseSelectorSolver
-
- getLastConstr() - Method in class org.sat4j.tools.FullClauseSelectorSolver
-
- getLearnedConstraints() - Method in class org.sat4j.minisat.core.Solver
-
- getLearnedConstraints() - Method in interface org.sat4j.specs.ISolverService
-
Read-Only access to the list of constraints learned and not deleted so
far in the solver.
- getLevel(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
-
- getLevel(int) - Method in interface org.sat4j.minisat.core.ILits
-
Returns the level at which that literal has been assigned a value, else
-1.
- getLimit() - Method in class org.sat4j.minisat.learning.ActiveLearning
-
- getLimit() - Method in class org.sat4j.minisat.learning.PercentLengthLearning
-
- getLiterals(String) - Method in class org.sat4j.reader.JSONReader
-
- getLiteralsPropagatedAt(int) - Method in class org.sat4j.minisat.core.Solver
-
- getLiteralsPropagatedAt(int) - Method in interface org.sat4j.specs.ISolverService
-
To access the literals propagated at a specific decision level.
- getLits() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
-
- getLits() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
-
- getLits() - Method in class org.sat4j.minisat.constraints.cnf.HTClause
-
- getLits() - Method in class org.sat4j.minisat.constraints.cnf.WLClause
-
- getLogger() - Method in interface org.sat4j.minisat.core.ICDCL
-
- getLogger() - Method in class org.sat4j.minisat.core.Solver
-
- getLogPrefix() - Method in class org.sat4j.minisat.core.Solver
-
- getLogPrefix() - Method in interface org.sat4j.specs.ISolver
-
- getLogPrefix() - Method in interface org.sat4j.specs.ISolverService
-
- getLogPrefix() - Method in class org.sat4j.tools.AbstractOutputSolver
-
- getLogPrefix() - Method in class org.sat4j.tools.ManyCore
-
- getLogPrefix() - Method in class org.sat4j.tools.SolverDecorator
-
- getLogPrefix() - Method in class org.sat4j.tools.StatisticsSolver
-
- getLogWriter() - Method in class org.sat4j.AbstractLauncher
-
- getMaxLength() - Method in class org.sat4j.minisat.learning.FixedLengthLearning
-
- getmin() - Method in class org.sat4j.minisat.core.Heap
-
- getMssList() - Method in class org.sat4j.tools.AllMUSes
-
- getNbexpectedclauses() - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
-
- getNumberOfSolutionFound() - Method in class org.sat4j.tools.SearchEnumeratorListener
-
- getObjectiveValue() - Method in class org.sat4j.opt.MaxSatDecorator
-
- getObjectiveValue() - Method in class org.sat4j.opt.MinOneDecorator
-
- getObjectiveValue() - Method in interface org.sat4j.specs.IOptimizationProblem
-
Read only access to the value of the objective function for the current
solution.
- getObjectiveValue() - Method in class org.sat4j.tools.LexicoDecorator
-
- getObjectiveValue(int) - Method in class org.sat4j.tools.LexicoDecorator
-
- getOrder() - Method in interface org.sat4j.minisat.core.ICDCL
-
- getOrder() - Method in class org.sat4j.minisat.core.Solver
-
- getOut() - Method in class org.sat4j.tools.DimacsStringSolver
-
- getOutLearnt() - Method in class org.sat4j.minisat.core.Solver
-
- getPeriod() - Method in class org.sat4j.minisat.orders.PureOrder
-
- getPeriod() - Method in class org.sat4j.minisat.restarts.FixedPeriodRestarts
-
- getPhaseSelectionStrategy() - Method in interface org.sat4j.minisat.core.IOrder
-
- getPhaseSelectionStrategy() - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
-
- getPhaseSelectionStrategy() - Method in class org.sat4j.minisat.orders.TabuListDecorator
-
- getPhaseSelectionStrategy() - Method in class org.sat4j.minisat.orders.VarOrderHeap
-
- getPrevboolmodel() - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
-
- getPrevfullmodel() - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
-
- getPrevmodel() - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
-
- getProbability() - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
-
- getReader() - Method in class org.sat4j.AbstractLauncher
-
- getReason(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
-
- getReason(int) - Method in interface org.sat4j.minisat.core.ILits
-
Returns the reason of the assignment of a literal.
- getRestartStrategy() - Method in interface org.sat4j.minisat.core.ICDCL
-
- getRestartStrategy() - Method in class org.sat4j.minisat.core.Solver
-
- getSearchListener() - Method in class org.sat4j.minisat.core.Solver
-
- getSearchListener() - Method in interface org.sat4j.specs.ISolver
-
Get the current SearchListener.
- getSearchListener() - Method in class org.sat4j.tools.AbstractOutputSolver
-
- getSearchListener() - Method in class org.sat4j.tools.ManyCore
-
- getSearchListener() - Method in class org.sat4j.tools.SolverDecorator
-
- getSearchListener() - Method in class org.sat4j.tools.StatisticsSolver
-
- getSearchParams() - Method in interface org.sat4j.minisat.core.ICDCL
-
- getSearchParams() - Method in class org.sat4j.minisat.core.Solver
-
- getSimplifier() - Method in interface org.sat4j.minisat.core.ICDCL
-
- getSimplifier() - Method in class org.sat4j.minisat.core.Solver
-
- getSolver() - Method in class org.sat4j.reader.DimacsReader
-
- getSolver() - Method in class org.sat4j.tools.DimacsArrayReader
-
- getSolverInstance() - Method in class org.sat4j.tools.AllMUSes
-
Gets an instance of ISolver that can be used to compute all MUSes
- getSolvers() - Method in class org.sat4j.tools.ManyCore
-
- getSolvingEngine() - Method in class org.sat4j.minisat.core.Solver
-
- getSolvingEngine() - Method in interface org.sat4j.specs.ISolver
-
Retrieve the real engine in case the engine is decorated by one or
several decorator.
- getSolvingEngine() - Method in class org.sat4j.tools.AbstractOutputSolver
-
- getSolvingEngine() - Method in class org.sat4j.tools.ManyCore
-
- getSolvingEngine() - Method in class org.sat4j.tools.SolverDecorator
-
- getSolvingEngine() - Method in class org.sat4j.tools.StatisticsSolver
-
- getStat() - Method in class org.sat4j.minisat.core.Solver
-
- getStat() - Method in interface org.sat4j.specs.ISolver
-
To obtain a map of the available statistics from the solver.
- getStat() - Method in class org.sat4j.tools.AbstractOutputSolver
-
- getStat() - Method in class org.sat4j.tools.ManyCore
-
- getStat() - Method in class org.sat4j.tools.SolverDecorator
-
- getStat() - Method in class org.sat4j.tools.StatisticsSolver
-
- getStats() - Method in interface org.sat4j.minisat.core.ICDCL
-
- getStats() - Method in class org.sat4j.minisat.core.Solver
-
- getString(String) - Static method in class org.sat4j.Messages
-
- getTimeout() - Method in class org.sat4j.minisat.core.Solver
-
- getTimeout() - Method in interface org.sat4j.specs.ISolver
-
Useful to check the internal timeout of the solver.
- getTimeout() - Method in class org.sat4j.tools.AbstractOutputSolver
-
- getTimeout() - Method in class org.sat4j.tools.ManyCore
-
- getTimeout() - Method in class org.sat4j.tools.SolverDecorator
-
- getTimeout() - Method in class org.sat4j.tools.StatisticsSolver
-
- getTimeoutMs() - Method in class org.sat4j.minisat.core.Solver
-
- getTimeoutMs() - Method in interface org.sat4j.specs.ISolver
-
Useful to check the internal timeout of the solver.
- getTimeoutMs() - Method in class org.sat4j.tools.AbstractOutputSolver
-
- getTimeoutMs() - Method in class org.sat4j.tools.ManyCore
-
- getTimeoutMs() - Method in class org.sat4j.tools.SolverDecorator
-
- getTimeoutMs() - Method in class org.sat4j.tools.StatisticsSolver
-
- getTimer() - Method in interface org.sat4j.minisat.core.LearnedConstraintsDeletionStrategy
-
- getValue() - Method in class org.sat4j.minisat.core.Counter
-
- getVarDecay() - Method in class org.sat4j.minisat.core.SearchParams
-
- getVariableHeuristics() - Method in interface org.sat4j.minisat.core.IOrder
-
Read-Only access to the value of the heuristics for each variable.
- getVariableHeuristics() - Method in class org.sat4j.minisat.core.Solver
-
- getVariableHeuristics() - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
-
- getVariableHeuristics() - Method in class org.sat4j.minisat.orders.TabuListDecorator
-
- getVariableHeuristics() - Method in class org.sat4j.minisat.orders.VarOrderHeap
-
- getVariableHeuristics() - Method in interface org.sat4j.specs.ISolverService
-
Read-Only access to the value of the heuristics for each variable.
- getVarToHighLevel() - Method in class org.sat4j.tools.GroupClauseSelectorSolver
-
- getVocabulary() - Method in class org.sat4j.minisat.constraints.AbstractDataStructureFactory
-
- getVocabulary() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
-
- getVocabulary() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
-
- getVocabulary() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
-
- getVocabulary() - Method in class org.sat4j.minisat.constraints.cnf.HTClause
-
- getVocabulary() - Method in class org.sat4j.minisat.constraints.cnf.WLClause
-
- getVocabulary() - Method in interface org.sat4j.minisat.core.DataStructureFactory
-
- getVocabulary() - Method in class org.sat4j.minisat.core.Solver
-
- getVocabulary() - Method in class org.sat4j.minisat.orders.VarOrderHeap
-
- getWatchesFor(int) - Method in class org.sat4j.minisat.constraints.AbstractDataStructureFactory
-
- getWatchesFor(int) - Method in interface org.sat4j.minisat.core.DataStructureFactory
-
- glucose - Variable in class org.sat4j.minisat.core.Solver
-
- Glucose21Restarts - Class in org.sat4j.minisat.restarts
-
Dynamic restart strategy of Glucose 2.1 as presented in Refining restarts
strategies for SAT and UNSAT formulae.
- Glucose21Restarts() - Constructor for class org.sat4j.minisat.restarts.Glucose21Restarts
-
- GroupClauseSelectorSolver<T extends ISolver> - Class in org.sat4j.tools
-
- GroupClauseSelectorSolver(T) - Constructor for class org.sat4j.tools.GroupClauseSelectorSolver
-
- GroupedCNFReader - Class in org.sat4j.reader
-
- GroupedCNFReader(IGroupSolver) - Constructor for class org.sat4j.reader.GroupedCNFReader
-
- growTo(int, T) - Method in class org.sat4j.core.ReadOnlyVec
-
- growTo(int, int) - Method in class org.sat4j.core.ReadOnlyVecInt
-
- growTo(int, T) - Method in class org.sat4j.core.Vec
-
- growTo(int, int) - Method in class org.sat4j.core.VecInt
-
- growTo(int, T) - Method in interface org.sat4j.specs.IVec
-
- growTo(int, int) - Method in interface org.sat4j.specs.IVecInt
-
- ICDCL<D extends DataStructureFactory> - Interface in org.sat4j.minisat.core
-
Abstraction for Conflict Driven Clause Learning Solver.
- IConstr - Interface in org.sat4j.specs
-
The most general abstraction for handling a constraint.
- IFF - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader
-
- iff(int, IVecInt) - Method in class org.sat4j.tools.GateTranslator
-
translate y <=> (x1 <=> x2 <=> ... <=> xn) into clauses.
- IFTHENELSE - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader
-
- ignoredclauses - Variable in class org.sat4j.minisat.core.SolverStats
-
- IGroupSolver - Interface in org.sat4j.specs
-
Represents a CNF in which clauses are grouped into levels.
- ILauncherMode - Interface in org.sat4j
-
Allow to change the behavior of the launcher (either decision or optimization
mode)
- ILits - Interface in org.sat4j.minisat.core
-
That interface manages the solver's internal vocabulary.
- ILogAble - Interface in org.sat4j.specs
-
Utility interface to catch objects with logging capability (able to log).
- IMPLIES - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader
-
- inc() - Method in class org.sat4j.minisat.core.Counter
-
- incActivity(double) - Method in class org.sat4j.minisat.constraints.card.AtLeast
-
- incActivity(double) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
-
Incr?
- incActivity(double) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
-
Increments activity of the constraint
- incActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.LearntBinaryClause
-
- incActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.LearntHTClause
-
- incActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.LearntWLClause
-
- incActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.OriginalBinaryClause
-
- incActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.OriginalHTClause
-
- incActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.OriginalWLClause
-
- incActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
-
- incActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
-
- incActivity(double) - Method in interface org.sat4j.minisat.core.Constr
-
Increase the constraint activity.
- increase(int) - Method in class org.sat4j.minisat.core.Heap
-
- indexOf(T) - Method in class org.sat4j.core.ReadOnlyVec
-
- indexOf(int) - Method in class org.sat4j.core.ReadOnlyVecInt
-
- indexOf(T) - Method in class org.sat4j.core.Vec
-
- indexOf(int) - Method in class org.sat4j.core.VecInt
-
- indexOf(T) - Method in interface org.sat4j.specs.IVec
-
- indexOf(int) - Method in interface org.sat4j.specs.IVecInt
-
- inHeap(int) - Method in class org.sat4j.minisat.core.Heap
-
- init(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
-
- init(int) - Method in interface org.sat4j.minisat.core.ILits
-
- init() - Method in interface org.sat4j.minisat.core.IOrder
-
that method has the responsibility to initialize all arrays in the
heuristics.
- init(int) - Method in interface org.sat4j.minisat.core.IPhaseSelectionStrategy
-
that method has the responsibility to initialize all arrays in the
heuristics.
- init(int, int) - Method in interface org.sat4j.minisat.core.IPhaseSelectionStrategy
-
initialize the phase of a given variable to the given value.
- init() - Method in interface org.sat4j.minisat.core.LearnedConstraintsDeletionStrategy
-
- init() - Method in interface org.sat4j.minisat.core.LearningStrategy
-
hook method called just before the search begins.
- init(SearchParams, SolverStats) - Method in interface org.sat4j.minisat.core.RestartStrategy
-
Hook method called just before the search starts.
- init() - Method in class org.sat4j.minisat.learning.FixedLengthLearning
-
- init() - Method in class org.sat4j.minisat.learning.LimitedLearning
-
- init() - Method in class org.sat4j.minisat.learning.PercentLengthLearning
-
- init(int) - Method in class org.sat4j.minisat.orders.NegativeLiteralSelectionStrategy
-
- init(int, int) - Method in class org.sat4j.minisat.orders.NegativeLiteralSelectionStrategy
-
- init(int) - Method in class org.sat4j.minisat.orders.PositiveLiteralSelectionStrategy
-
- init(int, int) - Method in class org.sat4j.minisat.orders.PositiveLiteralSelectionStrategy
-
- init(int) - Method in class org.sat4j.minisat.orders.RandomLiteralSelectionStrategy
-
- init(int, int) - Method in class org.sat4j.minisat.orders.RandomLiteralSelectionStrategy
-
- init() - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
-
- init() - Method in class org.sat4j.minisat.orders.SubsetVarOrder
-
- init() - Method in class org.sat4j.minisat.orders.TabuListDecorator
-
- init() - Method in class org.sat4j.minisat.orders.VarOrderHeap
-
that method has the responsability to initialize all arrays in the
heuristics.
- init(SearchParams, SolverStats) - Method in class org.sat4j.minisat.restarts.ArminRestarts
-
- init(SearchParams, SolverStats) - Method in class org.sat4j.minisat.restarts.FixedPeriodRestarts
-
- init(SearchParams, SolverStats) - Method in class org.sat4j.minisat.restarts.Glucose21Restarts
-
- init(SearchParams, SolverStats) - Method in class org.sat4j.minisat.restarts.LubyRestarts
-
- init(SearchParams, SolverStats) - Method in class org.sat4j.minisat.restarts.MiniSATRestarts
-
- init(SearchParams, SolverStats) - Method in class org.sat4j.minisat.restarts.NoRestarts
-
- init(S) - Method in interface org.sat4j.specs.SearchListener
-
Provide access to the solver's controllable interface.
- init(ISolverService) - Method in class org.sat4j.tools.ConflictDepthTracing
-
- init(ISolverService) - Method in class org.sat4j.tools.ConflictLevelTracing
-
- init(ISolverService) - Method in class org.sat4j.tools.DecisionTracing
-
- init() - Method in class org.sat4j.tools.FileBasedVisualizationTool
-
- init(ISolverService) - Method in class org.sat4j.tools.HeuristicsTracing
-
- init() - Method in interface org.sat4j.tools.IVisualizationTool
-
- init(ISolverService) - Method in class org.sat4j.tools.LearnedTracing
-
- init(T) - Method in class org.sat4j.tools.MultiTracing
-
- init(ISolverService) - Method in class org.sat4j.tools.SearchEnumeratorListener
-
- init(S) - Method in class org.sat4j.tools.SearchListenerAdapter
-
- init(ISolverService) - Method in class org.sat4j.tools.SearchMinOneListener
-
- init(ISolverService) - Method in class org.sat4j.tools.TextOutputTracing
-
- initStats(SolverStats) - Method in class org.sat4j.minisat.core.Solver
-
- insert(int) - Method in class org.sat4j.minisat.core.Heap
-
- insert(int) - Method in class org.sat4j.minisat.core.IntQueue
-
Add an element to the queue.
- insertFirst(T) - Method in class org.sat4j.core.ReadOnlyVec
-
- insertFirst(int) - Method in class org.sat4j.core.ReadOnlyVecInt
-
- insertFirst(T) - Method in class org.sat4j.core.Vec
-
Insert an element at the very beginning of the vector.
- insertFirst(int) - Method in class org.sat4j.core.VecInt
-
Insert an element at the very begining of the vector.
- insertFirst(T) - Method in interface org.sat4j.specs.IVec
-
Insert an element at the very begining of the vector.
- insertFirst(int) - Method in interface org.sat4j.specs.IVecInt
-
Insert an element at the very begining of the vector.
- insertFirstWithShifting(T) - Method in class org.sat4j.core.ReadOnlyVec
-
- insertFirstWithShifting(T) - Method in class org.sat4j.core.Vec
-
- insertFirstWithShifting(T) - Method in interface org.sat4j.specs.IVec
-
- InsertionStrategy - Class in org.sat4j.tools.xplain
-
An implementation of the ReplayXplain algorithm as explained by Ulrich Junker
in the following paper:
- InsertionStrategy() - Constructor for class org.sat4j.tools.xplain.InsertionStrategy
-
- inspects - Variable in class org.sat4j.minisat.core.SolverStats
-
- instance() - Static method in class org.sat4j.LightFactory
-
Access to the single instance of the factory.
- instance() - Static method in class org.sat4j.minisat.SolverFactory
-
Access to the single instance of the factory.
- InstanceReader - Class in org.sat4j.reader
-
An reader having the responsability to choose the right reader according to
the input.
- InstanceReader(ISolver) - Constructor for class org.sat4j.reader.InstanceReader
-
- internalState() - Method in class org.sat4j.tools.AbstractClauseSelectorSolver
-
In the internal state, the solver will allow the selector variables to be
satisfied.
- IntQueue - Class in org.sat4j.minisat.core
-
Implementation of a queue.
- IntQueue() - Constructor for class org.sat4j.minisat.core.IntQueue
-
- IOptimizationProblem - Interface in org.sat4j.specs
-
Represents an optimization problem.
- IOrder - Interface in org.sat4j.minisat.core
-
Interface for the variable ordering heuristics.
- IPhaseSelectionStrategy - Interface in org.sat4j.minisat.core
-
The responsibility of that class is to choose the phase (positive or
negative) of the variable that was selected by the IOrder.
- IProblem - Interface in org.sat4j.specs
-
Access to the information related to a given problem instance.
- isDBSimplificationAllowed() - Method in class org.sat4j.minisat.core.Solver
-
- isDBSimplificationAllowed() - Method in interface org.sat4j.specs.ISolver
-
Indicate whether the solver is allowed to simplify the formula by
propagating the truth value of top level satisfied variables.
- isDBSimplificationAllowed() - Method in class org.sat4j.tools.AbstractOutputSolver
-
- isDBSimplificationAllowed() - Method in class org.sat4j.tools.ManyCore
-
- isDBSimplificationAllowed() - Method in class org.sat4j.tools.SolverDecorator
-
- isDBSimplificationAllowed() - Method in class org.sat4j.tools.StatisticsSolver
-
- isEmpty() - Method in class org.sat4j.core.ReadOnlyVec
-
- isEmpty() - Method in class org.sat4j.core.ReadOnlyVecInt
-
- isEmpty() - Method in class org.sat4j.core.Vec
-
- isEmpty() - Method in class org.sat4j.core.VecInt
-
- isEmpty() - Method in interface org.sat4j.specs.IVec
-
To know if a vector is empty
- isEmpty() - Method in interface org.sat4j.specs.IVecInt
-
To know if a vector is empty
- isFalsified(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
-
- isFalsified(int) - Method in interface org.sat4j.minisat.core.ILits
-
Check if a literal is falsified.
- isFull() - Method in class org.sat4j.minisat.core.CircularBuffer
-
- isImplied(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
-
- isImplied(int) - Method in interface org.sat4j.minisat.core.ILits
-
- ISimplifier - Interface in org.sat4j.minisat.core
-
Strategy for simplifying the conflict clause derived by the solver.
- isNeedToReduceDB() - Method in class org.sat4j.minisat.core.Solver
-
- ISolver - Interface in org.sat4j.specs
-
This interface contains all services provided by a SAT solver.
- ISolverService - Interface in org.sat4j.specs
-
The aim on that interface is to allow power users to communicate with the SAT
solver using Dimacs format.
- isOptimal() - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
-
- isOptimal() - Method in class org.sat4j.opt.MinOneDecorator
-
- isOptimal() - Method in interface org.sat4j.specs.IOptimizationProblem
-
Allows to check afterwards if the solution provided by the solver is
optimal or not.
- isOptimal() - Method in class org.sat4j.tools.LexicoDecorator
-
- isOptimal() - Method in class org.sat4j.tools.OptToSatAdapter
-
Allow to easily check is the solution returned by isSatisfiable is
optimal or not.
- isSatisfiable() - Method in class org.sat4j.minisat.core.Solver
-
- isSatisfiable(boolean) - Method in class org.sat4j.minisat.core.Solver
-
- isSatisfiable(IVecInt) - Method in class org.sat4j.minisat.core.Solver
-
- isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.minisat.core.Solver
-
- isSatisfiable() - Method in interface org.sat4j.specs.IProblem
-
Check the satisfiability of the set of constraints contained inside the
solver.
- isSatisfiable(IVecInt, boolean) - Method in interface org.sat4j.specs.IProblem
-
Check the satisfiability of the set of constraints contained inside the
solver.
- isSatisfiable(boolean) - Method in interface org.sat4j.specs.IProblem
-
Check the satisfiability of the set of constraints contained inside the
solver.
- isSatisfiable(IVecInt) - Method in interface org.sat4j.specs.IProblem
-
Check the satisfiability of the set of constraints contained inside the
solver.
- isSatisfiable(boolean) - Method in class org.sat4j.tools.AbstractClauseSelectorSolver
-
- isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.tools.AbstractClauseSelectorSolver
-
- isSatisfiable() - Method in class org.sat4j.tools.AbstractClauseSelectorSolver
-
- isSatisfiable(IVecInt) - Method in class org.sat4j.tools.AbstractClauseSelectorSolver
-
- isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.tools.AbstractOutputSolver
-
- isSatisfiable(boolean) - Method in class org.sat4j.tools.AbstractOutputSolver
-
- isSatisfiable() - Method in class org.sat4j.tools.AbstractOutputSolver
-
- isSatisfiable(IVecInt) - Method in class org.sat4j.tools.AbstractOutputSolver
-
- isSatisfiable() - Method in class org.sat4j.tools.ManyCore
-
- isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.tools.ManyCore
-
- isSatisfiable(boolean) - Method in class org.sat4j.tools.ManyCore
-
- isSatisfiable(IVecInt) - Method in class org.sat4j.tools.ManyCore
-
- isSatisfiable() - Method in class org.sat4j.tools.ModelIterator
-
- isSatisfiable(IVecInt) - Method in class org.sat4j.tools.ModelIterator
-
- isSatisfiable() - Method in class org.sat4j.tools.ModelIteratorToSATAdapter
-
- isSatisfiable(IVecInt) - Method in class org.sat4j.tools.ModelIteratorToSATAdapter
-
- isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.tools.NegationDecorator
-
- isSatisfiable() - Method in class org.sat4j.tools.OptToSatAdapter
-
- isSatisfiable(boolean) - Method in class org.sat4j.tools.OptToSatAdapter
-
- isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.tools.OptToSatAdapter
-
- isSatisfiable(IVecInt) - Method in class org.sat4j.tools.OptToSatAdapter
-
- isSatisfiable(boolean) - Method in class org.sat4j.tools.SolverDecorator
-
- isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.tools.SolverDecorator
-
- isSatisfiable() - Method in class org.sat4j.tools.SolverDecorator
-
- isSatisfiable(IVecInt) - Method in class org.sat4j.tools.SolverDecorator
-
- isSatisfiable() - Method in class org.sat4j.tools.StatisticsSolver
-
- isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.tools.StatisticsSolver
-
- isSatisfiable(boolean) - Method in class org.sat4j.tools.StatisticsSolver
-
- isSatisfiable(IVecInt) - Method in class org.sat4j.tools.StatisticsSolver
-
- isSatisfiable() - Method in class org.sat4j.tools.xplain.HighLevelXplain
-
- isSatisfiable(boolean) - Method in class org.sat4j.tools.xplain.HighLevelXplain
-
- isSatisfiable(IVecInt) - Method in class org.sat4j.tools.xplain.HighLevelXplain
-
- isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.tools.xplain.HighLevelXplain
-
- isSatisfiable() - Method in class org.sat4j.tools.xplain.Xplain
-
- isSatisfiable(boolean) - Method in class org.sat4j.tools.xplain.Xplain
-
- isSatisfiable(IVecInt) - Method in class org.sat4j.tools.xplain.Xplain
-
- isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.tools.xplain.Xplain
-
- isSatisfied(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
-
- isSatisfied(int) - Method in interface org.sat4j.minisat.core.ILits
-
Check if a literal is satisfied.
- isSkipDuplicatedEntries() - Method in class org.sat4j.tools.FullClauseSelectorSolver
-
- isSolutionOptimal() - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
-
- isSolverKeptHot() - Method in class org.sat4j.minisat.core.Solver
-
- isSolverKeptHot() - Method in interface org.sat4j.specs.ISolver
-
Ask to the solver if it is in "hot" mode, meaning that the heuristics is
not reset after call is isSatisfiable().
- isSolverKeptHot() - Method in class org.sat4j.tools.AbstractOutputSolver
-
- isSolverKeptHot() - Method in class org.sat4j.tools.ManyCore
-
- isSolverKeptHot() - Method in class org.sat4j.tools.SolverDecorator
-
- isSolverKeptHot() - Method in class org.sat4j.tools.StatisticsSolver
-
- isSubsetOf(VecInt) - Method in class org.sat4j.core.VecInt
-
to detect that the vector is a subset of another one.
- isUnassigned(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
-
- isUnassigned(int) - Method in interface org.sat4j.minisat.core.ILits
-
Check if a literal is assigned a truth value.
- isVerbose() - Method in class org.sat4j.minisat.core.Solver
-
- isVerbose() - Method in class org.sat4j.reader.Reader
-
- isVerbose() - Method in interface org.sat4j.specs.ISolver
-
To know if the solver is in verbose mode (output allowed) or not.
- isVerbose() - Method in class org.sat4j.tools.AbstractOutputSolver
-
- isVerbose() - Method in class org.sat4j.tools.ManyCore
-
- isVerbose() - Method in class org.sat4j.tools.SolverDecorator
-
- isVerbose() - Method in class org.sat4j.tools.StatisticsSolver
-
- ite(int, int, int, int) - Method in class org.sat4j.tools.GateTranslator
-
translate y <=> if x1 then x2 else x3 into clauses.
- iterator() - Method in class org.sat4j.core.ReadOnlyVec
-
- iterator() - Method in class org.sat4j.core.ReadOnlyVecInt
-
- iterator() - Method in class org.sat4j.core.Vec
-
- iterator() - Method in class org.sat4j.core.VecInt
-
- iterator() - Method in interface org.sat4j.specs.IVec
-
- iterator() - Method in interface org.sat4j.specs.IVecInt
-
- IteratorInt - Interface in org.sat4j.specs
-
Iterator interface to avoid boxing int into Integer.
- IVec<T> - Interface in org.sat4j.specs
-
An abstraction on the type of vector used in the library.
- IVecInt - Interface in org.sat4j.specs
-
An abstraction for the vector of int used on the library.
- IVisualizationTool - Interface in org.sat4j.tools
-
- 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.specs.ILogAble
-
- lowerBound() - Method in class org.sat4j.tools.SolutionCounter
-
Get the number of solutions found before the timeout occurs.
- luby() - Method in class org.sat4j.minisat.restarts.LubyRestarts
-
returns the current value of the luby sequence.
- LubyRestarts - Class in org.sat4j.minisat.restarts
-
Luby series
- LubyRestarts() - Constructor for class org.sat4j.minisat.restarts.LubyRestarts
-
- LubyRestarts(int) - Constructor for class org.sat4j.minisat.restarts.LubyRestarts
-
- 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
-
- MaxWatchCard(ILits, IVecInt, boolean, int) - Constructor for class org.sat4j.minisat.constraints.card.MaxWatchCard
-
Constructeur de base cr?
- maxWatchCardNew(UnitPropagationListener, ILits, IVecInt, boolean, int) - Static method in class org.sat4j.minisat.constraints.card.MaxWatchCard
-
Permet la cr?
- memory_based - Variable in class org.sat4j.minisat.core.Solver
-
- Messages - Class in org.sat4j
-
That class is intented to manage internationalisation within the application.
- middleLits - Variable in class org.sat4j.minisat.constraints.cnf.HTClause
-
- Minimal4CardinalityModel - Class in org.sat4j.tools
-
Computes models with a minimal number (with respect to cardinality) of
negative literals.
- Minimal4CardinalityModel(ISolver) - Constructor for class org.sat4j.tools.Minimal4CardinalityModel
-
- Minimal4CardinalityModel(ISolver, IVecInt, SolutionFoundListener) - Constructor for class org.sat4j.tools.Minimal4CardinalityModel
-
- Minimal4CardinalityModel(ISolver, IVecInt) - Constructor for class org.sat4j.tools.Minimal4CardinalityModel
-
- Minimal4CardinalityModel(ISolver, SolutionFoundListener) - Constructor for class org.sat4j.tools.Minimal4CardinalityModel
-
- Minimal4InclusionModel - Class in org.sat4j.tools
-
Computes models with a minimal subset (with respect to set inclusion) of
negative literals.
- Minimal4InclusionModel(ISolver, IVecInt, SolutionFoundListener) - Constructor for class org.sat4j.tools.Minimal4InclusionModel
-
- Minimal4InclusionModel(ISolver, IVecInt) - Constructor for class org.sat4j.tools.Minimal4InclusionModel
-
- Minimal4InclusionModel(ISolver) - Constructor for class org.sat4j.tools.Minimal4InclusionModel
-
- minimalExplanation() - Method in interface org.sat4j.tools.xplain.Explainer
-
- minimalExplanation() - Method in class org.sat4j.tools.xplain.HighLevelXplain
-
- minimalExplanation() - Method in class org.sat4j.tools.xplain.Xplain
-
Provide an explanation of the inconsistency in terms of a subset minimal
set of constraints, each constraint being referred to as its index
(order) in the solver: first constraint is numbered 1, the second 2, etc.
- MinimizationStrategy - Interface in org.sat4j.tools.xplain
-
Minimization technique used to reduce an unsatisfiable set of constraints
into a minimally unsatisfiable subformula (MUS).
- MiniSATLearning<D extends DataStructureFactory> - Class in org.sat4j.minisat.learning
-
MiniSAT learning scheme.
- MiniSATLearning() - Constructor for class org.sat4j.minisat.learning.MiniSATLearning
-
- MiniSATRestarts - Class in org.sat4j.minisat.restarts
-
Minisat original restart strategy.
- MiniSATRestarts() - Constructor for class org.sat4j.minisat.restarts.MiniSATRestarts
-
- MinOneDecorator - Class in org.sat4j.opt
-
Computes a solution with the smallest number of satisfied literals.
- MinOneDecorator(ISolver) - Constructor for class org.sat4j.opt.MinOneDecorator
-
- MinWatchCard - Class in org.sat4j.minisat.constraints.card
-
- MinWatchCard(ILits, IVecInt, boolean, int) - Constructor for class org.sat4j.minisat.constraints.card.MinWatchCard
-
Constructs and normalizes a cardinality constraint. used by
minWatchCardNew in the non-normalized case.
- MinWatchCard(ILits, IVecInt, int) - Constructor for class org.sat4j.minisat.constraints.card.MinWatchCard
-
Constructs and normalizes a cardinality constraint. used by
MinWatchCardPB.normalizedMinWatchCardNew() in the normalized case.
- minWatchCardNew(UnitPropagationListener, ILits, IVecInt, boolean, int) - Static method in class org.sat4j.minisat.constraints.card.MinWatchCard
-
Constructs a cardinality constraint with a minimal set of watched
literals Permet la cr?
- MixedDataStructureDanielHT - Class in org.sat4j.minisat.constraints
-
Uses specific data structure for cardinality constraints.
- MixedDataStructureDanielHT() - Constructor for class org.sat4j.minisat.constraints.MixedDataStructureDanielHT
-
- MixedDataStructureDanielWL - Class in org.sat4j.minisat.constraints
-
- MixedDataStructureDanielWL() - Constructor for class org.sat4j.minisat.constraints.MixedDataStructureDanielWL
-
- MixedDataStructureSingleWL - Class in org.sat4j.minisat.constraints
-
- MixedDataStructureSingleWL() - Constructor for class org.sat4j.minisat.constraints.MixedDataStructureSingleWL
-
- model() - Method in class org.sat4j.minisat.core.Solver
-
Si un mod?
- model(int) - Method in class org.sat4j.minisat.core.Solver
-
- model() - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
-
- model(int) - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
-
- model() - Method in class org.sat4j.opt.MinOneDecorator
-
- model() - Method in interface org.sat4j.specs.IProblem
-
Provide a model (if any) for a satisfiable formula.
- model(int) - Method in interface org.sat4j.specs.RandomAccessModel
-
Provide the truth value of a specific variable in the model.
- model() - Method in class org.sat4j.tools.AbstractOutputSolver
-
- model(int) - Method in class org.sat4j.tools.AbstractOutputSolver
-
- model() - Method in class org.sat4j.tools.FullClauseSelectorSolver
-
- model() - Method in class org.sat4j.tools.GroupClauseSelectorSolver
-
- model() - Method in class org.sat4j.tools.LexicoDecorator
-
- model(int) - Method in class org.sat4j.tools.LexicoDecorator
-
- model() - Method in class org.sat4j.tools.ManyCore
-
- model(int) - Method in class org.sat4j.tools.ManyCore
-
- model() - Method in class org.sat4j.tools.Minimal4CardinalityModel
-
- model() - Method in class org.sat4j.tools.Minimal4InclusionModel
-
- model() - Method in class org.sat4j.tools.ModelIterator
-
- model() - Method in class org.sat4j.tools.ModelIteratorToSATAdapter
-
- model() - Method in class org.sat4j.tools.OptToSatAdapter
-
- model(int) - Method in class org.sat4j.tools.OptToSatAdapter
-
- model(int) - Method in class org.sat4j.tools.SolverDecorator
-
- model() - Method in class org.sat4j.tools.SolverDecorator
-
- model() - Method in class org.sat4j.tools.StatisticsSolver
-
- model(int) - Method in class org.sat4j.tools.StatisticsSolver
-
- ModelIterator - Class in org.sat4j.tools
-
That class allows to iterate through all the models (implicants) of a
formula.
- ModelIterator(ISolver) - Constructor for class org.sat4j.tools.ModelIterator
-
Create an iterator over the solutions available in solver
.
- ModelIterator(ISolver, long) - Constructor for class org.sat4j.tools.ModelIterator
-
Create an iterator over a limited number of solutions available in
solver
.
- ModelIteratorToSATAdapter - Class in org.sat4j.tools
-
This class allow to use the ModelIterator class as a solver.
- ModelIteratorToSATAdapter(ISolver, SolutionFoundListener) - Constructor for class org.sat4j.tools.ModelIteratorToSATAdapter
-
- ModelIteratorToSATAdapter(ISolver, long, SolutionFoundListener) - Constructor for class org.sat4j.tools.ModelIteratorToSATAdapter
-
- modelListener - Variable in class org.sat4j.tools.AbstractMinimalModel
-
- modelWithInternalVariables() - Method in class org.sat4j.minisat.core.Solver
-
- modelWithInternalVariables() - Method in 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.Minimal4CardinalityModel
-
- modelWithInternalVariables() - Method in class org.sat4j.tools.Minimal4InclusionModel
-
- modelWithInternalVariables() - Method in class org.sat4j.tools.SolverDecorator
-
- modelWithInternalVariables() - Method in class org.sat4j.tools.StatisticsSolver
-
- MoreThanSAT - Class in org.sat4j
-
This is an example of use of the SAT4J library for computing the backbone of
a CNF or to compute the number of solutions of a CNF.
- moveTo(IVec<T>) - Method in class org.sat4j.core.ReadOnlyVec
-
- moveTo(int, int) - Method in class org.sat4j.core.ReadOnlyVec
-
- moveTo(IVecInt) - Method in class org.sat4j.core.ReadOnlyVecInt
-
- moveTo(int[]) - Method in class org.sat4j.core.ReadOnlyVecInt
-
- moveTo(int, int) - Method in class org.sat4j.core.ReadOnlyVecInt
-
- moveTo(int, int[]) - Method in class org.sat4j.core.ReadOnlyVecInt
-
- moveTo(IVec<T>) - Method in class org.sat4j.core.Vec
-
- moveTo(int, int) - Method in class org.sat4j.core.Vec
-
- moveTo(IVecInt) - Method in class org.sat4j.core.VecInt
-
- moveTo(int, int) - Method in class org.sat4j.core.VecInt
-
- moveTo(int[]) - Method in class org.sat4j.core.VecInt
-
- moveTo(int, int[]) - Method in class org.sat4j.core.VecInt
-
- moveTo(IVec<T>) - Method in interface org.sat4j.specs.IVec
-
Move the content of the vector into dest.
- moveTo(int, int) - Method in interface org.sat4j.specs.IVec
-
Move elements inside the vector.
- moveTo(IVecInt) - Method in interface org.sat4j.specs.IVecInt
-
- moveTo(int, int[]) - Method in interface org.sat4j.specs.IVecInt
-
- moveTo(int[]) - Method in interface org.sat4j.specs.IVecInt
-
- moveTo(int, int) - Method in interface org.sat4j.specs.IVecInt
-
Move elements inside the vector.
- moveTo2(IVecInt) - Method in class org.sat4j.core.ReadOnlyVecInt
-
- moveTo2(IVecInt) - Method in class org.sat4j.core.VecInt
-
- moveTo2(IVecInt) - Method in interface org.sat4j.specs.IVecInt
-
- MultiTracing<T extends ISolverService> - Class in org.sat4j.tools
-
Allow to feed the solver with several SearchListener.
- MultiTracing(SearchListener<T>...) - Constructor for class org.sat4j.tools.MultiTracing
-
- MultiTracing(List<SearchListener<T>>) - Constructor for class org.sat4j.tools.MultiTracing
-
- MUSLauncher - Class in org.sat4j
-
- MUSLauncher() - Constructor for class org.sat4j.MUSLauncher
-
- NAND - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader
-
- nAssigns() - Method in class org.sat4j.minisat.core.Solver
-
- nbclauses - Variable in class org.sat4j.tools.AbstractOutputSolver
-
- nbvars - Variable in class org.sat4j.tools.AbstractOutputSolver
-
- nConstraints() - Method in class org.sat4j.minisat.core.Solver
-
- nConstraints() - Method in interface org.sat4j.specs.IProblem
-
To know the number of constraints currently available in the solver.
- nConstraints() - Method in class org.sat4j.tools.AbstractOutputSolver
-
- nConstraints() - Method in class org.sat4j.tools.DimacsOutputSolver
-
- nConstraints() - Method in class org.sat4j.tools.DimacsStringSolver
-
- nConstraints() - Method in class org.sat4j.tools.ManyCore
-
- nConstraints() - Method in class org.sat4j.tools.SolverDecorator
-
- nConstraints() - Method in class org.sat4j.tools.StatisticsSolver
-
- neg(int) - Static method in class org.sat4j.core.LiteralsUtils
-
Returns the opposite literal.
- NegationDecorator<T extends ISolver> - Class in org.sat4j.tools
-
Negates the formula inside a solver.
- NegationDecorator(T) - Constructor for class org.sat4j.tools.NegationDecorator
-
- negativeLiterals(ISolver) - Static method in class org.sat4j.tools.AbstractMinimalModel
-
- NegativeLiteralSelectionStrategy - Class in org.sat4j.minisat.orders
-
- NegativeLiteralSelectionStrategy() - Constructor for class org.sat4j.minisat.orders.NegativeLiteralSelectionStrategy
-
- negLit(int) - Static method in class org.sat4j.core.LiteralsUtils
-
Returns the negative literal associated with a variable.
- newBackjumping() - Static method in class org.sat4j.minisat.SolverFactory
-
- newBest17() - Static method in class org.sat4j.minisat.SolverFactory
-
- newBestHT() - Static method in class org.sat4j.minisat.SolverFactory
-
- newBestWL() - Static method in class org.sat4j.minisat.SolverFactory
-
- newConflict() - Method in interface org.sat4j.minisat.core.ConflictTimer
-
- newConflict() - Method in class org.sat4j.minisat.core.ConflictTimerAdapter
-
- newConflict() - Method in class org.sat4j.minisat.core.ConflictTimerContainer
-
- newConflict() - Method in class org.sat4j.minisat.restarts.ArminRestarts
-
- newConflict() - Method in class org.sat4j.minisat.restarts.FixedPeriodRestarts
-
- newConflict() - Method in class org.sat4j.minisat.restarts.Glucose21Restarts
-
- newConflict() - Method in class org.sat4j.minisat.restarts.LubyRestarts
-
- newConflict() - Method in class org.sat4j.minisat.restarts.MiniSATRestarts
-
- newConflict() - Method in class org.sat4j.minisat.restarts.NoRestarts
-
- newDefault() - Static method in class org.sat4j.minisat.SolverFactory
-
Default solver of the SolverFactory.
- newDefaultAutoErasePhaseSaving() - Static method in class org.sat4j.minisat.SolverFactory
-
- newDefaultMS21PhaseSaving() - Static method in class org.sat4j.minisat.SolverFactory
-
- newDimacsOutput() - Static method in class org.sat4j.minisat.SolverFactory
-
- newGlucose() - Static method in class org.sat4j.minisat.SolverFactory
-
- newGlucose21() - Static method in class org.sat4j.minisat.SolverFactory
-
- newGreedySolver() - Static method in class org.sat4j.minisat.SolverFactory
-
- newLearnedClause(Constr, int) - Method in interface org.sat4j.minisat.core.RestartStrategy
-
Callback method called when a new clause is learned by the solver, after
conflict analysis.
- newLearnedClause(Constr, int) - Method in class org.sat4j.minisat.restarts.ArminRestarts
-
- newLearnedClause(Constr, int) - Method in class org.sat4j.minisat.restarts.FixedPeriodRestarts
-
- newLearnedClause(Constr, int) - Method in class org.sat4j.minisat.restarts.Glucose21Restarts
-
- newLearnedClause(Constr, int) - Method in class org.sat4j.minisat.restarts.LubyRestarts
-
- newLearnedClause(Constr, int) - Method in class org.sat4j.minisat.restarts.MiniSATRestarts
-
- newLearnedClause(Constr, int) - Method in class org.sat4j.minisat.restarts.NoRestarts
-
- newLight() - Static method in class org.sat4j.minisat.SolverFactory
-
Small footprint SAT solver.
- newMiniLearning(DataStructureFactory, IOrder) - Static method in class org.sat4j.minisat.SolverFactory
-
- newMiniLearningHeap() - Static method in class org.sat4j.minisat.SolverFactory
-
- newMiniLearningHeap(DataStructureFactory) - Static method in class org.sat4j.minisat.SolverFactory
-
- newMiniLearningHeapExpSimp() - Static method in class org.sat4j.minisat.SolverFactory
-
- newMiniLearningHeapEZSimp() - Static method in class org.sat4j.minisat.SolverFactory
-
- newMiniLearningHeapEZSimpLongRestarts() - Static method in class org.sat4j.minisat.SolverFactory
-
- newMiniLearningHeapEZSimpNoRestarts() - Static method in class org.sat4j.minisat.SolverFactory
-
- newMiniLearningHeapRsatExpSimp() - Static method in class org.sat4j.minisat.SolverFactory
-
- newMiniLearningHeapRsatExpSimpBiere() - Static method in class org.sat4j.minisat.SolverFactory
-
- newMiniLearningHeapRsatExpSimpLuby() - Static method in class org.sat4j.minisat.SolverFactory
-
- newMiniSATHeap() - Static method in class org.sat4j.minisat.SolverFactory
-
- newMiniSATHeap(DataStructureFactory) - Static method in class org.sat4j.minisat.SolverFactory
-
- newMiniSATHeapExpSimp() - Static method in class org.sat4j.minisat.SolverFactory
-
- newMiniSATHeapEZSimp() - Static method in class org.sat4j.minisat.SolverFactory
-
- newMinOneSolver() - Static method in class org.sat4j.minisat.SolverFactory
-
- newStatistics() - 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
-
- newVar(int) - Method in class org.sat4j.tools.StatisticsSolver
-
- newVar() - Method in class org.sat4j.tools.StatisticsSolver
-
Deprecated.
- next() - Method in class org.sat4j.reader.EfficientScanner
-
- next() - Method in interface org.sat4j.specs.IteratorInt
-
- nextBigInteger() - Method in class org.sat4j.reader.EfficientScanner
-
- nextFreeVarId(boolean) - Method in class org.sat4j.minisat.constraints.cnf.Lits
-
- nextFreeVarId(boolean) - Method in interface org.sat4j.minisat.core.ILits
-
Ask the solver for a free variable identifier, in Dimacs format (i.e. a
positive number).
- nextFreeVarId(boolean) - Method in class org.sat4j.minisat.core.Solver
-
- nextFreeVarId(boolean) - Method in interface org.sat4j.specs.ISolver
-
Ask the solver for a free variable identifier, in Dimacs format (i.e. a
positive number).
- nextFreeVarId(boolean) - Method in class org.sat4j.tools.DimacsOutputSolver
-
- nextFreeVarId(boolean) - Method in class org.sat4j.tools.DimacsStringSolver
-
- nextFreeVarId(boolean) - Method in class org.sat4j.tools.ManyCore
-
- nextFreeVarId(boolean) - Method in class org.sat4j.tools.SolverDecorator
-
- nextFreeVarId(boolean) - Method in class org.sat4j.tools.StatisticsSolver
-
- nextInt() - Method in class org.sat4j.reader.EfficientScanner
-
To get the next available integer.
- nextLine() - Method in class org.sat4j.reader.EfficientScanner
-
- nextLuby() - Method in class org.sat4j.minisat.restarts.LubyRestarts
-
Computes and return the next value of the luby sequence.
- nextRestartNumberOfConflict() - Method in interface org.sat4j.minisat.core.RestartStrategy
-
Deprecated.
- nextRestartNumberOfConflict() - Method in class org.sat4j.minisat.restarts.ArminRestarts
-
- nextRestartNumberOfConflict() - Method in class org.sat4j.minisat.restarts.FixedPeriodRestarts
-
Deprecated.
- nextRestartNumberOfConflict() - Method in class org.sat4j.minisat.restarts.Glucose21Restarts
-
- nextRestartNumberOfConflict() - Method in class org.sat4j.minisat.restarts.LubyRestarts
-
- nextRestartNumberOfConflict() - Method in class org.sat4j.minisat.restarts.MiniSATRestarts
-
- nextRestartNumberOfConflict() - Method in class org.sat4j.minisat.restarts.NoRestarts
-
- niceParameters(UnitPropagationListener, ILits, IVecInt, int) - Static method in class org.sat4j.minisat.constraints.card.AtLeast
-
- NO_SIMPLIFICATION - Static variable in class org.sat4j.minisat.core.Solver
-
- NoLearningButHeuristics<D extends DataStructureFactory> - Class in org.sat4j.minisat.learning
-
Allows MiniSAT to do backjumping without learning.
- NoLearningButHeuristics() - Constructor for class org.sat4j.minisat.learning.NoLearningButHeuristics
-
- NoLearningNoHeuristics<D extends DataStructureFactory> - Class in org.sat4j.minisat.learning
-
Allows MiniSAT to do backjumping without learning.
- NoLearningNoHeuristics() - Constructor for class org.sat4j.minisat.learning.NoLearningNoHeuristics
-
- nonOptimalMeansSatisfiable() - Method in class org.sat4j.opt.MaxSatDecorator
-
- nonOptimalMeansSatisfiable() - Method in class org.sat4j.opt.MinOneDecorator
-
- nonOptimalMeansSatisfiable() - Method in interface org.sat4j.specs.IOptimizationProblem
-
A suboptimal solution has different meaning depending of the optimization
problem considered.
- nonOptimalMeansSatisfiable() - Method in class org.sat4j.tools.LexicoDecorator
-
- NOR - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader
-
- NoRestarts - Class in org.sat4j.minisat.restarts
-
Disable restarts in the solver.
- NoRestarts() - Constructor for class org.sat4j.minisat.restarts.NoRestarts
-
- normalize() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
-
On normalise la contrainte au sens de Barth
- normalize() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
-
normalize the constraint (cf.
- not(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
-
- not() - Method in class org.sat4j.specs.Lbool
-
boolean negation.
- NOT - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader
-
- not(int, int) - Method in class org.sat4j.tools.GateTranslator
-
Translate y <=> not x into clauses.
- NOTGOOD - Static variable in interface org.sat4j.tools.IVisualizationTool
-
- numberOfCriteria() - Method in class org.sat4j.tools.LexicoDecorator
-
- numberOfInterestingVariables() - Method in class org.sat4j.minisat.orders.VarOrderHeap
-
- numberOfModelsFoundSoFar() - Method in class org.sat4j.tools.ModelIterator
-
To know the number of models already found.
- numberOfSolvers - Variable in class org.sat4j.tools.ManyCore
-
- nVars() - Method in class org.sat4j.minisat.constraints.cnf.Lits
-
- nVars() - Method in interface org.sat4j.minisat.core.ILits
-
to obtain the max id of the variable
- nVars() - Method in class org.sat4j.minisat.core.Solver
-
- nVars() - Method in interface org.sat4j.specs.IProblem
-
To know the number of variables used in the solver as declared by
newVar()
In case the method newVar() has not been used, the method returns the
number of variables used in the solver.
- nVars() - Method in interface org.sat4j.specs.ISolverService
-
Read-Only access to the number of variables declared in the solver.
- nVars() - Method in class org.sat4j.tools.AbstractOutputSolver
-
- nVars() - Method in class org.sat4j.tools.DimacsOutputSolver
-
- nVars() - Method in class org.sat4j.tools.DimacsStringSolver
-
- nVars() - Method in class org.sat4j.tools.ManyCore
-
- nVars() - Method in class org.sat4j.tools.SolverDecorator
-
- nVars() - Method in class org.sat4j.tools.StatisticsSolver
-
- onBackjumpToRootLevel() - Method in interface org.sat4j.minisat.core.RestartStrategy
-
Called when the solver backjumps to the root level.
- onBackjumpToRootLevel() - Method in class org.sat4j.minisat.restarts.ArminRestarts
-
- onBackjumpToRootLevel() - Method in class org.sat4j.minisat.restarts.FixedPeriodRestarts
-
- onBackjumpToRootLevel() - Method in class org.sat4j.minisat.restarts.Glucose21Restarts
-
- onBackjumpToRootLevel() - Method in class org.sat4j.minisat.restarts.LubyRestarts
-
- onBackjumpToRootLevel() - Method in class org.sat4j.minisat.restarts.MiniSATRestarts
-
- onBackjumpToRootLevel() - Method in class org.sat4j.minisat.restarts.NoRestarts
-
- onClauseLearning(Constr) - Method in interface org.sat4j.minisat.core.LearnedConstraintsDeletionStrategy
-
Hook method called when a new clause has just been derived during
conflict analysis.
- onConflictAnalysis(Constr) - Method in interface org.sat4j.minisat.core.LearnedConstraintsDeletionStrategy
-
Hook method called on constraints participating to the conflict analysis.
- onFinishWithAnswer(boolean, boolean, int) - Method in class org.sat4j.tools.ManyCore
-
- onFinishWithAnswer(boolean, boolean, int) - Method in interface org.sat4j.tools.OutcomeListener
-
- onPropagation(Constr) - Method in interface org.sat4j.minisat.core.LearnedConstraintsDeletionStrategy
-
Hook method called when a unit clause is propagated thanks to from.
- onRestart() - Method in interface org.sat4j.minisat.core.RestartStrategy
-
Hook method called when a restart occurs (once the solver has backtracked
to top decision level).
- onRestart() - Method in class org.sat4j.minisat.restarts.ArminRestarts
-
- onRestart() - Method in class org.sat4j.minisat.restarts.FixedPeriodRestarts
-
- onRestart() - Method in class org.sat4j.minisat.restarts.Glucose21Restarts
-
- onRestart() - Method in class org.sat4j.minisat.restarts.LubyRestarts
-
- onRestart() - Method in class org.sat4j.minisat.restarts.MiniSATRestarts
-
- onRestart() - Method in class org.sat4j.minisat.restarts.NoRestarts
-
- onSolutionFound(int[]) - Method in class org.sat4j.tools.CheckMUSSolutionListener
-
- onSolutionFound(IVecInt) - Method in class org.sat4j.tools.CheckMUSSolutionListener
-
- onSolutionFound(int[]) - Method in interface org.sat4j.tools.SolutionFoundListener
-
Callback method called when a new solution is found.
- onSolutionFound(IVecInt) - Method in interface org.sat4j.tools.SolutionFoundListener
-
Callback method called when a new solution is found.
- onUnsatTermination() - Method in class org.sat4j.tools.CheckMUSSolutionListener
-
- onUnsatTermination() - Method in interface org.sat4j.tools.SolutionFoundListener
-
Callback method called when the search is finished (either unsat problem
or no more solutions found)
- optimisationFunction(IVecInt, IVec<BigInteger>, IVecInt) - Method in class org.sat4j.tools.GateTranslator
-
Translate an optimization function into constraints and provides the
binary literals in results.
- OPTIMIZATION - Static variable in interface org.sat4j.ILauncherMode
-
The launcher is in optimization mode: the answer is either SAT,
UPPER_BOUND, OPTIMUM_FOUND, UNSAT or UNKNOWN.
- OPTIMUM_FOUND - Static variable in class org.sat4j.ExitCode
-
- OptToSatAdapter - Class in org.sat4j.tools
-
- OptToSatAdapter(IOptimizationProblem) - Constructor for class org.sat4j.tools.OptToSatAdapter
-
- 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.
- Pair - Class in org.sat4j.minisat.core
-
Utility class to be used to return the two results of a conflict analysis.
- Pair() - Constructor for class org.sat4j.minisat.core.Pair
-
- ParseFormatException - Exception in org.sat4j.reader
-
Exception launched when there is a problem during parsing.
- ParseFormatException() - Constructor for exception org.sat4j.reader.ParseFormatException
-
Constructor for ParseFormatException.
- ParseFormatException(String) - Constructor for exception org.sat4j.reader.ParseFormatException
-
Constructor for ParseFormatException.
- ParseFormatException(String, Throwable) - Constructor for exception org.sat4j.reader.ParseFormatException
-
Constructor for ParseFormatException.
- ParseFormatException(Throwable) - Constructor for exception org.sat4j.reader.ParseFormatException
-
Constructor for ParseFormatException.
- parseInstance(InputStream) - Method in class org.sat4j.reader.AAGReader
-
- parseInstance(InputStream) - Method in class org.sat4j.reader.AIGReader
-
- parseInstance(InputStream) - Method in class org.sat4j.reader.DimacsReader
-
- parseInstance(String) - Method in class org.sat4j.reader.InstanceReader
-
- parseInstance(InputStream) - Method in class org.sat4j.reader.InstanceReader
-
- parseInstance(InputStream) - Method in class org.sat4j.reader.JSONReader
-
- parseInstance(InputStream) - Method in class org.sat4j.reader.LecteurDimacs
-
- parseInstance(String) - Method in class org.sat4j.reader.Reader
-
This is the usual method to feed a solver with a benchmark.
- parseInstance(InputStream) - Method in class org.sat4j.reader.Reader
-
Read a file from a stream.
- parseInstance(Reader) - Method in class org.sat4j.reader.Reader
-
Deprecated.
- parseInstance(int[], int[], int[][], int) - Method in class org.sat4j.tools.DimacsArrayReader
-
- parseString(String) - Method in class org.sat4j.reader.JSONReader
-
- PARSING_ERROR - Static variable in exception org.sat4j.reader.ParseFormatException
-
- PercentLengthLearning<D extends DataStructureFactory> - Class in org.sat4j.minisat.learning
-
Selects the constraints to learn according to its length as a percentage of
the total number of variables in the solver universe.
- PercentLengthLearning() - Constructor for class org.sat4j.minisat.learning.PercentLengthLearning
-
- PercentLengthLearning(int) - Constructor for class org.sat4j.minisat.learning.PercentLengthLearning
-
- PhaseCachingAutoEraseStrategy - Class in org.sat4j.minisat.orders
-
- PhaseCachingAutoEraseStrategy() - Constructor for class org.sat4j.minisat.orders.PhaseCachingAutoEraseStrategy
-
- PhaseInLastLearnedClauseSelectionStrategy - Class in org.sat4j.minisat.orders
-
Keeps record of the phase of a variable in the lastest recorded clause.
- PhaseInLastLearnedClauseSelectionStrategy() - Constructor for class org.sat4j.minisat.orders.PhaseInLastLearnedClauseSelectionStrategy
-
- phaseStrategy - Variable in class org.sat4j.minisat.orders.VarOrderHeap
-
- pLiterals - Variable in class org.sat4j.tools.AbstractMinimalModel
-
- Policy - Class in org.sat4j.tools.encoding
-
This class allows the use of different encodings for different cardinality
constraints.
- Policy() - Constructor for class org.sat4j.tools.encoding.Policy
-
- pop() - Method in class org.sat4j.core.ReadOnlyVec
-
- pop() - Method in class org.sat4j.core.ReadOnlyVecInt
-
- pop() - Method in class org.sat4j.core.Vec
-
Pop the last element on the stack.
- pop() - Method in class org.sat4j.core.VecInt
-
depile le dernier element du vecteur.
- pop() - Method in interface org.sat4j.specs.IVec
-
Pop the last element on the stack.
- pop() - Method in interface org.sat4j.specs.IVecInt
-
depile le dernier element du vecteur.
- positiveLiterals(ISolver) - Static method in class org.sat4j.tools.AbstractMinimalModel
-
- PositiveLiteralSelectionStrategy - Class in org.sat4j.minisat.orders
-
- PositiveLiteralSelectionStrategy() - Constructor for class org.sat4j.minisat.orders.PositiveLiteralSelectionStrategy
-
- posLit(int) - Static method in class org.sat4j.core.LiteralsUtils
-
Returns the positive literal associated with a variable.
- prevboolmodel - Variable in class org.sat4j.tools.LexicoDecorator
-
- prevfullmodel - Variable in class org.sat4j.tools.LexicoDecorator
-
- prime - Variable in class org.sat4j.AbstractLauncher
-
- primeImplicant() - Method in class org.sat4j.minisat.core.Solver
-
- primeImplicant(int) - Method in class org.sat4j.minisat.core.Solver
-
- primeImplicant() - Method in interface org.sat4j.specs.IProblem
-
Provide a prime implicant, i.e. a set of literal that is sufficient to
satisfy all constraints of the problem.
- primeImplicant(int) - Method in interface org.sat4j.specs.IProblem
-
- primeImplicant() - Method in class org.sat4j.tools.AbstractOutputSolver
-
- primeImplicant(int) - Method in class org.sat4j.tools.DimacsOutputSolver
-
- primeImplicant(int) - Method in class org.sat4j.tools.DimacsStringSolver
-
- primeImplicant() - Method in class org.sat4j.tools.ManyCore
-
- primeImplicant(int) - Method in class org.sat4j.tools.ManyCore
-
- primeImplicant() - Method in class org.sat4j.tools.ModelIterator
-
- primeImplicant() - Method in class org.sat4j.tools.SolverDecorator
-
- primeImplicant(int) - Method in class org.sat4j.tools.SolverDecorator
-
- primeImplicant() - Method in class org.sat4j.tools.StatisticsSolver
-
- primeImplicant(int) - Method in class org.sat4j.tools.StatisticsSolver
-
- printInfos(PrintWriter) - Method in class org.sat4j.minisat.core.Solver
-
- printInfos(PrintWriter, String) - Method in class org.sat4j.minisat.core.Solver
-
- printInfos(PrintWriter, String) - Method in interface org.sat4j.specs.IProblem
-
Deprecated.
- printInfos(PrintWriter) - Method in interface org.sat4j.specs.IProblem
-
To print additional informations regarding the problem.
- printInfos(PrintWriter, String) - Method in class org.sat4j.tools.AbstractOutputSolver
-
- printInfos(PrintWriter) - Method in class org.sat4j.tools.DimacsOutputSolver
-
- printInfos(PrintWriter) - Method in class org.sat4j.tools.DimacsStringSolver
-
- printInfos(PrintWriter, String) - Method in class org.sat4j.tools.ManyCore
-
- printInfos(PrintWriter) - Method in class org.sat4j.tools.ManyCore
-
- printInfos(PrintWriter, String) - Method in class org.sat4j.tools.SolverDecorator
-
- printInfos(PrintWriter) - Method in class org.sat4j.tools.SolverDecorator
-
- printInfos(PrintWriter, String) - Method in class org.sat4j.tools.StatisticsSolver
-
Deprecated.
- printInfos(PrintWriter) - Method in class org.sat4j.tools.StatisticsSolver
-
- printLearntClausesInfos(PrintWriter, String) - Method in class org.sat4j.minisat.core.Solver
-
- printStat(PrintWriter, String) - Method in interface org.sat4j.minisat.core.IOrder
-
Display statistics regarding the heuristics.
- printStat(PrintStream, String) - Method in class org.sat4j.minisat.core.Solver
-
- printStat(PrintWriter) - Method in class org.sat4j.minisat.core.Solver
-
- printStat(PrintWriter, String) - Method in class org.sat4j.minisat.core.Solver
-
- printStat(PrintWriter, String) - Method in class org.sat4j.minisat.core.SolverStats
-
- printStat(PrintWriter, String) - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
-
- printStat(PrintWriter, String) - Method in class org.sat4j.minisat.orders.TabuListDecorator
-
- printStat(PrintWriter, String) - Method in class org.sat4j.minisat.orders.VarOrderHeap
-
- printStat(PrintStream, String) - Method in interface org.sat4j.specs.ISolver
-
Deprecated.
- printStat(PrintWriter, String) - Method in interface org.sat4j.specs.ISolver
-
Deprecated.
using the prefix does no longer makes sense because the
solver owns it.
- printStat(PrintWriter) - Method in interface org.sat4j.specs.ISolver
-
Display statistics to the given output writer
- printStat(PrintStream, String) - Method in class org.sat4j.tools.AbstractOutputSolver
-
- printStat(PrintWriter, String) - Method in class org.sat4j.tools.AbstractOutputSolver
-
- printStat(PrintWriter) - Method in class org.sat4j.tools.DimacsOutputSolver
-
- printStat(PrintWriter) - Method in class org.sat4j.tools.DimacsStringSolver
-
- printStat(PrintStream, String) - Method in class org.sat4j.tools.ManyCore
-
Deprecated.
- printStat(PrintWriter, String) - Method in class org.sat4j.tools.ManyCore
-
- printStat(PrintWriter) - Method in class org.sat4j.tools.ManyCore
-
- printStat(PrintStream, String) - Method in class org.sat4j.tools.SolverDecorator
-
Deprecated.
- printStat(PrintWriter, String) - Method in class org.sat4j.tools.SolverDecorator
-
- printStat(PrintWriter) - Method in class org.sat4j.tools.SolverDecorator
-
- printStat(PrintStream, String) - Method in class org.sat4j.tools.StatisticsSolver
-
Deprecated.
- printStat(PrintWriter, String) - Method in class org.sat4j.tools.StatisticsSolver
-
Deprecated.
- printStat(PrintWriter) - Method in class org.sat4j.tools.StatisticsSolver
-
- problem - Variable in class org.sat4j.AbstractLauncher
-
- Product - Class in org.sat4j.tools.encoding
-
Implementation of product encoding for at most one and at most k constraints.
- Product() - Constructor for class org.sat4j.tools.encoding.Product
-
- Propagatable - Interface in org.sat4j.minisat.core
-
This interface is to be implemented by the classes wanted to be notified of
the falsification of a literal.
- propagate(UnitPropagationListener, int) - Method in class org.sat4j.minisat.constraints.card.AtLeast
-
- propagate(UnitPropagationListener, int) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
-
Propagation de la valeur de v?
- propagate(UnitPropagationListener, int) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
-
propagates the value of a falsified literal
- propagate(UnitPropagationListener, int) - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
-
- propagate(UnitPropagationListener, int) - Method in class org.sat4j.minisat.constraints.cnf.HTClause
-
- propagate(UnitPropagationListener, int) - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
-
- propagate(UnitPropagationListener, int) - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
-
- propagate(UnitPropagationListener, int) - Method in class org.sat4j.minisat.constraints.cnf.WLClause
-
- propagate(UnitPropagationListener, int) - Method in interface org.sat4j.minisat.core.Propagatable
-
Propagate the truth value of a literal in constraints in which that
literal is falsified.
- propagate() - Method in class org.sat4j.minisat.core.Solver
-
- propagating(int, IConstr) - Method in interface org.sat4j.specs.SearchListener
-
Unit propagation
- propagating(int, IConstr) - Method in class org.sat4j.tools.DotSearchTracing
-
- propagating(int, IConstr) - Method in class org.sat4j.tools.MultiTracing
-
- propagating(int, IConstr) - Method in class org.sat4j.tools.SearchListenerAdapter
-
- propagating(int, IConstr) - Method in class org.sat4j.tools.SpeedTracing
-
- propagating(int, IConstr) - Method in class org.sat4j.tools.TextOutputTracing
-
- propagations - Variable in class org.sat4j.minisat.core.SolverStats
-
- 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
-
- RAND - Static variable in class org.sat4j.minisat.orders.RandomLiteralSelectionStrategy
-
- RandomAccessModel - Interface in org.sat4j.specs
-
That interface allows to efficiently retrieve the truth value of a given
variable in the solver.
- RandomLiteralSelectionStrategy - Class in org.sat4j.minisat.orders
-
The variable selection strategy randomly picks one phase, either positive or
negative.
- RandomLiteralSelectionStrategy() - Constructor for class org.sat4j.minisat.orders.RandomLiteralSelectionStrategy
-
- RandomWalkDecorator - Class in org.sat4j.minisat.orders
-
- RandomWalkDecorator(VarOrderHeap) - Constructor for class org.sat4j.minisat.orders.RandomWalkDecorator
-
- RandomWalkDecorator(VarOrderHeap, double) - Constructor for class org.sat4j.minisat.orders.RandomWalkDecorator
-
- readConstrs() - Method in class org.sat4j.reader.DimacsReader
-
- reader - Variable in class org.sat4j.AbstractLauncher
-
- Reader - Class in org.sat4j.reader
-
A reader is responsible to feed an ISolver from a text file and to convert
the model found by the solver to a textual representation.
- Reader() - Constructor for class org.sat4j.reader.Reader
-
- ReadOnlyVec<T> - Class in org.sat4j.core
-
Utility class to allow Read Only access to an IVec.
- ReadOnlyVec(IVec<T>) - Constructor for class org.sat4j.core.ReadOnlyVec
-
- ReadOnlyVecInt - Class in org.sat4j.core
-
Utility class to allow Read Only access only to an IVecInt.
- ReadOnlyVecInt(IVecInt) - Constructor for class org.sat4j.core.ReadOnlyVecInt
-
- readProblem(String) - Method in class org.sat4j.AbstractLauncher
-
Reads a problem file from the command line.
- readProblemLine() - Method in class org.sat4j.reader.DimacsReader
-
- readProblemLine() - Method in class org.sat4j.reader.GroupedCNFReader
-
- realNumberOfVariables() - Method in class org.sat4j.minisat.core.Solver
-
- realNumberOfVariables() - Method in interface org.sat4j.specs.ISolver
-
Retrieve the real number of variables used in the solver.
- realNumberOfVariables() - Method in class org.sat4j.tools.DimacsOutputSolver
-
- realNumberOfVariables() - Method in class org.sat4j.tools.DimacsStringSolver
-
- realNumberOfVariables() - Method in class org.sat4j.tools.ManyCore
-
- realNumberOfVariables() - Method in class org.sat4j.tools.SolverDecorator
-
- realNumberOfVariables() - Method in class org.sat4j.tools.StatisticsSolver
-
- realnVars() - Method in class org.sat4j.minisat.constraints.cnf.Lits
-
- realnVars() - Method in interface org.sat4j.minisat.core.ILits
-
to obtain the real number of variables appearing in the formula
- reason - Variable in class org.sat4j.minisat.core.Pair
-
- reduce(IVec<Constr>) - Method in interface org.sat4j.minisat.core.LearnedConstraintsDeletionStrategy
-
Hook method called when the solver wants to reduce the set of learned
clauses.
- reduceDB() - Method in class org.sat4j.minisat.core.Solver
-
- reduceddb - Variable in class org.sat4j.minisat.core.SolverStats
-
- reducedliterals - Variable in class org.sat4j.minisat.core.SolverStats
-
- register() - Method in class org.sat4j.minisat.constraints.card.AtLeast
-
- register() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
-
- register() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
-
- register() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
-
- register() - Method in class org.sat4j.minisat.constraints.cnf.LearntHTClause
-
- register() - Method in class org.sat4j.minisat.constraints.cnf.LearntWLClause
-
- register() - Method in class org.sat4j.minisat.constraints.cnf.OriginalHTClause
-
- register() - Method in class org.sat4j.minisat.constraints.cnf.OriginalWLClause
-
- register() - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
-
- register() - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
-
- register() - Method in interface org.sat4j.minisat.core.Constr
-
Register the constraint to the solver.
- registerLiteral(int) - Method in class org.sat4j.minisat.core.Solver
-
- registerLiteral(int) - Method in interface org.sat4j.specs.ISolver
-
Tell the solver to consider that the literal is in the CNF.
- registerLiteral(int) - Method in class org.sat4j.tools.DimacsOutputSolver
-
- registerLiteral(int) - Method in class org.sat4j.tools.DimacsStringSolver
-
- registerLiteral(int) - Method in class org.sat4j.tools.ManyCore
-
- registerLiteral(int) - Method in class org.sat4j.tools.SolverDecorator
-
- registerLiteral(int) - Method in class org.sat4j.tools.StatisticsSolver
-
- RemiUtils - Class in org.sat4j.tools
-
Class dedicated to Remi Coletta utility methods :-)
- remove(T) - Method in class org.sat4j.core.ReadOnlyVec
-
- remove(int) - Method in class org.sat4j.core.ReadOnlyVecInt
-
- remove(T) - Method in class org.sat4j.core.Vec
-
Remove an element that belongs to the Vector.
- remove(int) - Method in class org.sat4j.core.VecInt
-
Enleve un element qui se trouve dans le vecteur!!!
- remove(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.card.AtLeast
-
- remove(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
-
- remove(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
-
Removes a constraint from the solver
- remove(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
-
- remove(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.HTClause
-
- remove(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
-
- remove(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
-
- remove(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.WLClause
-
- remove(UnitPropagationListener) - Method in interface org.sat4j.minisat.core.Constr
-
Remove a constraint from the solver.
- remove(T) - Method in interface org.sat4j.specs.IVec
-
Enleve un element qui se trouve dans le vecteur!!!
- remove(int) - Method in interface org.sat4j.specs.IVecInt
-
Enleve un element qui se trouve dans le vecteur!!!
- removeConstr(IConstr) - Method in class org.sat4j.minisat.core.Solver
-
- removeConstr(IConstr) - Method in interface org.sat4j.specs.ISolver
-
Remove a constraint returned by one of the add method from the solver.
- removeConstr(IConstr) - Method in class org.sat4j.tools.AbstractOutputSolver
-
- removeConstr(IConstr) - Method in class org.sat4j.tools.ManyCore
-
- removeConstr(IConstr) - Method in class org.sat4j.tools.SolverDecorator
-
- removeConstr(IConstr) - Method in class org.sat4j.tools.StatisticsSolver
-
- removeConstr(IConstr) - Method in class org.sat4j.tools.xplain.Xplain
-
- removeFrom(ISolver) - Method in class org.sat4j.core.ConstrGroup
-
- removeSubsumedConstr(IConstr) - Method in class org.sat4j.minisat.core.Solver
-
- removeSubsumedConstr(IConstr) - Method in interface org.sat4j.specs.ISolver
-
Remove a constraint returned by one of the add method from the solver
that is subsumed by a constraint already in the solver or to be added to
the solver.
- removeSubsumedConstr(IConstr) - Method in interface org.sat4j.specs.ISolverService
-
Remove a constraint returned by one of the add method from the solver
that is subsumed by a constraint already in the solver or to be added to
the solver.
- removeSubsumedConstr(IConstr) - Method in class org.sat4j.tools.AbstractOutputSolver
-
- removeSubsumedConstr(IConstr) - Method in class org.sat4j.tools.ManyCore
-
- removeSubsumedConstr(IConstr) - Method in class org.sat4j.tools.SolverDecorator
-
- removeSubsumedConstr(IConstr) - Method in class org.sat4j.tools.StatisticsSolver
-
- removeSubsumedConstr(IConstr) - Method in class org.sat4j.tools.xplain.Xplain
-
- rescaleBy(double) - Method in class org.sat4j.minisat.constraints.card.AtLeast
-
- rescaleBy(double) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
-
Permet le r??
- rescaleBy(double) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
-
Rescales the activity value of the constraint
- rescaleBy(double) - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
-
- rescaleBy(double) - Method in class org.sat4j.minisat.constraints.cnf.HTClause
-
- rescaleBy(double) - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
-
- rescaleBy(double) - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
-
- rescaleBy(double) - Method in class org.sat4j.minisat.constraints.cnf.WLClause
-
- rescaleBy(double) - Method in interface org.sat4j.minisat.core.Constr
-
Rescale the clause activity by a value.
- reset() - Method in class org.sat4j.minisat.constraints.AbstractDataStructureFactory
-
- reset(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
-
- reset() - Method in interface org.sat4j.minisat.core.ConflictTimer
-
- reset() - Method in class org.sat4j.minisat.core.ConflictTimerAdapter
-
- reset() - Method in class org.sat4j.minisat.core.ConflictTimerContainer
-
- reset() - Method in interface org.sat4j.minisat.core.DataStructureFactory
-
- reset(int) - Method in interface org.sat4j.minisat.core.ILits
-
Reset a literal in the vocabulary.
- reset() - Method in class org.sat4j.minisat.core.Solver
-
- reset() - Method in class org.sat4j.minisat.core.SolverStats
-
- reset() - Method in class org.sat4j.minisat.restarts.ArminRestarts
-
- reset() - Method in class org.sat4j.minisat.restarts.FixedPeriodRestarts
-
- reset() - Method in class org.sat4j.minisat.restarts.Glucose21Restarts
-
- reset() - Method in class org.sat4j.minisat.restarts.LubyRestarts
-
- reset() - Method in class org.sat4j.minisat.restarts.MiniSATRestarts
-
- reset() - Method in class org.sat4j.minisat.restarts.NoRestarts
-
- reset() - Method in class org.sat4j.opt.MaxSatDecorator
-
- reset() - Method in class org.sat4j.opt.MinOneDecorator
-
- reset() - Method in interface org.sat4j.specs.ISolver
-
Clean up the internal state of the solver.
- reset() - Method in class org.sat4j.tools.DimacsOutputSolver
-
- reset() - Method in class org.sat4j.tools.DimacsStringSolver
-
- reset() - Method in class org.sat4j.tools.ManyCore
-
- reset() - Method in class org.sat4j.tools.ModelIterator
-
- reset() - Method in class org.sat4j.tools.OptToSatAdapter
-
- reset() - Method in class org.sat4j.tools.SolverDecorator
-
- reset() - Method in class org.sat4j.tools.StatisticsSolver
-
- resetPool() - Method in class org.sat4j.minisat.constraints.cnf.Lits
-
- resetPool() - Method in interface org.sat4j.minisat.core.ILits
-
reset the vocabulary.
- restarting() - Method in interface org.sat4j.specs.SearchListener
-
The solver restarts the search.
- restarting() - Method in class org.sat4j.tools.ConflictDepthTracing
-
- restarting() - Method in class org.sat4j.tools.ConflictLevelTracing
-
- restarting() - Method in class org.sat4j.tools.DecisionTracing
-
- restarting() - Method in class org.sat4j.tools.HeuristicsTracing
-
- restarting() - Method in class org.sat4j.tools.LearnedClausesSizeTracing
-
- restarting() - Method in class org.sat4j.tools.LearnedTracing
-
- restarting() - Method in class org.sat4j.tools.MultiTracing
-
- restarting() - Method in class org.sat4j.tools.SearchListenerAdapter
-
- restarting() - Method in class org.sat4j.tools.SpeedTracing
-
- restarting() - Method in class org.sat4j.tools.TextOutputTracing
-
- RestartStrategy - Interface in org.sat4j.minisat.core
-
Abstraction allowing to choose various restarts strategies.
- rootLevel - Variable in class org.sat4j.minisat.core.Solver
-
position of assumptions before starting the search.
- rootSimplifications - Variable in class org.sat4j.minisat.core.SolverStats
-
- RSATLastLearnedClausesPhaseSelectionStrategy - Class in org.sat4j.minisat.orders
-
Keeps track of the phase of the latest assignment.
- RSATLastLearnedClausesPhaseSelectionStrategy() - Constructor for class org.sat4j.minisat.orders.RSATLastLearnedClausesPhaseSelectionStrategy
-
- RSATPhaseSelectionStrategy - Class in org.sat4j.minisat.orders
-
Keeps track of the phase of the latest assignment.
- RSATPhaseSelectionStrategy() - Constructor for class org.sat4j.minisat.orders.RSATPhaseSelectionStrategy
-
- run(String[]) - Method in class org.sat4j.AbstractLauncher
-
- run() - Method in class org.sat4j.minisat.core.ConflictTimerAdapter
-
- run(String[]) - Method in class org.sat4j.MUSLauncher
-
- sanityCheck(IVecInt, ILits, UnitPropagationListener) - Static method in class org.sat4j.minisat.constraints.cnf.Clauses
-
Perform some sanity check before constructing a clause a) if a literal is
assigned true, return null (the clause is satisfied) b) if a literal is
assigned false, remove it c) if a clause contains a literal and its
opposite (tautology) return null d) remove duplicate literals e) if the
clause is empty, return null f) if the clause if unit, transmit it to the
object responsible for unit propagation
- SATISFIABLE - Static variable in class org.sat4j.ExitCode
-
- satisfies(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
-
- satisfies(int) - Method in interface org.sat4j.minisat.core.ILits
-
Satisfies a boolean variable (truth value is TRUE).
- scanner - Variable in class org.sat4j.reader.DimacsReader
-
- SearchEnumeratorListener - Class in org.sat4j.tools
-
That class allows to iterate over the models from the inside: conflicts are
created to ask the solver to backtrack.
- SearchEnumeratorListener(SolutionFoundListener) - Constructor for class org.sat4j.tools.SearchEnumeratorListener
-
- SearchListener<S extends ISolverService> - Interface in org.sat4j.specs
-
Interface to the solver main steps.
- SearchListenerAdapter<S extends ISolverService> - Class in org.sat4j.tools
-
- SearchListenerAdapter() - Constructor for class org.sat4j.tools.SearchListenerAdapter
-
- SearchMinOneListener - Class in org.sat4j.tools
-
That class allows to iterate over the models from the inside: conflicts are
created to ask the solver to backtrack.
- SearchMinOneListener(SolutionFoundListener) - Constructor for class org.sat4j.tools.SearchMinOneListener
-
- SearchParams - Class in org.sat4j.minisat.core
-
Some parameters used during the search.
- SearchParams() - Constructor for class org.sat4j.minisat.core.SearchParams
-
Default search parameters.
- SearchParams(int) - Constructor for class org.sat4j.minisat.core.SearchParams
-
- SearchParams(double, int) - Constructor for class org.sat4j.minisat.core.SearchParams
-
- SearchParams(double, double, double, int) - Constructor for class org.sat4j.minisat.core.SearchParams
-
- select() - Method in interface org.sat4j.minisat.core.IOrder
-
Selects the next "best" unassigned literal.
- select(int) - Method in interface org.sat4j.minisat.core.IPhaseSelectionStrategy
-
selects the phase of the variable according to a phase selection
strategy.
- select(int) - Method in class org.sat4j.minisat.orders.NegativeLiteralSelectionStrategy
-
- select(int) - Method in class org.sat4j.minisat.orders.PositiveLiteralSelectionStrategy
-
- select() - Method in class org.sat4j.minisat.orders.PureOrder
-
- select(int) - Method in class org.sat4j.minisat.orders.RandomLiteralSelectionStrategy
-
- select() - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
-
- select() - Method in class org.sat4j.minisat.orders.TabuListDecorator
-
- select() - Method in class org.sat4j.minisat.orders.VarOrderHeap
-
Selectionne une nouvelle variable, non affectee, ayant l'activite la plus
elevee.
- Sequential - Class in org.sat4j.tools.encoding
-
Implementation of the sequential encoding for the at most k constraint.
- Sequential() - Constructor for class org.sat4j.tools.encoding.Sequential
-
- set(int, T) - Method in class org.sat4j.core.ReadOnlyVec
-
- set(int, int) - Method in class org.sat4j.core.ReadOnlyVecInt
-
- set(int, T) - Method in class org.sat4j.core.Vec
-
- set(int, int) - Method in class org.sat4j.core.VecInt
-
- set(int, T) - Method in interface org.sat4j.specs.IVec
-
- set(int, int) - Method in interface org.sat4j.specs.IVecInt
-
- setActivity(double) - Method in class org.sat4j.minisat.constraints.card.AtLeast
-
- setActivity(double) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
-
- setActivity(double) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
-
- setActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.LearntBinaryClause
-
- setActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.LearntHTClause
-
- setActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.OriginalBinaryClause
-
- setActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.OriginalHTClause
-
- setActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
-
- setActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
-
- setActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.WLClause
-
- setActivity(double) - Method in interface org.sat4j.minisat.core.Constr
-
Set the activity at a specific value
- setActivityPercent(double) - Method in class org.sat4j.minisat.learning.ActiveLearning
-
- setAtLeastKEncoding(EncodingStrategyAdapter) - Method in class org.sat4j.tools.encoding.Policy
-
- setAtLeastKEncoding(EncodingStrategy) - Method in class org.sat4j.tools.encoding.Policy
-
- setAtLeastOneEncoding(EncodingStrategyAdapter) - Method in class org.sat4j.tools.encoding.Policy
-
- setAtLeastOneEncoding(EncodingStrategy) - Method in class org.sat4j.tools.encoding.Policy
-
- setAtMostKEncoding(EncodingStrategyAdapter) - Method in class org.sat4j.tools.encoding.Policy
-
- setAtMostKEncoding(EncodingStrategy) - Method in class org.sat4j.tools.encoding.Policy
-
- setAtMostOneEncoding(EncodingStrategyAdapter) - Method in class org.sat4j.tools.encoding.Policy
-
- setAtMostOneEncoding(EncodingStrategy) - Method in class org.sat4j.tools.encoding.Policy
-
- setBound(int) - Method in class org.sat4j.minisat.learning.FixedLengthLearning
-
- setBound(int) - Method in class org.sat4j.minisat.learning.PercentLengthLearning
-
- setBounds(int) - Method in class org.sat4j.minisat.core.Heap
-
- setClaDecay(double) - Method in class org.sat4j.minisat.core.SearchParams
-
- setConflictBoundIncFactor(double) - Method in class org.sat4j.minisat.core.SearchParams
-
- setDataStructureFactory(D) - Method in interface org.sat4j.minisat.core.ICDCL
-
Change the internal representation of the constraints.
- setDataStructureFactory(D) - Method in class org.sat4j.minisat.core.Solver
-
- setDataStructureFactory(DataStructureFactory) - Method in class org.sat4j.minisat.learning.MiniSATLearning
-
- setDBSimplificationAllowed(boolean) - Method in class org.sat4j.minisat.core.Solver
-
- setDBSimplificationAllowed(boolean) - Method in interface org.sat4j.specs.ISolver
-
Set whether the solver is allowed to simplify the formula by propagating
the truth value of top level satisfied variables.
- setDBSimplificationAllowed(boolean) - Method in class org.sat4j.tools.AbstractOutputSolver
-
- setDBSimplificationAllowed(boolean) - Method in class org.sat4j.tools.ManyCore
-
- setDBSimplificationAllowed(boolean) - Method in class org.sat4j.tools.SolverDecorator
-
- setDBSimplificationAllowed(boolean) - Method in class org.sat4j.tools.StatisticsSolver
-
- setDisplaySolutionLine(boolean) - Method in class org.sat4j.AbstractLauncher
-
To change the display so that solution line appears or not.
- setDisplaySolutionLine(boolean) - Method in class org.sat4j.AbstractOptimizationLauncher
-
Deprecated.
- setExactlyKEncoding(EncodingStrategyAdapter) - Method in class org.sat4j.tools.encoding.Policy
-
- setExactlyKEncoding(EncodingStrategy) - Method in class org.sat4j.tools.encoding.Policy
-
- setExactlyOneEncoding(EncodingStrategyAdapter) - Method in class org.sat4j.tools.encoding.Policy
-
- setExactlyOneEncoding(EncodingStrategy) - Method in class org.sat4j.tools.encoding.Policy
-
- setExitCode(ExitCode) - Method in class org.sat4j.AbstractLauncher
-
Change the value of the exit code in the Launcher
- setExitCode(ExitCode) - Method in interface org.sat4j.ILauncherMode
-
Allow to set a specific exit code to the launcher (in case of trivial
unsatisfiability for instance).
- setExpectedNumberOfClauses(int) - Method in class org.sat4j.minisat.core.Solver
-
- setExpectedNumberOfClauses(int) - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
-
- setExpectedNumberOfClauses(int) - Method in class org.sat4j.opt.MaxSatDecorator
-
- setExpectedNumberOfClauses(int) - Method in interface org.sat4j.specs.ISolver
-
To inform the solver of the expected number of clauses to read.
- setExpectedNumberOfClauses(int) - Method in class org.sat4j.tools.DimacsOutputSolver
-
- setExpectedNumberOfClauses(int) - Method in class org.sat4j.tools.DimacsStringSolver
-
- setExpectedNumberOfClauses(int) - Method in class org.sat4j.tools.ManyCore
-
- setExpectedNumberOfClauses(int) - Method in class org.sat4j.tools.SolverDecorator
-
- setExpectedNumberOfClauses(int) - Method in class org.sat4j.tools.StatisticsSolver
-
- setFactor(int) - Method in class org.sat4j.minisat.restarts.LubyRestarts
-
- setFilename(String) - Method in class org.sat4j.tools.FileBasedVisualizationTool
-
- setIncomplete(boolean) - Method in class org.sat4j.AbstractLauncher
-
- setIncomplete(boolean) - Method in class org.sat4j.AbstractOptimizationLauncher
-
Deprecated.
- setIncomplete(boolean) - Method in interface org.sat4j.ILauncherMode
-
Allows the launcher to specifically return an upper bound of the optimal
solution in case of a time out (for maxsat competitions for instance).
- setInitConflictBound(int) - Method in class org.sat4j.minisat.core.SearchParams
-
- setKeepSolverHot(boolean) - Method in class org.sat4j.minisat.core.Solver
-
- setKeepSolverHot(boolean) - Method in interface org.sat4j.specs.ISolver
-
Changed the behavior of the SAT solver heuristics between successive
calls.
- setKeepSolverHot(boolean) - Method in class org.sat4j.tools.AbstractOutputSolver
-
- setKeepSolverHot(boolean) - Method in class org.sat4j.tools.ManyCore
-
- setKeepSolverHot(boolean) - Method in class org.sat4j.tools.SolverDecorator
-
- setKeepSolverHot(boolean) - Method in class org.sat4j.tools.StatisticsSolver
-
- setLastConstr(IConstr) - Method in class org.sat4j.tools.FullClauseSelectorSolver
-
- setLauncherMode(ILauncherMode) - Method in class org.sat4j.AbstractLauncher
-
- setLearnedConstraintsDeletionStrategy(LearnedConstraintsDeletionStrategy) - Method in interface org.sat4j.minisat.core.ICDCL
-
- setLearnedConstraintsDeletionStrategy(ConflictTimer, LearnedConstraintsEvaluationType) - Method in interface org.sat4j.minisat.core.ICDCL
-
- setLearnedConstraintsDeletionStrategy(LearnedConstraintsEvaluationType) - Method in interface org.sat4j.minisat.core.ICDCL
-
- setLearnedConstraintsDeletionStrategy(LearnedConstraintsDeletionStrategy) - Method in class org.sat4j.minisat.core.Solver
-
- setLearnedConstraintsDeletionStrategy(ConflictTimer, LearnedConstraintsEvaluationType) - Method in class org.sat4j.minisat.core.Solver
-
- setLearnedConstraintsDeletionStrategy(LearnedConstraintsEvaluationType) - Method in class org.sat4j.minisat.core.Solver
-
- setLearner(Learner) - Method in class org.sat4j.minisat.constraints.AbstractDataStructureFactory
-
- setLearner(Learner) - Method in interface org.sat4j.minisat.core.DataStructureFactory
-
- setLearner(LearningStrategy<D>) - Method in interface org.sat4j.minisat.core.ICDCL
-
Deprecated.
renamed into setLearningStrategy()
- setLearner(LearningStrategy<D>) - Method in class org.sat4j.minisat.core.Solver
-
- setLearningStrategy(LearningStrategy<D>) - Method in interface org.sat4j.minisat.core.ICDCL
-
Allow to change the learning strategy, i.e. to decide which
clauses/constraints should be learned by the solver after conflict
analysis.
- setLearningStrategy(LearningStrategy<D>) - Method in class org.sat4j.minisat.core.Solver
-
- setLearnt() - Method in class org.sat4j.minisat.constraints.card.AtLeast
-
- setLearnt() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
-
- setLearnt() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
-
- setLearnt() - Method in class org.sat4j.minisat.constraints.cnf.LearntBinaryClause
-
- setLearnt() - Method in class org.sat4j.minisat.constraints.cnf.LearntHTClause
-
- setLearnt() - Method in class org.sat4j.minisat.constraints.cnf.LearntWLClause
-
- setLearnt() - Method in class org.sat4j.minisat.constraints.cnf.OriginalBinaryClause
-
- setLearnt() - Method in class org.sat4j.minisat.constraints.cnf.OriginalHTClause
-
- setLearnt() - Method in class org.sat4j.minisat.constraints.cnf.OriginalWLClause
-
- setLearnt() - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
-
- setLearnt() - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
-
- setLearnt() - Method in interface org.sat4j.minisat.core.Constr
-
Mark a constraint as learnt.
- setLevel(int, int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
-
- setLevel(int, int) - Method in interface org.sat4j.minisat.core.ILits
-
Sets the decision level of a literal.
- setLimit(int) - Method in class org.sat4j.minisat.learning.ActiveLearning
-
- setLimit(int) - Method in class org.sat4j.minisat.learning.PercentLengthLearning
-
- setLits(ILits) - Method in interface org.sat4j.minisat.core.IOrder
-
Method used to provide an easy access the the solver vocabulary.
- setLits(ILits) - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
-
- setLits(ILits) - Method in class org.sat4j.minisat.orders.TabuListDecorator
-
- setLits(ILits) - Method in class org.sat4j.minisat.orders.VarOrderHeap
-
- setLogger(ILogAble) - Method in interface org.sat4j.minisat.core.ICDCL
-
- setLogger(ILogAble) - Method in class org.sat4j.minisat.core.Solver
-
- setLogPrefix(String) - Method in class org.sat4j.minisat.core.Solver
-
- setLogPrefix(String) - Method in interface org.sat4j.specs.ISolver
-
Set the prefix used to display information.
- setLogPrefix(String) - Method in class org.sat4j.tools.AbstractOutputSolver
-
- setLogPrefix(String) - Method in class org.sat4j.tools.ManyCore
-
- setLogPrefix(String) - Method in class org.sat4j.tools.SolverDecorator
-
- setLogPrefix(String) - Method in class org.sat4j.tools.StatisticsSolver
-
- setLogWriter(PrintWriter) - Method in class org.sat4j.AbstractLauncher
-
To change the output stream on which statistics are displayed.
- setMaxLength(int) - Method in class org.sat4j.minisat.learning.FixedLengthLearning
-
- setMinimizationStrategy(MinimizationStrategy) - Method in interface org.sat4j.tools.xplain.Explainer
-
- setMinimizationStrategy(MinimizationStrategy) - Method in class org.sat4j.tools.xplain.HighLevelXplain
-
- setMinimizationStrategy(MinimizationStrategy) - Method in class org.sat4j.tools.xplain.Xplain
-
- setNbexpectedclauses(int) - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
-
- setNbVars(int) - Method in class org.sat4j.tools.DimacsStringSolver
-
- setNeedToReduceDB(boolean) - Method in interface org.sat4j.minisat.core.ICDCL
-
- setNeedToReduceDB(boolean) - Method in class org.sat4j.minisat.core.Solver
-
- setOrder(IOrder) - Method in interface org.sat4j.minisat.core.ICDCL
-
- setOrder(IOrder) - Method in class org.sat4j.minisat.core.Solver
-
- setOrder(IOrder) - Method in class org.sat4j.minisat.learning.ActiveLearning
-
- setPeriod(int) - Method in class org.sat4j.minisat.orders.PureOrder
-
- setPeriod(long) - Method in class org.sat4j.minisat.restarts.FixedPeriodRestarts
-
- setPhaseSelectionStrategy(IPhaseSelectionStrategy) - Method in interface org.sat4j.minisat.core.IOrder
-
- setPhaseSelectionStrategy(IPhaseSelectionStrategy) - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
-
- setPhaseSelectionStrategy(IPhaseSelectionStrategy) - Method in class org.sat4j.minisat.orders.TabuListDecorator
-
- setPhaseSelectionStrategy(IPhaseSelectionStrategy) - Method in class org.sat4j.minisat.orders.VarOrderHeap
-
Change the selection strategy.
- setPrevboolmodel(boolean[]) - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
-
- setPrevfullmodel(int[]) - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
-
- setPrevmodel(int[]) - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
-
- setProbability(double) - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
-
- setReason(int, Constr) - Method in class org.sat4j.minisat.constraints.cnf.Lits
-
- setReason(int, Constr) - Method in interface org.sat4j.minisat.core.ILits
-
Sets the reason of the assignment of a literal.
- setRestartStrategy(RestartStrategy) - Method in interface org.sat4j.minisat.core.ICDCL
-
- setRestartStrategy(RestartStrategy) - Method in class org.sat4j.minisat.core.Solver
-
- setSearchListener(SearchListener<S>) - Method in class org.sat4j.minisat.core.Solver
-
- setSearchListener(SearchListener<S>) - Method in interface org.sat4j.specs.ISolver
-
Allow the user to hook a listener to the solver to be notified of the
main steps of the search process.
- setSearchListener(SearchListener<S>) - Method in class org.sat4j.tools.AbstractOutputSolver
-
- setSearchListener(SearchListener<I>) - Method in class org.sat4j.tools.ManyCore
-
- setSearchListener(SearchListener<S>) - Method in class org.sat4j.tools.SolverDecorator
-
- setSearchListener(SearchListener<S>) - Method in class org.sat4j.tools.StatisticsSolver
-
- setSearchParams(SearchParams) - Method in interface org.sat4j.minisat.core.ICDCL
-
- setSearchParams(SearchParams) - Method in class org.sat4j.minisat.core.Solver
-
- setSilent(boolean) - Method in class org.sat4j.AbstractLauncher
-
- setSimplifier(SimplificationType) - Method in interface org.sat4j.minisat.core.ICDCL
-
Setup the reason simplification strategy.
- setSimplifier(ISimplifier) - Method in interface org.sat4j.minisat.core.ICDCL
-
Setup the reason simplification strategy.
- setSimplifier(SimplificationType) - Method in class org.sat4j.minisat.core.Solver
-
- setSimplifier(ISimplifier) - Method in class org.sat4j.minisat.core.Solver
-
- setSolutionOptimal(boolean) - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator
-
- setSolver(Solver<D>) - Method in interface org.sat4j.minisat.core.LearningStrategy
-
- setSolver(Solver<D>) - Method in class org.sat4j.minisat.learning.ActiveLearning
-
- setSolver(Solver<D>) - Method in class org.sat4j.minisat.learning.LimitedLearning
-
- setSolver(Solver<D>) - Method in class org.sat4j.minisat.learning.MiniSATLearning
-
- setTimeout(int) - Method in class org.sat4j.minisat.core.Solver
-
- setTimeout(int) - Method in interface org.sat4j.specs.ISolver
-
To set the internal timeout of the solver.
- setTimeout(int) - Method in class org.sat4j.tools.AbstractOutputSolver
-
- setTimeout(int) - Method in class org.sat4j.tools.ManyCore
-
- setTimeout(int) - Method in class org.sat4j.tools.SolverDecorator
-
- setTimeout(int) - Method in class org.sat4j.tools.StatisticsSolver
-
- setTimeoutForFindingBetterSolution(int) - Method in class org.sat4j.opt.MaxSatDecorator
-
- setTimeoutForFindingBetterSolution(int) - Method in class org.sat4j.opt.MinOneDecorator
-
- setTimeoutForFindingBetterSolution(int) - Method in interface org.sat4j.specs.IOptimizationProblem
-
Allow to set a specific timeout when the solver is in optimization mode.
- setTimeoutForFindingBetterSolution(int) - Method in class org.sat4j.tools.LexicoDecorator
-
- setTimeoutMs(long) - Method in class org.sat4j.minisat.core.Solver
-
- setTimeoutMs(long) - Method in interface org.sat4j.specs.ISolver
-
To set the internal timeout of the solver.
- setTimeoutMs(long) - Method in class org.sat4j.tools.AbstractOutputSolver
-
- setTimeoutMs(long) - Method in class org.sat4j.tools.ManyCore
-
- setTimeoutMs(long) - Method in class org.sat4j.tools.SolverDecorator
-
- setTimeoutMs(long) - Method in class org.sat4j.tools.StatisticsSolver
-
- setTimeoutOnConflicts(int) - Method in class org.sat4j.minisat.core.Solver
-
- setTimeoutOnConflicts(int) - Method in interface org.sat4j.specs.ISolver
-
To set the internal timeout of the solver.
- setTimeoutOnConflicts(int) - Method in class org.sat4j.tools.AbstractOutputSolver
-
- setTimeoutOnConflicts(int) - Method in class org.sat4j.tools.ManyCore
-
- setTimeoutOnConflicts(int) - Method in class org.sat4j.tools.SolverDecorator
-
- setTimeoutOnConflicts(int) - Method in class org.sat4j.tools.StatisticsSolver
-
- setUnitPropagationListener(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.AbstractDataStructureFactory
-
- setUnitPropagationListener(UnitPropagationListener) - Method in interface org.sat4j.minisat.core.DataStructureFactory
-
- setVarActivityListener(VarActivityListener) - Method in interface org.sat4j.minisat.core.LearningStrategy
-
- setVarActivityListener(VarActivityListener) - Method in class org.sat4j.minisat.learning.LimitedLearning
-
- setVarDecay(double) - Method in interface org.sat4j.minisat.core.IOrder
-
Sets the variable activity decay as a growing factor for the next
variable activity.
- setVarDecay(double) - Method in class org.sat4j.minisat.core.SearchParams
-
- setVarDecay(double) - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
-
- setVarDecay(double) - Method in class org.sat4j.minisat.orders.TabuListDecorator
-
- setVarDecay(double) - Method in class org.sat4j.minisat.orders.VarOrderHeap
-
Change la valeur de varDecay.
- setVerbose(boolean) - Method in class org.sat4j.minisat.core.Solver
-
- setVerbose(boolean) - Method in interface org.sat4j.specs.ISolver
-
Set the verbosity of the solver
- setVerbose(boolean) - Method in class org.sat4j.tools.AbstractOutputSolver
-
- setVerbose(boolean) - Method in class org.sat4j.tools.ManyCore
-
- setVerbose(boolean) - Method in class org.sat4j.tools.SolverDecorator
-
- setVerbose(boolean) - Method in class org.sat4j.tools.StatisticsSolver
-
- setVerbosity(boolean) - Method in class org.sat4j.reader.Reader
-
- sharedConflict - Variable in class org.sat4j.minisat.core.Solver
-
- shortcuts - Variable in class org.sat4j.minisat.core.SolverStats
-
- shouldRestart() - Method in interface org.sat4j.minisat.core.RestartStrategy
-
Ask the strategy if the solver should restart.
- shouldRestart() - Method in class org.sat4j.minisat.restarts.ArminRestarts
-
- shouldRestart() - Method in class org.sat4j.minisat.restarts.FixedPeriodRestarts
-
- shouldRestart() - Method in class org.sat4j.minisat.restarts.Glucose21Restarts
-
- shouldRestart() - Method in class org.sat4j.minisat.restarts.LubyRestarts
-
- shouldRestart() - Method in class org.sat4j.minisat.restarts.MiniSATRestarts
-
- shouldRestart() - Method in class org.sat4j.minisat.restarts.NoRestarts
-
- showAvailableSolvers(ASolverFactory<T>) - Method in class org.sat4j.AbstractLauncher
-
- showAvailableSolvers(ASolverFactory<T>, String) - Method in class org.sat4j.AbstractLauncher
-
- shrink(int) - Method in class org.sat4j.core.ReadOnlyVec
-
- shrink(int) - Method in class org.sat4j.core.ReadOnlyVecInt
-
- shrink(int) - Method in class org.sat4j.core.Vec
-
Remove nofelems from the Vector.
- shrink(int) - Method in class org.sat4j.core.VecInt
-
Remove the latest nofelems elements from the vector
- shrink(int) - Method in interface org.sat4j.specs.IVec
-
Remove nofelems from the Vector.
- shrink(int) - Method in interface org.sat4j.specs.IVecInt
-
Remove the latest nofelems elements from the vector
- shrinkTo(int) - Method in class org.sat4j.core.ReadOnlyVec
-
- shrinkTo(int) - Method in class org.sat4j.core.ReadOnlyVecInt
-
- shrinkTo(int) - Method in class org.sat4j.core.Vec
-
reduce the Vector to exactly newsize elements
- shrinkTo(int) - Method in class org.sat4j.core.VecInt
-
- shrinkTo(int) - Method in interface org.sat4j.specs.IVec
-
reduce the Vector to exactly newsize elements
- shrinkTo(int) - Method in interface org.sat4j.specs.IVecInt
-
- shutdownHook - Variable in class org.sat4j.AbstractLauncher
-
- silent - Variable in class org.sat4j.AbstractLauncher
-
- SIMPLE_SIMPLIFICATION - Variable in class org.sat4j.minisat.core.Solver
-
- SimplificationType - Enum in org.sat4j.minisat.core
-
List the available simplification techniques available.
- simplify() - Method in class org.sat4j.minisat.constraints.card.AtLeast
-
- simplify() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
-
Simplifie la contrainte(l'all?
- simplify() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
-
simplifies the constraint
- simplify() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
-
- simplify() - Method in class org.sat4j.minisat.constraints.cnf.HTClause
-
- simplify() - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
-
- simplify() - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
-
- simplify() - Method in class org.sat4j.minisat.constraints.cnf.WLClause
-
- simplify() - Method in interface org.sat4j.minisat.core.Constr
-
Simplifies a constraint, by removing top level falsified literals for
instance.
- simplify(IVecInt) - Method in interface org.sat4j.minisat.core.ISimplifier
-
- simplifyDB() - Method in class org.sat4j.minisat.core.Solver
-
- SingleSolutionDetector - Class in org.sat4j.tools
-
This solver decorator allows to detect whether or not the set of constraints
available in the solver has only one solution or not.
- SingleSolutionDetector(ISolver) - Constructor for class org.sat4j.tools.SingleSolutionDetector
-
- size() - Method in class org.sat4j.core.ConstrGroup
-
- size() - Method in class org.sat4j.core.ReadOnlyVec
-
- size() - Method in class org.sat4j.core.ReadOnlyVecInt
-
- size() - Method in class org.sat4j.core.Vec
-
- size() - Method in class org.sat4j.core.VecInt
-
- size() - Method in class org.sat4j.minisat.constraints.card.AtLeast
-
- size() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
-
- size() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
-
- size() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
-
- size() - Method in class org.sat4j.minisat.constraints.cnf.HTClause
-
- size() - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
-
- size() - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses
-
- size() - Method in class org.sat4j.minisat.constraints.cnf.WLClause
-
- size() - Method in class org.sat4j.minisat.core.Heap
-
- size() - Method in class org.sat4j.minisat.core.IntQueue
-
Pour connaitre la taille de la queue.
- size() - Method in interface org.sat4j.specs.IConstr
-
- size() - Method in interface org.sat4j.specs.IVec
-
- size() - Method in interface org.sat4j.specs.IVecInt
-
- skipComments() - Method in class org.sat4j.reader.DimacsReader
-
Skip comments at the beginning of the input stream.
- skipComments() - Method in class org.sat4j.reader.EfficientScanner
-
Skip commented lines.
- skipRestOfLine() - Method in class org.sat4j.reader.EfficientScanner
-
- skipSpaces() - Method in class org.sat4j.reader.EfficientScanner
-
- slistener - Variable in class org.sat4j.minisat.core.Solver
-
- SOLUTION_PREFIX - Static variable in interface org.sat4j.ILauncherMode
-
- SolutionCounter - Class in org.sat4j.tools
-
Another solver decorator that counts the number of solutions.
- SolutionCounter(ISolver) - Constructor for class org.sat4j.tools.SolutionCounter
-
- solutionFound(int[], RandomAccessModel) - Method in interface org.sat4j.specs.SearchListener
-
a solution is found.
- solutionFound(int[], RandomAccessModel) - Method in class org.sat4j.tools.DotSearchTracing
-
- solutionFound(int[], RandomAccessModel) - Method in class org.sat4j.tools.HeuristicsTracing
-
- solutionFound(int[], RandomAccessModel) - Method in class org.sat4j.tools.LearnedTracing
-
- solutionFound(int[], RandomAccessModel) - Method in class org.sat4j.tools.MultiTracing
-
- solutionFound(int[], RandomAccessModel) - Method in class org.sat4j.tools.SearchEnumeratorListener
-
- solutionFound(int[], RandomAccessModel) - Method in class org.sat4j.tools.SearchListenerAdapter
-
- solutionFound(int[], RandomAccessModel) - Method in class org.sat4j.tools.SearchMinOneListener
-
- solutionFound(int[], RandomAccessModel) - Method in class org.sat4j.tools.TextOutputTracing
-
- SolutionFoundListener - Interface in org.sat4j.tools
-
Allows the end user to react when a new solution is found.
- solve(IProblem) - Method in class org.sat4j.AbstractLauncher
-
- solve(IProblem) - Method in class org.sat4j.AbstractOptimizationLauncher
-
Deprecated.
- solve(IProblem, Reader, ILogAble, PrintWriter, long) - Method in interface org.sat4j.ILauncherMode
-
Main solver call: one call for a decision problem, a loop for an
optimization problem.
- solver - Variable in class org.sat4j.AbstractLauncher
-
- solver - Variable in class org.sat4j.minisat.constraints.AbstractDataStructureFactory
-
- Solver<D extends DataStructureFactory> - Class in org.sat4j.minisat.core
-
The backbone of the library providing the modular implementation of a MiniSAT
(Chaff) like solver.
- Solver(LearningStrategy<D>, D, IOrder, RestartStrategy) - Constructor for class org.sat4j.minisat.core.Solver
-
creates a Solver without LearningListener.
- Solver(LearningStrategy<D>, D, SearchParams, IOrder, RestartStrategy) - Constructor for class org.sat4j.minisat.core.Solver
-
- Solver(LearningStrategy<D>, D, SearchParams, IOrder, RestartStrategy, ILogAble) - Constructor for class org.sat4j.minisat.core.Solver
-
- solver - Variable in class org.sat4j.reader.DimacsReader
-
- solver - Variable in class org.sat4j.reader.JSONReader
-
- solver - Variable in class org.sat4j.tools.DimacsArrayReader
-
- SolverDecorator<T extends ISolver> - Class in org.sat4j.tools
-
The aim of that class is to allow adding dynamic responsibilities to SAT
solvers using the Decorator design pattern.
- SolverDecorator(T) - Constructor for class org.sat4j.tools.SolverDecorator
-
- SolverFactory - Class in org.sat4j.minisat
-
User friendly access to pre-constructed solvers.
- solverNames() - Method in class org.sat4j.core.ASolverFactory
-
This methods returns names of solvers to be used with the method
getSolverByName().
- solvers - Variable in class org.sat4j.tools.ManyCore
-
- SolverStats - Class in org.sat4j.minisat.core
-
Contains some statistics regarding the search.
- SolverStats() - Constructor for class org.sat4j.minisat.core.SolverStats
-
- sort(Comparator<T>) - Method in class org.sat4j.core.ReadOnlyVec
-
- sort() - Method in class org.sat4j.core.ReadOnlyVecInt
-
- sort(Comparator<T>) - Method in class org.sat4j.core.Vec
-
- sort() - Method in class org.sat4j.core.VecInt
-
sort the vector using a custom quicksort.
- sort(Comparator<T>) - Method in interface org.sat4j.specs.IVec
-
- sort() - Method in interface org.sat4j.specs.IVecInt
-
- sortOnActivity() - Method in class org.sat4j.minisat.core.Solver
-
- sortUnique(Comparator<T>) - Method in class org.sat4j.core.ReadOnlyVec
-
- sortUnique() - Method in class org.sat4j.core.ReadOnlyVecInt
-
- sortUnique(Comparator<T>) - Method in class org.sat4j.core.Vec
-
- sortUnique() - Method in class org.sat4j.core.VecInt
-
- sortUnique(Comparator<T>) - Method in interface org.sat4j.specs.IVec
-
- sortUnique() - Method in interface org.sat4j.specs.IVecInt
-
- SpeedTracing - Class in org.sat4j.tools
-
- SpeedTracing(IVisualizationTool, IVisualizationTool, IVisualizationTool) - Constructor for class org.sat4j.tools.SpeedTracing
-
- start() - Method in interface org.sat4j.specs.SearchListener
-
Start the search.
- start() - Method in class org.sat4j.tools.ConflictDepthTracing
-
- start() - Method in class org.sat4j.tools.ConflictLevelTracing
-
- start() - Method in class org.sat4j.tools.DecisionLevelTracing
-
- start() - Method in class org.sat4j.tools.DecisionTracing
-
- start() - Method in class org.sat4j.tools.DotSearchTracing
-
- start() - Method in class org.sat4j.tools.LBDTracing
-
- start() - Method in class org.sat4j.tools.LearnedClausesSizeTracing
-
- start() - Method in class org.sat4j.tools.MultiTracing
-
- start() - Method in class org.sat4j.tools.SearchListenerAdapter
-
- start() - Method in class org.sat4j.tools.SpeedTracing
-
- start() - Method in class org.sat4j.tools.TextOutputTracing
-
- starts - Variable in class org.sat4j.minisat.core.SolverStats
-
- StatisticsSolver - Class in org.sat4j.tools
-
- StatisticsSolver() - Constructor for class org.sat4j.tools.StatisticsSolver
-
- stop() - Method in class org.sat4j.minisat.core.Solver
-
- stop() - Method in interface org.sat4j.specs.ISolverService
-
Ask the SAT solver to stop the search.
- subset(int) - Method in class org.sat4j.core.ReadOnlyVecInt
-
- subset(int) - Method in class org.sat4j.core.VecInt
-
- subset(int) - Method in interface org.sat4j.specs.IVecInt
-
Compute all subsets of cardinal k of the vector.
- SubsetVarOrder - Class in org.sat4j.minisat.orders
-
- SubsetVarOrder(int[]) - Constructor for class org.sat4j.minisat.orders.SubsetVarOrder
-
- suggestNextLiteralToBranchOn(int) - Method in class org.sat4j.minisat.core.Solver
-
- suggestNextLiteralToBranchOn(int) - Method in interface org.sat4j.specs.ISolverService
-
Suggests to the SAT solver to branch next on the given literal.
- TabuListDecorator - Class in org.sat4j.minisat.orders
-
Uses a tabu list to prevent the solver to
- TabuListDecorator(VarOrderHeap) - Constructor for class org.sat4j.minisat.orders.TabuListDecorator
-
- TabuListDecorator(VarOrderHeap, int) - Constructor for class org.sat4j.minisat.orders.TabuListDecorator
-
- tail - Variable in class org.sat4j.minisat.constraints.cnf.BinaryClause
-
- tail - Variable in class org.sat4j.minisat.constraints.cnf.HTClause
-
- TextOutputTracing<T> - Class in org.sat4j.tools
-
Debugging Search Listener allowing to follow the search in a textual way.
- TextOutputTracing(Map<Integer, T>) - Constructor for class org.sat4j.tools.TextOutputTracing
-
- TimeoutException - Exception in org.sat4j.specs
-
Exception launched when the solver cannot solve a problem within its allowed
time.
- TimeoutException() - Constructor for exception org.sat4j.specs.TimeoutException
-
Constructor for TimeoutException.
- TimeoutException(String) - Constructor for exception org.sat4j.specs.TimeoutException
-
Constructor for TimeoutException.
- TimeoutException(String, Throwable) - Constructor for exception org.sat4j.specs.TimeoutException
-
Constructor for TimeoutException.
- TimeoutException(Throwable) - Constructor for exception org.sat4j.specs.TimeoutException
-
Constructor for TimeoutException.
- toArray() - Method in class org.sat4j.core.ReadOnlyVec
-
- toArray() - Method in class org.sat4j.core.ReadOnlyVecInt
-
- toArray() - Method in class org.sat4j.core.Vec
-
- toArray() - Method in class org.sat4j.core.VecInt
-
- toArray() - Method in interface org.sat4j.specs.IVec
-
Allow to access the internal representation of the vector as an array.
- toArray() - Method in interface org.sat4j.specs.IVecInt
-
Allow to access the internal representation of the vector as an array.
- toConstraint() - Method in class org.sat4j.minisat.constraints.card.AtLeast
-
- toConstraint() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
-
- toConstraint() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
-
- toConstraint() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
-
- toConstraint() - Method in class org.sat4j.minisat.constraints.cnf.HTClause
-
- toConstraint() - Method in class org.sat4j.minisat.constraints.cnf.WLClause
-
- toConstraint() - Method in interface org.sat4j.minisat.core.Propagatable
-
Allow to access a constraint view of the propagatable to avoid casting.
- toDimacs(int) - Static method in class org.sat4j.core.LiteralsUtils
-
decode the internal representation of a literal in internal
representation into Dimacs format.
- toInternal(int) - Static method in class org.sat4j.core.LiteralsUtils
-
encode the classical Dimacs representation (negated integers for negated
literals) into the internal format.
- toMap() - Method in class org.sat4j.minisat.core.SolverStats
-
- toString() - Method in class org.sat4j.core.ConstrGroup
-
- toString() - Method in class org.sat4j.core.ReadOnlyVec
-
- toString() - Method in class org.sat4j.core.ReadOnlyVecInt
-
- toString() - Method in class org.sat4j.core.Vec
-
- toString() - Method in class org.sat4j.core.VecInt
-
- toString() - Method in class org.sat4j.ExitCode
-
- toString() - Method in class org.sat4j.minisat.constraints.card.AtLeast
-
Textual representation of the constraint
- toString() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard
-
Cha?
- toString() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard
-
Returns a string representation of the constraint.
- toString() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause
-
- toString() - Method in class org.sat4j.minisat.constraints.cnf.HTClause
-
- toString(int) - Static method in class org.sat4j.minisat.constraints.cnf.Lits
-
- toString() - Method in class org.sat4j.minisat.constraints.cnf.UnitClause
-
- toString() - Method in class org.sat4j.minisat.constraints.cnf.WLClause
-
- toString() - Method in class org.sat4j.minisat.core.Counter
-
- toString() - Method in class org.sat4j.minisat.core.IntQueue
-
- toString() - Method in class org.sat4j.minisat.core.SearchParams
-
- toString(String) - Method in class org.sat4j.minisat.core.Solver
-
- toString() - Method in class org.sat4j.minisat.core.Solver
-
- toString() - Method in class org.sat4j.minisat.learning.ActiveLearning
-
- toString() - Method in class org.sat4j.minisat.learning.ClauseOnlyLearning
-
- toString() - Method in class org.sat4j.minisat.learning.FixedLengthLearning
-
- toString() - Method in class org.sat4j.minisat.learning.MiniSATLearning
-
- toString() - Method in class org.sat4j.minisat.learning.PercentLengthLearning
-
- toString() - Method in class org.sat4j.minisat.orders.NegativeLiteralSelectionStrategy
-
- toString() - Method in class org.sat4j.minisat.orders.PhaseCachingAutoEraseStrategy
-
- toString() - Method in class org.sat4j.minisat.orders.PhaseInLastLearnedClauseSelectionStrategy
-
- toString() - Method in class org.sat4j.minisat.orders.PositiveLiteralSelectionStrategy
-
- toString() - Method in class org.sat4j.minisat.orders.PureOrder
-
- toString() - Method in class org.sat4j.minisat.orders.RandomLiteralSelectionStrategy
-
- toString() - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
-
- toString() - Method in class org.sat4j.minisat.orders.RSATLastLearnedClausesPhaseSelectionStrategy
-
- toString() - Method in class org.sat4j.minisat.orders.RSATPhaseSelectionStrategy
-
- toString() - Method in class org.sat4j.minisat.orders.TabuListDecorator
-
- toString() - Method in class org.sat4j.minisat.orders.UserFixedPhaseSelectionStrategy
-
- toString() - Method in class org.sat4j.minisat.orders.VarOrderHeap
-
- toString() - Method in class org.sat4j.minisat.restarts.ArminRestarts
-
- toString() - Method in class org.sat4j.minisat.restarts.FixedPeriodRestarts
-
- toString() - Method in class org.sat4j.minisat.restarts.Glucose21Restarts
-
- toString() - Method in class org.sat4j.minisat.restarts.LubyRestarts
-
- toString() - Method in class org.sat4j.minisat.restarts.MiniSATRestarts
-
- toString() - Method in class org.sat4j.minisat.restarts.NoRestarts
-
- toString(String) - Method in interface org.sat4j.specs.ISolver
-
Display a textual representation of the solver configuration.
- toString() - Method in class org.sat4j.specs.Lbool
-
Textual representation for the truth value.
- toString() - Method in class org.sat4j.tools.ClausalCardinalitiesDecorator
-
- toString(String) - Method in class org.sat4j.tools.ClausalCardinalitiesDecorator
-
- toString(String) - Method in class org.sat4j.tools.DimacsOutputSolver
-
- toString(String) - Method in class org.sat4j.tools.DimacsStringSolver
-
- toString() - Method in class org.sat4j.tools.DimacsStringSolver
-
- toString() - Method in enum org.sat4j.tools.encoding.EncodingStrategy
-
- toString() - Method in class org.sat4j.tools.encoding.EncodingStrategyAdapter
-
- toString() - Method in class org.sat4j.tools.encoding.Policy
-
- toString(String) - Method in class org.sat4j.tools.ManyCore
-
- toString(String) - Method in class org.sat4j.tools.OptToSatAdapter
-
- toString(String) - Method in class org.sat4j.tools.SolverDecorator
-
- toString() - Method in class org.sat4j.tools.SolverDecorator
-
- toString(String) - Method in class org.sat4j.tools.StatisticsSolver
-
- toString() - Method in class org.sat4j.tools.xplain.DeletionStrategy
-
- toString(String) - Method in class org.sat4j.tools.xplain.HighLevelXplain
-
- toString() - Method in class org.sat4j.tools.xplain.InsertionStrategy
-
- toString() - Method in class org.sat4j.tools.xplain.QuickXplain2001Strategy
-
- toString() - Method in class org.sat4j.tools.xplain.QuickXplainStrategy
-
- toString(String) - Method in class org.sat4j.tools.xplain.Xplain
-
- trail - Variable in class org.sat4j.minisat.core.Solver
-
variable assignments (literals) in chronological order.
- trailLim - Variable in class org.sat4j.minisat.core.Solver
-
position of the decision levels on the trail.
- TRUE - Static variable in class org.sat4j.specs.Lbool
-
- TRUE - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader
-
- truthValue(int) - Method in class org.sat4j.minisat.core.Solver
-
- truthValue(int) - Method in interface org.sat4j.specs.ISolverService
-
To access the truth value of a specific literal under current assignment.
- 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
-
- unsatExplanation() - Method in class org.sat4j.tools.StatisticsSolver
-
- UNSATISFIABLE - Static variable in class org.sat4j.ExitCode
-
- unset(int) - Method in class org.sat4j.minisat.core.Solver
-
- unset(int) - Method in interface org.sat4j.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
-
- value() - Method in class org.sat4j.ExitCode
-
- valueOf(String) - Static method in enum org.sat4j.minisat.core.LearnedConstraintsEvaluationType
-
Returns the enum constant of this type with the specified name.
- valueOf(String) - Static method in enum org.sat4j.minisat.core.SimplificationType
-
Returns the enum constant of this type with the specified name.
- valueOf(String) - Static method in enum org.sat4j.tools.encoding.EncodingStrategy
-
Returns the enum constant of this type with the specified name.
- values() - Static method in enum org.sat4j.minisat.core.LearnedConstraintsEvaluationType
-
Returns an array containing the constants of this enum type, in
the order they are declared.
- values() - Static method in enum org.sat4j.minisat.core.SimplificationType
-
Returns an array containing the constants of this enum type, in
the order they are declared.
- values() - Static method in enum org.sat4j.tools.encoding.EncodingStrategy
-
Returns an array containing the constants of this enum type, in
the order they are declared.
- valueToString(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits
-
- valueToString(int) - Method in interface org.sat4j.minisat.core.ILits
-
Returns a textual representation of the truth value of that literal.
- var(int) - Static method in class org.sat4j.core.LiteralsUtils
-
Returns the variable associated to the literal
- varActivity(int) - Method in interface org.sat4j.minisat.core.IOrder
-
To obtain the current activity of a variable.
- varActivity(int) - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
-
- varActivity(int) - Method in class org.sat4j.minisat.orders.TabuListDecorator
-
- varActivity(int) - Method in class org.sat4j.minisat.orders.VarOrderHeap
-
- VarActivityListener - Interface in org.sat4j.minisat.core
-
Interface providing the capability to increase the activity of a given
variable.
- varBumpActivity(int) - Method in class org.sat4j.minisat.core.Solver
-
- varBumpActivity(int) - Method in interface org.sat4j.minisat.core.VarActivityListener
-
Update the activity of a variable v.
- varDecayActivity() - Method in interface org.sat4j.minisat.core.IOrder
-
Decay the variables activities.
- varDecayActivity() - Method in class org.sat4j.minisat.orders.RandomWalkDecorator
-
- varDecayActivity() - Method in class org.sat4j.minisat.orders.TabuListDecorator
-
- varDecayActivity() - Method in class org.sat4j.minisat.orders.VarOrderHeap
-
- VarOrderHeap - Class in org.sat4j.minisat.orders
-
- VarOrderHeap() - Constructor for class org.sat4j.minisat.orders.VarOrderHeap
-
- VarOrderHeap(IPhaseSelectionStrategy) - Constructor for class org.sat4j.minisat.orders.VarOrderHeap
-
- Vec<T> - Class in org.sat4j.core
-
Simple but efficient vector implementation, based on the vector
implementation available in MiniSAT.
- Vec() - Constructor for class org.sat4j.core.Vec
-
Create a Vector with an initial capacity of 5 elements.
- Vec(T[]) - Constructor for class org.sat4j.core.Vec
-
Adapter method to translate an array of int into an IVec.
- Vec(int) - Constructor for class org.sat4j.core.Vec
-
Create a Vector with a given capacity.
- Vec(int, T) - Constructor for class org.sat4j.core.Vec
-
Construit un vecteur contenant de taille size rempli a l'aide de size
pad.
- VecInt - Class in org.sat4j.core
-
A vector specific for primitive integers, widely used in the solver.
- VecInt() - Constructor for class org.sat4j.core.VecInt
-
- VecInt(int) - Constructor for class org.sat4j.core.VecInt
-
- VecInt(int[]) - Constructor for class org.sat4j.core.VecInt
-
Adapter method to translate an array of int into an IVecInt.
- VecInt(int, int) - Constructor for class org.sat4j.core.VecInt
-
Build a vector of a given initial size filled with an integer.
- voc - Variable in class org.sat4j.minisat.constraints.card.AtLeast
-
- voc - Variable in class org.sat4j.minisat.constraints.cnf.HTClause
-
- voc - Variable in class org.sat4j.minisat.constraints.cnf.WLClause
-
- voc - Variable in class org.sat4j.minisat.core.Solver
-
- VOID - Static variable in interface org.sat4j.tools.SolutionFoundListener
-