| Package | Description |
|---|---|
| org.sat4j | |
| org.sat4j.opt | |
| org.sat4j.pb | |
| org.sat4j.pb.tools | |
| org.sat4j.tools | |
| org.sat4j.tools.xplain |
| Class and Description |
|---|
| SolutionFoundListener
Allows the end user to react when a new solution is found.
|
| Class and Description |
|---|
| SolverDecorator
The aim of that class is to allow adding dynamic responsibilities to SAT
solvers using the Decorator design pattern.
|
| Class and Description |
|---|
| AbstractOutputSolver |
| DimacsStringSolver
Solver used to write down a CNF into a String.
|
| SolutionFoundListener
Allows the end user to react when a new solution is found.
|
| SolverDecorator
The aim of that class is to allow adding dynamic responsibilities to SAT
solvers using the Decorator design pattern.
|
| Class and Description |
|---|
| AbstractClauseSelectorSolver |
| ClausalCardinalitiesDecorator
A decorator for clausal cardinalities constraints.
|
| FullClauseSelectorSolver |
| LexicoDecorator |
| ManyCore
A class allowing to run several solvers in parallel.
|
| OutcomeListener
Simple interface to check the outcome of running a solver in parallel.
|
| SearchListenerAdapter |
| SolutionFoundListener
Allows the end user to react when a new solution is found.
|
| SolverDecorator
The aim of that class is to allow adding dynamic responsibilities to SAT
solvers using the Decorator design pattern.
|
| Class and Description |
|---|
| AbstractClauseSelectorSolver |
| AbstractMinimalModel |
| AbstractOutputSolver |
| DimacsArrayReader
Very simple Dimacs array reader.
|
| IVisualizationTool |
| ModelIterator
That class allows to iterate through all the models (implicants) of a
formula.
|
| OutcomeListener
Simple interface to check the outcome of running a solver in parallel.
|
| SearchListenerAdapter |
| SolutionFoundListener
Allows the end user to react when a new solution is found.
|
| SolverDecorator
The aim of that class is to allow adding dynamic responsibilities to SAT
solvers using the Decorator design pattern.
|
| Class and Description |
|---|
| AbstractClauseSelectorSolver |
| FullClauseSelectorSolver |
| GroupClauseSelectorSolver |
| SolverDecorator
The aim of that class is to allow adding dynamic responsibilities to SAT
solvers using the Decorator design pattern.
|