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.



Copyright © 2010 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.