|
||||||||||
PREV PACKAGE NEXT PACKAGE | FRAMES NO FRAMES |
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. |
Tools to be used on top of an ISolver.
|
||||||||||
PREV PACKAGE NEXT PACKAGE | FRAMES NO FRAMES |