| Interface | Description |
|---|---|
| IVisualizationTool | |
| OutcomeListener |
Simple interface to check the outcome of running a solver in parallel.
|
| SolutionFoundListener |
Allows the end user to react when a new solution is found.
|
| Class | Description |
|---|---|
| AbstractClauseSelectorSolver<T extends ISolver> | |
| AbstractMinimalModel | |
| AbstractOutputSolver | |
| AllMUSes |
This is a tool for computing all the MUSes (Minimum Unsatisfiable Sets) of a
set of clauses.
|
| Backbone |
The aim of this class is to compute efficiently the literals implied by the
set of constraints (also called backbone or unit implicates).
|
| CheckMUSSolutionListener | |
| 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 | |
| FullClauseSelectorSolver<T extends ISolver> | |
| GateTranslator |
Utility class to easily feed a SAT solver using logical gates.
|
| GroupClauseSelectorSolver<T extends ISolver> | |
| 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.
|
| ModelIteratorToSATAdapter |
This class allow to use the ModelIterator class as a solver.
|
| MultiTracing<T extends ISolverService> |
Allow to feed the solver with several SearchListener.
|
| NegationDecorator<T extends ISolver> |
Negates the formula inside a solver.
|
| OptToSatAdapter | |
| RemiUtils |
Class dedicated to Remi Coletta utility methods :-)
|
| RupSearchListener<S extends ISolverService> |
Output an unsat proof using the reverse unit propagation (RUP) format.
|
| 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> | |
| SearchMinOneListener |
That class allows to iterate over the models from the inside: conflicts are
created to ask the solver to backtrack.
|
| 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 | |
| StatisticsSolver | |
| TextOutputTracing<T> |
Debugging Search Listener allowing to follow the search in a textual way.
|
ISolver.Copyright © 2013 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.