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

A

AAGReader - Class in org.sat4j.reader

Reader for the ASCII And Inverter Graph format defined by Armin Biere.

AbstractCardinalityDataStructure - Class in org.sat4j.minisat.constraints

AbstractCardinalityDataStructure() - Constructor for class org.sat4j.minisat.constraints.AbstractCardinalityDataStructure

AbstractDataStructureFactory - Class in org.sat4j.minisat.constraints

AbstractDataStructureFactory() - Constructor for class org.sat4j.minisat.constraints.AbstractDataStructureFactory

AbstractLauncher - Class in org.sat4j

That class is used by launchers used to solve decision problems, i.e.

AbstractLauncher() - Constructor for class org.sat4j.AbstractLauncher

AbstractOptimizationLauncher - Class in org.sat4j

This class is intended to be used by launchers to solve optimization problems, i.e. problems for which a loop is needed to find the optimal solution.

AbstractOptimizationLauncher() - Constructor for class org.sat4j.AbstractOptimizationLauncher

AbstractOutputSolver - Class in org.sat4j.tools

AbstractOutputSolver() - Constructor for class org.sat4j.tools.AbstractOutputSolver

AbstractSelectorVariablesDecorator - Class in org.sat4j.opt

Abstract class which adds a new "selector" variable for each clause entered in the solver.

AbstractSelectorVariablesDecorator(ISolver) - Constructor for class org.sat4j.opt.AbstractSelectorVariablesDecorator

ActiveLearning<D extends DataStructureFactory> - Class in org.sat4j.minisat.learning

Learn clauses with a great number of active variables.

ActiveLearning() - Constructor for class org.sat4j.minisat.learning.ActiveLearning

ActiveLearning(double) - Constructor for class org.sat4j.minisat.learning.ActiveLearning

activity - Variable in class org.sat4j.minisat.constraints.cnf.BinaryClause

activity - Variable in class org.sat4j.minisat.constraints.cnf.HTClause

activity - Variable in class org.sat4j.minisat.constraints.cnf.WLClause

activity - Variable in class org.sat4j.minisat.orders.VarOrderHeap

mesure heuristique de l'activite d'une variable.

ActivityComparator - Class in org.sat4j.minisat.core

Utility class to sort the constraints according to their activity.

ActivityComparator() - Constructor for class org.sat4j.minisat.core.ActivityComparator

add(IConstr) - Method in class org.sat4j.core.ConstrGroup

addAllClauses(IVec<IVecInt>) - Method in class org.sat4j.minisat.core.Solver

addAllClauses(IVec<IVecInt>) - Method in interface org.sat4j.specs.ISolver

Create clauses from a set of set of literals.

addAllClauses(IVec<IVecInt>) - Method in class org.sat4j.tools.AbstractOutputSolver

addAllClauses(IVec<IVecInt>) - Method in class org.sat4j.tools.ManyCore

addAllClauses(IVec<IVecInt>) - Method in class org.sat4j.tools.SolverDecorator

addAtLeast(IVecInt, int) - Method in class org.sat4j.minisat.core.Solver

addAtLeast(IVecInt, int) - Method in interface org.sat4j.specs.ISolver

Create a cardinality constraint of the type "at least n of those literals must be satisfied"

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

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

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

