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

I

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

IConstr - Interface in org.sat4j.specs

The most general abstraction for handling a constraint.

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

IFF - Static variable in class org.sat4j.reader.ExtendedDimacsReader

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

IFF - Static variable in class org.sat4j.tools.ExtendedDimacsArrayToDimacsConverter

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

translate y <=> (x1 <=> x2 <=> ... <=> xn) into clauses.

IFTHENELSE - Static variable in class org.sat4j.reader.ExtendedDimacsReader

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

IFTHENELSE - Static variable in class org.sat4j.tools.ExtendedDimacsArrayToDimacsConverter

IInternalPBConstraintCreator - Interface in org.sat4j.minisat.constraints.pb

ILits - Interface in org.sat4j.minisat.core

That interface manages the solver's internal vocabulary.

ILits2 - Interface in org.sat4j.minisat.core

Specific vocabulary taking special care of binary clauses.

ILits23 - Interface in org.sat4j.minisat.core

Specific vocabulary taking special care of binary and ternary clauses.

IMarkableLits - Interface in org.sat4j.minisat.core

Vocabulary in which literals can be marked.

IMPLIES - Static variable in class org.sat4j.reader.ExtendedDimacsReader

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

IMPLIES - Static variable in class org.sat4j.tools.ExtendedDimacsArrayToDimacsConverter

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

incActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.CBClause

incActivity(double) - Method in class org.sat4j.minisat.constraints.cnf.TernaryClauses

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

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

increase activity value of the constraint

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

Increase the constraint activity.

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

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 class org.sat4j.minisat.constraints.cnf.MarkableLits

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

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

that method has the responsability to initialize all arrays in the heuristics.

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() - Method in class org.sat4j.minisat.orders.JWOrder

init() - Method in class org.sat4j.minisat.orders.MyOrder

init() - Method in class org.sat4j.minisat.orders.VarOrder

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

that method has the responsability to initialize all arrays in the heuristics.

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

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

initAnalyze() - Method in interface org.sat4j.minisat.core.AssertingClauseGenerator

hook method called before the analysis.

initAnalyze() - Method in class org.sat4j.minisat.uip.DecisionUIP

initAnalyze() - Method in class org.sat4j.minisat.uip.FirstUIP

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

Insert an element at the very begining 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.Vec

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

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

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

Access to the single instance of the factory.

instance() - Static method in class org.sat4j.reader.csp.BinarySupportEncoding

instance() - Static method in class org.sat4j.reader.csp.DirectEncoding

instance() - Static method in class org.sat4j.reader.csp.GeneralizedSupportEncoding

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

IOrder<L extends ILits> - Interface in org.sat4j.minisat.core

Interface for the variable ordering heuristics.

IProblem - Interface in org.sat4j.specs

Access to the information related to a given problem instance.

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

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

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

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

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

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

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

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

isMarked(int) - Method in class org.sat4j.minisat.constraints.cnf.MarkableLits

isMarked(int) - Method in interface org.sat4j.minisat.core.IMarkableLits

To know if a given literal is marked, i.e. has a mark different from MARKLESS.

ISolver - Interface in org.sat4j.specs

That interface contains all the services available on a SAT solver.

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

isSatisfiable(IVecInt) - 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) - Method in interface org.sat4j.specs.IProblem

Check the satisfiability of the set of constraints contained inside the solver.

isSatisfiable() - Method in class org.sat4j.tools.DimacsOutputSolver

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

isSatisfiable() - Method in class org.sat4j.tools.ModelIterator

isSatisfiable(IVecInt) - Method in class org.sat4j.tools.ModelIterator

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

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

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

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

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

isVerbose() - Method in class org.sat4j.reader.Reader

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

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

iterator() - Method in class org.sat4j.reader.csp.EnumeratedDomain

iterator() - Method in class org.sat4j.reader.csp.RangeDomain

iterator() - Method in class org.sat4j.reader.csp.SingletonDomain

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.