Package | Description |
---|---|
org.sat4j.minisat.core | |
org.sat4j.pb.core | |
org.sat4j.pb.tools | |
org.sat4j.specs | |
org.sat4j.tools |
Modifier and Type | Field and Description |
---|---|
protected SearchListener |
Solver.slistener |
Modifier and Type | Method and Description |
---|---|
<S extends ISolverService> |
Solver.getSearchListener() |
Modifier and Type | Method and Description |
---|---|
<S extends ISolverService> |
Solver.setSearchListener(SearchListener<S> sl) |
Modifier and Type | Method and Description |
---|---|
<S extends ISolverService> |
ObjectiveReducerPBSolverDecorator.getSearchListener() |
Modifier and Type | Method and Description |
---|---|
<S extends ISolverService> |
ObjectiveReducerPBSolverDecorator.setSearchListener(SearchListener<S> sl) |
Modifier and Type | Class and Description |
---|---|
class |
ConflictTracing |
class |
ManyCorePB |
class |
SearchOptimizerListener |
Modifier and Type | Method and Description |
---|---|
<S extends ISolverService> |
ISolver.getSearchListener()
Get the current SearchListener.
|
Modifier and Type | Method and Description |
---|---|
<S extends ISolverService> |
ISolver.setSearchListener(SearchListener<S> sl)
Allow the user to hook a listener to the solver to be notified of the
main steps of the search process.
|
Modifier and Type | Class and Description |
---|---|
class |
ConflictDepthTracing |
class |
ConflictLevelTracing |
class |
DecisionLevelTracing |
class |
DecisionTracing |
class |
DotSearchTracing<T>
Class allowing to express the search as a tree in the dot language.
|
class |
HeuristicsTracing |
class |
LBDTracing |
class |
LearnedClauseSizeTracing |
class |
LearnedClausesSizeTracing |
class |
LearnedTracing |
class |
ManyCore<S extends ISolver>
A class allowing to run several solvers in parallel.
|
class |
MultiTracing<T extends ISolverService>
Allow to feed the solver with several SearchListener.
|
class |
RupSearchListener<S extends ISolverService>
Output an unsat proof using the reverse unit propagation (RUP) format.
|
class |
SearchEnumeratorListener
That class allows to iterate over the models from the inside: conflicts are
created to ask the solver to backtrack.
|
class |
SearchListenerAdapter<S extends ISolverService> |
class |
SearchMinOneListener
That class allows to iterate over the models from the inside: conflicts are
created to ask the solver to backtrack.
|
class |
SpeedTracing |
class |
TextOutputTracing<T>
Debugging Search Listener allowing to follow the search in a textual way.
|
Modifier and Type | Method and Description |
---|---|
<I extends ISolverService> |
ManyCore.getSearchListener() |
<S extends ISolverService> |
AbstractOutputSolver.getSearchListener() |
<S extends ISolverService> |
SolverDecorator.getSearchListener() |
<S extends ISolverService> |
StatisticsSolver.getSearchListener() |
Modifier and Type | Method and Description |
---|---|
<I extends ISolverService> |
ManyCore.setSearchListener(SearchListener<I> sl) |
<S extends ISolverService> |
AbstractOutputSolver.setSearchListener(SearchListener<S> sl) |
<S extends ISolverService> |
SolverDecorator.setSearchListener(SearchListener<S> sl) |
<S extends ISolverService> |
StatisticsSolver.setSearchListener(SearchListener<S> sl) |
Constructor and Description |
---|
MultiTracing(SearchListener<T>... listeners) |
Constructor and Description |
---|
MultiTracing(java.util.List<SearchListener<T>> listenersList) |