| Interface | Description |
|---|---|
| IConstr |
The most general abstraction for handling a constraint.
|
| IGroupSolver |
Represents a CNF in which clauses are grouped into levels.
|
| ILogAble |
Utility interface to catch objects with logging capability (able to log).
|
| IOptimizationProblem |
Represents an optimization problem.
|
| IProblem |
Access to the information related to a given problem instance.
|
| ISolver |
This interface contains all services provided by a SAT solver.
|
| ISolverService |
The aim on that interface is to allow power users to communicate with the SAT
solver using Dimacs format.
|
| IteratorInt |
Iterator interface to avoid boxing int into Integer.
|
| IVec<T> |
An abstraction on the type of vector used in the library.
|
| IVecInt |
An abstraction for the vector of int used on the library.
|
| RandomAccessModel |
That interface allows to efficiently retrieve the truth value of a given
variable in the solver.
|
| SearchListener<S extends ISolverService> |
Interface to the solver main steps.
|
| UnitClauseProvider |
Interface for engines able to derive unit clauses for the current problem.
|
| UnitPropagationListener |
Interface providing the unit propagation capability.
|
| Class | Description |
|---|---|
| Lbool |
That enumeration defines the possible truth value for a variable: satisfied,
falsified or unknown/undefined.
|
| Exception | Description |
|---|---|
| ContradictionException |
That exception is launched whenever a trivial contradiction is found (e.g.
|
| TimeoutException |
Exception launched when the solver cannot solve a problem within its allowed
time.
|