Package org.sat4j.tools

Tools to be used on top of an ISolver.

See:
Description

Interface Summary

IVisualizationTool
OutcomeListener	Simple interface to check the outcome of running a solver in parallel.

Class Summary

AbstractOutputSolver
ClausalCardinalitiesDecorator<T extends ISolver>	A decorator for clausal cardinalities constraints.
ConflictDepthTracing
ConflictLevelTracing
DecisionLevelTracing
DecisionTracing
DimacsArrayReader	Very simple Dimacs array reader.
DimacsOutputSolver	Solver used to display in a writer the CNF instance in Dimacs format.
DimacsStringSolver	Solver used to write down a CNF into a String.
DotSearchTracing<T>	Class allowing to express the search as a tree in the dot language.
ExtendedDimacsArrayReader	Reader for the Extended Dimacs format proposed by Fahiem Bacchus and Toby Walsh in array representation (without the terminating 0).
FileBasedVisualizationTool
GateTranslator	Utility class to easily feed a SAT solver using logical gates.
HeuristicsTracing
LBDTracing
LearnedClauseSizeTracing
LearnedClausesSizeTracing
LearnedTracing
LexicoDecorator<T extends ISolver>
ManyCore<S extends ISolver>	A class allowing to run several solvers in parallel.
Minimal4CardinalityModel	Computes models with a minimal number (with respect to cardinality) of negative literals.
Minimal4InclusionModel	Computes models with a minimal subset (with respect to set inclusion) of negative literals.
ModelIterator	That class allows to iterate through all the models (implicants) of a formula.
MultiTracing	Allow to feed the solver with several SearchListener.
OptToSatAdapter
RemiUtils	Class dedicated to Remi Coletta utility methods :-)
SearchEnumeratorListener	That class allows to iterate over the models from the inside: conflicts are created to ask the solver to backtrack.
SearchListenerAdapter<S extends ISolverService>
SingleSolutionDetector	This solver decorator allows to detect whether or not the set of constraints available in the solver has only one solution or not.
SolutionCounter	Another solver decorator that counts the number of solutions.
SolverDecorator<T extends ISolver>	The aim of that class is to allow adding dynamic responsibilities to SAT solvers using the Decorator design pattern.
SpeedTracing
TextOutputTracing<T>	Debugging Search Listener allowing to follow the search in a textual way.

Package org.sat4j.tools Description

Tools to be used on top of an ISolver.