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

A

AAGReader - Class in org.sat4j.reader

AbstractCardinalityDataStructure - Class in org.sat4j.minisat.constraints

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

AbstractDataStructureFactory<L extends ILits> - Class in org.sat4j.minisat.constraints

AbstractLauncher - Class in org.sat4j

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

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

AbstractPBClauseCardConstrDataStructure - Class in org.sat4j.minisat.constraints

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

AbstractPBDataStructureFactory - Class in org.sat4j.minisat.constraints

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

AbstractSelectorVariablesDecorator - Class in org.sat4j.opt

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

ActiveLearning<L extends ILits> - 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

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

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

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

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

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

addBinaryClause(int) - Method in class org.sat4j.minisat.constraints.cnf.BinaryClauses

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

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

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

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

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

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

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

addConstantParameter(String, int) - Method in class org.sat4j.reader.CSPReader

addDomainValue(int) - Method in class org.sat4j.reader.CSPReader

addDomainValue(int, int) - Method in class org.sat4j.reader.CSPReader

addEffectiveParameter(String) - Method in class org.sat4j.reader.CSPReader

addEffectiveParameter(int) - Method in class org.sat4j.reader.CSPReader

addFormalParameter(String, String) - Method in class org.sat4j.reader.CSPReader

adding(int) - Method in class org.sat4j.minisat.core.DotSearchListener

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

adding forced variable (conflict driven assignment)

adding(int) - Method in class org.sat4j.minisat.core.TextOutputListener

addIntegerItem(int) - Method in class org.sat4j.reader.CSPReader

addPseudoBoolean(IVecInt, IVec<BigInteger>, boolean, BigInteger) - Method in class org.sat4j.minisat.constraints.pb.PBSolverWithImpliedClause

addPseudoBoolean(IVecInt, IVec<BigInteger>, boolean, BigInteger) - Method in class org.sat4j.minisat.core.Solver

addPseudoBoolean(IVecInt, IVec<BigInteger>, boolean, BigInteger) - Method in interface org.sat4j.specs.ISolver

Create a Pseudo-Boolean constraint of the type "at least n of those literals must be satisfied"

addPseudoBoolean(IVecInt, IVec<BigInteger>, boolean, BigInteger) - Method in class org.sat4j.tools.DimacsOutputSolver

addPseudoBoolean(IVecInt, IVec<BigInteger>, boolean, BigInteger) - Method in class org.sat4j.tools.SolverDecorator

addRelationTuple(int[]) - Method in class org.sat4j.reader.CSPReader

addTernaryClause(int, int) - Method in class org.sat4j.minisat.constraints.cnf.TernaryClauses

addTuple(int, int[]) - Method in class org.sat4j.reader.csp.Nogoods

addTuple(int, int[]) - Method in interface org.sat4j.reader.csp.Relation

addTuple(int, int[]) - Method in class org.sat4j.reader.csp.Supports

addVariable(String) - Method in class org.sat4j.reader.csp.Predicate

addVariable(String, String) - Method in class org.sat4j.reader.CSPReader

addVariableItem(String) - Method in class org.sat4j.reader.CSPReader

addVariableToConstraint(String) - Method in class org.sat4j.reader.CSPReader

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

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

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

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

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

AIGReader - Class in org.sat4j.reader

AllDiff - Class in org.sat4j.reader.csp

AllDiff() - Constructor for class org.sat4j.reader.csp.AllDiff

analyze(Constr, Handle<Constr>) - Method in class org.sat4j.minisat.constraints.pb.PBSolver

analyze(Constr, Handle<Constr>) - Method in class org.sat4j.minisat.core.Solver

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

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

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

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

arity() - Method in class org.sat4j.reader.csp.Nogoods

arity() - Method in interface org.sat4j.reader.csp.Relation

arity() - Method in class org.sat4j.reader.csp.Supports

ArminRestarts - Class in org.sat4j.minisat.restarts

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

ASolverFactory - Class in org.sat4j.core

A solver factory is responsible to provide 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.BinaryClauses

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

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

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

assertConstraint(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.pb.AtLeastPB

assertConstraint(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.pb.MinWatchCardPB

assertConstraint(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.pb.MixableCBClausePB

assertConstraint(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.pb.WatchPb

assertConstraint(UnitPropagationListener) - Method in class org.sat4j.minisat.constraints.pb.WLClausePB

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

Method called when the constraint is to be asserted.

AssertingClauseGenerator - Interface in org.sat4j.minisat.core

An assertingClauseGenerator is responsible for the creation of an asserting clause during conflict analysis.

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

indicate that a literal has been satisfied.

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

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

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

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

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

assuming(int) - Method in class org.sat4j.minisat.core.DotSearchListener

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

decision variable

assuming(int) - Method in class org.sat4j.minisat.core.TextOutputListener

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

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

ATLEAST - Static variable in class org.sat4j.minisat.constraints.pb.WatchPb

constant for the initial type of inequality more than or equal

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

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

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

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

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

atLeastNew(ILits, IVecInt, int) - Static method in class org.sat4j.minisat.constraints.pb.AtLeastPB

AtLeastPB - Class in org.sat4j.minisat.constraints.pb

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

ATMOST - Static variable in class org.sat4j.minisat.constraints.pb.WatchPb

constant for the initial type of inequality less than or equal

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

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

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