Serialized Form
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
vec
IVec<T> vec
serialVersionUID: 1L
vec
IVecInt vec
serialVersionUID: 1L
nbelem
int nbelem
myarray
Object[] myarray
Class org.sat4j.core.Vec$1 extends Object implements Serializable |
serialVersionUID: 1L
nbelem
int nbelem
myarray
int[] myarray
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
costs
int[] costs
prevmodel
int[] prevmodel
vars
IVecInt vars
coeffs
IVec<T> coeffs
objectivevalue
int objectivevalue
prevConstr
IConstr prevConstr
serialVersionUID: 1L
serialVersionUID: 1L
nborigvars
int nborigvars
nbexpectedclauses
int nbexpectedclauses
falsifiedWeight
BigInteger falsifiedWeight
nbnewvar
int nbnewvar
prevmodel
int[] prevmodel
prevboolmodel
boolean[] prevboolmodel
prevfullmodel
int[] prevfullmodel
previousPBConstr
IConstr previousPBConstr
top
BigInteger top
counter
BigInteger counter
lits
IVecInt lits
coefs
IVec<T> coefs
obj
ObjectiveFunction obj
Package org.sat4j.maxsat.reader |
serialVersionUID: 1L
weight
BigInteger weight
top
BigInteger top
decorator
WeightedMaxSatDecorator decorator
Package org.sat4j.minisat |
serialVersionUID: 1L
Package org.sat4j.minisat.constraints |
serialVersionUID: 1L
serialVersionUID: 1L
lits
ILits lits
tmp
IVec<T> tmp
solver
UnitPropagationListener solver
learner
Learner learner
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
Package org.sat4j.minisat.constraints.card |
serialVersionUID: 1L
maxUnsatisfied
int maxUnsatisfied
- number of allowed falsified literal
counter
int counter
- current number of falsified literals
lits
int[] lits
- constraint literals
voc
ILits voc
serialVersionUID: 1L
degree
int degree
- Degr? de la contrainte de cardinalit?
lits
int[] lits
- Liste des litt?raux de la contrainte
moreThan
boolean moreThan
- D?termine si c'est une in?galit? sup?rieure ou ?gale
watchCumul
int watchCumul
- Somme des coefficients des litt?raux observ?s
voc
ILits voc
- Vocabulaire de la contrainte
serialVersionUID: 1L
degree
int degree
- degree of the cardinality constraint
lits
int[] lits
- literals involved in the constraint
moreThan
boolean moreThan
- contains the sign of the constraint : ATLEAT or ATMOST
watchCumul
int watchCumul
- contains the sum of the coefficients of the watched literals
voc
ILits voc
- Vocabulary of the constraint
Package org.sat4j.minisat.constraints.cnf |
serialVersionUID: 1L
activity
double activity
voc
ILits voc
head
int head
tail
int tail
serialVersionUID: 1L
falsified
int falsified
learnt
boolean learnt
lits
int[] lits
voc
ILits voc
activity
double activity
serialVersionUID: 1L
activity
double activity
middleLits
int[] middleLits
voc
ILits voc
head
int head
tail
int tail
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
pool
boolean[] pool
realnVars
int realnVars
watches
IVec<T>[] watches
level
int[] level
reason
Constr[] reason
maxvarid
int maxvarid
undos
IVec<T>[] undos
falsified
boolean[] falsified
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
activity
double activity
- Since:
- 2.1
lits
int[] lits
voc
ILits voc
Package org.sat4j.minisat.core |
serialVersionUID: 1L
heap
IVecInt heap
indices
IVecInt indices
activity
double[] activity
serialVersionUID: 1L
myarray
int[] myarray
size
int size
first
int first
serialVersionUID: 1L
backtrackLevel
int backtrackLevel
reason
Constr reason
serialVersionUID: 1L
claDecay
double claDecay
varDecay
double varDecay
conflictBoundIncFactor
double conflictBoundIncFactor
initConflictBound
int initConflictBound
serialVersionUID: 1L
constrs
IVec<T> constrs
- Set of original constraints.
learnts
IVec<T> learnts
- Set of learned constraints.
claInc
double claInc
- incr?ment pour l'activit? des clauses.
claDecay
double claDecay
- decay factor pour l'activit? des clauses.
qhead
int qhead
- Queue de propagation
trail
IVecInt trail
- affectation en ordre chronologique
trailLim
IVecInt trailLim
- indice des s?parateurs des diff?rents niveau de d?cision dans trail
rootLevel
int rootLevel
- S?pare les hypoth?ses incr?mentale et recherche
model
int[] model
voc
ILits voc
order
IOrder order
comparator
org.sat4j.minisat.core.ActivityComparator comparator
stats
SolverStats stats
learner
LearningStrategy<D extends DataStructureFactory> learner
analyzer
AssertingClauseGenerator analyzer
undertimeout
boolean undertimeout
timeout
long timeout
timeBasedTimeout
boolean timeBasedTimeout
dsfactory
DataStructureFactory dsfactory
params
SearchParams params
__dimacs_out
IVecInt __dimacs_out
slistener
SearchListener slistener
restarter
RestartStrategy restarter
constrTypes
Map<K,V> constrTypes
isDBSimplificationAllowed
boolean isDBSimplificationAllowed
learnedLiterals
IVecInt learnedLiterals
verbose
boolean verbose
prefix
String prefix
mseen
boolean[] mseen
mpreason
IVecInt mpreason
moutLearnt
IVecInt moutLearnt
SIMPLE_SIMPLIFICATION
org.sat4j.minisat.core.Solver.ISimplifier SIMPLE_SIMPLIFICATION
EXPENSIVE_SIMPLIFICATION
org.sat4j.minisat.core.Solver.ISimplifier EXPENSIVE_SIMPLIFICATION
simplifier
org.sat4j.minisat.core.Solver.ISimplifier simplifier
analyzetoclear
IVecInt analyzetoclear
analyzestack
IVecInt analyzestack
analysisResult
Pair analysisResult
fullmodel
boolean[] fullmodel
unsatExplanationInTermsOfAssumptions
IVecInt unsatExplanationInTermsOfAssumptions
timebegin
double timebegin
needToReduceDB
boolean needToReduceDB
conflictCount
org.sat4j.minisat.core.ConflictTimer conflictCount
memory_based
org.sat4j.minisat.core.Solver.LearnedConstraintsDeletionStrategy memory_based
- Since:
- 2.1
glucose
org.sat4j.minisat.core.Solver.LearnedConstraintsDeletionStrategy glucose
- Since:
- 2.1
learnedConstraintsDeletionStrategy
org.sat4j.minisat.core.Solver.LearnedConstraintsDeletionStrategy learnedConstraintsDeletionStrategy
serialVersionUID: 1L
starts
int starts
decisions
long decisions
propagations
long propagations
inspects
long inspects
conflicts
long conflicts
learnedliterals
long learnedliterals
learnedbinaryclauses
long learnedbinaryclauses
learnedternaryclauses
long learnedternaryclauses
learnedclauses
long learnedclauses
ignoredclauses
long ignoredclauses
rootSimplifications
long rootSimplifications
reducedliterals
long reducedliterals
changedreason
long changedreason
reduceddb
int reduceddb
Package org.sat4j.minisat.learning |
serialVersionUID: 1L
percent
double percent
order
IOrder order
maxpercent
int maxpercent
serialVersionUID: 1L
serialVersionUID: 1L
maxlength
int maxlength
bound
int bound
serialVersionUID: 1L
none
NoLearningButHeuristics<D extends DataStructureFactory> none
all
MiniSATLearning<D extends DataStructureFactory> all
lits
ILits lits
stats
SolverStats stats
serialVersionUID: 1L
dsf
DataStructureFactory dsf
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
maxpercent
int maxpercent
bound
int bound
Package org.sat4j.minisat.orders |
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
period
int period
cpt
int cpt
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
activity
double[] activity
- mesure heuristique de l'activite d'une variable.
varDecay
double varDecay
varInc
double varInc
- increment pour l'activite des variables.
lits
ILits lits
nullchoice
long nullchoice
heap
Heap heap
phaseStrategy
IPhaseSelectionStrategy phaseStrategy
Package org.sat4j.minisat.restarts |
serialVersionUID: 1L
inner
double inner
outer
double outer
conflicts
long conflicts
params
SearchParams params
serialVersionUID: 1L
factor
int factor
count
int count
serialVersionUID: 1L
nofConflicts
double nofConflicts
params
SearchParams params
serialVersionUID: 1L
Package org.sat4j.minisat.uip |
serialVersionUID: 1L
serialVersionUID: 1L
counter
int counter
Package org.sat4j.multicore |
serialVersionUID: 1L
availableSolvers
String[] availableSolvers
solvers
List<E> solvers
numberOfSolvers
int numberOfSolvers
winnerId
int winnerId
resultFound
boolean resultFound
remainingSolvers
int remainingSolvers
solved
boolean solved
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
nborigvars
int nborigvars
nbexpectedclauses
int nbexpectedclauses
nbnewvar
int nbnewvar
prevfullmodel
int[] prevfullmodel
prevmodel
int[] prevmodel
- Since:
- 2.1
prevboolmodel
boolean[] prevboolmodel
- Since:
- 2.1
serialVersionUID: 1L
lits
IVecInt lits
counter
int counter
prevConstr
IConstr prevConstr
serialVersionUID: 1L
prevmodel
int[] prevmodel
counter
int counter
literals
IVecInt literals
previousConstr
IConstr previousConstr
serialVersionUID: 1L
factory
ASolverFactory<T extends ISolver> factory
obfct
ObjectiveFunction obfct
serialVersionUID: 1L
serialVersionUID: 1L
quickxplain
XplainPB quickxplain
serialVersionUID: 1L
coeffs
IVec<T> coeffs
vars
IVecInt vars
serialVersionUID: 1L
indxConstrObj
int indxConstrObj
nbOfConstraints
int nbOfConstraints
obj
ObjectiveFunction obj
inserted
boolean inserted
serialVersionUID: 1L
problem
IOptimizationProblem problem
modelComputed
boolean modelComputed
assumps
IVecInt assumps
begin
long begin
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
objfct
ObjectiveFunction objfct
objectiveValue
BigInteger objectiveValue
prevmodel
int[] prevmodel
prevfullmodel
boolean[] prevfullmodel
previousPBConstr
IConstr previousPBConstr
serialVersionUID: 1L
serialVersionUID: 1L
indxConstrObj
int indxConstrObj
nbOfConstraints
int nbOfConstraints
obj
ObjectiveFunction obj
inserted
boolean inserted
mapping
Map<K,V> mapping
Package org.sat4j.pb.constraints |
serialVersionUID: 1L
serialVersionUID: 1L
norm
org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer norm
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
Package org.sat4j.pb.constraints.pb |
serialVersionUID: 1L
degree
BigInteger degree
learnt
boolean learnt
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
watchCumul
BigInteger watchCumul
- sum of the coefficients of the literals satisfied or unvalued
serialVersionUID: 1L
bigDegree
BigInteger bigDegree
learnt
boolean learnt
serialVersionUID: 1L
watchCumul
BigInteger watchCumul
- sum of the coefficients of the literals satisfied or unvalued
watched
boolean[] watched
- is the literal of index i watching the constraint ?
watching
int[] watching
- indexes of literals watching the constraint
watchingCount
int watchingCount
- number of literals watching the constraint.
This is the real size of the array watching
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
activity
double activity
- constraint activity
coefs
BigInteger[] coefs
- coefficients of the literals of the constraint
degree
BigInteger degree
- degree of the pseudo-boolean constraint
lits
int[] lits
- literals of the constraint
learnt
boolean learnt
- true if the constraint is a learned constraint
voc
ILits voc
- constraint's vocabulary
Package org.sat4j.pb.core |
serialVersionUID: 1L
objf
ObjectiveFunction objf
stats
PBSolverStats stats
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
conflictVariables
IVec<T> conflictVariables
conflictConstraints
IVec<T> conflictConstraints
serialVersionUID: 1L
serialVersionUID: 1L
bound
long bound
serialVersionUID: 1L
serialVersionUID: 1L
numberOfReductions
long numberOfReductions
numberOfLearnedConstraintsReduced
long numberOfLearnedConstraintsReduced
numberOfResolution
long numberOfResolution
numberOfCP
long numberOfCP
serialVersionUID: 1L
Package org.sat4j.pb.orders |
serialVersionUID: 1L
obj
ObjectiveFunction obj
Package org.sat4j.pb.reader |
serialVersionUID: 1L
varExplain
IVecInt varExplain
serialVersionUID: 1L
solver
IPBSolver solver
lits
IVecInt lits
coeffs
IVec<T> coeffs
d
BigInteger d
operator
String operator
objectiveVars
IVecInt objectiveVars
objectiveCoeffs
IVec<T> objectiveCoeffs
hasObjFunc
boolean hasObjFunc
hasVariablesExplanation
boolean hasVariablesExplanation
nbVars
int nbVars
nbConstr
int nbConstr
nbConstraintsRead
int nbConstraintsRead
savedChar
char savedChar
charAvailable
boolean charAvailable
eofReached
boolean eofReached
eolReached
boolean eolReached
serialVersionUID: 1L
serialVersionUID: 1L
nbNewSymbols
int nbNewSymbols
- contains the number of new symbols generated to linearize products
varToProduct
Map<K,V> varToProduct
binaryProductToVar
Map<K,V> binaryProductToVar
serialVersionUID: 1L
isWbo
boolean isWbo
softLimit
BigInteger softLimit
softConstraint
boolean softConstraint
Package org.sat4j.pb.tools |
serialVersionUID: 1L
filename
String filename
out
PrintStream out
index
long index
serialVersionUID: 1L
serialVersionUID: 1L
expectedNbOfConstr
int expectedNbOfConstr
solver
ISolver solver
checkConstrNb
boolean checkConstrNb
formatString
String formatString
scanner
EfficientScanner scanner
- Since:
- 2.1
literals
IVecInt literals
- Since:
- 2.1
serialVersionUID: 1L
commentChar
char commentChar
serialVersionUID: 1L
s
ISolver s
nbVars
int nbVars
nbClauses
int nbClauses
serialVersionUID: 1L
serialVersionUID: 1L
factory
ASolverFactory<T extends ISolver> factory
filename
String filename
k
int k
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
filename
String filename
out
PrintStream out
serialVersionUID: 1L
filename
String filename
out
PrintStream out
serialVersionUID: 1L
filename
String filename
out
PrintStream out
serialVersionUID: 1L
solver
ISolver solver
serialVersionUID: 1L
readObject
private void readObject(ObjectInputStream stream)
nbvars
int nbvars
nbclauses
int nbclauses
fixedNbClauses
boolean fixedNbClauses
firstConstr
boolean firstConstr
serialVersionUID: 1L
out
StringBuffer out
nbvars
int nbvars
nbclauses
int nbclauses
fixedNbClauses
boolean fixedNbClauses
firstConstr
boolean firstConstr
firstCharPos
int firstCharPos
initBuilderSize
int initBuilderSize
maxvarid
int maxvarid
serialVersionUID: 1L
readObject
private void readObject(ObjectInputStream stream)
throws IOException,
ClassNotFoundException
- Throws:
IOException
ClassNotFoundException
pile
Vec<T> pile
currentNodeName
String currentNodeName
estOrange
boolean estOrange
mapping
Map<K,V> mapping
serialVersionUID: 1L
gater
GateTranslator gater
serialVersionUID: 1L
serialVersionUID: 1L
filename
String filename
out
PrintStream out
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
trivialfalsity
boolean trivialfalsity
bound
int bound
nbModelFound
int nbModelFound
serialVersionUID: 1L
problem
IOptimizationProblem problem
modelComputed
boolean modelComputed
optimalValueForced
boolean optimalValueForced
serialVersionUID: 1L
serialVersionUID: 1L
lowerBound
int lowerBound
serialVersionUID: 1L
solver
ISolver solver
serialVersionUID: 1L
mapping
Map<K,V> mapping
Package org.sat4j.tools.xplain |
serialVersionUID: 1L
constrs
Map<K,V> constrs
assump
IVecInt assump
lastCreatedVar
int lastCreatedVar
pooledVarId
boolean pooledVarId
lastClause
IVecInt lastClause
Copyright © 2010 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.