addAtLeast(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Binary

addAtLeast(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Binomial

addAtLeast(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Commander

addAtLeast(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.EncodingStrategyAdapter

addAtLeast(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Policy

addAtLeast(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Product

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

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

addAtLeast(IVecInt, int) - Method in class org.sat4j.tools.xplain.HighLevelXplain

addAtLeast(IVecInt, int) - Method in class org.sat4j.tools.xplain.Xplain

addAtLeastOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Binomial

addAtLeastOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.EncodingStrategyAdapter

addAtMost(IVecInt, int) - Method in class org.sat4j.minisat.core.Solver

addAtMost(IVecInt, int) - Method in interface org.sat4j.specs.ISolver

Create a cardinality constraint of the type "at most n of those literals must be satisfied"

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

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

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

addAtMost(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Binary

addAtMost(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Binomial

addAtMost(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Commander

addAtMost(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.EncodingStrategyAdapter

addAtMost(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Policy

addAtMost(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Product

addAtMost(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Sequential

This encoding adds (n-1)*k variables (n is the number of variables in the at most constraint and k is the degree of the constraint) and 2nk+n-3k-1 clauses.

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

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

addAtMost(IVecInt, int) - Method in class org.sat4j.tools.xplain.HighLevelXplain

addAtMost(IVecInt, int) - Method in class org.sat4j.tools.xplain.Xplain

addAtMostNonOpt(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Product

addAtMostOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Binary

p being the smaller integer greater than log_2(n), this encoding adds p variables and n*p clauses.

addAtMostOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Binomial

addAtMostOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Commander

In this encoding, variables are partitioned in groups.

addAtMostOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.EncodingStrategyAdapter

addAtMostOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Ladder

addAtMostOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Product

addBlockingClause(IVecInt) - Method in class org.sat4j.minisat.core.Solver

addBlockingClause(IVecInt) - Method in interface org.sat4j.specs.ISolver

Add a clause in order to prevent an assignment to occur.

addBlockingClause(IVecInt) - Method in class org.sat4j.tools.AbstractOutputSolver

addBlockingClause(IVecInt) - Method in class org.sat4j.tools.ManyCore

addBlockingClause(IVecInt) - Method in class org.sat4j.tools.SolverDecorator

addClause(IVecInt) - Method in class org.sat4j.minisat.core.Solver

addClause(int[]) - Method in class org.sat4j.minisat.core.Solver

addClause(IVecInt) - Method in class org.sat4j.opt.MaxSatDecorator

addClause(IVecInt) - Method in interface org.sat4j.specs.ISolver

Create a clause from a set of literals The literals are represented by non null integers such that opposite literals a represented by opposite values.

addClause(int[]) - Method in interface org.sat4j.specs.ISolverService

Add a new clause in the SAT solver.

addClause(IVecInt) - Method in class org.sat4j.tools.DimacsOutputSolver

addClause(IVecInt) - Method in class org.sat4j.tools.DimacsStringSolver

addClause(IVecInt) - Method in class org.sat4j.tools.ManyCore

addClause(IVecInt) - Method in class org.sat4j.tools.SolverDecorator

addClause(IVecInt, int) - Method in class org.sat4j.tools.xplain.HighLevelXplain

addClause(IVecInt) - Method in class org.sat4j.tools.xplain.Xplain

addConstr(Constr) - Method in class org.sat4j.minisat.core.Solver

addCriterion(IVecInt) - Method in class org.sat4j.tools.LexicoDecorator

addExactly(IVecInt, int) - Method in class org.sat4j.minisat.core.Solver

addExactly(IVecInt, int) - Method in interface org.sat4j.specs.ISolver

Create a cardinality constraint of the type "exactly n of those literals must be satisfied".

addExactly(IVecInt, int) - Method in class org.sat4j.tools.ClausalCardinalitiesDecorator

addExactly(IVecInt, int) - Method in class org.sat4j.tools.DimacsOutputSolver

addExactly(IVecInt, int) - Method in class org.sat4j.tools.DimacsStringSolver

addExactly(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Binary

addExactly(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Binomial

addExactly(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Commander

addExactly(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.EncodingStrategyAdapter

addExactly(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Policy

addExactly(ISolver, IVecInt, int) - Method in class org.sat4j.tools.encoding.Product

addExactly(IVecInt, int) - Method in class org.sat4j.tools.ManyCore

addExactly(IVecInt, int) - Method in class org.sat4j.tools.SolverDecorator

addExactly(IVecInt, int) - Method in class org.sat4j.tools.xplain.Xplain

addExactlyOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Binary

addExactlyOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Binomial

addExactlyOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Commander

addExactlyOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.EncodingStrategyAdapter

addExactlyOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Ladder

addExactlyOne(ISolver, IVecInt) - Method in class org.sat4j.tools.encoding.Product

adding(int) - Method in interface org.sat4j.specs.SearchListener

adding forced variable (conflict driven assignment)

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

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

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

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

addInvisiblePoint(double, double) - Method in class org.sat4j.tools.FileBasedVisualizationTool

addInvisiblePoint(double, double) - Method in interface org.sat4j.tools.IVisualizationTool

additionalFullAdderConstraints(int, int, int, int, int) - Method in class org.sat4j.tools.GateTranslator

addPoint(double, double) - Method in class org.sat4j.tools.FileBasedVisualizationTool

addPoint(double, double) - Method in interface org.sat4j.tools.IVisualizationTool

admitABetterSolution() - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator

admitABetterSolution(IVecInt) - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator

admitABetterSolution(IVecInt) - Method in class org.sat4j.opt.MaxSatDecorator

admitABetterSolution() - Method in class org.sat4j.opt.MinOneDecorator

admitABetterSolution(IVecInt) - Method in class org.sat4j.opt.MinOneDecorator

admitABetterSolution() - Method in interface org.sat4j.specs.IOptimizationProblem

Look for a solution of the optimization problem.

admitABetterSolution(IVecInt) - Method in interface org.sat4j.specs.IOptimizationProblem

Look for a solution of the optimization problem when some literals are satisfied.

admitABetterSolution() - Method in class org.sat4j.tools.LexicoDecorator

admitABetterSolution(IVecInt) - Method in class org.sat4j.tools.LexicoDecorator

AIGReader - Class in org.sat4j.reader

Reader for the Binary And Inverter Graph format defined by Armin Biere.

analyze(Constr, Pair) - Method in class org.sat4j.minisat.core.Solver

analyzeAtRootLevel(Constr) - Method in class org.sat4j.minisat.core.Solver

analyzeFinalConflictInTermsOfAssumptions(Constr, IVecInt, int) - Method in class org.sat4j.minisat.core.Solver

Derive a subset of the assumptions causing the inconistency.

AND - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader

and(int, IVecInt) - Method in class org.sat4j.tools.GateTranslator

Translate y <=> x1 /\ x2 /\ ... /\ xn into clauses.

and(int, int, int) - Method in class org.sat4j.tools.GateTranslator

Translate y <=> x1 /\ x2

ANSWER_PREFIX - Static variable in class org.sat4j.AbstractLauncher

ArminRestarts - Class in org.sat4j.minisat.restarts

Rapid restart strategy presented by Armin Biere during it's SAT 07 invited talk.

ArminRestarts() - Constructor for class org.sat4j.minisat.restarts.ArminRestarts

ASolverFactory<T extends ISolver> - Class in org.sat4j.core

A solver factory is responsible for providing prebuilt solvers to the end user.

ASolverFactory() - Constructor for class org.sat4j.core.ASolverFactory

assertConstraint(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.card.AtLeast

assertConstraint(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard

assertConstraint(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard

assertConstraint(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause

assertConstraint(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.HTClause

assertConstraint(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.UnitClause

assertConstraint(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses

assertConstraint(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.WLClause

assertConstraint(UnitPropagationListener) - Method in interface org.sat4j.minisat.core.Constr

Method called when the constraint is to be asserted.

assignLiteral(int) - Method in interface org.sat4j.minisat.core.IOrder

indicate that a literal has been satisfied.

assignLiteral(int) - Method in interface org.sat4j.minisat.core.IPhaseSelectionStrategy

indicate that a literal has been satisfied.

assignLiteral(int) - Method in class org.sat4j.minisat.orders.NegativeLiteralSelectionStrategy

assignLiteral(int) - Method in class org.sat4j.minisat.orders.PhaseCachingAutoEraseStrategy

assignLiteral(int) - Method in class org.sat4j.minisat.orders.PhaseInLastLearnedClauseSelectionStrategy

assignLiteral(int) - Method in class org.sat4j.minisat.orders.PositiveLiteralSelectionStrategy

assignLiteral(int) - Method in class org.sat4j.minisat.orders.RandomLiteralSelectionStrategy

assignLiteral(int) - Method in class org.sat4j.minisat.orders.RandomWalkDecorator

assignLiteral(int) - Method in class org.sat4j.minisat.orders.RSATLastLearnedClausesPhaseSelectionStrategy

assignLiteral(int) - Method in class org.sat4j.minisat.orders.RSATPhaseSelectionStrategy

assignLiteral(int) - Method in class org.sat4j.minisat.orders.TabuListDecorator

assignLiteral(int) - Method in class org.sat4j.minisat.orders.UserFixedPhaseSelectionStrategy

assignLiteral(int) - Method in class org.sat4j.minisat.orders.VarOrderHeap

assume(int) - Method in class org.sat4j.minisat.core.Solver

assuming(int) - Method in interface org.sat4j.specs.SearchListener

decision variable

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

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

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

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

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

assump - Variable in class org.sat4j.tools.xplain.HighLevelXplain

assump - Variable in class org.sat4j.tools.xplain.Xplain

AtLeast - Class in org.sat4j.minisat.constraints.card

AtLeast(ILits, IVecInt, int) - Constructor for class org.sat4j.minisat.constraints.card.AtLeast

ATLEAST - Static variable in class org.sat4j.minisat.constraints.card.MinWatchCard

ATLEAST - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader

atLeastNew(UnitPropagationListener, ILits, IVecInt, int) - Static method in class org.sat4j.minisat.constraints.card.AtLeast

ATMOST - Static variable in class org.sat4j.minisat.constraints.card.MinWatchCard

ATMOST - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader

average() - Method in class org.sat4j.minisat.core.CircularBuffer

B

backbone(ISolver) - Static method in class org.sat4j.tools.RemiUtils

Compute the set of literals common to all models of the formula.

backjump(int) - Method in interface org.sat4j.specs.SearchListener

The solver is asked to backjump to a given decision level.

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

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

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

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

backtrack(int[]) - Method in class org.sat4j.minisat.core.Solver

backtrack(int[]) - Method in interface org.sat4j.specs.ISolverService

Ask the SAT solver to backtrack.

backtracking(int) - Method in interface org.sat4j.specs.SearchListener

backtrack on a decision variable

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

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

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

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

backtrackLevel - Variable in class org.sat4j.minisat.core.Pair

BasicLauncher<T extends ISolver> - Class in org.sat4j

Very simple launcher, to be used during the SAT competition or the SAT race for instance.

BasicLauncher(ASolverFactory<T>) - Constructor for class org.sat4j.BasicLauncher

beginLoop() - Method in interface org.sat4j.specs.SearchListener

starts a propagation

beginLoop() - Method in class org.sat4j.tools.DotSearchTracing

beginLoop() - Method in class org.sat4j.tools.MultiTracing

beginLoop() - Method in class org.sat4j.tools.SearchListenerAdapter

beginLoop() - Method in class org.sat4j.tools.TextOutputTracing

beginTime - Variable in class org.sat4j.AbstractLauncher

belongsToPool(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits

belongsToPool(int) - Method in interface org.sat4j.minisat.core.ILits

Returns true iff the variable is used in the set of constraints.

Binary - Class in org.sat4j.tools.encoding

Binary encoding for the "at most one" and "at most k" cases.

Binary() - Constructor for class org.sat4j.tools.encoding.Binary

BinaryClause - Class in org.sat4j.minisat.constraints.cnf

Data structure for binary clause.

BinaryClause(IVecInt, ILits) - Constructor for class org.sat4j.minisat.constraints.cnf.BinaryClause

Creates a new basic clause

Binomial - Class in org.sat4j.tools.encoding

Binomial encoding for the "at most one" and "at most k" cases.

Binomial() - Constructor for class org.sat4j.tools.encoding.Binomial

bound() - Method in class org.sat4j.minisat.core.ConflictTimerAdapter

brandNewClause(UnitPropagationListener, ILits, IVecInt) - Static method in class org.sat4j.minisat.constraints.cnf.OriginalBinaryClause

Creates a brand new clause, presumably from external data.

brandNewClause(UnitPropagationListener, ILits, IVecInt) - Static method in class org.sat4j.minisat.constraints.cnf.OriginalHTClause

Creates a brand new clause, presumably from external data.

brandNewClause(UnitPropagationListener, ILits, IVecInt) - Static method in class org.sat4j.minisat.constraints.cnf.OriginalWLClause

Creates a brand new clause, presumably from external data.

C

calcReason(int, IVecInt) - Method in class org.sat4j.minisat.constraints.card.AtLeast

calcReason(int, IVecInt) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard

Calcule la cause de l'affection d'un litt?

calcReason(int, IVecInt) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard

computes the reason for a literal

calcReason(int, IVecInt) - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause

calcReason(int, IVecInt) - Method in class org.sat4j.minisat.constraints.cnf.HTClause

calcReason(int, IVecInt) - Method in class org.sat4j.minisat.constraints.cnf.UnitClause

calcReason(int, IVecInt) - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses

calcReason(int, IVecInt) - Method in class org.sat4j.minisat.constraints.cnf.WLClause

calcReason(int, IVecInt) - Method in interface org.sat4j.minisat.core.Constr

Compute the reason for a given assignment.

calculateObjective() - Method in class org.sat4j.opt.MaxSatDecorator

calculateObjective() - Method in class org.sat4j.opt.MinOneDecorator

calculateObjective() - Method in interface org.sat4j.specs.IOptimizationProblem

Deprecated.

calculateObjective() - Method in class org.sat4j.tools.LexicoDecorator

canBePropagatedMultipleTimes() - Method in class org.sat4j.core.ConstrGroup

canBePropagatedMultipleTimes() - Method in class org.sat4j.minisat.constraints.card.AtLeast

canBePropagatedMultipleTimes() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard

canBePropagatedMultipleTimes() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard

canBePropagatedMultipleTimes() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause

canBePropagatedMultipleTimes() - Method in class org.sat4j.minisat.constraints.cnf.HTClause

canBePropagatedMultipleTimes() - Method in class org.sat4j.minisat.constraints.cnf.UnitClause

canBePropagatedMultipleTimes() - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses

canBePropagatedMultipleTimes() - Method in class org.sat4j.minisat.constraints.cnf.WLClause

canBePropagatedMultipleTimes() - Method in interface org.sat4j.specs.IConstr

Partition constraints into the ones that can only be found once on the trail (e.g. clauses) and the ones that can be found several times (e.g.

cancelExplanation() - Method in class org.sat4j.tools.xplain.HighLevelXplain

cancelExplanation() - Method in class org.sat4j.tools.xplain.Xplain

cancelExplanationComputation() - Method in class org.sat4j.tools.xplain.DeletionStrategy

cancelExplanationComputation() - Method in class org.sat4j.tools.xplain.InsertionStrategy

cancelExplanationComputation() - Method in interface org.sat4j.tools.xplain.MinimizationStrategy

cancelExplanationComputation() - Method in class org.sat4j.tools.xplain.QuickXplain2001Strategy

cancelExplanationComputation() - Method in class org.sat4j.tools.xplain.QuickXplainStrategy

cancelUntil(int) - Method in class org.sat4j.minisat.core.Solver

Cancel several levels of assumptions

capacity() - Method in class org.sat4j.minisat.constraints.cnf.Lits

To get the capacity of the current vocabulary.

CardinalityDataStructure - Class in org.sat4j.minisat.constraints

CardinalityDataStructure() - Constructor for class org.sat4j.minisat.constraints.CardinalityDataStructure

CardinalityDataStructureYanMax - Class in org.sat4j.minisat.constraints

CardinalityDataStructureYanMax() - Constructor for class org.sat4j.minisat.constraints.CardinalityDataStructureYanMax

CardinalityDataStructureYanMin - Class in org.sat4j.minisat.constraints

CardinalityDataStructureYanMin() - Constructor for class org.sat4j.minisat.constraints.CardinalityDataStructureYanMin

changedreason - Variable in class org.sat4j.minisat.core.SolverStats

CircularBuffer - Class in org.sat4j.minisat.core

Create a circular buffer of a given capacity allowing to compute efficiently the mean of the values storied.

CircularBuffer(int) - Constructor for class org.sat4j.minisat.core.CircularBuffer

claBumpActivity(Constr) - Method in class org.sat4j.minisat.core.Solver

Propagate activity to a constraint

ClausalCardinalitiesDecorator<T extends ISolver> - Class in org.sat4j.tools

A decorator for clausal cardinalities constraints.

ClausalCardinalitiesDecorator(T) - Constructor for class org.sat4j.tools.ClausalCardinalitiesDecorator

ClausalCardinalitiesDecorator(T, EncodingStrategyAdapter) - Constructor for class org.sat4j.tools.ClausalCardinalitiesDecorator

ClausalDataStructureWL - Class in org.sat4j.minisat.constraints

ClausalDataStructureWL() - Constructor for class org.sat4j.minisat.constraints.ClausalDataStructureWL

ClauseOnlyLearning<D extends DataStructureFactory> - Class in org.sat4j.minisat.learning

The solver only records among all the constraints only the clauses.

ClauseOnlyLearning() - Constructor for class org.sat4j.minisat.learning.ClauseOnlyLearning

Clauses - Class in org.sat4j.minisat.constraints.cnf

Clauses() - Constructor for class org.sat4j.minisat.constraints.cnf.Clauses

cleaning() - Method in interface org.sat4j.specs.SearchListener

The solver is going to delete some learned clauses.

cleaning() - Method in class org.sat4j.tools.ConflictDepthTracing

cleaning() - Method in class org.sat4j.tools.ConflictLevelTracing

cleaning() - Method in class org.sat4j.tools.DecisionTracing

cleaning() - Method in class org.sat4j.tools.LearnedClausesSizeTracing

cleaning() - Method in class org.sat4j.tools.LearnedTracing

cleaning() - Method in class org.sat4j.tools.MultiTracing

cleaning() - Method in class org.sat4j.tools.SearchListenerAdapter

cleaning() - Method in class org.sat4j.tools.SpeedTracing

cleaning() - Method in class org.sat4j.tools.TextOutputTracing

clear() - Method in class org.sat4j.core.ConstrGroup

clear() - Method in class org.sat4j.core.ReadOnlyVec

clear() - Method in class org.sat4j.core.ReadOnlyVecInt

clear() - Method in class org.sat4j.core.Vec

clear() - Method in class org.sat4j.core.VecInt

clear() - Method in class org.sat4j.minisat.core.CircularBuffer

clear() - Method in class org.sat4j.minisat.core.IntQueue

Vide la queue

clear() - Method in interface org.sat4j.specs.IVec

clear() - Method in interface org.sat4j.specs.IVecInt

clearDecorated() - Method in class org.sat4j.tools.SolverDecorator

Method to be called to clear the decorator from its decorated solver.

clearLearntClauses() - Method in class org.sat4j.minisat.core.Solver

clearLearntClauses() - Method in interface org.sat4j.specs.ISolver

Remove clauses learned during the solving process.

clearLearntClauses() - Method in class org.sat4j.tools.AbstractOutputSolver

clearLearntClauses() - Method in class org.sat4j.tools.ManyCore

clearLearntClauses() - Method in class org.sat4j.tools.SolverDecorator

close() - Method in class org.sat4j.reader.EfficientScanner

Commander - Class in org.sat4j.tools.encoding

Commander encoding for "at most one" and "at most k" cases.

Commander() - Constructor for class org.sat4j.tools.encoding.Commander

COMMENT_PREFIX - Static variable in class org.sat4j.AbstractLauncher

compare(A, A) - Method in class org.sat4j.core.DefaultComparator

compare(Constr, Constr) - Method in class org.sat4j.minisat.core.ActivityComparator

computePropagation(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard

computeWatches() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard

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

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

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

ConflictDepthTracing - Class in org.sat4j.tools

ConflictDepthTracing(IVisualizationTool, IVisualizationTool, IVisualizationTool) - Constructor for class org.sat4j.tools.ConflictDepthTracing

conflictDetectedInWatchesFor(int, int) - Method in class org.sat4j.minisat.constraints.AbstractDataStructureFactory

conflictDetectedInWatchesFor(int, int) - Method in interface org.sat4j.minisat.core.DataStructureFactory

conflictFound(IConstr, int, int) - Method in interface org.sat4j.specs.SearchListener

a conflict has been found.

conflictFound(int) - Method in interface org.sat4j.specs.SearchListener

a conflict has been found while propagating values.

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

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

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

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

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

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

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

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

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

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

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

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

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

ConflictLevelTracing - Class in org.sat4j.tools

ConflictLevelTracing(IVisualizationTool, IVisualizationTool, IVisualizationTool) - Constructor for class org.sat4j.tools.ConflictLevelTracing

conflicts - Variable in class org.sat4j.minisat.core.SolverStats

ConflictTimer - Interface in org.sat4j.minisat.core

Conflict based timer.

ConflictTimerAdapter - Class in org.sat4j.minisat.core

Perform a task when a given number of conflicts is reached.

ConflictTimerAdapter(int) - Constructor for class org.sat4j.minisat.core.ConflictTimerAdapter

ConflictTimerContainer - Class in org.sat4j.minisat.core

Agregator for conflict timers (composite design pattern).

ConflictTimerContainer() - Constructor for class org.sat4j.minisat.core.ConflictTimerContainer

CONSOLE - Static variable in interface org.sat4j.minisat.core.ICDCLLogger

Constr - Interface in org.sat4j.minisat.core

Basic constraint abstraction used in Solver.

ConstrGroup - Class in org.sat4j.core

A utility class used to manage easily group of clauses to be deleted at some point in the solver.

ConstrGroup() - Constructor for class org.sat4j.core.ConstrGroup

Create a ConstrGroup that cannot contain null constrs.

ConstrGroup(boolean) - Constructor for class org.sat4j.core.ConstrGroup

Create a new constrGroup.

constrs - Variable in class org.sat4j.minisat.core.Solver

Set of original constraints.

constrs - Variable in class org.sat4j.tools.xplain.HighLevelXplain

constrs - Variable in class org.sat4j.tools.xplain.Xplain

contains(T) - Method in class org.sat4j.core.ReadOnlyVec

contains(int) - Method in class org.sat4j.core.ReadOnlyVecInt

contains(T) - Method in class org.sat4j.core.Vec

contains(int) - Method in class org.sat4j.core.VecInt

contains(T) - Method in interface org.sat4j.specs.IVec

contains(int) - Method in interface org.sat4j.specs.IVecInt

containsAt(int) - Method in class org.sat4j.core.ReadOnlyVecInt

containsAt(int, int) - Method in class org.sat4j.core.ReadOnlyVecInt

containsAt(int) - Method in class org.sat4j.core.VecInt

containsAt(int, int) - Method in class org.sat4j.core.VecInt

containsAt(int) - Method in interface org.sat4j.specs.IVecInt

returns the index of the first occurrence of e, else -1.

containsAt(int, int) - Method in interface org.sat4j.specs.IVecInt

returns the index of the first occurence of e occurring after from (excluded), else -1.

ContradictionException - Exception in org.sat4j.specs

That exception is launched whenever a trivial contradiction is found (e.g.

ContradictionException() - Constructor for exception org.sat4j.specs.ContradictionException

ContradictionException(String) - Constructor for exception org.sat4j.specs.ContradictionException

ContradictionException(Throwable) - Constructor for exception org.sat4j.specs.ContradictionException

ContradictionException(String, Throwable) - Constructor for exception org.sat4j.specs.ContradictionException

copyTo(IVec<T>) - Method in class org.sat4j.core.ReadOnlyVec

copyTo(E[]) - Method in class org.sat4j.core.ReadOnlyVec

copyTo(IVecInt) - Method in class org.sat4j.core.ReadOnlyVecInt

copyTo(int[]) - Method in class org.sat4j.core.ReadOnlyVecInt

copyTo(IVec<T>) - Method in class org.sat4j.core.Vec

Ces operations devraient se faire en temps constant.

copyTo(E[]) - Method in class org.sat4j.core.Vec

copyTo(IVecInt) - Method in class org.sat4j.core.VecInt

Copy the content of this vector into another one.

copyTo(int[]) - Method in class org.sat4j.core.VecInt

Copy the content of this vector into an array of integer.

copyTo(IVec<T>) - Method in interface org.sat4j.specs.IVec

Ces operations devraient se faire en temps constant.

copyTo(E[]) - Method in interface org.sat4j.specs.IVec

copyTo(IVecInt) - Method in interface org.sat4j.specs.IVecInt

C'est operations devraient se faire en temps constant.

copyTo(int[]) - Method in interface org.sat4j.specs.IVecInt

COUNT - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader

Counter - Class in org.sat4j.minisat.core

Counter() - Constructor for class org.sat4j.minisat.core.Counter

Counter(int) - Constructor for class org.sat4j.minisat.core.Counter

countSolutions() - Method in class org.sat4j.tools.SolutionCounter

Naive approach to count the solutions available in a boolean formula: each time a solution is found, a new clause is added to prevent it to be found again.

createCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.AbstractDataStructureFactory

createCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructure

createCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructureYanMax

createCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructureYanMin

createCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.MixedDataStructureDanielHT

createCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.MixedDataStructureDanielWL

createCardinalityConstraint(IVecInt, int) - Method in class org.sat4j.minisat.constraints.MixedDataStructureSingleWL

createCardinalityConstraint(IVecInt, int) - Method in interface org.sat4j.minisat.core.DataStructureFactory

Create a cardinality constraint of the form sum li >= degree.

createClause(IVecInt) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructure

createClause(IVecInt) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructureYanMax

createClause(IVecInt) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructureYanMin

createClause(IVecInt) - Method in class org.sat4j.minisat.constraints.ClausalDataStructureWL

createClause(IVecInt) - Method in class org.sat4j.minisat.constraints.MixedDataStructureDanielHT

createClause(IVecInt) - Method in class org.sat4j.minisat.constraints.MixedDataStructureDanielWL

createClause(IVecInt) - Method in class org.sat4j.minisat.constraints.MixedDataStructureSingleWL

createClause(IVecInt) - Method in interface org.sat4j.minisat.core.DataStructureFactory

createLits() - Method in class org.sat4j.minisat.constraints.AbstractCardinalityDataStructure

createLits() - Method in class org.sat4j.minisat.constraints.AbstractDataStructureFactory

createLits() - Method in class org.sat4j.minisat.constraints.ClausalDataStructureWL

createLits() - Method in class org.sat4j.minisat.constraints.MixedDataStructureDanielHT

createLits() - Method in class org.sat4j.minisat.constraints.MixedDataStructureDanielWL

createLits() - Method in class org.sat4j.minisat.constraints.MixedDataStructureSingleWL

createNewVar(IVecInt) - Method in class org.sat4j.tools.xplain.HighLevelXplain

createNewVar(IVecInt) - Method in class org.sat4j.tools.xplain.Xplain

createReader(ISolver, String) - Method in class org.sat4j.AbstractLauncher

createReader(ISolver, String) - Method in class org.sat4j.BasicLauncher

createReader(ISolver, String) - Method in class org.sat4j.MUSLauncher

createSolverByName(String) - Method in class org.sat4j.core.ASolverFactory

create a solver from its String name. the solvername Xxxx must map one of the newXxxx methods.

createUnregisteredClause(IVecInt) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructure

createUnregisteredClause(IVecInt) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructureYanMax

createUnregisteredClause(IVecInt) - Method in class org.sat4j.minisat.constraints.CardinalityDataStructureYanMin

createUnregisteredClause(IVecInt) - Method in class org.sat4j.minisat.constraints.ClausalDataStructureWL

createUnregisteredClause(IVecInt) - Method in class org.sat4j.minisat.constraints.MixedDataStructureDanielHT

createUnregisteredClause(IVecInt) - Method in class org.sat4j.minisat.constraints.MixedDataStructureDanielWL

createUnregisteredClause(IVecInt) - Method in class org.sat4j.minisat.constraints.MixedDataStructureSingleWL

createUnregisteredClause(IVecInt) - Method in interface org.sat4j.minisat.core.DataStructureFactory

criteria - Variable in class org.sat4j.tools.LexicoDecorator

currentChar() - Method in class org.sat4j.reader.EfficientScanner

currentCriterion - Variable in class org.sat4j.tools.LexicoDecorator

currentDecisionLevel() - Method in class org.sat4j.minisat.core.Solver

currentDecisionLevel() - Method in interface org.sat4j.specs.ISolverService

To access the current decision level

D

DataStructureFactory - Interface in org.sat4j.minisat.core

The aim of the factory is to provide a concrete implementation of clauses, cardinality constraints and pseudo boolean consraints.

dec() - Method in class org.sat4j.minisat.core.Counter

decayActivities() - Method in class org.sat4j.minisat.core.Solver

decisionLevel() - Method in class org.sat4j.minisat.core.Solver

DecisionLevelTracing - Class in org.sat4j.tools

DecisionLevelTracing(IVisualizationTool) - Constructor for class org.sat4j.tools.DecisionLevelTracing

decisions - Variable in class org.sat4j.minisat.core.SolverStats

DecisionTracing - Class in org.sat4j.tools

DecisionTracing(IVisualizationTool, IVisualizationTool, IVisualizationTool, IVisualizationTool) - Constructor for class org.sat4j.tools.DecisionTracing

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

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

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

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

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

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

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

Deprecated.

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

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

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

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

Deprecated.

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

Produce a model using the reader format on a provided printwriter.

decode(int[]) - Method in class org.sat4j.tools.DimacsArrayReader

decorated() - Method in class org.sat4j.tools.SolverDecorator

DEFAULT_LUBY_FACTOR - Static variable in class org.sat4j.minisat.restarts.LubyRestarts

DefaultComparator<A extends Comparable<A>> - Class in org.sat4j.core

A simple comparator for comparable objects.

DefaultComparator() - Constructor for class org.sat4j.core.DefaultComparator

defaultSolver() - Method in class org.sat4j.core.ASolverFactory

To obtain the default solver of the library.

defaultSolver() - Method in class org.sat4j.LightFactory

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

degree - Variable in class org.sat4j.minisat.constraints.card.MinWatchCard

degree of the cardinality constraint

delete(int) - Method in class org.sat4j.core.ReadOnlyVec

delete(int) - Method in class org.sat4j.core.ReadOnlyVecInt

delete(int) - Method in class org.sat4j.core.Vec

Delete the ith element of the vector.

delete(int) - Method in class org.sat4j.core.VecInt

Delete the ith element of the vector.

delete(int) - Method in interface org.sat4j.specs.IVec

Delete the ith element of the vector.

delete(int) - Method in interface org.sat4j.specs.IVecInt

Delete the ith element of the vector.

delete(int[]) - Method in interface org.sat4j.specs.SearchListener

delete a clause

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

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

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

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

DeletionStrategy - Class in org.sat4j.tools.xplain

An implementation of the deletion based minimization.

DeletionStrategy() - Constructor for class org.sat4j.tools.xplain.DeletionStrategy

dequeue() - Method in class org.sat4j.minisat.core.IntQueue

returns the nexdt element in the queue.

dimacs2internal(IVecInt) - Method in class org.sat4j.minisat.core.Solver

DimacsArrayReader - Class in org.sat4j.tools

Very simple Dimacs array reader.

DimacsArrayReader(ISolver) - Constructor for class org.sat4j.tools.DimacsArrayReader

DimacsOutputSolver - Class in org.sat4j.tools

Solver used to display in a writer the CNF instance in Dimacs format.

DimacsOutputSolver() - Constructor for class org.sat4j.tools.DimacsOutputSolver

DimacsOutputSolver(PrintWriter) - Constructor for class org.sat4j.tools.DimacsOutputSolver

DimacsReader - Class in org.sat4j.reader

Very simple Dimacs file parser.

DimacsReader(ISolver) - Constructor for class org.sat4j.reader.DimacsReader

DimacsReader(ISolver, String) - Constructor for class org.sat4j.reader.DimacsReader

DimacsStringSolver - Class in org.sat4j.tools

Solver used to write down a CNF into a String.

DimacsStringSolver() - Constructor for class org.sat4j.tools.DimacsStringSolver

DimacsStringSolver(int) - Constructor for class org.sat4j.tools.DimacsStringSolver

disableNumberOfConstraintCheck() - Method in class org.sat4j.reader.DimacsReader

discard() - Method in class org.sat4j.opt.MaxSatDecorator

discard() - Method in class org.sat4j.opt.MinOneDecorator

discard() - Method in interface org.sat4j.specs.IOptimizationProblem

Deprecated.

discard() - Method in class org.sat4j.tools.LexicoDecorator

discardCurrentSolution() - Method in class org.sat4j.opt.MaxSatDecorator

discardCurrentSolution() - Method in class org.sat4j.opt.MinOneDecorator

discardCurrentSolution() - Method in interface org.sat4j.specs.IOptimizationProblem

Discard the current solution in the optimization problem.

discardCurrentSolution() - Method in class org.sat4j.tools.LexicoDecorator

discardLastestVar() - Method in class org.sat4j.tools.xplain.HighLevelXplain

discardLastestVar() - Method in class org.sat4j.tools.xplain.Xplain

discardSolutionsForOptimizing() - Method in class org.sat4j.tools.LexicoDecorator

displayAnswer() - Method in class org.sat4j.AbstractOptimizationLauncher

displayHeader() - Method in class org.sat4j.AbstractLauncher

displayLicense() - Method in class org.sat4j.AbstractLauncher

displayResult() - Method in class org.sat4j.AbstractLauncher

displayResult() - Method in class org.sat4j.AbstractOptimizationLauncher

displayResult() - Method in class org.sat4j.MUSLauncher

DotSearchTracing<T> - Class in org.sat4j.tools

Class allowing to express the search as a tree in the dot language.

DotSearchTracing(String, Map<Integer, T>) - Constructor for class org.sat4j.tools.DotSearchTracing

dsfactory - Variable in class org.sat4j.minisat.core.Solver

E

EfficientScanner - Class in org.sat4j.reader

Efficient scanner based on the LecteurDimacs class written by Frederic Laihem.

EfficientScanner(InputStream, char) - Constructor for class org.sat4j.reader.EfficientScanner

EfficientScanner(InputStream) - Constructor for class org.sat4j.reader.EfficientScanner

EMPTY - Static variable in class org.sat4j.core.VecInt

empty() - Method in class org.sat4j.minisat.core.Heap

EncodingStrategy - Enum in org.sat4j.tools.encoding

This Enum describes the different encodings that can be used for the "at most one", "at most k", "exactly one", "exactly k" constraints.

EncodingStrategyAdapter - Class in org.sat4j.tools.encoding

The aim of this class is to use different encodings for specific constraints.

EncodingStrategyAdapter() - Constructor for class org.sat4j.tools.encoding.EncodingStrategyAdapter

end(Lbool) - Method in interface org.sat4j.specs.SearchListener

End the search.

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

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

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

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

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

end() - Method in class org.sat4j.tools.FileBasedVisualizationTool

end() - Method in interface org.sat4j.tools.IVisualizationTool

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

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

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

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

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

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

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

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

enqueue(int) - Method in class org.sat4j.minisat.core.Solver

enqueue(int, Constr) - Method in class org.sat4j.minisat.core.Solver

enqueue(int) - Method in interface org.sat4j.minisat.core.UnitPropagationListener

satisfies a literal

enqueue(int, Constr) - Method in interface org.sat4j.minisat.core.UnitPropagationListener

satisfies a literal

ensure(int) - Method in class org.sat4j.core.ReadOnlyVec

ensure(int) - Method in class org.sat4j.core.ReadOnlyVecInt

ensure(int) - Method in class org.sat4j.core.Vec

ensure(int) - Method in class org.sat4j.core.VecInt

ensure(int) - Method in class org.sat4j.minisat.core.IntQueue

Utilisee pour accroitre dynamiquement la taille de la queue.

ensure(int) - Method in interface org.sat4j.specs.IVec

ensure(int) - Method in interface org.sat4j.specs.IVecInt

ensurePool(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits

ensurePool(int) - Method in interface org.sat4j.minisat.core.ILits

Make sure that all data structures are ready to manage howmany boolean variables.

eof() - Method in class org.sat4j.reader.EfficientScanner

equals(Object) - Method in class org.sat4j.core.Vec

equals(Object) - Method in class org.sat4j.core.VecInt

Two vectors are equals iff they have the very same elements in the order.

equals(Object) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard

equals(Object) - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause

equals(Object) - Method in class org.sat4j.minisat.constraints.cnf.HTClause

equals(Object) - Method in class org.sat4j.minisat.constraints.cnf.WLClause

evaluate() - Method in class org.sat4j.tools.LexicoDecorator

exitCode - Variable in class org.sat4j.AbstractLauncher

ExitCode - Class in org.sat4j

Enumeration allowing to manage easily exit code for the SAT and PB Competitions.

expectedNbOfConstr - Variable in class org.sat4j.reader.DimacsReader

EXPENSIVE_SIMPLIFICATION - Variable in class org.sat4j.minisat.core.Solver

EXPENSIVE_SIMPLIFICATION_WLONLY - Variable in class org.sat4j.minisat.core.Solver

expireTimeout() - Method in class org.sat4j.minisat.core.Solver

expireTimeout() - Method in interface org.sat4j.specs.ISolver

Expire the timeout of the solver.

expireTimeout() - Method in class org.sat4j.tools.AbstractOutputSolver

expireTimeout() - Method in class org.sat4j.tools.ManyCore

expireTimeout() - Method in class org.sat4j.tools.SolverDecorator

explain(ISolver, Map<Integer, ?>, IVecInt) - Method in class org.sat4j.tools.xplain.DeletionStrategy

explain() - Method in class org.sat4j.tools.xplain.HighLevelXplain

explain(ISolver, Map<Integer, ?>, IVecInt) - Method in class org.sat4j.tools.xplain.InsertionStrategy

explain(ISolver, Map<Integer, ?>, IVecInt) - Method in interface org.sat4j.tools.xplain.MinimizationStrategy

explain(ISolver, Map<Integer, ?>, IVecInt) - Method in class org.sat4j.tools.xplain.QuickXplain2001Strategy

explain(ISolver, Map<Integer, ?>, IVecInt) - Method in class org.sat4j.tools.xplain.QuickXplainStrategy

explain() - Method in class org.sat4j.tools.xplain.Xplain

Explainer - Interface in org.sat4j.tools.xplain

ExtendedDimacsArrayReader - Class in org.sat4j.tools

Reader for the Extended Dimacs format proposed by Fahiem Bacchus and Toby Walsh in array representation (without the terminating 0).

ExtendedDimacsArrayReader(ISolver) - Constructor for class org.sat4j.tools.ExtendedDimacsArrayReader

F

FALSE - Static variable in class org.sat4j.specs.Lbool

FALSE - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader

FileBasedVisualizationTool - Class in org.sat4j.tools

FileBasedVisualizationTool(String) - Constructor for class org.sat4j.tools.FileBasedVisualizationTool

findModel() - Method in class org.sat4j.minisat.core.Solver

findModel(IVecInt) - Method in class org.sat4j.minisat.core.Solver

findModel() - Method in interface org.sat4j.specs.IProblem

Look for a model satisfying all the clauses available in the problem.

findModel(IVecInt) - Method in interface org.sat4j.specs.IProblem

Look for a model satisfying all the clauses available in the problem.

findModel() - Method in class org.sat4j.tools.AbstractOutputSolver

findModel(IVecInt) - Method in class org.sat4j.tools.AbstractOutputSolver

findModel() - Method in class org.sat4j.tools.ManyCore

findModel(IVecInt) - Method in class org.sat4j.tools.ManyCore

findModel() - Method in class org.sat4j.tools.SolverDecorator

findModel(IVecInt) - Method in class org.sat4j.tools.SolverDecorator

findModel() - Method in class org.sat4j.tools.xplain.HighLevelXplain

findModel(IVecInt) - Method in class org.sat4j.tools.xplain.HighLevelXplain

findModel() - Method in class org.sat4j.tools.xplain.Xplain

findModel(IVecInt) - Method in class org.sat4j.tools.xplain.Xplain

firstConstr - Variable in class org.sat4j.tools.AbstractOutputSolver

fixCriterionValue() - Method in class org.sat4j.tools.LexicoDecorator

FixedLengthLearning<D extends DataStructureFactory> - Class in org.sat4j.minisat.learning

A learning scheme for learning constraints of size smaller than a given constant.

FixedLengthLearning() - Constructor for class org.sat4j.minisat.learning.FixedLengthLearning

FixedLengthLearning(int) - Constructor for class org.sat4j.minisat.learning.FixedLengthLearning

fixedNbClauses - Variable in class org.sat4j.tools.AbstractOutputSolver

fixedSize(int) - Method in class org.sat4j.minisat.core.Solver

flushConstraint() - Method in class org.sat4j.reader.DimacsReader

flushConstraint() - Method in class org.sat4j.reader.GroupedCNFReader

forceObjectiveValueTo(Number) - Method in class org.sat4j.opt.MaxSatDecorator

forceObjectiveValueTo(Number) - Method in class org.sat4j.opt.MinOneDecorator

forceObjectiveValueTo(Number) - Method in interface org.sat4j.specs.IOptimizationProblem

Force the value of the objective function.

forceObjectiveValueTo(Number) - Method in class org.sat4j.tools.LexicoDecorator

forgets(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits

forgets(int) - Method in interface org.sat4j.minisat.core.ILits

Removes a variable from the formula.

formatString - Variable in class org.sat4j.reader.DimacsReader

forwardActivity(double) - Method in class org.sat4j.minisat.constraints.card.AtLeast

forwardActivity(double) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard

forwardActivity(double) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard

forwardActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.LearntBinaryClause

forwardActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.LearntHTClause

forwardActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.LearntWLClause

forwardActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.OriginalBinaryClause

forwardActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.OriginalHTClause

forwardActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.OriginalWLClause

forwardActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.UnitClause

forwardActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses

forwardActivity(double) - Method in interface org.sat4j.minisat.core.Constr

Deprecated.

fullAdderCarry(int, int, int, int) - Method in class org.sat4j.tools.GateTranslator

fullAdderSum(int, int, int, int) - Method in class org.sat4j.tools.GateTranslator

G

gateFalse(int) - Method in class org.sat4j.tools.GateTranslator

translate y <=> FALSE into a clause.

GateTranslator - Class in org.sat4j.tools

Utility class to easily feed a SAT solver using logical gates.

GateTranslator(ISolver) - Constructor for class org.sat4j.tools.GateTranslator

gateTrue(int) - Method in class org.sat4j.tools.GateTranslator

translate y <=> TRUE into a clause.

get(int) - Method in class org.sat4j.core.ConstrGroup

get(int) - Method in class org.sat4j.core.ReadOnlyVec

get(int) - Method in class org.sat4j.core.ReadOnlyVecInt

get(int) - Method in class org.sat4j.core.Vec

get(int) - Method in class org.sat4j.core.VecInt

get(int) - Method in class org.sat4j.minisat.constraints.card.AtLeast

get(int) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard

get(int) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard

get(int) - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause

Retourne le ieme literal de la clause.

get(int) - Method in class org.sat4j.minisat.constraints.cnf.HTClause

Return the ith literal of the clause.

get(int) - Method in class org.sat4j.minisat.constraints.cnf.UnitClause

get(int) - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses

get(int) - Method in class org.sat4j.minisat.constraints.cnf.WLClause

Retourne le ieme literal de la clause.

get(int) - Method in class org.sat4j.minisat.core.Heap

get(int) - Method in interface org.sat4j.specs.IConstr

returns the ith literal in the constraint

get(int) - Method in interface org.sat4j.specs.IVec

get(int) - Method in interface org.sat4j.specs.IVecInt

getActivity() - Method in class org.sat4j.core.ConstrGroup

getActivity() - Method in class org.sat4j.minisat.constraints.card.AtLeast

getActivity() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard

Obtenir la valeur de l'activit?

getActivity() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard

Returns the activity of the constraint

getActivity() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause

getActivity() - Method in class org.sat4j.minisat.constraints.cnf.HTClause

getActivity() - Method in class org.sat4j.minisat.constraints.cnf.UnitClause

getActivity() - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses

getActivity() - Method in class org.sat4j.minisat.constraints.cnf.WLClause

getActivity() - Method in interface org.sat4j.specs.IConstr

To obtain the activity of the constraint.

getActivityPercent() - Method in class org.sat4j.minisat.learning.ActiveLearning

getAtLeastKEncoding() - Method in class org.sat4j.tools.encoding.Policy

getAtLeastOneEncoding() - Method in class org.sat4j.tools.encoding.Policy

getAtMostKEncoding() - Method in class org.sat4j.tools.encoding.Policy

getAtMostOneEncoding() - Method in class org.sat4j.tools.encoding.Policy

getBeginTime() - Method in class org.sat4j.AbstractLauncher

Obtaining the current time spent since the beginning of the solving process.

getClaDecay() - Method in class org.sat4j.minisat.core.SearchParams

getCoef(int) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard

getConflictBoundIncFactor() - Method in class org.sat4j.minisat.core.SearchParams

getConstr(int) - Method in class org.sat4j.core.ConstrGroup

getConstraints() - Method in class org.sat4j.tools.xplain.Xplain

getDegree() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard

getDSFactory() - Method in class org.sat4j.minisat.core.Solver

getExactlyKEncoding() - Method in class org.sat4j.tools.encoding.Policy

getExactlyOneEncoding() - Method in class org.sat4j.tools.encoding.Policy

getExitCode() - Method in class org.sat4j.AbstractLauncher

Get the value of the ExitCode

getExpectedNumberOfClauses() - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator

getFactor() - Method in class org.sat4j.minisat.restarts.LubyRestarts

getFilename() - Method in class org.sat4j.tools.FileBasedVisualizationTool

getFromPool(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits

getFromPool(int) - Method in interface org.sat4j.minisat.core.ILits

Translates a Dimacs literal into an internal representation literal.

getInitConflictBound() - Method in class org.sat4j.minisat.core.SearchParams

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

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

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

getIthConstr(int) - Method in class org.sat4j.minisat.core.Solver

returns the ith constraint in the solver.

getLearnedConstraints() - Method in class org.sat4j.minisat.core.Solver

getLearnedConstraints() - Method in interface org.sat4j.specs.ISolverService

Read-Only access to the list of constraints learned and not deleted so far in the solver.

getLevel(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits

getLevel(int) - Method in interface org.sat4j.minisat.core.ILits

Returns the level at which that literal has been assigned a value, else -1.

getLimit() - Method in class org.sat4j.minisat.learning.ActiveLearning

getLimit() - Method in class org.sat4j.minisat.learning.PercentLengthLearning

getLiteralsPropagatedAt(int) - Method in class org.sat4j.minisat.core.Solver

getLiteralsPropagatedAt(int) - Method in interface org.sat4j.specs.ISolverService

To access the literals propagated at a specific decision level.

getLits() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard

getLits() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause

getLits() - Method in class org.sat4j.minisat.constraints.cnf.HTClause

getLits() - Method in class org.sat4j.minisat.constraints.cnf.WLClause

getLogger() - Method in interface org.sat4j.minisat.core.ICDCL

getLogger() - Method in class org.sat4j.minisat.core.Solver

getLogPrefix() - Method in class org.sat4j.minisat.core.Solver

getLogPrefix() - Method in interface org.sat4j.specs.ISolver

getLogPrefix() - Method in class org.sat4j.tools.AbstractOutputSolver

getLogPrefix() - Method in class org.sat4j.tools.ManyCore

getLogPrefix() - Method in class org.sat4j.tools.SolverDecorator

getLogWriter() - Method in class org.sat4j.AbstractLauncher

getMaxLength() - Method in class org.sat4j.minisat.learning.FixedLengthLearning

getmin() - Method in class org.sat4j.minisat.core.Heap

getNumberOfSolutionFound() - Method in class org.sat4j.tools.SearchEnumeratorListener

getObjectiveValue() - Method in class org.sat4j.opt.MaxSatDecorator

getObjectiveValue() - Method in class org.sat4j.opt.MinOneDecorator

getObjectiveValue() - Method in interface org.sat4j.specs.IOptimizationProblem

Read only access to the value of the objective function for the current solution.

getObjectiveValue() - Method in class org.sat4j.tools.LexicoDecorator

getOrder() - Method in interface org.sat4j.minisat.core.ICDCL

getOrder() - Method in class org.sat4j.minisat.core.Solver

getOut() - Method in class org.sat4j.tools.DimacsStringSolver

getOutLearnt() - Method in class org.sat4j.minisat.core.Solver

getPeriod() - Method in class org.sat4j.minisat.orders.PureOrder

getPhaseSelectionStrategy() - Method in interface org.sat4j.minisat.core.IOrder

getPhaseSelectionStrategy() - Method in class org.sat4j.minisat.orders.RandomWalkDecorator

getPhaseSelectionStrategy() - Method in class org.sat4j.minisat.orders.TabuListDecorator

getPhaseSelectionStrategy() - Method in class org.sat4j.minisat.orders.VarOrderHeap

getProbability() - Method in class org.sat4j.minisat.orders.RandomWalkDecorator

getReader() - Method in class org.sat4j.AbstractLauncher

getReason(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits

getReason(int) - Method in interface org.sat4j.minisat.core.ILits

Returns the reason of the assignment of a literal.

getRestartStrategy() - Method in interface org.sat4j.minisat.core.ICDCL

getRestartStrategy() - Method in class org.sat4j.minisat.core.Solver

getSearchListener() - Method in class org.sat4j.minisat.core.Solver

getSearchListener() - Method in interface org.sat4j.specs.ISolver

Get the current SearchListener.

getSearchListener() - Method in class org.sat4j.tools.AbstractOutputSolver

getSearchListener() - Method in class org.sat4j.tools.ManyCore

getSearchListener() - Method in class org.sat4j.tools.SolverDecorator

getSearchParams() - Method in interface org.sat4j.minisat.core.RestartStrategy

getSearchParams() - Method in class org.sat4j.minisat.restarts.ArminRestarts

getSearchParams() - Method in class org.sat4j.minisat.restarts.LubyRestarts

getSearchParams() - Method in class org.sat4j.minisat.restarts.MiniSATRestarts

getSearchParams() - Method in class org.sat4j.minisat.restarts.NoRestarts

getSimplifier() - Method in interface org.sat4j.minisat.core.ICDCL

getSimplifier() - Method in class org.sat4j.minisat.core.Solver

getSolver() - Method in class org.sat4j.reader.DimacsReader

getSolver() - Method in class org.sat4j.tools.DimacsArrayReader

getSolvers() - Method in class org.sat4j.tools.ManyCore

getStat() - Method in class org.sat4j.minisat.core.Solver

getStat() - Method in interface org.sat4j.specs.ISolver

To obtain a map of the available statistics from the solver.

getStat() - Method in class org.sat4j.tools.AbstractOutputSolver

getStat() - Method in class org.sat4j.tools.ManyCore

getStat() - Method in class org.sat4j.tools.SolverDecorator

getStats() - Method in class org.sat4j.minisat.core.Solver

getString(String) - Static method in class org.sat4j.Messages

getTimeout() - Method in class org.sat4j.minisat.core.Solver

getTimeout() - Method in interface org.sat4j.specs.ISolver

Useful to check the internal timeout of the solver.

getTimeout() - Method in class org.sat4j.tools.AbstractOutputSolver

getTimeout() - Method in class org.sat4j.tools.ManyCore

getTimeout() - Method in class org.sat4j.tools.SolverDecorator

getTimeoutMs() - Method in class org.sat4j.minisat.core.Solver

getTimeoutMs() - Method in interface org.sat4j.specs.ISolver

Useful to check the internal timeout of the solver.

getTimeoutMs() - Method in class org.sat4j.tools.AbstractOutputSolver

getTimeoutMs() - Method in class org.sat4j.tools.ManyCore

getTimeoutMs() - Method in class org.sat4j.tools.SolverDecorator

getTimer() - Method in interface org.sat4j.minisat.core.LearnedConstraintsDeletionStrategy

getValue() - Method in class org.sat4j.minisat.core.Counter

getVarDecay() - Method in class org.sat4j.minisat.core.SearchParams

getVariableHeuristics() - Method in interface org.sat4j.minisat.core.IOrder

Read-Only access to the value of the heuristics for each variable.

getVariableHeuristics() - Method in class org.sat4j.minisat.core.Solver

getVariableHeuristics() - Method in class org.sat4j.minisat.orders.RandomWalkDecorator

getVariableHeuristics() - Method in class org.sat4j.minisat.orders.TabuListDecorator

getVariableHeuristics() - Method in class org.sat4j.minisat.orders.VarOrderHeap

getVariableHeuristics() - Method in interface org.sat4j.specs.ISolverService

Read-Only access to the value of the heuristics for each variable.

getVocabulary() - Method in class org.sat4j.minisat.constraints.AbstractDataStructureFactory

getVocabulary() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard

getVocabulary() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard

getVocabulary() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause

getVocabulary() - Method in class org.sat4j.minisat.constraints.cnf.HTClause

getVocabulary() - Method in class org.sat4j.minisat.constraints.cnf.WLClause

getVocabulary() - Method in interface org.sat4j.minisat.core.DataStructureFactory

getVocabulary() - Method in class org.sat4j.minisat.core.Solver

getVocabulary() - Method in class org.sat4j.minisat.orders.VarOrderHeap

getWatchesFor(int) - Method in class org.sat4j.minisat.constraints.AbstractDataStructureFactory

getWatchesFor(int) - Method in interface org.sat4j.minisat.core.DataStructureFactory

glucose - Variable in class org.sat4j.minisat.core.Solver

GroupedCNFReader - Class in org.sat4j.reader

GroupedCNFReader(HighLevelXplain<ISolver>) - Constructor for class org.sat4j.reader.GroupedCNFReader

growTo(int, T) - Method in class org.sat4j.core.ReadOnlyVec

growTo(int, int) - Method in class org.sat4j.core.ReadOnlyVecInt

growTo(int, T) - Method in class org.sat4j.core.Vec

growTo(int, int) - Method in class org.sat4j.core.VecInt

growTo(int, T) - Method in interface org.sat4j.specs.IVec

growTo(int, int) - Method in interface org.sat4j.specs.IVecInt

H

halfAdderCarry(int, int, int) - Method in class org.sat4j.tools.GateTranslator

halfAdderSum(int, int, int) - Method in class org.sat4j.tools.GateTranslator

halfOr(int, IVecInt) - Method in class org.sat4j.tools.GateTranslator

translate y <= x1 \/ x2 \/ ... \/ xn into clauses.

handleConstr(int, int, int[]) - Method in class org.sat4j.tools.DimacsArrayReader

handleConstr(int, int, int[]) - Method in class org.sat4j.tools.ExtendedDimacsArrayReader

Handles a single constraint (constraint == Extended Dimacs circuit gate).

handleLine() - Method in class org.sat4j.reader.DimacsReader

handleLine() - Method in class org.sat4j.reader.GroupedCNFReader

hasASingleSolution() - Method in class org.sat4j.tools.SingleSolutionDetector

Please use that method only after a positive answer from isSatisfiable() (else a runtime exception will be launched).

hasASingleSolution(IVecInt) - Method in class org.sat4j.tools.SingleSolutionDetector

Please use that method only after a positive answer from isSatisfiable(assumptions) (else a runtime exception will be launched).

hashCode() - Method in class org.sat4j.core.Vec

hashCode() - Method in class org.sat4j.core.VecInt

hashCode() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard

hashCode() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause

hashCode() - Method in class org.sat4j.minisat.constraints.cnf.HTClause

hashCode() - Method in class org.sat4j.minisat.constraints.cnf.WLClause

hasNext() - Method in interface org.sat4j.specs.IteratorInt

hasNoObjectiveFunction() - Method in class org.sat4j.opt.MaxSatDecorator

hasNoObjectiveFunction() - Method in class org.sat4j.opt.MinOneDecorator

hasNoObjectiveFunction() - Method in interface org.sat4j.specs.IOptimizationProblem

If the optimization problem has no objective function, then it is a simple decision problem.

hasNoObjectiveFunction() - Method in class org.sat4j.tools.LexicoDecorator

head - Variable in class org.sat4j.minisat.constraints.cnf.BinaryClause

head - Variable in class org.sat4j.minisat.constraints.cnf.HTClause

Heap - Class in org.sat4j.minisat.core

Heap implementation used to maintain the variables order in some heuristics.

Heap(double[]) - Constructor for class org.sat4j.minisat.core.Heap

heap - Variable in class org.sat4j.minisat.orders.VarOrderHeap

heapProperty() - Method in class org.sat4j.minisat.core.Heap

heapProperty(int) - Method in class org.sat4j.minisat.core.Heap

HeuristicsTracing - Class in org.sat4j.tools

HeuristicsTracing(IVisualizationTool) - Constructor for class org.sat4j.tools.HeuristicsTracing

HighLevelXplain<T extends ISolver> - Class in org.sat4j.tools.xplain

Computation of MUS in a structured CNF, i.e. the clauses belong to components, the explanation is to be extracted in terms of components.

HighLevelXplain(T) - Constructor for class org.sat4j.tools.xplain.HighLevelXplain

HTClause - Class in org.sat4j.minisat.constraints.cnf

Lazy data structure for clause using the Head Tail data structure from SATO, The original scheme is improved by avoiding moving pointers to literals but moving the literals themselves.

HTClause(IVecInt, ILits) - Constructor for class org.sat4j.minisat.constraints.cnf.HTClause

Creates a new basic clause

I

ICDCL<D extends DataStructureFactory> - Interface in org.sat4j.minisat.core

Abstraction for Conflict Driven Clause Learning Solver.

ICDCLLogger - Interface in org.sat4j.minisat.core

IConstr - Interface in org.sat4j.specs

The most general abstraction for handling a constraint.

IFF - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader

iff(int, IVecInt) - Method in class org.sat4j.tools.GateTranslator

translate y <=> (x1 <=> x2 <=> ... <=> xn) into clauses.

IFTHENELSE - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader

ignoredclauses - Variable in class org.sat4j.minisat.core.SolverStats

ILits - Interface in org.sat4j.minisat.core

That interface manages the solver's internal vocabulary.

IMPLIES - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader

inc() - Method in class org.sat4j.minisat.core.Counter

incActivity(double) - Method in class org.sat4j.minisat.constraints.card.AtLeast

incActivity(double) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard

Incr?

incActivity(double) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard

Increments activity of the constraint

incActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.LearntBinaryClause

incActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.LearntHTClause

incActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.LearntWLClause

incActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.OriginalBinaryClause

incActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.OriginalHTClause

incActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.OriginalWLClause

incActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.UnitClause

incActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses

incActivity(double) - Method in interface org.sat4j.minisat.core.Constr

Increase the constraint activity.

increase(int) - Method in class org.sat4j.minisat.core.Heap

indexOf(T) - Method in class org.sat4j.core.ReadOnlyVec

indexOf(int) - Method in class org.sat4j.core.ReadOnlyVecInt

indexOf(T) - Method in class org.sat4j.core.Vec

indexOf(int) - Method in class org.sat4j.core.VecInt

indexOf(T) - Method in interface org.sat4j.specs.IVec

indexOf(int) - Method in interface org.sat4j.specs.IVecInt

inHeap(int) - Method in class org.sat4j.minisat.core.Heap

init(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits

init(int) - Method in interface org.sat4j.minisat.core.ILits

init() - Method in interface org.sat4j.minisat.core.IOrder

that method has the responsibility to initialize all arrays in the heuristics.

init(int) - Method in interface org.sat4j.minisat.core.IPhaseSelectionStrategy

that method has the responsibility to initialize all arrays in the heuristics.

init(int, int) - Method in interface org.sat4j.minisat.core.IPhaseSelectionStrategy

initialize the phase of a given variable to the given value.

init() - Method in interface org.sat4j.minisat.core.LearnedConstraintsDeletionStrategy

init() - Method in interface org.sat4j.minisat.core.LearningStrategy

hook method called just before the search begins.

init(SearchParams) - Method in interface org.sat4j.minisat.core.RestartStrategy

Hook method called just before the search starts.

init() - Method in class org.sat4j.minisat.learning.FixedLengthLearning

init() - Method in class org.sat4j.minisat.learning.LimitedLearning

init() - Method in class org.sat4j.minisat.learning.PercentLengthLearning

init(int) - Method in class org.sat4j.minisat.orders.NegativeLiteralSelectionStrategy

init(int, int) - Method in class org.sat4j.minisat.orders.NegativeLiteralSelectionStrategy

init(int) - Method in class org.sat4j.minisat.orders.PositiveLiteralSelectionStrategy

init(int, int) - Method in class org.sat4j.minisat.orders.PositiveLiteralSelectionStrategy

init(int) - Method in class org.sat4j.minisat.orders.RandomLiteralSelectionStrategy

init(int, int) - Method in class org.sat4j.minisat.orders.RandomLiteralSelectionStrategy

init() - Method in class org.sat4j.minisat.orders.RandomWalkDecorator

init() - Method in class org.sat4j.minisat.orders.SubsetVarOrder

init() - Method in class org.sat4j.minisat.orders.TabuListDecorator

init() - Method in class org.sat4j.minisat.orders.VarOrderHeap

that method has the responsability to initialize all arrays in the heuristics.

init(SearchParams) - Method in class org.sat4j.minisat.restarts.ArminRestarts

init(SearchParams) - Method in class org.sat4j.minisat.restarts.LubyRestarts

init(SearchParams) - Method in class org.sat4j.minisat.restarts.MiniSATRestarts

init(SearchParams) - Method in class org.sat4j.minisat.restarts.NoRestarts

init(S) - Method in interface org.sat4j.specs.SearchListener

Provide access to the solver's controllable interface.

init(ISolverService) - Method in class org.sat4j.tools.ConflictDepthTracing

init(ISolverService) - Method in class org.sat4j.tools.ConflictLevelTracing

init(ISolverService) - Method in class org.sat4j.tools.DecisionTracing

init() - Method in class org.sat4j.tools.FileBasedVisualizationTool

init(ISolverService) - Method in class org.sat4j.tools.HeuristicsTracing

init() - Method in interface org.sat4j.tools.IVisualizationTool

init(ISolverService) - Method in class org.sat4j.tools.LearnedTracing

init(ISolverService) - Method in class org.sat4j.tools.MultiTracing

init(ISolverService) - Method in class org.sat4j.tools.SearchEnumeratorListener

init(S) - Method in class org.sat4j.tools.SearchListenerAdapter

init(ISolverService) - Method in class org.sat4j.tools.SpeedTracing

init(ISolverService) - Method in class org.sat4j.tools.TextOutputTracing

initStats(SolverStats) - Method in class org.sat4j.minisat.core.Solver

insert(int) - Method in class org.sat4j.minisat.core.Heap

insert(int) - Method in class org.sat4j.minisat.core.IntQueue

Add an element to the queue.

insertFirst(T) - Method in class org.sat4j.core.ReadOnlyVec

insertFirst(int) - Method in class org.sat4j.core.ReadOnlyVecInt

insertFirst(T) - Method in class org.sat4j.core.Vec

Insert an element at the very beginning of the vector.

insertFirst(int) - Method in class org.sat4j.core.VecInt

Insert an element at the very begining of the vector.

insertFirst(T) - Method in interface org.sat4j.specs.IVec

Insert an element at the very begining of the vector.

insertFirst(int) - Method in interface org.sat4j.specs.IVecInt

Insert an element at the very begining of the vector.

insertFirstWithShifting(T) - Method in class org.sat4j.core.ReadOnlyVec

insertFirstWithShifting(T) - Method in class org.sat4j.core.Vec

insertFirstWithShifting(T) - Method in interface org.sat4j.specs.IVec

InsertionStrategy - Class in org.sat4j.tools.xplain

An implementation of the ReplayXplain algorithm as explained by Ulrich Junker in the following paper:

InsertionStrategy() - Constructor for class org.sat4j.tools.xplain.InsertionStrategy

inspects - Variable in class org.sat4j.minisat.core.SolverStats

instance() - Static method in class org.sat4j.LightFactory

Access to the single instance of the factory.

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

Access to the single instance of the factory.

InstanceReader - Class in org.sat4j.reader

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

InstanceReader(ISolver) - Constructor for class org.sat4j.reader.InstanceReader

IntQueue - Class in org.sat4j.minisat.core

Implementation of a queue.

IntQueue() - Constructor for class org.sat4j.minisat.core.IntQueue

IOptimizationProblem - Interface in org.sat4j.specs

Represents an optimization problem.

IOrder - Interface in org.sat4j.minisat.core

Interface for the variable ordering heuristics.

IPhaseSelectionStrategy - Interface in org.sat4j.minisat.core

The responsibility of that class is to choose the phase (positive or negative) of the variable that was selected by the IOrder.

IProblem - Interface in org.sat4j.specs

Access to the information related to a given problem instance.

isDBSimplificationAllowed() - Method in class org.sat4j.minisat.core.Solver

isDBSimplificationAllowed() - Method in interface org.sat4j.specs.ISolver

Indicate whether the solver is allowed to simplify the formula by propagating the truth value of top level satisfied variables.

isDBSimplificationAllowed() - Method in class org.sat4j.tools.AbstractOutputSolver

isDBSimplificationAllowed() - Method in class org.sat4j.tools.ManyCore

isDBSimplificationAllowed() - Method in class org.sat4j.tools.SolverDecorator

isEmpty() - Method in class org.sat4j.core.ReadOnlyVec

isEmpty() - Method in class org.sat4j.core.ReadOnlyVecInt

isEmpty() - Method in class org.sat4j.core.Vec

isEmpty() - Method in class org.sat4j.core.VecInt

isEmpty() - Method in interface org.sat4j.specs.IVec

To know if a vector is empty

isEmpty() - Method in interface org.sat4j.specs.IVecInt

To know if a vector is empty

isFalsified(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits

isFalsified(int) - Method in interface org.sat4j.minisat.core.ILits

Check if a literal is falsified.

isFull() - Method in class org.sat4j.minisat.core.CircularBuffer

isImplied(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits

isImplied(int) - Method in interface org.sat4j.minisat.core.ILits

ISimplifier - Interface in org.sat4j.minisat.core

Strategy for simplifying the conflict clause derived by the solver.

isNeedToReduceDB() - Method in class org.sat4j.minisat.core.Solver

ISolver - Interface in org.sat4j.specs

This interface contains all services provided by a SAT solver.

ISolverService - Interface in org.sat4j.specs

The aim on that interface is to allow power users to communicate with the SAT solver using Dimacs format.

isOptimal() - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator

isOptimal() - Method in class org.sat4j.opt.MinOneDecorator

isOptimal() - Method in interface org.sat4j.specs.IOptimizationProblem

Allows to check afterwards if the solution provided by the solver is optimal or not.

isOptimal() - Method in class org.sat4j.tools.LexicoDecorator

isOptimal() - Method in class org.sat4j.tools.OptToSatAdapter

Allow to easily check is the solution returned by isSatisfiable is optimal or not.

isSatisfiable() - Method in class org.sat4j.minisat.core.Solver

isSatisfiable(boolean) - Method in class org.sat4j.minisat.core.Solver

isSatisfiable(IVecInt) - Method in class org.sat4j.minisat.core.Solver

isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.minisat.core.Solver

isSatisfiable() - Method in interface org.sat4j.specs.IProblem

Check the satisfiability of the set of constraints contained inside the solver.

isSatisfiable(IVecInt, boolean) - Method in interface org.sat4j.specs.IProblem

Check the satisfiability of the set of constraints contained inside the solver.

isSatisfiable(boolean) - Method in interface org.sat4j.specs.IProblem

Check the satisfiability of the set of constraints contained inside the solver.

isSatisfiable(IVecInt) - Method in interface org.sat4j.specs.IProblem

Check the satisfiability of the set of constraints contained inside the solver.

isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.tools.AbstractOutputSolver

isSatisfiable(boolean) - Method in class org.sat4j.tools.AbstractOutputSolver

isSatisfiable() - Method in class org.sat4j.tools.AbstractOutputSolver

isSatisfiable(IVecInt) - Method in class org.sat4j.tools.AbstractOutputSolver

isSatisfiable() - Method in class org.sat4j.tools.ManyCore

isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.tools.ManyCore

isSatisfiable(boolean) - Method in class org.sat4j.tools.ManyCore

isSatisfiable(IVecInt) - Method in class org.sat4j.tools.ManyCore

isSatisfiable() - Method in class org.sat4j.tools.ModelIterator

isSatisfiable(IVecInt) - Method in class org.sat4j.tools.ModelIterator

isSatisfiable() - Method in class org.sat4j.tools.OptToSatAdapter

isSatisfiable(boolean) - Method in class org.sat4j.tools.OptToSatAdapter

isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.tools.OptToSatAdapter

isSatisfiable(IVecInt) - Method in class org.sat4j.tools.OptToSatAdapter

isSatisfiable(boolean) - Method in class org.sat4j.tools.SolverDecorator

isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.tools.SolverDecorator

isSatisfiable() - Method in class org.sat4j.tools.SolverDecorator

isSatisfiable(IVecInt) - Method in class org.sat4j.tools.SolverDecorator

isSatisfiable() - Method in class org.sat4j.tools.xplain.HighLevelXplain

isSatisfiable(boolean) - Method in class org.sat4j.tools.xplain.HighLevelXplain

isSatisfiable(IVecInt) - Method in class org.sat4j.tools.xplain.HighLevelXplain

isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.tools.xplain.HighLevelXplain

isSatisfiable() - Method in class org.sat4j.tools.xplain.Xplain

isSatisfiable(boolean) - Method in class org.sat4j.tools.xplain.Xplain

isSatisfiable(IVecInt) - Method in class org.sat4j.tools.xplain.Xplain

isSatisfiable(IVecInt, boolean) - Method in class org.sat4j.tools.xplain.Xplain

isSatisfied(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits

isSatisfied(int) - Method in interface org.sat4j.minisat.core.ILits

Check if a literal is satisfied.

isSolutionOptimal - Variable in class org.sat4j.opt.AbstractSelectorVariablesDecorator

isSolverKeptHot() - Method in class org.sat4j.minisat.core.Solver

isSolverKeptHot() - Method in interface org.sat4j.specs.ISolver

Ask to the solver if it is in "hot" mode, meaning that the heuristics is not reset after call is isSatisfiable().

isSolverKeptHot() - Method in class org.sat4j.tools.AbstractOutputSolver

isSolverKeptHot() - Method in class org.sat4j.tools.ManyCore

isSolverKeptHot() - Method in class org.sat4j.tools.SolverDecorator

isSubsetOf(VecInt) - Method in class org.sat4j.core.VecInt

to detect that the vector is a subset of another one.

isUnassigned(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits

isUnassigned(int) - Method in interface org.sat4j.minisat.core.ILits

Check if a literal is assigned a truth value.

isVerbose() - Method in class org.sat4j.minisat.core.Solver

isVerbose() - Method in class org.sat4j.reader.Reader

isVerbose() - Method in interface org.sat4j.specs.ISolver

To know if the solver is in verbose mode (output allowed) or not.

isVerbose() - Method in class org.sat4j.tools.AbstractOutputSolver

isVerbose() - Method in class org.sat4j.tools.ManyCore

isVerbose() - Method in class org.sat4j.tools.SolverDecorator

ite(int, int, int, int) - Method in class org.sat4j.tools.GateTranslator

translate y <=> if x1 then x2 else x3 into clauses.

iterator() - Method in class org.sat4j.core.ReadOnlyVec

iterator() - Method in class org.sat4j.core.ReadOnlyVecInt

iterator() - Method in class org.sat4j.core.Vec

iterator() - Method in class org.sat4j.core.VecInt

iterator() - Method in interface org.sat4j.specs.IVec

iterator() - Method in interface org.sat4j.specs.IVecInt

IteratorInt - Interface in org.sat4j.specs

Iterator interface to avoid boxing int into Integer.

IVec<T> - Interface in org.sat4j.specs

An abstraction on the type of vector used in the library.

IVecInt - Interface in org.sat4j.specs

An abstraction for the vector of int used on the library.

IVisualizationTool - Interface in org.sat4j.tools

L

Ladder - Class in org.sat4j.tools.encoding

Ladder encoding for the "at most one" and "exactly one" cases.

Ladder() - Constructor for class org.sat4j.tools.encoding.Ladder

last() - Method in class org.sat4j.core.ReadOnlyVec

last() - Method in class org.sat4j.core.ReadOnlyVecInt

last() - Method in class org.sat4j.core.Vec

return the latest element on the stack.

last() - Method in class org.sat4j.core.VecInt

last() - Method in interface org.sat4j.specs.IVec

return the latest element on the stack.

last() - Method in interface org.sat4j.specs.IVecInt

LBDTracing - Class in org.sat4j.tools

LBDTracing(IVisualizationTool) - Constructor for class org.sat4j.tools.LBDTracing

Lbool - Class in org.sat4j.specs

That enumeration defines the possible truth value for a variable: satisfied, falsified or unknown/undefined.

learn(Constr) - Method in interface org.sat4j.minisat.core.Learner

learn(Constr) - Method in class org.sat4j.minisat.core.Solver

learn(IConstr) - Method in interface org.sat4j.specs.SearchListener

learning a new clause

learn(IConstr) - Method in class org.sat4j.tools.DotSearchTracing

learn(IConstr) - Method in class org.sat4j.tools.LearnedClausesSizeTracing

learn(IConstr) - Method in class org.sat4j.tools.MultiTracing

learn(IConstr) - Method in class org.sat4j.tools.SearchListenerAdapter

learn(IConstr) - Method in class org.sat4j.tools.TextOutputTracing

learnConstraint(Constr) - Method in class org.sat4j.minisat.constraints.AbstractDataStructureFactory

learnConstraint(Constr) - Method in interface org.sat4j.minisat.core.DataStructureFactory

learnedbinaryclauses - Variable in class org.sat4j.minisat.core.SolverStats

learnedclauses - Variable in class org.sat4j.minisat.core.SolverStats

LearnedClauseSizeTracing - Class in org.sat4j.tools

LearnedClauseSizeTracing(IVisualizationTool) - Constructor for class org.sat4j.tools.LearnedClauseSizeTracing

LearnedClausesSizeTracing - Class in org.sat4j.tools

LearnedClausesSizeTracing(IVisualizationTool, IVisualizationTool, IVisualizationTool) - Constructor for class org.sat4j.tools.LearnedClausesSizeTracing

LearnedConstraintsDeletionStrategy - Interface in org.sat4j.minisat.core

Strategy for cleaning the database of learned clauses.

learnedConstraintsDeletionStrategy - Variable in class org.sat4j.minisat.core.Solver

LearnedConstraintsEvaluationType - Enum in org.sat4j.minisat.core

List the available strategies to evaluate learned clauses.

learnedliterals - Variable in class org.sat4j.minisat.core.SolverStats

learnedternaryclauses - Variable in class org.sat4j.minisat.core.SolverStats

LearnedTracing - Class in org.sat4j.tools

LearnedTracing(IVisualizationTool) - Constructor for class org.sat4j.tools.LearnedTracing

learner - Variable in class org.sat4j.minisat.constraints.AbstractDataStructureFactory

Learner - Interface in org.sat4j.minisat.core

Provide the learning service.

learningCondition(Constr) - Method in class org.sat4j.minisat.learning.ActiveLearning

learningCondition(Constr) - Method in class org.sat4j.minisat.learning.ClauseOnlyLearning

learningCondition(Constr) - Method in class org.sat4j.minisat.learning.FixedLengthLearning

learningCondition(Constr) - Method in class org.sat4j.minisat.learning.LimitedLearning

learningCondition(Constr) - Method in class org.sat4j.minisat.learning.PercentLengthLearning

LearningStrategy<D extends DataStructureFactory> - Interface in org.sat4j.minisat.core

Implementation of the strategy design pattern for allowing various learning schemes.

learns(Constr) - Method in interface org.sat4j.minisat.core.LearningStrategy

learns(Constr) - Method in class org.sat4j.minisat.learning.LimitedLearning

learns(Constr) - Method in class org.sat4j.minisat.learning.MiniSATLearning

learns(Constr) - Method in class org.sat4j.minisat.learning.NoLearningButHeuristics

learns(Constr) - Method in class org.sat4j.minisat.learning.NoLearningNoHeuristics

learnt() - Method in class org.sat4j.core.ConstrGroup

learnt() - Method in class org.sat4j.minisat.constraints.card.AtLeast

learnt() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard

D?

learnt() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard

Returns wether the constraint is learnt or not.

learnt() - Method in class org.sat4j.minisat.constraints.cnf.LearntBinaryClause

learnt() - Method in class org.sat4j.minisat.constraints.cnf.LearntHTClause

learnt() - Method in class org.sat4j.minisat.constraints.cnf.LearntWLClause

learnt() - Method in class org.sat4j.minisat.constraints.cnf.OriginalBinaryClause

learnt() - Method in class org.sat4j.minisat.constraints.cnf.OriginalHTClause

learnt() - Method in class org.sat4j.minisat.constraints.cnf.OriginalWLClause

learnt() - Method in class org.sat4j.minisat.constraints.cnf.UnitClause

learnt() - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses

learnt() - Method in interface org.sat4j.specs.IConstr

LearntBinaryClause - Class in org.sat4j.minisat.constraints.cnf

LearntBinaryClause(IVecInt, ILits) - Constructor for class org.sat4j.minisat.constraints.cnf.LearntBinaryClause

LearntHTClause - Class in org.sat4j.minisat.constraints.cnf

LearntHTClause(IVecInt, ILits) - Constructor for class org.sat4j.minisat.constraints.cnf.LearntHTClause

learnts - Variable in class org.sat4j.minisat.core.Solver

Set of learned constraints.

LearntWLClause - Class in org.sat4j.minisat.constraints.cnf

LearntWLClause(IVecInt, ILits) - Constructor for class org.sat4j.minisat.constraints.cnf.LearntWLClause

LecteurDimacs - Class in org.sat4j.reader

Dimacs Reader written by Frederic Laihem.

LecteurDimacs(ISolver) - Constructor for class org.sat4j.reader.LecteurDimacs

LexicoDecorator<T extends ISolver> - Class in org.sat4j.tools

LexicoDecorator(T) - Constructor for class org.sat4j.tools.LexicoDecorator

LightFactory - Class in org.sat4j

That class is the entry point to the default, best performing configuration of SAT4J.

LightFactory() - Constructor for class org.sat4j.LightFactory

lightSolver() - Method in class org.sat4j.core.ASolverFactory

To obtain a solver that is suitable for solving many small instances of SAT problems.

lightSolver() - Method in class org.sat4j.LightFactory

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

LimitedLearning<D extends DataStructureFactory> - Class in org.sat4j.minisat.learning

Learn only clauses which size is smaller than a percentage of the number of variables.

LimitedLearning() - Constructor for class org.sat4j.minisat.learning.LimitedLearning

linearisation(ILits, IVecInt) - Static method in class org.sat4j.minisat.constraints.card.MinWatchCard

Simplifies the constraint w.r.t. the assignments of the literals

literal - Variable in class org.sat4j.minisat.constraints.cnf.UnitClause

literals - Variable in class org.sat4j.minisat.constraints.cnf.UnitClauses

literals - Variable in class org.sat4j.reader.DimacsReader

LiteralsUtils - Class in org.sat4j.core

Utility methods to avoid using bit manipulation inside code.

lits - Variable in class org.sat4j.minisat.constraints.AbstractDataStructureFactory

lits - Variable in class org.sat4j.minisat.constraints.card.AtLeast

constraint literals

Lits - Class in org.sat4j.minisat.constraints.cnf

Lits() - Constructor for class org.sat4j.minisat.constraints.cnf.Lits

lits - Variable in class org.sat4j.minisat.constraints.cnf.WLClause

lits - Variable in class org.sat4j.minisat.learning.LimitedLearning

lits - Variable in class org.sat4j.minisat.orders.VarOrderHeap

locked() - Method in class org.sat4j.minisat.constraints.card.AtLeast

locked() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard

La contrainte est la cause d'une propagation unitaire

locked() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard

Returns if the constraint is the reason for a unit propagation.

locked() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause

locked() - Method in class org.sat4j.minisat.constraints.cnf.HTClause

locked() - Method in class org.sat4j.minisat.constraints.cnf.UnitClause

locked() - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses

locked() - Method in class org.sat4j.minisat.constraints.cnf.WLClause

locked() - Method in interface org.sat4j.minisat.core.Constr

Indicate wether a constraint is responsible from an assignment.

log(String) - Method in class org.sat4j.AbstractLauncher

Display messages as comments on STDOUT

log(String) - Method in interface org.sat4j.minisat.core.ICDCLLogger

lowerBound() - Method in class org.sat4j.tools.SolutionCounter

Get the number of solutions found before the timeout occurs.

luby() - Method in class org.sat4j.minisat.restarts.LubyRestarts

returns the current value of the luby sequence.

LubyRestarts - Class in org.sat4j.minisat.restarts

Luby series

LubyRestarts() - Constructor for class org.sat4j.minisat.restarts.LubyRestarts

LubyRestarts(int) - Constructor for class org.sat4j.minisat.restarts.LubyRestarts

M

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

Lance le prouveur sur un fichier Dimacs.

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

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

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

ManyCore<S extends ISolver> - Class in org.sat4j.tools

A class allowing to run several solvers in parallel.

ManyCore(ASolverFactory<S>, String...) - Constructor for class org.sat4j.tools.ManyCore

ManyCore(String[], S...) - Constructor for class org.sat4j.tools.ManyCore

Create a parallel solver from a list of solvers and a list of names.

ManyCore(S...) - Constructor for class org.sat4j.tools.ManyCore

MaxSatDecorator - Class in org.sat4j.opt

Computes a solution that satisfies the maximum of clauses.

MaxSatDecorator(ISolver) - Constructor for class org.sat4j.opt.MaxSatDecorator

MaxSatDecorator(ISolver, boolean) - Constructor for class org.sat4j.opt.MaxSatDecorator

maxUnsatisfied - Variable in class org.sat4j.minisat.constraints.card.AtLeast

number of allowed falsified literal

MaxWatchCard - Class in org.sat4j.minisat.constraints.card

maxWatchCardNew(UnitPropagationListener, ILits, IVecInt, boolean, int) - Static method in class org.sat4j.minisat.constraints.card.MaxWatchCard

Permet la cr?

memory_based - Variable in class org.sat4j.minisat.core.Solver

Messages - Class in org.sat4j

That class is intented to manage internationalisation within the application.

middleLits - Variable in class org.sat4j.minisat.constraints.cnf.HTClause

Minimal4CardinalityModel - Class in org.sat4j.tools

Computes models with a minimal number (with respect to cardinality) of negative literals.

Minimal4CardinalityModel(ISolver) - Constructor for class org.sat4j.tools.Minimal4CardinalityModel

Minimal4InclusionModel - Class in org.sat4j.tools

Computes models with a minimal subset (with respect to set inclusion) of negative literals.

Minimal4InclusionModel(ISolver) - Constructor for class org.sat4j.tools.Minimal4InclusionModel

minimalExplanation() - Method in interface org.sat4j.tools.xplain.Explainer

minimalExplanation() - Method in class org.sat4j.tools.xplain.HighLevelXplain

minimalExplanation() - Method in class org.sat4j.tools.xplain.Xplain

MinimizationStrategy - Interface in org.sat4j.tools.xplain

Minimization technique used to reduce an unsatisfiable set of constraints into a minimally unsatisfiable subformula (MUS).

MiniSATLearning<D extends DataStructureFactory> - Class in org.sat4j.minisat.learning

MiniSAT learning scheme.

MiniSATLearning() - Constructor for class org.sat4j.minisat.learning.MiniSATLearning

MiniSATRestarts - Class in org.sat4j.minisat.restarts

Minisat original restart strategy.

MiniSATRestarts() - Constructor for class org.sat4j.minisat.restarts.MiniSATRestarts

MinOneDecorator - Class in org.sat4j.opt

Computes a solution with the smallest number of satisfied literals.

MinOneDecorator(ISolver) - Constructor for class org.sat4j.opt.MinOneDecorator

MinWatchCard - Class in org.sat4j.minisat.constraints.card

MinWatchCard(ILits, IVecInt, boolean, int) - Constructor for class org.sat4j.minisat.constraints.card.MinWatchCard

Constructs and normalizes a cardinality constraint. used by minWatchCardNew in the non-normalized case.

MinWatchCard(ILits, IVecInt, int) - Constructor for class org.sat4j.minisat.constraints.card.MinWatchCard

Constructs and normalizes a cardinality constraint. used by MinWatchCardPB.normalizedMinWatchCardNew() in the normalized case.

minWatchCardNew(UnitPropagationListener, ILits, IVecInt, boolean, int) - Static method in class org.sat4j.minisat.constraints.card.MinWatchCard

Constructs a cardinality constraint with a minimal set of watched literals Permet la cr?

MixedDataStructureDanielHT - Class in org.sat4j.minisat.constraints

Uses specific data structure for cardinality constraints.

MixedDataStructureDanielHT() - Constructor for class org.sat4j.minisat.constraints.MixedDataStructureDanielHT

MixedDataStructureDanielWL - Class in org.sat4j.minisat.constraints

MixedDataStructureDanielWL() - Constructor for class org.sat4j.minisat.constraints.MixedDataStructureDanielWL

MixedDataStructureSingleWL - Class in org.sat4j.minisat.constraints

MixedDataStructureSingleWL() - Constructor for class org.sat4j.minisat.constraints.MixedDataStructureSingleWL

model() - Method in class org.sat4j.minisat.core.Solver

Si un mod?

model(int) - Method in class org.sat4j.minisat.core.Solver

model() - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator

model(int) - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator

model() - Method in class org.sat4j.opt.MinOneDecorator

model() - Method in interface org.sat4j.specs.IProblem

Provide a model (if any) for a satisfiable formula.

model(int) - Method in interface org.sat4j.specs.IProblem

Provide the truth value of a specific variable in the model.

model() - Method in class org.sat4j.tools.AbstractOutputSolver

model(int) - Method in class org.sat4j.tools.AbstractOutputSolver

model() - Method in class org.sat4j.tools.LexicoDecorator

model(int) - Method in class org.sat4j.tools.LexicoDecorator

model() - Method in class org.sat4j.tools.ManyCore

model(int) - Method in class org.sat4j.tools.ManyCore

model() - Method in class org.sat4j.tools.Minimal4CardinalityModel

model() - Method in class org.sat4j.tools.Minimal4InclusionModel

model() - Method in class org.sat4j.tools.ModelIterator

model() - Method in class org.sat4j.tools.OptToSatAdapter

model(int) - Method in class org.sat4j.tools.OptToSatAdapter

model(int) - Method in class org.sat4j.tools.SolverDecorator

model() - Method in class org.sat4j.tools.SolverDecorator

model() - Method in class org.sat4j.tools.xplain.HighLevelXplain

model() - Method in class org.sat4j.tools.xplain.Xplain

ModelIterator - Class in org.sat4j.tools

That class allows to iterate through all the models (implicants) of a formula.

ModelIterator(ISolver) - Constructor for class org.sat4j.tools.ModelIterator

Create an iterator over the solutions available in solver.

ModelIterator(ISolver, long) - Constructor for class org.sat4j.tools.ModelIterator

Create an iterator over a limited number of solutions available in solver.

modelWithInternalVariables() - Method in class org.sat4j.minisat.core.Solver

modelWithInternalVariables() - Method in interface org.sat4j.specs.ISolver

That method is designed to be used to retrieve the real model of the current set of constraints, i.e. to provide the truth value of boolean variables used internally in the solver (for encoding purposes for instance).

modelWithInternalVariables() - Method in class org.sat4j.tools.DimacsOutputSolver

modelWithInternalVariables() - Method in class org.sat4j.tools.DimacsStringSolver

modelWithInternalVariables() - Method in class org.sat4j.tools.ManyCore

modelWithInternalVariables() - Method in class org.sat4j.tools.SolverDecorator

MoreThanSAT - Class in org.sat4j

This is an example of use of the SAT4J library for computing the backbone of a CNF or to compute the number of solutions of a CNF.

moveTo(IVec<T>) - Method in class org.sat4j.core.ReadOnlyVec

moveTo(int, int) - Method in class org.sat4j.core.ReadOnlyVec

moveTo(IVecInt) - Method in class org.sat4j.core.ReadOnlyVecInt

moveTo(int[]) - Method in class org.sat4j.core.ReadOnlyVecInt

moveTo(int, int) - Method in class org.sat4j.core.ReadOnlyVecInt

moveTo(int, int[]) - Method in class org.sat4j.core.ReadOnlyVecInt

moveTo(IVec<T>) - Method in class org.sat4j.core.Vec

moveTo(int, int) - Method in class org.sat4j.core.Vec

moveTo(IVecInt) - Method in class org.sat4j.core.VecInt

moveTo(int, int) - Method in class org.sat4j.core.VecInt

moveTo(int[]) - Method in class org.sat4j.core.VecInt

moveTo(int, int[]) - Method in class org.sat4j.core.VecInt

moveTo(IVec<T>) - Method in interface org.sat4j.specs.IVec

Move the content of the vector into dest.

moveTo(int, int) - Method in interface org.sat4j.specs.IVec

Move elements inside the vector.

moveTo(IVecInt) - Method in interface org.sat4j.specs.IVecInt

moveTo(int, int[]) - Method in interface org.sat4j.specs.IVecInt

moveTo(int[]) - Method in interface org.sat4j.specs.IVecInt

moveTo(int, int) - Method in interface org.sat4j.specs.IVecInt

Move elements inside the vector.

moveTo2(IVecInt) - Method in class org.sat4j.core.ReadOnlyVecInt

moveTo2(IVecInt) - Method in class org.sat4j.core.VecInt

moveTo2(IVecInt) - Method in interface org.sat4j.specs.IVecInt

MultiTracing - Class in org.sat4j.tools

Allow to feed the solver with several SearchListener.

MultiTracing(SearchListener...) - Constructor for class org.sat4j.tools.MultiTracing

MultiTracing(List<SearchListener>) - Constructor for class org.sat4j.tools.MultiTracing

MUSLauncher - Class in org.sat4j

MUSLauncher() - Constructor for class org.sat4j.MUSLauncher

N

NAND - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader

nAssigns() - Method in class org.sat4j.minisat.core.Solver

nbclauses - Variable in class org.sat4j.tools.AbstractOutputSolver

nbvars - Variable in class org.sat4j.tools.AbstractOutputSolver

nConstraints() - Method in class org.sat4j.minisat.core.Solver

nConstraints() - Method in interface org.sat4j.specs.IProblem

To know the number of constraints currently available in the solver.

nConstraints() - Method in class org.sat4j.tools.AbstractOutputSolver

nConstraints() - Method in class org.sat4j.tools.DimacsOutputSolver

nConstraints() - Method in class org.sat4j.tools.DimacsStringSolver

nConstraints() - Method in class org.sat4j.tools.ManyCore

nConstraints() - Method in class org.sat4j.tools.SolverDecorator

neg(int) - Static method in class org.sat4j.core.LiteralsUtils

Returns the opposite literal.

NegativeLiteralSelectionStrategy - Class in org.sat4j.minisat.orders

NegativeLiteralSelectionStrategy() - Constructor for class org.sat4j.minisat.orders.NegativeLiteralSelectionStrategy

negLit(int) - Static method in class org.sat4j.core.LiteralsUtils

Returns the negative literal associated with a variable.

newBackjumping() - Static method in class org.sat4j.minisat.SolverFactory

newBest17() - Static method in class org.sat4j.minisat.SolverFactory

newBestHT() - Static method in class org.sat4j.minisat.SolverFactory

newBestSingleWL() - Static method in class org.sat4j.minisat.SolverFactory

newBestWL() - Static method in class org.sat4j.minisat.SolverFactory

newConflict() - Method in interface org.sat4j.minisat.core.ConflictTimer

newConflict() - Method in class org.sat4j.minisat.core.ConflictTimerAdapter

newConflict() - Method in class org.sat4j.minisat.core.ConflictTimerContainer

newConflict() - Method in class org.sat4j.minisat.restarts.ArminRestarts

newConflict() - Method in class org.sat4j.minisat.restarts.LubyRestarts

newConflict() - Method in class org.sat4j.minisat.restarts.MiniSATRestarts

newConflict() - Method in class org.sat4j.minisat.restarts.NoRestarts

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

Default solver of the SolverFactory.

newDefaultAutoErasePhaseSaving() - Static method in class org.sat4j.minisat.SolverFactory

newDefaultMS21PhaseSaving() - Static method in class org.sat4j.minisat.SolverFactory

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

newGlucose() - Static method in class org.sat4j.minisat.SolverFactory

newGreedySolver() - Static method in class org.sat4j.minisat.SolverFactory

newLearnedClause(Constr, int) - Method in interface org.sat4j.minisat.core.RestartStrategy

newLearnedClause(Constr, int) - Method in class org.sat4j.minisat.restarts.ArminRestarts

newLearnedClause(Constr, int) - Method in class org.sat4j.minisat.restarts.LubyRestarts

newLearnedClause(Constr, int) - Method in class org.sat4j.minisat.restarts.MiniSATRestarts

newLearnedClause(Constr, int) - Method in class org.sat4j.minisat.restarts.NoRestarts

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

Small footprint SAT solver.

newMiniLearning(DataStructureFactory, IOrder) - Static method in class org.sat4j.minisat.SolverFactory

newMiniLearningHeap() - Static method in class org.sat4j.minisat.SolverFactory

newMiniLearningHeap(DataStructureFactory) - Static method in class org.sat4j.minisat.SolverFactory

newMiniLearningHeapExpSimp() - Static method in class org.sat4j.minisat.SolverFactory

newMiniLearningHeapEZSimp() - Static method in class org.sat4j.minisat.SolverFactory

newMiniLearningHeapEZSimpLongRestarts() - Static method in class org.sat4j.minisat.SolverFactory

newMiniLearningHeapEZSimpNoRestarts() - Static method in class org.sat4j.minisat.SolverFactory

newMiniLearningHeapRsatExpSimp() - Static method in class org.sat4j.minisat.SolverFactory

newMiniLearningHeapRsatExpSimpBiere() - Static method in class org.sat4j.minisat.SolverFactory

newMiniLearningHeapRsatExpSimpLuby() - Static method in class org.sat4j.minisat.SolverFactory

newMiniLearningPure() - Static method in class org.sat4j.minisat.SolverFactory

newMiniSATHeap() - Static method in class org.sat4j.minisat.SolverFactory

newMiniSATHeap(DataStructureFactory) - Static method in class org.sat4j.minisat.SolverFactory

newMiniSATHeapExpSimp() - Static method in class org.sat4j.minisat.SolverFactory

newMiniSATHeapEZSimp() - Static method in class org.sat4j.minisat.SolverFactory

newMinOneSolver() - Static method in class org.sat4j.minisat.SolverFactory

newVar() - Method in class org.sat4j.minisat.core.Solver

Deprecated.

newVar(int) - Method in class org.sat4j.minisat.core.Solver

newVar(int) - Method in interface org.sat4j.specs.IProblem

Declare howmany variables in the problem (and thus in the vocabulary), that will be represented using the Dimacs format by integers ranging from 1 to howmany.

newVar() - Method in interface org.sat4j.specs.ISolver

Deprecated.

newVar(int) - Method in class org.sat4j.tools.AbstractOutputSolver

newVar() - Method in class org.sat4j.tools.DimacsOutputSolver

newVar(int) - Method in class org.sat4j.tools.DimacsOutputSolver

newVar() - Method in class org.sat4j.tools.DimacsStringSolver

newVar(int) - Method in class org.sat4j.tools.DimacsStringSolver

newVar() - Method in class org.sat4j.tools.ManyCore

newVar(int) - Method in class org.sat4j.tools.ManyCore

newVar() - Method in class org.sat4j.tools.SolverDecorator

Deprecated.

newVar(int) - Method in class org.sat4j.tools.SolverDecorator

next() - Method in class org.sat4j.reader.EfficientScanner

next() - Method in interface org.sat4j.specs.IteratorInt

nextBigInteger() - Method in class org.sat4j.reader.EfficientScanner

nextFreeVarId(boolean) - Method in class org.sat4j.minisat.constraints.cnf.Lits

nextFreeVarId(boolean) - Method in interface org.sat4j.minisat.core.ILits

Ask the solver for a free variable identifier, in Dimacs format (i.e. a positive number).

nextFreeVarId(boolean) - Method in class org.sat4j.minisat.core.Solver

nextFreeVarId(boolean) - Method in interface org.sat4j.specs.ISolver

Ask the solver for a free variable identifier, in Dimacs format (i.e. a positive number).

nextFreeVarId(boolean) - Method in class org.sat4j.tools.DimacsOutputSolver

nextFreeVarId(boolean) - Method in class org.sat4j.tools.DimacsStringSolver

nextFreeVarId(boolean) - Method in class org.sat4j.tools.ManyCore

nextFreeVarId(boolean) - Method in class org.sat4j.tools.SolverDecorator

nextInt() - Method in class org.sat4j.reader.EfficientScanner

To get the next available integer.

nextLine() - Method in class org.sat4j.reader.EfficientScanner

nextLuby() - Method in class org.sat4j.minisat.restarts.LubyRestarts

Computes and return the next value of the luby sequence.

nextRestartNumberOfConflict() - Method in interface org.sat4j.minisat.core.RestartStrategy

Deprecated.

nextRestartNumberOfConflict() - Method in class org.sat4j.minisat.restarts.ArminRestarts

nextRestartNumberOfConflict() - Method in class org.sat4j.minisat.restarts.LubyRestarts

nextRestartNumberOfConflict() - Method in class org.sat4j.minisat.restarts.MiniSATRestarts

nextRestartNumberOfConflict() - Method in class org.sat4j.minisat.restarts.NoRestarts

niceParameters(UnitPropagationListener, ILits, IVecInt, int) - Static method in class org.sat4j.minisat.constraints.card.AtLeast

NO_SIMPLIFICATION - Static variable in class org.sat4j.minisat.core.Solver

NoLearningButHeuristics<D extends DataStructureFactory> - Class in org.sat4j.minisat.learning

Allows MiniSAT to do backjumping without learning.

NoLearningButHeuristics() - Constructor for class org.sat4j.minisat.learning.NoLearningButHeuristics

NoLearningNoHeuristics<D extends DataStructureFactory> - Class in org.sat4j.minisat.learning

Allows MiniSAT to do backjumping without learning.

NoLearningNoHeuristics() - Constructor for class org.sat4j.minisat.learning.NoLearningNoHeuristics

nonOptimalMeansSatisfiable() - Method in class org.sat4j.opt.MaxSatDecorator

nonOptimalMeansSatisfiable() - Method in class org.sat4j.opt.MinOneDecorator

nonOptimalMeansSatisfiable() - Method in interface org.sat4j.specs.IOptimizationProblem

A suboptimal solution has different meaning depending of the optimization problem considered.

nonOptimalMeansSatisfiable() - Method in class org.sat4j.tools.LexicoDecorator

NOR - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader

NoRestarts - Class in org.sat4j.minisat.restarts

Disable restarts in the solver.

NoRestarts() - Constructor for class org.sat4j.minisat.restarts.NoRestarts

normalize() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard

On normalise la contrainte au sens de Barth

normalize() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard

normalize the constraint (cf.

not(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits

not() - Method in class org.sat4j.specs.Lbool

boolean negation.

NOT - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader

not(int, int) - Method in class org.sat4j.tools.GateTranslator

Translate y <=> not x into clauses.

NOTGOOD - Static variable in interface org.sat4j.tools.IVisualizationTool

numberOfCriteria() - Method in class org.sat4j.tools.LexicoDecorator

numberOfInterestingVariables() - Method in class org.sat4j.minisat.orders.VarOrderHeap

numberOfModelsFoundSoFar() - Method in class org.sat4j.tools.ModelIterator

To know the number of models already found.

numberOfSolvers - Variable in class org.sat4j.tools.ManyCore

nVars() - Method in class org.sat4j.minisat.constraints.cnf.Lits

nVars() - Method in interface org.sat4j.minisat.core.ILits

to obtain the max id of the variable

nVars() - Method in class org.sat4j.minisat.core.Solver

nVars() - Method in interface org.sat4j.specs.IProblem

To know the number of variables used in the solver as declared by newVar() In case the method newVar() has not been used, the method returns the number of variables used in the solver.

nVars() - Method in interface org.sat4j.specs.ISolverService

Read-Only access to the number of variables declared in the solver.

nVars() - Method in class org.sat4j.tools.AbstractOutputSolver

nVars() - Method in class org.sat4j.tools.DimacsOutputSolver

nVars() - Method in class org.sat4j.tools.DimacsStringSolver

nVars() - Method in class org.sat4j.tools.ManyCore

nVars() - Method in class org.sat4j.tools.SolverDecorator

O

onBackjumpToRootLevel() - Method in interface org.sat4j.minisat.core.RestartStrategy

Called when the solver backjumps to the root level.

onBackjumpToRootLevel() - Method in class org.sat4j.minisat.restarts.ArminRestarts

onBackjumpToRootLevel() - Method in class org.sat4j.minisat.restarts.LubyRestarts

onBackjumpToRootLevel() - Method in class org.sat4j.minisat.restarts.MiniSATRestarts

onBackjumpToRootLevel() - Method in class org.sat4j.minisat.restarts.NoRestarts

onClauseLearning(Constr) - Method in interface org.sat4j.minisat.core.LearnedConstraintsDeletionStrategy

Hook method called when a new clause has just been derived during conflict analysis.

onConflictAnalysis(Constr) - Method in interface org.sat4j.minisat.core.LearnedConstraintsDeletionStrategy

Hook method called on constraints participating to the conflict analysis.

onFinishWithAnswer(boolean, boolean, int) - Method in class org.sat4j.tools.ManyCore

onFinishWithAnswer(boolean, boolean, int) - Method in interface org.sat4j.tools.OutcomeListener

onPropagation(Constr) - Method in interface org.sat4j.minisat.core.LearnedConstraintsDeletionStrategy

Hook method called when a unit clause is propagated thanks to from.

onRestart() - Method in interface org.sat4j.minisat.core.RestartStrategy

Hook method called when a restart occurs (once the solver has backtracked to top decision level).

onRestart() - Method in class org.sat4j.minisat.restarts.ArminRestarts

onRestart() - Method in class org.sat4j.minisat.restarts.LubyRestarts

onRestart() - Method in class org.sat4j.minisat.restarts.MiniSATRestarts

onRestart() - Method in class org.sat4j.minisat.restarts.NoRestarts

optimisationFunction(IVecInt, IVec<BigInteger>, IVecInt) - Method in class org.sat4j.tools.GateTranslator

Translate an optimization function into constraints and provides the binary literals in results.

OPTIMUM_FOUND - Static variable in class org.sat4j.ExitCode

OptToSatAdapter - Class in org.sat4j.tools

OptToSatAdapter(IOptimizationProblem) - Constructor for class org.sat4j.tools.OptToSatAdapter

OR - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader

or(int, IVecInt) - Method in class org.sat4j.tools.GateTranslator

translate y <=> x1 \/ x2 \/ ... \/ xn into clauses.

org.sat4j - package org.sat4j

Contains a command line launcher for the SAT solvers.

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

Implementation of the data structures available in org.sat4j.specs.

org.sat4j.minisat - package org.sat4j.minisat

Implementation of the MiniSAT specification in Java.

org.sat4j.minisat.constraints - package org.sat4j.minisat.constraints

Implementations of various constraints for MiniSAT.

org.sat4j.minisat.constraints.card - package org.sat4j.minisat.constraints.card

Implementations of cardinality constraints.

org.sat4j.minisat.constraints.cnf - package org.sat4j.minisat.constraints.cnf

Implementations of clausal constraints.

org.sat4j.minisat.core - package org.sat4j.minisat.core

Implementation of the MiniSAT solver skeleton.

org.sat4j.minisat.learning - package org.sat4j.minisat.learning

Various learning strategies.

org.sat4j.minisat.orders - package org.sat4j.minisat.orders

Various heuristics to select the next variable to branch on.

org.sat4j.minisat.restarts - package org.sat4j.minisat.restarts

Various restart strategies.

org.sat4j.opt - package org.sat4j.opt

Built-in optimization framework.

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

Some utility classes to read problems from plain text files.

org.sat4j.specs - package org.sat4j.specs

Those classes are intended for users dealing with SAT solvers as black boxes.

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

Tools to be used on top of an ISolver.

org.sat4j.tools.encoding - package org.sat4j.tools.encoding

Implementation of different encodings.

org.sat4j.tools.xplain - package org.sat4j.tools.xplain

Implementation of an explanation engine in case of unsatisfiability.

OriginalBinaryClause - Class in org.sat4j.minisat.constraints.cnf

OriginalBinaryClause(IVecInt, ILits) - Constructor for class org.sat4j.minisat.constraints.cnf.OriginalBinaryClause

OriginalHTClause - Class in org.sat4j.minisat.constraints.cnf

OriginalHTClause(IVecInt, ILits) - Constructor for class org.sat4j.minisat.constraints.cnf.OriginalHTClause

OriginalWLClause - Class in org.sat4j.minisat.constraints.cnf

OriginalWLClause(IVecInt, ILits) - Constructor for class org.sat4j.minisat.constraints.cnf.OriginalWLClause

out - Variable in class org.sat4j.AbstractLauncher

out - Variable in class org.sat4j.minisat.core.Solver

OutcomeListener - Interface in org.sat4j.tools

Simple interface to check the outcome of running a solver in parallel.

P

Pair - Class in org.sat4j.minisat.core

Utility class to be used to return the two results of a conflict analysis.

Pair() - Constructor for class org.sat4j.minisat.core.Pair

ParseFormatException - Exception in org.sat4j.reader

Exception launched when there is a problem during parsing.

ParseFormatException() - Constructor for exception org.sat4j.reader.ParseFormatException

Constructor for ParseFormatException.

ParseFormatException(String) - Constructor for exception org.sat4j.reader.ParseFormatException

Constructor for ParseFormatException.

ParseFormatException(String, Throwable) - Constructor for exception org.sat4j.reader.ParseFormatException

Constructor for ParseFormatException.

ParseFormatException(Throwable) - Constructor for exception org.sat4j.reader.ParseFormatException

Constructor for ParseFormatException.

parseInstance(InputStream) - Method in class org.sat4j.reader.AAGReader

parseInstance(InputStream) - Method in class org.sat4j.reader.AIGReader

parseInstance(InputStream) - Method in class org.sat4j.reader.DimacsReader

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

parseInstance(InputStream) - Method in class org.sat4j.reader.InstanceReader

parseInstance(InputStream) - Method in class org.sat4j.reader.LecteurDimacs

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

This is the usual method to feed a solver with a benchmark.

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

Read a file from a stream.

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

Deprecated.

parseInstance(int[], int[], int[][], int) - Method in class org.sat4j.tools.DimacsArrayReader

PARSING_ERROR - Static variable in exception org.sat4j.reader.ParseFormatException

PercentLengthLearning<D extends DataStructureFactory> - Class in org.sat4j.minisat.learning

Selects the constraints to learn according to its length as a percentage of the total number of variables in the solver universe.

PercentLengthLearning() - Constructor for class org.sat4j.minisat.learning.PercentLengthLearning

PercentLengthLearning(int) - Constructor for class org.sat4j.minisat.learning.PercentLengthLearning

PhaseCachingAutoEraseStrategy - Class in org.sat4j.minisat.orders

PhaseCachingAutoEraseStrategy() - Constructor for class org.sat4j.minisat.orders.PhaseCachingAutoEraseStrategy

PhaseInLastLearnedClauseSelectionStrategy - Class in org.sat4j.minisat.orders

Keeps record of the phase of a variable in the lastest recorded clause.

PhaseInLastLearnedClauseSelectionStrategy() - Constructor for class org.sat4j.minisat.orders.PhaseInLastLearnedClauseSelectionStrategy

phaseStrategy - Variable in class org.sat4j.minisat.orders.VarOrderHeap

Policy - Class in org.sat4j.tools.encoding

This class allows the use of different encodings for different cardinality constraints.

Policy() - Constructor for class org.sat4j.tools.encoding.Policy

pop() - Method in class org.sat4j.core.ReadOnlyVec

pop() - Method in class org.sat4j.core.ReadOnlyVecInt

pop() - Method in class org.sat4j.core.Vec

Pop the last element on the stack.

pop() - Method in class org.sat4j.core.VecInt

depile le dernier element du vecteur.

pop() - Method in interface org.sat4j.specs.IVec

Pop the last element on the stack.

pop() - Method in interface org.sat4j.specs.IVecInt

depile le dernier element du vecteur.

PositiveLiteralSelectionStrategy - Class in org.sat4j.minisat.orders

PositiveLiteralSelectionStrategy() - Constructor for class org.sat4j.minisat.orders.PositiveLiteralSelectionStrategy

posLit(int) - Static method in class org.sat4j.core.LiteralsUtils

Returns the positive literal associated with a variable.

prevboolmodel - Variable in class org.sat4j.opt.AbstractSelectorVariablesDecorator

prevboolmodel - Variable in class org.sat4j.tools.LexicoDecorator

prevfullmodel - Variable in class org.sat4j.opt.AbstractSelectorVariablesDecorator

prevfullmodel - Variable in class org.sat4j.tools.LexicoDecorator

prevmodel - Variable in class org.sat4j.opt.AbstractSelectorVariablesDecorator

prime - Variable in class org.sat4j.AbstractLauncher

primeImplicant() - Method in class org.sat4j.minisat.core.Solver

primeImplicant(int) - Method in class org.sat4j.minisat.core.Solver

primeImplicant() - Method in interface org.sat4j.specs.IProblem

Provide a prime implicant, i.e. a set of literal that is sufficient to satisfy all constraints of the problem.

primeImplicant(int) - Method in interface org.sat4j.specs.IProblem

Check if a given literal is part of the prime implicant computed by the IProblem.primeImplicant() method.

primeImplicant() - Method in class org.sat4j.tools.AbstractOutputSolver

primeImplicant(int) - Method in class org.sat4j.tools.DimacsOutputSolver

primeImplicant(int) - Method in class org.sat4j.tools.DimacsStringSolver

primeImplicant() - Method in class org.sat4j.tools.ManyCore

primeImplicant(int) - Method in class org.sat4j.tools.ManyCore

primeImplicant() - Method in class org.sat4j.tools.ModelIterator

primeImplicant() - Method in class org.sat4j.tools.SolverDecorator

primeImplicant(int) - Method in class org.sat4j.tools.SolverDecorator

printInfos(PrintWriter, String) - Method in class org.sat4j.minisat.core.Solver

printInfos(PrintWriter, String) - Method in interface org.sat4j.specs.IProblem

To print additional informations regarding the problem.

printInfos(PrintWriter, String) - Method in class org.sat4j.tools.AbstractOutputSolver

printInfos(PrintWriter, String) - Method in class org.sat4j.tools.ManyCore

printInfos(PrintWriter, String) - Method in class org.sat4j.tools.SolverDecorator

printLearntClausesInfos(PrintWriter, String) - Method in class org.sat4j.minisat.core.Solver

printStat(PrintWriter, String) - Method in interface org.sat4j.minisat.core.IOrder

Display statistics regarding the heuristics.

printStat(PrintStream, String) - Method in class org.sat4j.minisat.core.Solver

printStat(PrintWriter, String) - Method in class org.sat4j.minisat.core.Solver

printStat(PrintWriter, String) - Method in class org.sat4j.minisat.core.SolverStats

printStat(PrintWriter, String) - Method in class org.sat4j.minisat.orders.RandomWalkDecorator

printStat(PrintWriter, String) - Method in class org.sat4j.minisat.orders.TabuListDecorator

printStat(PrintWriter, String) - Method in class org.sat4j.minisat.orders.VarOrderHeap

printStat(PrintStream, String) - Method in interface org.sat4j.specs.ISolver

Deprecated.

printStat(PrintWriter, String) - Method in interface org.sat4j.specs.ISolver

Display statistics to the given output writer

printStat(PrintStream, String) - Method in class org.sat4j.tools.AbstractOutputSolver

printStat(PrintWriter, String) - Method in class org.sat4j.tools.AbstractOutputSolver

printStat(PrintStream, String) - Method in class org.sat4j.tools.ManyCore

Deprecated.

printStat(PrintWriter, String) - Method in class org.sat4j.tools.ManyCore

printStat(PrintStream, String) - Method in class org.sat4j.tools.SolverDecorator

Deprecated.

printStat(PrintWriter, String) - Method in class org.sat4j.tools.SolverDecorator

Product - Class in org.sat4j.tools.encoding

Implementation of product encoding for at most one and at most k constraints.

Product() - Constructor for class org.sat4j.tools.encoding.Product

Propagatable - Interface in org.sat4j.minisat.core

This interface is to be implemented by the classes wanted to be notified of the falsification of a literal.

propagate(UnitPropagationListener, int) - Method in class org.sat4j.minisat.constraints.card.AtLeast

propagate(UnitPropagationListener, int) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard

Propagation de la valeur de v?

propagate(UnitPropagationListener, int) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard

propagates the value of a falsified literal

propagate(UnitPropagationListener, int) - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause

propagate(UnitPropagationListener, int) - Method in class org.sat4j.minisat.constraints.cnf.HTClause

propagate(UnitPropagationListener, int) - Method in class org.sat4j.minisat.constraints.cnf.UnitClause

propagate(UnitPropagationListener, int) - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses

propagate(UnitPropagationListener, int) - Method in class org.sat4j.minisat.constraints.cnf.WLClause

propagate(UnitPropagationListener, int) - Method in interface org.sat4j.minisat.core.Propagatable

Propagate the truth value of a literal in constraints in which that literal is falsified.

propagate() - Method in class org.sat4j.minisat.core.Solver

propagating(int, IConstr) - Method in interface org.sat4j.specs.SearchListener

Unit propagation

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

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

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

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

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

propagations - Variable in class org.sat4j.minisat.core.SolverStats

PureOrder - Class in org.sat4j.minisat.orders

PureOrder() - Constructor for class org.sat4j.minisat.orders.PureOrder

PureOrder(int) - Constructor for class org.sat4j.minisat.orders.PureOrder

push(T) - Method in class org.sat4j.core.ReadOnlyVec

push(int) - Method in class org.sat4j.core.ReadOnlyVecInt

push(T) - Method in class org.sat4j.core.Vec

push(int) - Method in class org.sat4j.core.VecInt

push(int) - Method in class org.sat4j.minisat.core.CircularBuffer

push(T) - Method in interface org.sat4j.specs.IVec

push(int) - Method in interface org.sat4j.specs.IVecInt

pushAll(IVecInt) - Method in class org.sat4j.core.VecInt

Q

QuickXplain2001Strategy - Class in org.sat4j.tools.xplain

An implementation of the QuickXplain algorithm as explained by Ulrich Junker in the following paper:

QuickXplain2001Strategy() - Constructor for class org.sat4j.tools.xplain.QuickXplain2001Strategy

QuickXplainStrategy - Class in org.sat4j.tools.xplain

An implementation of the QuickXplain algorithm as explained by Ulrich Junker in the following paper:

QuickXplainStrategy() - Constructor for class org.sat4j.tools.xplain.QuickXplainStrategy

R

RAND - Static variable in class org.sat4j.minisat.orders.RandomLiteralSelectionStrategy

RandomLiteralSelectionStrategy - Class in org.sat4j.minisat.orders

The variable selection strategy randomly picks one phase, either positive or negative.

RandomLiteralSelectionStrategy() - Constructor for class org.sat4j.minisat.orders.RandomLiteralSelectionStrategy

RandomWalkDecorator - Class in org.sat4j.minisat.orders

RandomWalkDecorator(VarOrderHeap) - Constructor for class org.sat4j.minisat.orders.RandomWalkDecorator

RandomWalkDecorator(VarOrderHeap, double) - Constructor for class org.sat4j.minisat.orders.RandomWalkDecorator

readConstrs() - Method in class org.sat4j.reader.DimacsReader

reader - Variable in class org.sat4j.AbstractLauncher

Reader - Class in org.sat4j.reader

A reader is responsible to feed an ISolver from a text file and to convert the model found by the solver to a textual representation.

Reader() - Constructor for class org.sat4j.reader.Reader

ReadOnlyVec<T> - Class in org.sat4j.core

Utility class to allow Read Only access to an IVec.

ReadOnlyVec(IVec<T>) - Constructor for class org.sat4j.core.ReadOnlyVec

ReadOnlyVecInt - Class in org.sat4j.core

Utility class to allow Read Only access only to an IVecInt.

ReadOnlyVecInt(IVecInt) - Constructor for class org.sat4j.core.ReadOnlyVecInt

readProblem(String) - Method in class org.sat4j.AbstractLauncher

Reads a problem file from the command line.

readProblemLine() - Method in class org.sat4j.reader.DimacsReader

readProblemLine() - Method in class org.sat4j.reader.GroupedCNFReader

realNumberOfVariables() - Method in class org.sat4j.minisat.core.Solver

realNumberOfVariables() - Method in interface org.sat4j.specs.ISolver

Retrieve the real number of variables used in the solver.

realNumberOfVariables() - Method in class org.sat4j.tools.DimacsOutputSolver

realNumberOfVariables() - Method in class org.sat4j.tools.DimacsStringSolver

realNumberOfVariables() - Method in class org.sat4j.tools.ManyCore

realNumberOfVariables() - Method in class org.sat4j.tools.SolverDecorator

realnVars() - Method in class org.sat4j.minisat.constraints.cnf.Lits

realnVars() - Method in interface org.sat4j.minisat.core.ILits

to obtain the real number of variables appearing in the formula

reason - Variable in class org.sat4j.minisat.core.Pair

reduce(IVec<Constr>) - Method in interface org.sat4j.minisat.core.LearnedConstraintsDeletionStrategy

Hook method called when the solver wants to reduce the set of learned clauses.

reduceDB() - Method in class org.sat4j.minisat.core.Solver

reduceddb - Variable in class org.sat4j.minisat.core.SolverStats

reducedliterals - Variable in class org.sat4j.minisat.core.SolverStats

register() - Method in class org.sat4j.minisat.constraints.card.AtLeast

register() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard

register() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard

register() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause

register() - Method in class org.sat4j.minisat.constraints.cnf.LearntHTClause

register() - Method in class org.sat4j.minisat.constraints.cnf.LearntWLClause

register() - Method in class org.sat4j.minisat.constraints.cnf.OriginalHTClause

register() - Method in class org.sat4j.minisat.constraints.cnf.OriginalWLClause

register() - Method in class org.sat4j.minisat.constraints.cnf.UnitClause

register() - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses

register() - Method in interface org.sat4j.minisat.core.Constr

Register the constraint to the solver.

registerLiteral(int) - Method in class org.sat4j.minisat.core.Solver

registerLiteral(int) - Method in interface org.sat4j.specs.ISolver

Tell the solver to consider that the literal is in the CNF.

registerLiteral(int) - Method in class org.sat4j.tools.DimacsOutputSolver

registerLiteral(int) - Method in class org.sat4j.tools.DimacsStringSolver

registerLiteral(int) - Method in class org.sat4j.tools.ManyCore

registerLiteral(int) - Method in class org.sat4j.tools.SolverDecorator

RemiUtils - Class in org.sat4j.tools

Class dedicated to Remi Coletta utility methods :-)

remove(T) - Method in class org.sat4j.core.ReadOnlyVec

remove(int) - Method in class org.sat4j.core.ReadOnlyVecInt

remove(T) - Method in class org.sat4j.core.Vec

Remove an element that belongs to the Vector.

remove(int) - Method in class org.sat4j.core.VecInt

Enleve un element qui se trouve dans le vecteur!!!

remove(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.card.AtLeast

remove(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard

remove(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard

Removes a constraint from the solver

remove(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause

remove(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.HTClause

remove(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.UnitClause

remove(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses

remove(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.cnf.WLClause

remove(UnitPropagationListener) - Method in interface org.sat4j.minisat.core.Constr

Remove a constraint from the solver.

remove(T) - Method in interface org.sat4j.specs.IVec

Enleve un element qui se trouve dans le vecteur!!!

remove(int) - Method in interface org.sat4j.specs.IVecInt

Enleve un element qui se trouve dans le vecteur!!!

removeConstr(IConstr) - Method in class org.sat4j.minisat.core.Solver

removeConstr(IConstr) - Method in interface org.sat4j.specs.ISolver

Remove a constraint returned by one of the add method from the solver.

removeConstr(IConstr) - Method in class org.sat4j.tools.AbstractOutputSolver

removeConstr(IConstr) - Method in class org.sat4j.tools.ManyCore

removeConstr(IConstr) - Method in class org.sat4j.tools.SolverDecorator

removeConstr(IConstr) - Method in class org.sat4j.tools.xplain.Xplain

removeFrom(ISolver) - Method in class org.sat4j.core.ConstrGroup

removeSubsumedConstr(IConstr) - Method in class org.sat4j.minisat.core.Solver

removeSubsumedConstr(IConstr) - Method in interface org.sat4j.specs.ISolver

Remove a constraint returned by one of the add method from the solver that is subsumed by a constraint already in the solver or to be added to the solver.

removeSubsumedConstr(IConstr) - Method in class org.sat4j.tools.AbstractOutputSolver

removeSubsumedConstr(IConstr) - Method in class org.sat4j.tools.ManyCore

removeSubsumedConstr(IConstr) - Method in class org.sat4j.tools.SolverDecorator

removeSubsumedConstr(IConstr) - Method in class org.sat4j.tools.xplain.Xplain

rescaleBy(double) - Method in class org.sat4j.minisat.constraints.card.AtLeast

rescaleBy(double) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard

Permet le r??

rescaleBy(double) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard

Rescales the activity value of the constraint

rescaleBy(double) - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause

rescaleBy(double) - Method in class org.sat4j.minisat.constraints.cnf.HTClause

rescaleBy(double) - Method in class org.sat4j.minisat.constraints.cnf.UnitClause

rescaleBy(double) - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses

rescaleBy(double) - Method in class org.sat4j.minisat.constraints.cnf.WLClause

rescaleBy(double) - Method in interface org.sat4j.minisat.core.Constr

Rescale the clause activity by a value.

reset() - Method in class org.sat4j.minisat.constraints.AbstractDataStructureFactory

reset(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits

reset() - Method in interface org.sat4j.minisat.core.ConflictTimer

reset() - Method in class org.sat4j.minisat.core.ConflictTimerAdapter

reset() - Method in class org.sat4j.minisat.core.ConflictTimerContainer

reset() - Method in interface org.sat4j.minisat.core.DataStructureFactory

reset(int) - Method in interface org.sat4j.minisat.core.ILits

Reset a literal in the vocabulary.

reset() - Method in class org.sat4j.minisat.core.Solver

reset() - Method in class org.sat4j.minisat.core.SolverStats

reset() - Method in class org.sat4j.minisat.restarts.ArminRestarts

reset() - Method in class org.sat4j.minisat.restarts.LubyRestarts

reset() - Method in class org.sat4j.minisat.restarts.MiniSATRestarts

reset() - Method in class org.sat4j.minisat.restarts.NoRestarts

reset() - Method in class org.sat4j.opt.MaxSatDecorator

reset() - Method in class org.sat4j.opt.MinOneDecorator

reset() - Method in interface org.sat4j.specs.ISolver

Clean up the internal state of the solver.

reset() - Method in class org.sat4j.tools.DimacsOutputSolver

reset() - Method in class org.sat4j.tools.DimacsStringSolver

reset() - Method in class org.sat4j.tools.ManyCore

reset() - Method in class org.sat4j.tools.ModelIterator

reset() - Method in class org.sat4j.tools.OptToSatAdapter

reset() - Method in class org.sat4j.tools.SolverDecorator

resetPool() - Method in class org.sat4j.minisat.constraints.cnf.Lits

resetPool() - Method in interface org.sat4j.minisat.core.ILits

reset the vocabulary.

restarting() - Method in interface org.sat4j.specs.SearchListener

The solver restarts the search.

restarting() - Method in class org.sat4j.tools.ConflictDepthTracing

restarting() - Method in class org.sat4j.tools.ConflictLevelTracing

restarting() - Method in class org.sat4j.tools.DecisionTracing

restarting() - Method in class org.sat4j.tools.HeuristicsTracing

restarting() - Method in class org.sat4j.tools.LearnedClausesSizeTracing

restarting() - Method in class org.sat4j.tools.LearnedTracing

restarting() - Method in class org.sat4j.tools.MultiTracing

restarting() - Method in class org.sat4j.tools.SearchListenerAdapter

restarting() - Method in class org.sat4j.tools.SpeedTracing

restarting() - Method in class org.sat4j.tools.TextOutputTracing

RestartStrategy - Interface in org.sat4j.minisat.core

Abstraction allowing to choose various restarts strategies.

rootLevel - Variable in class org.sat4j.minisat.core.Solver

S?

rootSimplifications - Variable in class org.sat4j.minisat.core.SolverStats

RSATLastLearnedClausesPhaseSelectionStrategy - Class in org.sat4j.minisat.orders

Keeps track of the phase of the latest assignment.

RSATLastLearnedClausesPhaseSelectionStrategy() - Constructor for class org.sat4j.minisat.orders.RSATLastLearnedClausesPhaseSelectionStrategy

RSATPhaseSelectionStrategy - Class in org.sat4j.minisat.orders

Keeps track of the phase of the latest assignment.

RSATPhaseSelectionStrategy() - Constructor for class org.sat4j.minisat.orders.RSATPhaseSelectionStrategy

run(String[]) - Method in class org.sat4j.AbstractLauncher

run() - Method in class org.sat4j.minisat.core.ConflictTimerAdapter

run(String[]) - Method in class org.sat4j.MUSLauncher

S

sanityCheck(IVecInt, ILits, UnitPropagationListener) - Static method in class org.sat4j.minisat.constraints.cnf.Clauses

Perform some sanity check before constructing a clause a) if a literal is assigned true, return null (the clause is satisfied) b) if a literal is assigned false, remove it c) if a clause contains a literal and its opposite (tautology) return null d) remove duplicate literals e) if the clause is empty, return null f) if the clause if unit, transmit it to the object responsible for unit propagation

SATISFIABLE - Static variable in class org.sat4j.ExitCode

satisfies(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits

satisfies(int) - Method in interface org.sat4j.minisat.core.ILits

Satisfies a boolean variable (truth value is TRUE).

scanner - Variable in class org.sat4j.reader.DimacsReader

SearchEnumeratorListener - Class in org.sat4j.tools

That class allows to iterate over the models from the inside: conflicts are created to ask the solver to backtrack.

SearchEnumeratorListener() - Constructor for class org.sat4j.tools.SearchEnumeratorListener

SearchListener<S extends ISolverService> - Interface in org.sat4j.specs

Interface to the solver main steps.

SearchListenerAdapter<S extends ISolverService> - Class in org.sat4j.tools

SearchListenerAdapter() - Constructor for class org.sat4j.tools.SearchListenerAdapter

SearchParams - Class in org.sat4j.minisat.core

Some parameters used during the search.

SearchParams() - Constructor for class org.sat4j.minisat.core.SearchParams

Default search parameters.

SearchParams(int) - Constructor for class org.sat4j.minisat.core.SearchParams

SearchParams(double, int) - Constructor for class org.sat4j.minisat.core.SearchParams

SearchParams(double, double, double, int) - Constructor for class org.sat4j.minisat.core.SearchParams

select() - Method in interface org.sat4j.minisat.core.IOrder

Selects the next "best" unassigned literal.

select(int) - Method in interface org.sat4j.minisat.core.IPhaseSelectionStrategy

selects the phase of the variable according to a phase selection strategy.

select(int) - Method in class org.sat4j.minisat.orders.NegativeLiteralSelectionStrategy

select(int) - Method in class org.sat4j.minisat.orders.PositiveLiteralSelectionStrategy

select() - Method in class org.sat4j.minisat.orders.PureOrder

select(int) - Method in class org.sat4j.minisat.orders.RandomLiteralSelectionStrategy

select() - Method in class org.sat4j.minisat.orders.RandomWalkDecorator

select() - Method in class org.sat4j.minisat.orders.TabuListDecorator

select() - Method in class org.sat4j.minisat.orders.VarOrderHeap

Selectionne une nouvelle variable, non affectee, ayant l'activite la plus elevee.

Sequential - Class in org.sat4j.tools.encoding

Implementation of the sequential encoding for the at most k constraint.

Sequential() - Constructor for class org.sat4j.tools.encoding.Sequential

set(int, T) - Method in class org.sat4j.core.ReadOnlyVec

set(int, int) - Method in class org.sat4j.core.ReadOnlyVecInt

set(int, T) - Method in class org.sat4j.core.Vec

set(int, int) - Method in class org.sat4j.core.VecInt

set(int, T) - Method in interface org.sat4j.specs.IVec

set(int, int) - Method in interface org.sat4j.specs.IVecInt

setActivity(double) - Method in class org.sat4j.minisat.constraints.card.AtLeast

setActivity(double) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard

setActivity(double) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard

setActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.LearntBinaryClause

setActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.LearntHTClause

setActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.OriginalBinaryClause

setActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.OriginalHTClause

setActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.UnitClause

setActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses

setActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.WLClause

setActivity(double) - Method in interface org.sat4j.minisat.core.Constr

Set the activity at a specific value

setActivityPercent(double) - Method in class org.sat4j.minisat.learning.ActiveLearning

setAtLeastKEncoding(EncodingStrategyAdapter) - Method in class org.sat4j.tools.encoding.Policy

setAtLeastKEncoding(EncodingStrategy) - Method in class org.sat4j.tools.encoding.Policy

setAtLeastOneEncoding(EncodingStrategyAdapter) - Method in class org.sat4j.tools.encoding.Policy

setAtLeastOneEncoding(EncodingStrategy) - Method in class org.sat4j.tools.encoding.Policy

setAtMostKEncoding(EncodingStrategyAdapter) - Method in class org.sat4j.tools.encoding.Policy

setAtMostKEncoding(EncodingStrategy) - Method in class org.sat4j.tools.encoding.Policy

setAtMostOneEncoding(EncodingStrategyAdapter) - Method in class org.sat4j.tools.encoding.Policy

setAtMostOneEncoding(EncodingStrategy) - Method in class org.sat4j.tools.encoding.Policy

setBound(int) - Method in class org.sat4j.minisat.learning.FixedLengthLearning

setBound(int) - Method in class org.sat4j.minisat.learning.PercentLengthLearning

setBounds(int) - Method in class org.sat4j.minisat.core.Heap

setClaDecay(double) - Method in class org.sat4j.minisat.core.SearchParams

setConflictBoundIncFactor(double) - Method in class org.sat4j.minisat.core.SearchParams

setDataStructureFactory(D) - Method in interface org.sat4j.minisat.core.ICDCL

Change the internal representation of the constraints.

setDataStructureFactory(D) - Method in class org.sat4j.minisat.core.Solver

setDataStructureFactory(DataStructureFactory) - Method in class org.sat4j.minisat.learning.MiniSATLearning

setDBSimplificationAllowed(boolean) - Method in class org.sat4j.minisat.core.Solver

setDBSimplificationAllowed(boolean) - Method in interface org.sat4j.specs.ISolver

Set whether the solver is allowed to simplify the formula by propagating the truth value of top level satisfied variables.

setDBSimplificationAllowed(boolean) - Method in class org.sat4j.tools.AbstractOutputSolver

setDBSimplificationAllowed(boolean) - Method in class org.sat4j.tools.ManyCore

setDBSimplificationAllowed(boolean) - Method in class org.sat4j.tools.SolverDecorator

setDisplaySolutionLine(boolean) - Method in class org.sat4j.AbstractOptimizationLauncher

setExactlyKEncoding(EncodingStrategyAdapter) - Method in class org.sat4j.tools.encoding.Policy

setExactlyKEncoding(EncodingStrategy) - Method in class org.sat4j.tools.encoding.Policy

setExactlyOneEncoding(EncodingStrategyAdapter) - Method in class org.sat4j.tools.encoding.Policy

setExactlyOneEncoding(EncodingStrategy) - Method in class org.sat4j.tools.encoding.Policy

setExitCode(ExitCode) - Method in class org.sat4j.AbstractLauncher

Change the value of the exit code in the Launcher

setExpectedNumberOfClauses(int) - Method in class org.sat4j.minisat.core.Solver

setExpectedNumberOfClauses(int) - Method in class org.sat4j.opt.AbstractSelectorVariablesDecorator

setExpectedNumberOfClauses(int) - Method in class org.sat4j.opt.MaxSatDecorator

setExpectedNumberOfClauses(int) - Method in interface org.sat4j.specs.ISolver

To inform the solver of the expected number of clauses to read.

setExpectedNumberOfClauses(int) - Method in class org.sat4j.tools.DimacsOutputSolver

setExpectedNumberOfClauses(int) - Method in class org.sat4j.tools.DimacsStringSolver

setExpectedNumberOfClauses(int) - Method in class org.sat4j.tools.ManyCore

setExpectedNumberOfClauses(int) - Method in class org.sat4j.tools.SolverDecorator

setFactor(int) - Method in class org.sat4j.minisat.restarts.LubyRestarts

setFilename(String) - Method in class org.sat4j.tools.FileBasedVisualizationTool

setIncomplete(boolean) - Method in class org.sat4j.AbstractOptimizationLauncher

setInitConflictBound(int) - Method in class org.sat4j.minisat.core.SearchParams

setKeepSolverHot(boolean) - Method in class org.sat4j.minisat.core.Solver

setKeepSolverHot(boolean) - Method in interface org.sat4j.specs.ISolver

Changed the behavior of the SAT solver heuristics between successive calls.

setKeepSolverHot(boolean) - Method in class org.sat4j.tools.AbstractOutputSolver

setKeepSolverHot(boolean) - Method in class org.sat4j.tools.ManyCore

setKeepSolverHot(boolean) - Method in class org.sat4j.tools.SolverDecorator

setLearnedConstraintsDeletionStrategy(LearnedConstraintsDeletionStrategy) - Method in interface org.sat4j.minisat.core.ICDCL

setLearnedConstraintsDeletionStrategy(ConflictTimer, LearnedConstraintsEvaluationType) - Method in interface org.sat4j.minisat.core.ICDCL

setLearnedConstraintsDeletionStrategy(LearnedConstraintsEvaluationType) - Method in interface org.sat4j.minisat.core.ICDCL

setLearnedConstraintsDeletionStrategy(LearnedConstraintsDeletionStrategy) - Method in class org.sat4j.minisat.core.Solver

setLearnedConstraintsDeletionStrategy(ConflictTimer, LearnedConstraintsEvaluationType) - Method in class org.sat4j.minisat.core.Solver

setLearnedConstraintsDeletionStrategy(LearnedConstraintsEvaluationType) - Method in class org.sat4j.minisat.core.Solver

setLearner(Learner) - Method in class org.sat4j.minisat.constraints.AbstractDataStructureFactory

setLearner(Learner) - Method in interface org.sat4j.minisat.core.DataStructureFactory

setLearner(LearningStrategy<D>) - Method in interface org.sat4j.minisat.core.ICDCL

setLearner(LearningStrategy<D>) - Method in class org.sat4j.minisat.core.Solver

setLearnt() - Method in class org.sat4j.minisat.constraints.card.AtLeast

setLearnt() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard

setLearnt() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard

setLearnt() - Method in class org.sat4j.minisat.constraints.cnf.LearntBinaryClause

setLearnt() - Method in class org.sat4j.minisat.constraints.cnf.LearntHTClause

setLearnt() - Method in class org.sat4j.minisat.constraints.cnf.LearntWLClause

setLearnt() - Method in class org.sat4j.minisat.constraints.cnf.OriginalBinaryClause

setLearnt() - Method in class org.sat4j.minisat.constraints.cnf.OriginalHTClause

setLearnt() - Method in class org.sat4j.minisat.constraints.cnf.OriginalWLClause

setLearnt() - Method in class org.sat4j.minisat.constraints.cnf.UnitClause

setLearnt() - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses

setLearnt() - Method in interface org.sat4j.minisat.core.Constr

Mark a constraint as learnt.

setLevel(int, int) - Method in class org.sat4j.minisat.constraints.cnf.Lits

setLevel(int, int) - Method in interface org.sat4j.minisat.core.ILits

Sets the decision level of a literal.

setLimit(int) - Method in class org.sat4j.minisat.learning.ActiveLearning

setLimit(int) - Method in class org.sat4j.minisat.learning.PercentLengthLearning

setLits(ILits) - Method in interface org.sat4j.minisat.core.IOrder

Method used to provide an easy access the the solver vocabulary.

setLits(ILits) - Method in class org.sat4j.minisat.orders.RandomWalkDecorator

setLits(ILits) - Method in class org.sat4j.minisat.orders.TabuListDecorator

setLits(ILits) - Method in class org.sat4j.minisat.orders.VarOrderHeap

setLogger(ICDCLLogger) - Method in interface org.sat4j.minisat.core.ICDCL

setLogger(ICDCLLogger) - Method in class org.sat4j.minisat.core.Solver

setLogPrefix(String) - Method in class org.sat4j.minisat.core.Solver

setLogPrefix(String) - Method in interface org.sat4j.specs.ISolver

Set the prefix used to display information.

setLogPrefix(String) - Method in class org.sat4j.tools.AbstractOutputSolver

setLogPrefix(String) - Method in class org.sat4j.tools.ManyCore

setLogPrefix(String) - Method in class org.sat4j.tools.SolverDecorator

setLogWriter(PrintWriter) - Method in class org.sat4j.AbstractLauncher

To change the output stream on which statistics are displayed.

setMaxLength(int) - Method in class org.sat4j.minisat.learning.FixedLengthLearning

setMinimizationStrategy(MinimizationStrategy) - Method in interface org.sat4j.tools.xplain.Explainer

setMinimizationStrategy(MinimizationStrategy) - Method in class org.sat4j.tools.xplain.HighLevelXplain

setMinimizationStrategy(MinimizationStrategy) - Method in class org.sat4j.tools.xplain.Xplain

setNbVars(int) - Method in class org.sat4j.tools.DimacsStringSolver

setNeedToReduceDB(boolean) - Method in interface org.sat4j.minisat.core.ICDCL

setNeedToReduceDB(boolean) - Method in class org.sat4j.minisat.core.Solver

setOrder(IOrder) - Method in interface org.sat4j.minisat.core.ICDCL

setOrder(IOrder) - Method in class org.sat4j.minisat.core.Solver

setOrder(IOrder) - Method in class org.sat4j.minisat.learning.ActiveLearning

setPeriod(int) - Method in class org.sat4j.minisat.orders.PureOrder

setPhaseSelectionStrategy(IPhaseSelectionStrategy) - Method in interface org.sat4j.minisat.core.IOrder

setPhaseSelectionStrategy(IPhaseSelectionStrategy) - Method in class org.sat4j.minisat.orders.RandomWalkDecorator

setPhaseSelectionStrategy(IPhaseSelectionStrategy) - Method in class org.sat4j.minisat.orders.TabuListDecorator

setPhaseSelectionStrategy(IPhaseSelectionStrategy) - Method in class org.sat4j.minisat.orders.VarOrderHeap

Change the selection strategy.

setProbability(double) - Method in class org.sat4j.minisat.orders.RandomWalkDecorator

setReason(int, Constr) - Method in class org.sat4j.minisat.constraints.cnf.Lits

setReason(int, Constr) - Method in interface org.sat4j.minisat.core.ILits

Sets the reason of the assignment of a literal.

setRestartStrategy(RestartStrategy) - Method in interface org.sat4j.minisat.core.ICDCL

setRestartStrategy(RestartStrategy) - Method in class org.sat4j.minisat.core.Solver

setSearchListener(SearchListener<S>) - Method in class org.sat4j.minisat.core.Solver

setSearchListener(SearchListener<S>) - Method in interface org.sat4j.specs.ISolver

Allow the user to hook a listener to the solver to be notified of the main steps of the search process.

setSearchListener(SearchListener<S>) - Method in class org.sat4j.tools.AbstractOutputSolver

setSearchListener(SearchListener<I>) - Method in class org.sat4j.tools.ManyCore

setSearchListener(SearchListener<S>) - Method in class org.sat4j.tools.SolverDecorator

setSearchParams(SearchParams) - Method in interface org.sat4j.minisat.core.ICDCL

setSearchParams(SearchParams) - Method in class org.sat4j.minisat.core.Solver

setSilent(boolean) - Method in class org.sat4j.AbstractLauncher

setSimplifier(SimplificationType) - Method in interface org.sat4j.minisat.core.ICDCL

Setup the reason simplification strategy.

setSimplifier(ISimplifier) - Method in interface org.sat4j.minisat.core.ICDCL

Setup the reason simplification strategy.

setSimplifier(SimplificationType) - Method in class org.sat4j.minisat.core.Solver

setSimplifier(ISimplifier) - Method in class org.sat4j.minisat.core.Solver

setSolver(Solver<D>) - Method in interface org.sat4j.minisat.core.LearningStrategy

setSolver(Solver<D>) - Method in class org.sat4j.minisat.learning.ActiveLearning

setSolver(Solver<D>) - Method in class org.sat4j.minisat.learning.LimitedLearning

setSolver(Solver<D>) - Method in class org.sat4j.minisat.learning.MiniSATLearning

setTimeout(int) - Method in class org.sat4j.minisat.core.Solver

setTimeout(int) - Method in interface org.sat4j.specs.ISolver

To set the internal timeout of the solver.

setTimeout(int) - Method in class org.sat4j.tools.AbstractOutputSolver

setTimeout(int) - Method in class org.sat4j.tools.ManyCore

setTimeout(int) - Method in class org.sat4j.tools.SolverDecorator

setTimeoutMs(long) - Method in class org.sat4j.minisat.core.Solver

setTimeoutMs(long) - Method in interface org.sat4j.specs.ISolver

To set the internal timeout of the solver.

setTimeoutMs(long) - Method in class org.sat4j.tools.AbstractOutputSolver

setTimeoutMs(long) - Method in class org.sat4j.tools.ManyCore

setTimeoutMs(long) - Method in class org.sat4j.tools.SolverDecorator

setTimeoutOnConflicts(int) - Method in class org.sat4j.minisat.core.Solver

setTimeoutOnConflicts(int) - Method in interface org.sat4j.specs.ISolver

To set the internal timeout of the solver.

setTimeoutOnConflicts(int) - Method in class org.sat4j.tools.AbstractOutputSolver

setTimeoutOnConflicts(int) - Method in class org.sat4j.tools.ManyCore

setTimeoutOnConflicts(int) - Method in class org.sat4j.tools.SolverDecorator

setUnitPropagationListener(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.AbstractDataStructureFactory

setUnitPropagationListener(UnitPropagationListener) - Method in interface org.sat4j.minisat.core.DataStructureFactory

setVarActivityListener(VarActivityListener) - Method in interface org.sat4j.minisat.core.LearningStrategy

setVarActivityListener(VarActivityListener) - Method in class org.sat4j.minisat.learning.LimitedLearning

setVarDecay(double) - Method in interface org.sat4j.minisat.core.IOrder

Sets the variable activity decay as a growing factor for the next variable activity.

setVarDecay(double) - Method in class org.sat4j.minisat.core.SearchParams

setVarDecay(double) - Method in class org.sat4j.minisat.orders.RandomWalkDecorator

setVarDecay(double) - Method in class org.sat4j.minisat.orders.TabuListDecorator

setVarDecay(double) - Method in class org.sat4j.minisat.orders.VarOrderHeap

Change la valeur de varDecay.

setVerbose(boolean) - Method in class org.sat4j.minisat.core.Solver

setVerbose(boolean) - Method in interface org.sat4j.specs.ISolver

Set the verbosity of the solver

setVerbose(boolean) - Method in class org.sat4j.tools.AbstractOutputSolver

setVerbose(boolean) - Method in class org.sat4j.tools.ManyCore

setVerbose(boolean) - Method in class org.sat4j.tools.SolverDecorator

setVerbosity(boolean) - Method in class org.sat4j.reader.Reader

shortcuts - Variable in class org.sat4j.minisat.core.SolverStats

shouldRestart() - Method in interface org.sat4j.minisat.core.RestartStrategy

Ask the strategy if the solver should restart.

shouldRestart() - Method in class org.sat4j.minisat.restarts.ArminRestarts

shouldRestart() - Method in class org.sat4j.minisat.restarts.LubyRestarts

shouldRestart() - Method in class org.sat4j.minisat.restarts.MiniSATRestarts

shouldRestart() - Method in class org.sat4j.minisat.restarts.NoRestarts

showAvailableSolvers(ASolverFactory<T>) - Method in class org.sat4j.AbstractLauncher

showAvailableSolvers(ASolverFactory<T>, String) - Method in class org.sat4j.AbstractLauncher

shrink(int) - Method in class org.sat4j.core.ReadOnlyVec

shrink(int) - Method in class org.sat4j.core.ReadOnlyVecInt

shrink(int) - Method in class org.sat4j.core.Vec

Remove nofelems from the Vector.

shrink(int) - Method in class org.sat4j.core.VecInt

Remove the latest nofelems elements from the vector

shrink(int) - Method in interface org.sat4j.specs.IVec

Remove nofelems from the Vector.

shrink(int) - Method in interface org.sat4j.specs.IVecInt

Remove the latest nofelems elements from the vector

shrinkTo(int) - Method in class org.sat4j.core.ReadOnlyVec

shrinkTo(int) - Method in class org.sat4j.core.ReadOnlyVecInt

shrinkTo(int) - Method in class org.sat4j.core.Vec

reduce the Vector to exactly newsize elements

shrinkTo(int) - Method in class org.sat4j.core.VecInt

shrinkTo(int) - Method in interface org.sat4j.specs.IVec

reduce the Vector to exactly newsize elements

shrinkTo(int) - Method in interface org.sat4j.specs.IVecInt

shutdownHook - Variable in class org.sat4j.AbstractLauncher

silent - Variable in class org.sat4j.AbstractLauncher

SIMPLE_SIMPLIFICATION - Variable in class org.sat4j.minisat.core.Solver

SimplificationType - Enum in org.sat4j.minisat.core

List the available simplification techniques available.

simplify() - Method in class org.sat4j.minisat.constraints.card.AtLeast

simplify() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard

Simplifie la contrainte(l'all?

simplify() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard

simplifies the constraint

simplify() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause

simplify() - Method in class org.sat4j.minisat.constraints.cnf.HTClause

simplify() - Method in class org.sat4j.minisat.constraints.cnf.UnitClause

simplify() - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses

simplify() - Method in class org.sat4j.minisat.constraints.cnf.WLClause

simplify() - Method in interface org.sat4j.minisat.core.Constr

Simplifies a constraint, by removing top level falsified literals for instance.

simplify(IVecInt) - Method in interface org.sat4j.minisat.core.ISimplifier

simplifyDB() - Method in class org.sat4j.minisat.core.Solver

SingleSolutionDetector - Class in org.sat4j.tools

This solver decorator allows to detect whether or not the set of constraints available in the solver has only one solution or not.

SingleSolutionDetector(ISolver) - Constructor for class org.sat4j.tools.SingleSolutionDetector

size() - Method in class org.sat4j.core.ConstrGroup

size() - Method in class org.sat4j.core.ReadOnlyVec

size() - Method in class org.sat4j.core.ReadOnlyVecInt

size() - Method in class org.sat4j.core.Vec

size() - Method in class org.sat4j.core.VecInt

size() - Method in class org.sat4j.minisat.constraints.card.AtLeast

size() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard

size() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard

size() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause

size() - Method in class org.sat4j.minisat.constraints.cnf.HTClause

size() - Method in class org.sat4j.minisat.constraints.cnf.UnitClause

size() - Method in class org.sat4j.minisat.constraints.cnf.UnitClauses

size() - Method in class org.sat4j.minisat.constraints.cnf.WLClause

size() - Method in class org.sat4j.minisat.core.Heap

size() - Method in class org.sat4j.minisat.core.IntQueue

Pour connaitre la taille de la queue.

size() - Method in interface org.sat4j.specs.IConstr

size() - Method in interface org.sat4j.specs.IVec

size() - Method in interface org.sat4j.specs.IVecInt

skipComments() - Method in class org.sat4j.reader.DimacsReader

Skip comments at the beginning of the input stream.

skipComments() - Method in class org.sat4j.reader.EfficientScanner

Skip commented lines.

skipRestOfLine() - Method in class org.sat4j.reader.EfficientScanner

skipSpaces() - Method in class org.sat4j.reader.EfficientScanner

slistener - Variable in class org.sat4j.minisat.core.Solver

SOLUTION_PREFIX - Static variable in class org.sat4j.AbstractLauncher

SolutionCounter - Class in org.sat4j.tools

Another solver decorator that counts the number of solutions.

SolutionCounter(ISolver) - Constructor for class org.sat4j.tools.SolutionCounter

solutionFound(int[]) - Method in interface org.sat4j.specs.SearchListener

a solution is found.

solutionFound(int[]) - Method in class org.sat4j.tools.DotSearchTracing

solutionFound(int[]) - Method in class org.sat4j.tools.HeuristicsTracing

solutionFound(int[]) - Method in class org.sat4j.tools.LearnedTracing

solutionFound(int[]) - Method in class org.sat4j.tools.MultiTracing

solutionFound(int[]) - Method in class org.sat4j.tools.SearchEnumeratorListener

solutionFound(int[]) - Method in class org.sat4j.tools.SearchListenerAdapter

solutionFound(int[]) - Method in class org.sat4j.tools.TextOutputTracing

solve(IProblem) - Method in class org.sat4j.AbstractLauncher

solve(IProblem) - Method in class org.sat4j.AbstractOptimizationLauncher

solver - Variable in class org.sat4j.AbstractLauncher

solver - Variable in class org.sat4j.minisat.constraints.AbstractDataStructureFactory

Solver<D extends DataStructureFactory> - Class in org.sat4j.minisat.core

The backbone of the library providing the modular implementation of a MiniSAT (Chaff) like solver.

Solver(LearningStrategy<D>, D, IOrder, RestartStrategy) - Constructor for class org.sat4j.minisat.core.Solver

creates a Solver without LearningListener.

Solver(LearningStrategy<D>, D, SearchParams, IOrder, RestartStrategy) - Constructor for class org.sat4j.minisat.core.Solver

Solver(LearningStrategy<D>, D, SearchParams, IOrder, RestartStrategy, ICDCLLogger) - Constructor for class org.sat4j.minisat.core.Solver

solver - Variable in class org.sat4j.reader.DimacsReader

solver - Variable in class org.sat4j.tools.DimacsArrayReader

SolverDecorator<T extends ISolver> - Class in org.sat4j.tools

The aim of that class is to allow adding dynamic responsibilities to SAT solvers using the Decorator design pattern.

SolverDecorator(T) - Constructor for class org.sat4j.tools.SolverDecorator

SolverFactory - Class in org.sat4j.minisat

User friendly access to pre-constructed solvers.

solverNames() - Method in class org.sat4j.core.ASolverFactory

This methods returns names of solvers to be used with the method getSolverByName().

solvers - Variable in class org.sat4j.tools.ManyCore

SolverStats - Class in org.sat4j.minisat.core

Contains some statistics regarding the search.

SolverStats() - Constructor for class org.sat4j.minisat.core.SolverStats

sort(Comparator<T>) - Method in class org.sat4j.core.ReadOnlyVec

sort() - Method in class org.sat4j.core.ReadOnlyVecInt

sort(Comparator<T>) - Method in class org.sat4j.core.Vec

sort() - Method in class org.sat4j.core.VecInt

sort the vector using a custom quicksort.

sort(Comparator<T>) - Method in interface org.sat4j.specs.IVec

sort() - Method in interface org.sat4j.specs.IVecInt

sortOnActivity() - Method in class org.sat4j.minisat.core.Solver

sortUnique(Comparator<T>) - Method in class org.sat4j.core.ReadOnlyVec

sortUnique() - Method in class org.sat4j.core.ReadOnlyVecInt

sortUnique(Comparator<T>) - Method in class org.sat4j.core.Vec

sortUnique() - Method in class org.sat4j.core.VecInt

sortUnique(Comparator<T>) - Method in interface org.sat4j.specs.IVec

sortUnique() - Method in interface org.sat4j.specs.IVecInt

SpeedTracing - Class in org.sat4j.tools

SpeedTracing(IVisualizationTool, IVisualizationTool, IVisualizationTool) - Constructor for class org.sat4j.tools.SpeedTracing

start() - Method in interface org.sat4j.specs.SearchListener

Start the search.

start() - Method in class org.sat4j.tools.ConflictDepthTracing

start() - Method in class org.sat4j.tools.ConflictLevelTracing

start() - Method in class org.sat4j.tools.DecisionLevelTracing

start() - Method in class org.sat4j.tools.DecisionTracing

start() - Method in class org.sat4j.tools.DotSearchTracing

start() - Method in class org.sat4j.tools.LBDTracing

start() - Method in class org.sat4j.tools.LearnedClausesSizeTracing

start() - Method in class org.sat4j.tools.MultiTracing

start() - Method in class org.sat4j.tools.SearchListenerAdapter

start() - Method in class org.sat4j.tools.SpeedTracing

start() - Method in class org.sat4j.tools.TextOutputTracing

starts - Variable in class org.sat4j.minisat.core.SolverStats

stop() - Method in class org.sat4j.minisat.core.Solver

stop() - Method in interface org.sat4j.specs.ISolverService

Ask the SAT solver to stop the search.

subset(int) - Method in class org.sat4j.core.ReadOnlyVecInt

subset(int) - Method in class org.sat4j.core.VecInt

subset(int) - Method in interface org.sat4j.specs.IVecInt

Compute all subsets of cardinal k of the vector.

SubsetVarOrder - Class in org.sat4j.minisat.orders

SubsetVarOrder(int[]) - Constructor for class org.sat4j.minisat.orders.SubsetVarOrder

suggestNextLiteralToBranchOn(int) - Method in class org.sat4j.minisat.core.Solver

suggestNextLiteralToBranchOn(int) - Method in interface org.sat4j.specs.ISolverService

Suggests to the SAT solver to branch next on the given literal.

T

TabuListDecorator - Class in org.sat4j.minisat.orders

Uses a tabu list to prevent the solver to

TabuListDecorator(VarOrderHeap) - Constructor for class org.sat4j.minisat.orders.TabuListDecorator

TabuListDecorator(VarOrderHeap, int) - Constructor for class org.sat4j.minisat.orders.TabuListDecorator

tail - Variable in class org.sat4j.minisat.constraints.cnf.BinaryClause

tail - Variable in class org.sat4j.minisat.constraints.cnf.HTClause

TextOutputTracing<T> - Class in org.sat4j.tools

Debugging Search Listener allowing to follow the search in a textual way.

TextOutputTracing(Map<Integer, T>) - Constructor for class org.sat4j.tools.TextOutputTracing

TimeoutException - Exception in org.sat4j.specs

Exception launched when the solver cannot solve a problem within its allowed time.

TimeoutException() - Constructor for exception org.sat4j.specs.TimeoutException

Constructor for TimeoutException.

TimeoutException(String) - Constructor for exception org.sat4j.specs.TimeoutException

Constructor for TimeoutException.

TimeoutException(String, Throwable) - Constructor for exception org.sat4j.specs.TimeoutException

Constructor for TimeoutException.

TimeoutException(Throwable) - Constructor for exception org.sat4j.specs.TimeoutException

Constructor for TimeoutException.

toArray() - Method in class org.sat4j.core.ReadOnlyVec

toArray() - Method in class org.sat4j.core.ReadOnlyVecInt

toArray() - Method in class org.sat4j.core.Vec

toArray() - Method in class org.sat4j.core.VecInt

toArray() - Method in interface org.sat4j.specs.IVec

Allow to access the internal representation of the vector as an array.

toArray() - Method in interface org.sat4j.specs.IVecInt

Allow to access the internal representation of the vector as an array.

toConstraint() - Method in class org.sat4j.minisat.constraints.card.AtLeast

toConstraint() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard

toConstraint() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard

toConstraint() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause

toConstraint() - Method in class org.sat4j.minisat.constraints.cnf.HTClause

toConstraint() - Method in class org.sat4j.minisat.constraints.cnf.WLClause

toConstraint() - Method in interface org.sat4j.minisat.core.Propagatable

Allow to access a constraint view of the propagatable to avoid casting.

toDimacs(int) - Static method in class org.sat4j.core.LiteralsUtils

decode the internal representation of a literal in internal representation into Dimacs format.

toInternal(int) - Static method in class org.sat4j.core.LiteralsUtils

encode the classical Dimacs representation (negated integers for negated literals) into the internal format.

toMap() - Method in class org.sat4j.minisat.core.SolverStats

toString() - Method in class org.sat4j.core.ConstrGroup

toString() - Method in class org.sat4j.core.ReadOnlyVec

toString() - Method in class org.sat4j.core.ReadOnlyVecInt

toString() - Method in class org.sat4j.core.Vec

toString() - Method in class org.sat4j.core.VecInt

toString() - Method in class org.sat4j.ExitCode

toString() - Method in class org.sat4j.minisat.constraints.card.AtLeast

Textual representation of the constraint

toString() - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard

Cha?

toString() - Method in class org.sat4j.minisat.constraints.card.MinWatchCard

Returns a string representation of the constraint.

toString() - Method in class org.sat4j.minisat.constraints.cnf.BinaryClause

toString() - Method in class org.sat4j.minisat.constraints.cnf.HTClause

toString(int) - Static method in class org.sat4j.minisat.constraints.cnf.Lits

toString() - Method in class org.sat4j.minisat.constraints.cnf.UnitClause

toString() - Method in class org.sat4j.minisat.constraints.cnf.WLClause

toString() - Method in class org.sat4j.minisat.core.Counter

toString() - Method in class org.sat4j.minisat.core.IntQueue

toString() - Method in class org.sat4j.minisat.core.SearchParams

toString(String) - Method in class org.sat4j.minisat.core.Solver

toString() - Method in class org.sat4j.minisat.core.Solver

toString() - Method in class org.sat4j.minisat.learning.ActiveLearning

toString() - Method in class org.sat4j.minisat.learning.ClauseOnlyLearning

toString() - Method in class org.sat4j.minisat.learning.FixedLengthLearning

toString() - Method in class org.sat4j.minisat.learning.MiniSATLearning

toString() - Method in class org.sat4j.minisat.learning.PercentLengthLearning

toString() - Method in class org.sat4j.minisat.orders.NegativeLiteralSelectionStrategy

toString() - Method in class org.sat4j.minisat.orders.PhaseCachingAutoEraseStrategy

toString() - Method in class org.sat4j.minisat.orders.PhaseInLastLearnedClauseSelectionStrategy

toString() - Method in class org.sat4j.minisat.orders.PositiveLiteralSelectionStrategy

toString() - Method in class org.sat4j.minisat.orders.PureOrder

toString() - Method in class org.sat4j.minisat.orders.RandomLiteralSelectionStrategy

toString() - Method in class org.sat4j.minisat.orders.RandomWalkDecorator

toString() - Method in class org.sat4j.minisat.orders.RSATLastLearnedClausesPhaseSelectionStrategy

toString() - Method in class org.sat4j.minisat.orders.RSATPhaseSelectionStrategy

toString() - Method in class org.sat4j.minisat.orders.TabuListDecorator

toString() - Method in class org.sat4j.minisat.orders.UserFixedPhaseSelectionStrategy

toString() - Method in class org.sat4j.minisat.orders.VarOrderHeap

toString() - Method in class org.sat4j.minisat.restarts.ArminRestarts

toString() - Method in class org.sat4j.minisat.restarts.LubyRestarts

toString() - Method in class org.sat4j.minisat.restarts.MiniSATRestarts

toString() - Method in class org.sat4j.minisat.restarts.NoRestarts

toString(String) - Method in interface org.sat4j.specs.ISolver

Display a textual representation of the solver configuration.

toString() - Method in class org.sat4j.specs.Lbool

Textual representation for the truth value.

toString() - Method in class org.sat4j.tools.ClausalCardinalitiesDecorator

toString(String) - Method in class org.sat4j.tools.ClausalCardinalitiesDecorator

toString(String) - Method in class org.sat4j.tools.DimacsOutputSolver

toString(String) - Method in class org.sat4j.tools.DimacsStringSolver

toString() - Method in class org.sat4j.tools.DimacsStringSolver

toString() - Method in class org.sat4j.tools.encoding.EncodingStrategyAdapter

toString(String) - Method in class org.sat4j.tools.ManyCore

toString(String) - Method in class org.sat4j.tools.OptToSatAdapter

toString(String) - Method in class org.sat4j.tools.SolverDecorator

toString() - Method in class org.sat4j.tools.SolverDecorator

toString() - Method in class org.sat4j.tools.xplain.DeletionStrategy

toString(String) - Method in class org.sat4j.tools.xplain.HighLevelXplain

toString() - Method in class org.sat4j.tools.xplain.InsertionStrategy

toString() - Method in class org.sat4j.tools.xplain.QuickXplain2001Strategy

toString() - Method in class org.sat4j.tools.xplain.QuickXplainStrategy

toString(String) - Method in class org.sat4j.tools.xplain.Xplain

trail - Variable in class org.sat4j.minisat.core.Solver

affectation en ordre chronologique

trailLim - Variable in class org.sat4j.minisat.core.Solver

indice des s?

TRUE - Static variable in class org.sat4j.specs.Lbool

TRUE - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader

truthValue(int) - Method in class org.sat4j.minisat.core.Solver

truthValue(int) - Method in interface org.sat4j.specs.ISolverService

To access the truth value of a specific literal under current assignment.

U

unassign(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits

unassign(int) - Method in interface org.sat4j.minisat.core.ILits

Unassigns a boolean variable (truth value if UNDEF).

UNDEFINED - Static variable in interface org.sat4j.minisat.core.ILits

UNDEFINED - Static variable in class org.sat4j.specs.Lbool

undertimeout - Variable in class org.sat4j.minisat.core.Solver

undo(int) - Method in class org.sat4j.minisat.constraints.card.AtLeast

undo(int) - Method in class org.sat4j.minisat.constraints.card.MaxWatchCard

M?

undo(int) - Method in class org.sat4j.minisat.constraints.card.MinWatchCard

Updates information on the constraint in case of a backtrack

undo(int) - Method in interface org.sat4j.minisat.core.IOrder

Method called when a variable is unassigned.

undo(int) - Method in interface org.sat4j.minisat.core.Undoable

Method called when backtracking

undo(int) - Method in class org.sat4j.minisat.orders.RandomWalkDecorator

undo(int) - Method in class org.sat4j.minisat.orders.TabuListDecorator

undo(int) - Method in class org.sat4j.minisat.orders.VarOrderHeap

Methode appelee quand la variable x est desaffectee.

Undoable - Interface in org.sat4j.minisat.core

Interface providing the undoable service.

undoOne() - Method in class org.sat4j.minisat.core.Solver

undos(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits

undos(int) - Method in interface org.sat4j.minisat.core.ILits

Retrieve the methods to call when the solver backtracks.

UnitClause - Class in org.sat4j.minisat.constraints.cnf

UnitClause(int) - Constructor for class org.sat4j.minisat.constraints.cnf.UnitClause

UnitClauses - Class in org.sat4j.minisat.constraints.cnf

UnitClauses(IVecInt) - Constructor for class org.sat4j.minisat.constraints.cnf.UnitClauses

UnitPropagationListener - Interface in org.sat4j.minisat.core

Interface providing the unit propagation capability.

UNKNOWN - Static variable in class org.sat4j.ExitCode

unsafeGet(int) - Method in class org.sat4j.core.ReadOnlyVecInt

unsafeGet(int) - Method in class org.sat4j.core.VecInt

unsafeGet(int) - Method in interface org.sat4j.specs.IVecInt

unsafePush(T) - Method in class org.sat4j.core.ReadOnlyVec

unsafePush(int) - Method in class org.sat4j.core.ReadOnlyVecInt

unsafePush(T) - Method in class org.sat4j.core.Vec

unsafePush(int) - Method in class org.sat4j.core.VecInt

unsafePush(T) - Method in interface org.sat4j.specs.IVec

To push an element in the vector when you know you have space for it.

unsafePush(int) - Method in interface org.sat4j.specs.IVecInt

Push the element in the Vector without verifying if there is room for it.

unsatExplanation() - Method in class org.sat4j.minisat.core.Solver

unsatExplanation() - Method in interface org.sat4j.specs.ISolver

Retrieve an explanation of the inconsistency in terms of assumption literals.

unsatExplanation() - Method in class org.sat4j.tools.AbstractOutputSolver

unsatExplanation() - Method in class org.sat4j.tools.ManyCore

unsatExplanation() - Method in class org.sat4j.tools.SolverDecorator

UNSATISFIABLE - Static variable in class org.sat4j.ExitCode

unset(int) - Method in class org.sat4j.minisat.core.Solver

unset(int) - Method in interface org.sat4j.minisat.core.UnitPropagationListener

Unset a unit clause.

updateActivity(int) - Method in class org.sat4j.minisat.orders.VarOrderHeap

updateLBD - Variable in class org.sat4j.minisat.core.SolverStats

updateVar(int) - Method in interface org.sat4j.minisat.core.IOrder

To be called when the activity of a literal changed.

updateVar(int) - Method in interface org.sat4j.minisat.core.IPhaseSelectionStrategy

To be called when the activity of a literal changed.

updateVar(int) - Method in class org.sat4j.minisat.orders.NegativeLiteralSelectionStrategy

updateVar(int) - Method in class org.sat4j.minisat.orders.PhaseCachingAutoEraseStrategy

updateVar(int) - Method in class org.sat4j.minisat.orders.PhaseInLastLearnedClauseSelectionStrategy

updateVar(int) - Method in class org.sat4j.minisat.orders.PositiveLiteralSelectionStrategy

updateVar(int) - Method in class org.sat4j.minisat.orders.RandomLiteralSelectionStrategy

updateVar(int) - Method in class org.sat4j.minisat.orders.RandomWalkDecorator

updateVar(int) - Method in class org.sat4j.minisat.orders.RSATLastLearnedClausesPhaseSelectionStrategy

updateVar(int) - Method in class org.sat4j.minisat.orders.RSATPhaseSelectionStrategy

updateVar(int) - Method in class org.sat4j.minisat.orders.TabuListDecorator

updateVar(int) - Method in class org.sat4j.minisat.orders.UserFixedPhaseSelectionStrategy

updateVar(int) - Method in class org.sat4j.minisat.orders.VarOrderHeap

Appelee lorsque l'activite de la variable x a change.

updateVarAtDecisionLevel(int) - Method in interface org.sat4j.minisat.core.IOrder

Allow to perform a specific action when a literal of the current decision level is updated.

updateVarAtDecisionLevel(int) - Method in interface org.sat4j.minisat.core.IPhaseSelectionStrategy

Allow to perform a specific action when a literal of the current decision level is updated.

updateVarAtDecisionLevel(int) - Method in class org.sat4j.minisat.orders.NegativeLiteralSelectionStrategy

updateVarAtDecisionLevel(int) - Method in class org.sat4j.minisat.orders.PhaseCachingAutoEraseStrategy

updateVarAtDecisionLevel(int) - Method in class org.sat4j.minisat.orders.PhaseInLastLearnedClauseSelectionStrategy

updateVarAtDecisionLevel(int) - Method in class org.sat4j.minisat.orders.PositiveLiteralSelectionStrategy

updateVarAtDecisionLevel(int) - Method in class org.sat4j.minisat.orders.RandomLiteralSelectionStrategy

updateVarAtDecisionLevel(int) - Method in class org.sat4j.minisat.orders.RandomWalkDecorator

updateVarAtDecisionLevel(int) - Method in class org.sat4j.minisat.orders.RSATLastLearnedClausesPhaseSelectionStrategy

updateVarAtDecisionLevel(int) - Method in class org.sat4j.minisat.orders.RSATPhaseSelectionStrategy

updateVarAtDecisionLevel(int) - Method in class org.sat4j.minisat.orders.TabuListDecorator

updateVarAtDecisionLevel(int) - Method in class org.sat4j.minisat.orders.UserFixedPhaseSelectionStrategy

updateVarAtDecisionLevel(int) - Method in class org.sat4j.minisat.orders.VarOrderHeap

updateWriter() - Method in class org.sat4j.tools.FileBasedVisualizationTool

UPPER_BOUND - Static variable in class org.sat4j.ExitCode

usage() - Method in class org.sat4j.AbstractLauncher

usage() - Method in class org.sat4j.BasicLauncher

usage() - Method in class org.sat4j.MUSLauncher

UserFixedPhaseSelectionStrategy - Class in org.sat4j.minisat.orders

Selection strategy where the phase selection is decided at init time and is not updated during the search.

UserFixedPhaseSelectionStrategy() - Constructor for class org.sat4j.minisat.orders.UserFixedPhaseSelectionStrategy

V

value() - Method in class org.sat4j.ExitCode

valueOf(String) - Static method in enum org.sat4j.minisat.core.LearnedConstraintsEvaluationType

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum org.sat4j.minisat.core.SimplificationType

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum org.sat4j.tools.encoding.EncodingStrategy

Returns the enum constant of this type with the specified name.

values() - Static method in enum org.sat4j.minisat.core.LearnedConstraintsEvaluationType

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum org.sat4j.minisat.core.SimplificationType

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum org.sat4j.tools.encoding.EncodingStrategy

Returns an array containing the constants of this enum type, in the order they are declared.

valueToString(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits

valueToString(int) - Method in interface org.sat4j.minisat.core.ILits

Returns a textual representation of the truth value of that literal.

var(int) - Static method in class org.sat4j.core.LiteralsUtils

Returns the variable associated to the literal

varActivity(int) - Method in interface org.sat4j.minisat.core.IOrder

To obtain the current activity of a variable.

varActivity(int) - Method in class org.sat4j.minisat.orders.RandomWalkDecorator

varActivity(int) - Method in class org.sat4j.minisat.orders.TabuListDecorator

varActivity(int) - Method in class org.sat4j.minisat.orders.VarOrderHeap

VarActivityListener - Interface in org.sat4j.minisat.core

Interface providing the capability to increase the activity of a given variable.

varBumpActivity(int) - Method in class org.sat4j.minisat.core.Solver

varBumpActivity(int) - Method in interface org.sat4j.minisat.core.VarActivityListener

Update the activity of a variable v.

varDecayActivity() - Method in interface org.sat4j.minisat.core.IOrder

Decay the variables activities.

varDecayActivity() - Method in class org.sat4j.minisat.orders.RandomWalkDecorator

varDecayActivity() - Method in class org.sat4j.minisat.orders.TabuListDecorator

varDecayActivity() - Method in class org.sat4j.minisat.orders.VarOrderHeap

VarOrderHeap - Class in org.sat4j.minisat.orders

VarOrderHeap() - Constructor for class org.sat4j.minisat.orders.VarOrderHeap

VarOrderHeap(IPhaseSelectionStrategy) - Constructor for class org.sat4j.minisat.orders.VarOrderHeap

Vec<T> - Class in org.sat4j.core

Simple but efficient vector implementation, based on the vector implementation available in MiniSAT.

Vec() - Constructor for class org.sat4j.core.Vec

Create a Vector with an initial capacity of 5 elements.

Vec(T[]) - Constructor for class org.sat4j.core.Vec

Adapter method to translate an array of int into an IVec.

Vec(int) - Constructor for class org.sat4j.core.Vec

Create a Vector with a given capacity.

Vec(int, T) - Constructor for class org.sat4j.core.Vec

Construit un vecteur contenant de taille size rempli a l'aide de size pad.

VecInt - Class in org.sat4j.core

A vector specific for primitive integers, widely used in the solver.

VecInt() - Constructor for class org.sat4j.core.VecInt

VecInt(int) - Constructor for class org.sat4j.core.VecInt

VecInt(int[]) - Constructor for class org.sat4j.core.VecInt

Adapter method to translate an array of int into an IVecInt.

VecInt(int, int) - Constructor for class org.sat4j.core.VecInt

Build a vector of a given initial size filled with an integer.

voc - Variable in class org.sat4j.minisat.constraints.card.AtLeast

voc - Variable in class org.sat4j.minisat.constraints.cnf.HTClause

voc - Variable in class org.sat4j.minisat.constraints.cnf.WLClause

voc - Variable in class org.sat4j.minisat.core.Solver

W

watch(int, Propagatable) - Method in class org.sat4j.minisat.constraints.cnf.Lits

watch(int, Propagatable) - Method in interface org.sat4j.minisat.core.ILits

Record a new constraint to watch when a literal is satisfied.

watchCumul - Variable in class org.sat4j.minisat.constraints.card.MinWatchCard

contains the sum of the coefficients of the watched literals

watches(int) - Method in class org.sat4j.minisat.constraints.cnf.Lits

watches(int) - Method in interface org.sat4j.minisat.core.ILits

WLClause - Class in org.sat4j.minisat.constraints.cnf

Lazy data structure for clause using Watched Literals.

WLClause(IVecInt, ILits) - Constructor for class org.sat4j.minisat.constraints.cnf.WLClause

Creates a new basic clause

X

XNOR - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader

XOR - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader

xor(int, IVecInt) - Method in class org.sat4j.tools.GateTranslator

translate y <=> x1 xor x2 xor ... xor xn into clauses.

xor(int, int, int) - Method in class org.sat4j.tools.GateTranslator

Xplain<T extends ISolver> - Class in org.sat4j.tools.xplain

Explanation framework for SAT4J.

Xplain(T, boolean) - Constructor for class org.sat4j.tools.xplain.Xplain

Xplain(T) - Constructor for class org.sat4j.tools.xplain.Xplain

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