Overview
Package
Class
Use
Tree
Deprecated
Index
Help
PREV LETTER
NEXT LETTER
FRAMES
NO FRAMES
All Classes
A
B
C
D
E
F
G
H
I
J
L
M
N
O
P
R
S
T
U
V
W
X
A
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. problems with YES/NO/UNKNOWN answers.
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
ActiveLearning
- 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.
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.
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.
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.
SolverDecorator
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
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.
SolverDecorator
addTernaryClause(int, int)
- Method in class org.sat4j.minisat.constraints.cnf.
TernaryClauses
admitABetterSolution()
- Method in class org.sat4j.opt.
MaxSatDecorator
admitABetterSolution()
- Method in class org.sat4j.opt.
MinOneDecorator
admitABetterSolution()
- Method in class org.sat4j.opt.
PseudoOptDecorator
admitABetterSolution()
- Method in class org.sat4j.opt.
WeightedMaxSatDecorator
admitABetterSolution()
- Method in interface org.sat4j.specs.
IOptimizationProblem
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
ANSWER_PREFIX
- Static variable in class org.sat4j.
AbstractLauncher
ArrayPb
- Class in
org.sat4j.minisat.constraints.pb
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.
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
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
Overview
Package
Class
Use
Tree
Deprecated
Index
Help
PREV LETTER
NEXT LETTER
FRAMES
NO FRAMES
All Classes
A
B
C
D
E
F
G
H
I
J
L
M
N
O
P
R
S
T
U
V
W
X