Serialized Form
readObject
private void readObject(java.io.ObjectInputStream stream)
throws java.io.IOException,
java.lang.ClassNotFoundException
- Throws:
java.io.IOException
java.lang.ClassNotFoundException
beginTime
long beginTime
exitCode
ExitCode exitCode
reader
Reader reader
solver
ISolver solver
silent
boolean silent
serialVersionUID: 1L
serialVersionUID: 1L
factory
ASolverFactory<T extends ISolver> factory
filename
java.lang.String filename
serialVersionUID: 1L
serialVersionUID: 1L
nbelem
int nbelem
myarray
java.lang.Object[] myarray
serialVersionUID: 1L
nbelem
int nbelem
myarray
int[] myarray
Package org.sat4j.minisat |
serialVersionUID: 1L
Package org.sat4j.minisat.constraints |
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
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
voc
ILits voc
clauses
IVecInt clauses
reason
int reason
conflictindex
int conflictindex
serialVersionUID: 1L
falsified
int falsified
learnt
boolean learnt
lits
int[] lits
voc
ILits voc
activity
double activity
serialVersionUID: 1L
learnt
boolean learnt
serialVersionUID: 1L
serialVersionUID: 1L
pool
boolean[] pool
realnVars
int realnVars
watches
IVec<T>[] watches
level
int[] level
reason
Constr[] reason
undos
IVec<T>[] undos
falsified
boolean[] falsified
serialVersionUID: 1L
binclauses
BinaryClauses[] binclauses
serialVersionUID: 1L
ternclauses
TernaryClauses[] ternclauses
serialVersionUID: 1L
marks
int[] marks
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
stubs
IVecInt stubs
voc
ILits voc
phead
int phead
serialVersionUID: 1L
activity
double activity
lits
int[] lits
voc
ILits voc
Package org.sat4j.minisat.core |
serialVersionUID: 1L
readObject
private void readObject(java.io.ObjectInputStream stream)
throws java.io.IOException,
java.lang.ClassNotFoundException
- Throws:
java.io.IOException
java.lang.ClassNotFoundException
pile
Vec<T> pile
currentNodeName
java.lang.String currentNodeName
estOrange
boolean estOrange
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
- List des contraintes du probl?me.
learnts
IVec<T> learnts
- Liste des clauses apprises.
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<L extends ILits> order
comparator
org.sat4j.minisat.core.ActivityComparator comparator
stats
SolverStats stats
learner
LearningStrategy<L extends ILits,D extends DataStructureFactory<L>> learner
analyzer
AssertingClauseGenerator analyzer
undertimeout
boolean undertimeout
timeout
long timeout
timeBasedTimeout
boolean timeBasedTimeout
dsfactory
DataStructureFactory<L extends ILits> dsfactory
params
SearchParams params
__dimacs_out
IVecInt __dimacs_out
slistener
SearchListener slistener
restarter
RestartStrategy restarter
constrTypes
java.util.Map<K,V> constrTypes
mseen
boolean[] mseen
preason
IVecInt preason
outLearnt
IVecInt outLearnt
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
timebegin
double timebegin
needToReduceDB
boolean needToReduceDB
conflictCount
org.sat4j.minisat.core.ConflictTimer conflictCount
timer
java.util.Timer timer
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
serialVersionUID: 1L
Package org.sat4j.minisat.learning |
serialVersionUID: 1L
percent
double percent
order
IOrder<L extends ILits> order
maxpercent
int maxpercent
serialVersionUID: 1L
serialVersionUID: 1L
maxlength
int maxlength
bound
int bound
serialVersionUID: 1L
none
NoLearningButHeuristics<L extends ILits,D extends DataStructureFactory<L>> none
all
MiniSATLearning<L extends ILits,D extends DataStructureFactory<L>> all
lits
ILits lits
stats
SolverStats stats
serialVersionUID: 1L
dsf
DataStructureFactory<L extends ILits> 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
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.
lastVar
int lastVar
- Derniere variable choisie
order
int[] order
- Ordre des variables
varDecay
double varDecay
varInc
double varInc
- increment pour l'activite des variables.
varpos
int[] varpos
- position des variables
lits
ILits lits
nullchoice
long nullchoice
phaseStrategy
IPhaseSelectionStrategy phaseStrategy
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
Package org.sat4j.minisat.uip |
serialVersionUID: 1L
serialVersionUID: 1L
counter
int counter
nborigvars
int nborigvars
nbexpectedclauses
int nbexpectedclauses
nbnewvar
int nbnewvar
prevfullmodel
int[] prevfullmodel
serialVersionUID: 1L
lits
IVecInt lits
counter
int counter
serialVersionUID: 1L
prevmodel
int[] prevmodel
counter
int counter
literals
IVecInt literals
serialVersionUID: 3258130241376368435L
serialVersionUID: 1L
expectedNbOfConstr
int expectedNbOfConstr
solver
ISolver solver
checkConstrNb
boolean checkConstrNb
formatString
java.lang.String formatString
serialVersionUID: 1L
serialVersionUID: 1L
s
ISolver s
nbLit
int nbLit
nbClauses
int nbClauses
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
solver
ISolver solver
serialVersionUID: 1L
readObject
private void readObject(java.io.ObjectInputStream stream)
nbvars
int nbvars
nbclauses
int nbclauses
fixedNbClauses
boolean fixedNbClauses
firstConstr
boolean firstConstr
serialVersionUID: 1L
out
java.lang.StringBuffer out
nbvars
int nbvars
nbclauses
int nbclauses
fixedNbClauses
boolean fixedNbClauses
firstConstr
boolean firstConstr
firstCharPos
int firstCharPos
initBuilderSize
int initBuilderSize
serialVersionUID: 1L
gater
GateTranslator gater
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
trivialfalsity
boolean trivialfalsity
serialVersionUID: 1L
problem
IOptimizationProblem problem
modelComputed
boolean modelComputed
serialVersionUID: 1L
serialVersionUID: 1L
solver
ISolver solver