Package org.sat4j.tools

Tools to be used on top of an ISolver.

See:
Description

Class Summary

ConflictLevelTracing
ConstrGroup	A utility class used to manage easily group of clauses to be deleted at some point in the solver.
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).
GateTranslator	Utility class to easily feed a SAT solver using logical gates.
LearnedClauseSizeTracing
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.
OptToSatAdapter
RemiUtils	Class dedicated to Remi Coletta utility methods :-)
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 responsabilities to SAT solvers using the Decorator design pattern.
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.