Serialized Form
serialVersionUID: 1L
readObject
private void readObject(ObjectInputStream stream)
throws IOException,
ClassNotFoundException
- Throws:
IOException
ClassNotFoundException
beginTime
long beginTime
exitCode
ExitCode exitCode
reader
Reader reader
solver
ISolver solver
silent
boolean silent
prime
boolean prime
serialVersionUID: 1L
incomplete
boolean incomplete
displaySolutionLine
boolean displaySolutionLine
serialVersionUID: 1L
factory
ASolverFactory<T extends ISolver> factory
serialVersionUID: 1460304168178023681L
serialVersionUID: 1L
mus
int[] mus
xplain
Explainer xplain
highLevel
boolean highLevel
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
vec
IVec<T> vec
serialVersionUID: 1L
vec
IVecInt vec
serialVersionUID: 1L
nbelem
int nbelem
myarray
Object[] myarray
serialVersionUID: 1L
nbelem
int nbelem
myarray
int[] myarray
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
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
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
activity
double activity
- Since:
- 2.1
lits
int[] lits
voc
ILits voc
Package org.sat4j.minisat.core |
serialVersionUID: 1L
serialVersionUID: 1L
counter
int counter
bound
int bound
serialVersionUID: 1L
timers
IVec<T> timers
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
out
ICDCLLogger out
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
ActivityComparator comparator
stats
SolverStats stats
learner
LearningStrategy<D extends DataStructureFactory> learner
undertimeout
boolean undertimeout
timeout
long timeout
timeBasedTimeout
boolean timeBasedTimeout
dsfactory
DataStructureFactory dsfactory
params
SearchParams params
__dimacs_out
IVecInt __dimacs_out
slistener
SearchListener<S extends ISolverService> slistener
restarter
RestartStrategy restarter
constrTypes
Map<K,V> constrTypes
isDBSimplificationAllowed
boolean isDBSimplificationAllowed
learnedLiterals
IVecInt learnedLiterals
verbose
boolean verbose
keepHot
boolean keepHot
prefix
String prefix
declaredMaxVarId
int declaredMaxVarId
mseen
boolean[] mseen
mpreason
IVecInt mpreason
moutLearnt
IVecInt moutLearnt
SIMPLE_SIMPLIFICATION
ISimplifier SIMPLE_SIMPLIFICATION
EXPENSIVE_SIMPLIFICATION
ISimplifier EXPENSIVE_SIMPLIFICATION
EXPENSIVE_SIMPLIFICATION_WLONLY
ISimplifier EXPENSIVE_SIMPLIFICATION_WLONLY
simplifier
ISimplifier simplifier
analyzetoclear
IVecInt analyzetoclear
analyzestack
IVecInt analyzestack
watched
IVec<T> watched
analysisResult
Pair analysisResult
userbooleanmodel
boolean[] userbooleanmodel
unsatExplanationInTermsOfAssumptions
IVecInt unsatExplanationInTermsOfAssumptions
implied
IVecInt implied
decisions
IVecInt decisions
fullmodel
int[] fullmodel
prime
int[] prime
timebegin
double timebegin
needToReduceDB
boolean needToReduceDB
conflictCount
ConflictTimerContainer conflictCount
memoryTimer
ConflictTimer memoryTimer
memory_based
LearnedConstraintsDeletionStrategy memory_based
- Since:
- 2.1
lbdTimer
ConflictTimer lbdTimer
glucose
LearnedConstraintsDeletionStrategy glucose
- Since:
- 2.1
learnedConstraintsDeletionStrategy
LearnedConstraintsDeletionStrategy learnedConstraintsDeletionStrategy
lastConflictMeansUnsat
boolean lastConflictMeansUnsat
sharedConflict
Constr sharedConflict
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
shortcuts
int shortcuts
updateLBD
long updateLBD
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
varsToTest
int[] varsToTest
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
conflictcount
long conflictcount
serialVersionUID: 1L
un
int un
vn
int vn
factor
int factor
bound
int bound
conflictcount
int conflictcount
serialVersionUID: 1L
nofConflicts
double nofConflicts
params
SearchParams params
conflictcount
int conflictcount
serialVersionUID: 1L
serialVersionUID: 1L
nbexpectedclauses
int nbexpectedclauses
prevfullmodel
int[] prevfullmodel
prevmodel
int[] prevmodel
- Since:
- 2.1
prevboolmodel
boolean[] prevboolmodel
- Since:
- 2.1
isSolutionOptimal
boolean isSolutionOptimal
serialVersionUID: 1L
equivalence
boolean equivalence
lits
IVecInt lits
counter
int counter
prevConstr
IConstr prevConstr
serialVersionUID: 1L
prevmodel
int[] prevmodel
isSolutionOptimal
boolean isSolutionOptimal
counter
int counter
literals
IVecInt literals
previousConstr
IConstr previousConstr
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
numberOfComponents
int numberOfComponents
hlxplain
HighLevelXplain<T extends ISolver> hlxplain
currentComponentIndex
int currentComponentIndex
serialVersionUID: 1L
s
ISolver s
nbVars
int nbVars
nbClauses
int nbClauses
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
nbvars
int nbvars
nbclauses
int nbclauses
fixedNbClauses
boolean fixedNbClauses
firstConstr
boolean firstConstr
serialVersionUID: 1L
encodingAdapter
EncodingStrategyAdapter encodingAdapter
serialVersionUID: 1L
counter
int counter
nVar
int nVar
conflictDepthVisu
IVisualizationTool conflictDepthVisu
conflictDepthRestartVisu
IVisualizationTool conflictDepthRestartVisu
conflictDepthCleanVisu
IVisualizationTool conflictDepthCleanVisu
serialVersionUID: 1L
counter
int counter
nVar
int nVar
maxDLevel
int maxDLevel
visuTool
IVisualizationTool visuTool
restartVisuTool
IVisualizationTool restartVisuTool
cleanTool
IVisualizationTool cleanTool
serialVersionUID: 1L
counter
int counter
visuTool
IVisualizationTool visuTool
serialVersionUID: 1L
counter
int counter
positiveVisu
IVisualizationTool positiveVisu
negativeVisu
IVisualizationTool negativeVisu
restartVisu
IVisualizationTool restartVisu
cleanVisu
IVisualizationTool cleanVisu
nVar
int nVar
serialVersionUID: 1L
solver
ISolver solver
serialVersionUID: 1L
readObject
private void readObject(ObjectInputStream stream)
serialVersionUID: 1L
out
StringBuffer out
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
solverService
ISolverService solverService
visuTool
IVisualizationTool visuTool
serialVersionUID: 1L
visuTool
IVisualizationTool visuTool
counter
int counter
serialVersionUID: 1L
visuTool
IVisualizationTool visuTool
counter
int counter
serialVersionUID: 1L
visuTool
IVisualizationTool visuTool
restartTool
IVisualizationTool restartTool
cleanTool
IVisualizationTool cleanTool
counter
int counter
maxSize
int maxSize
serialVersionUID: 1L
solverService
ISolverService solverService
visuTool
IVisualizationTool visuTool
serialVersionUID: 1L
criteria
List<E> criteria
currentCriterion
int currentCriterion
prevConstr
IConstr prevConstr
currentValue
Number currentValue
prevfullmodel
int[] prevfullmodel
prevboolmodel
boolean[] prevboolmodel
isSolutionOptimal
boolean isSolutionOptimal
serialVersionUID: 1L
availableSolvers
String[] availableSolvers
solvers
List<E> solvers
numberOfSolvers
int numberOfSolvers
winnerId
int winnerId
resultFound
boolean resultFound
remainingSolvers
int remainingSolvers
sleepTime
int sleepTime
solved
boolean solved
solversStats
IVec<T> solversStats
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
trivialfalsity
boolean trivialfalsity
bound
long bound
nbModelFound
long nbModelFound
serialVersionUID: 1L
listeners
Collection<E> listeners
serialVersionUID: 1L
problem
IOptimizationProblem problem
modelComputed
boolean modelComputed
optimalValueForced
boolean optimalValueForced
serialVersionUID: 1L
solverService
ISolverService solverService
nbsolutions
int nbsolutions
serialVersionUID: 1L
serialVersionUID: 1L
serialVersionUID: 1L
lowerBound
int lowerBound
serialVersionUID: 1L
solver
ISolver solver
serialVersionUID: 1L
visuTool
IVisualizationTool visuTool
cleanVisuTool
IVisualizationTool cleanVisuTool
restartVisuTool
IVisualizationTool restartVisuTool
begin
long begin
end
long end
counter
int counter
index
long index
nVar
int nVar
maxY
double maxY
serialVersionUID: 1L
mapping
Map<K,V> mapping
Package org.sat4j.tools.xplain |
serialVersionUID: 1L
computationCanceled
boolean computationCanceled
serialVersionUID: 1L
constrs
Map<K,V> constrs
assump
IVecInt assump
lastCreatedVar
int lastCreatedVar
pooledVarId
boolean pooledVarId
xplainStrategy
MinimizationStrategy xplainStrategy
highLevelToVar
Map<K,V> highLevelToVar
serialVersionUID: 1L
computationCanceled
boolean computationCanceled
serialVersionUID: 1L
computationCanceled
boolean computationCanceled
serialVersionUID: 1L
computationCanceled
boolean computationCanceled
serialVersionUID: 1L
constrs
Map<K,V> constrs
assump
IVecInt assump
lastCreatedVar
int lastCreatedVar
pooledVarId
boolean pooledVarId
lastClause
IVecInt lastClause
lastConstr
IConstr lastConstr
skipDuplicatedEntries
boolean skipDuplicatedEntries
xplainStrategy
MinimizationStrategy xplainStrategy
Copyright © 2012 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.