| Class and Description |
|---|
| DataStructureFactory
The aim of the factory is to provide a concrete implementation of clauses,
cardinality constraints and pseudo boolean consraints.
|
| ICDCL
Abstraction for Conflict Driven Clause Learning Solver.
|
| IOrder
Interface for the variable ordering heuristics.
|
| Solver
The backbone of the library providing the modular implementation of a MiniSAT
(Chaff) like solver.
|
| Class and Description |
|---|
| Constr
Basic constraint abstraction used in Solver.
|
| DataStructureFactory
The aim of the factory is to provide a concrete implementation of clauses,
cardinality constraints and pseudo boolean consraints.
|
| ILits
That interface manages the solver's internal vocabulary.
|
| Learner
Provide the learning service.
|
| Propagatable
This interface is to be implemented by the classes wanted to be notified of
the falsification of a literal.
|
| Class and Description |
|---|
| Constr
Basic constraint abstraction used in Solver.
|
| ILits
That interface manages the solver's internal vocabulary.
|
| Propagatable
This interface is to be implemented by the classes wanted to be notified of
the falsification of a literal.
|
| Undoable
Interface providing the undoable service.
|
| Class and Description |
|---|
| Constr
Basic constraint abstraction used in Solver.
|
| ILits
That interface manages the solver's internal vocabulary.
|
| Propagatable
This interface is to be implemented by the classes wanted to be notified of
the falsification of a literal.
|
| Undoable
Interface providing the undoable service.
|
| Class and Description |
|---|
| ConflictTimer
Conflict based timer.
|
| Constr
Basic constraint abstraction used in Solver.
|
| DataStructureFactory
The aim of the factory is to provide a concrete implementation of clauses,
cardinality constraints and pseudo boolean consraints.
|
| ICDCL
Abstraction for Conflict Driven Clause Learning Solver.
|
| ILits
That interface manages the solver's internal vocabulary.
|
| IOrder
Interface for the variable ordering heuristics.
|
| IPhaseSelectionStrategy
The responsibility of that class is to choose the phase (positive or
negative) of the variable that was selected by the IOrder.
|
| ISimplifier
Strategy for simplifying the conflict clause derived by the solver.
|
| LearnedConstraintsDeletionStrategy
Strategy for cleaning the database of learned clauses.
|
| LearnedConstraintsEvaluationType
List the available strategies to evaluate learned clauses.
|
| Learner
Provide the learning service.
|
| LearningStrategy
Implementation of the strategy design pattern for allowing various learning
schemes.
|
| Pair
Utility class to be used to return the two results of a conflict analysis.
|
| Propagatable
This interface is to be implemented by the classes wanted to be notified of
the falsification of a literal.
|
| RestartStrategy
Abstraction allowing to choose various restarts strategies.
|
| SearchParams
Some parameters used during the search.
|
| SimplificationType
List the available simplification techniques available.
|
| Solver
The backbone of the library providing the modular implementation of a MiniSAT
(Chaff) like solver.
|
| SolverStats
Contains some statistics regarding the search.
|
| Undoable
Interface providing the undoable service.
|
| VarActivityListener
Interface providing the capability to increase the activity of a given
variable.
|
| Class and Description |
|---|
| Constr
Basic constraint abstraction used in Solver.
|
| DataStructureFactory
The aim of the factory is to provide a concrete implementation of clauses,
cardinality constraints and pseudo boolean consraints.
|
| ILits
That interface manages the solver's internal vocabulary.
|
| IOrder
Interface for the variable ordering heuristics.
|
| LearningStrategy
Implementation of the strategy design pattern for allowing various learning
schemes.
|
| Solver
The backbone of the library providing the modular implementation of a MiniSAT
(Chaff) like solver.
|
| VarActivityListener
Interface providing the capability to increase the activity of a given
variable.
|
| Class and Description |
|---|
| Heap
Heap implementation used to maintain the variables order in some heuristics.
|
| ILits
That interface manages the solver's internal vocabulary.
|
| IOrder
Interface for the variable ordering heuristics.
|
| IPhaseSelectionStrategy
The responsibility of that class is to choose the phase (positive or
negative) of the variable that was selected by the IOrder.
|
| Class and Description |
|---|
| ConflictTimer
Conflict based timer.
|
| Constr
Basic constraint abstraction used in Solver.
|
| RestartStrategy
Abstraction allowing to choose various restarts strategies.
|
| SearchParams
Some parameters used during the search.
|
| SolverStats
Contains some statistics regarding the search.
|
| Class and Description |
|---|
| Constr
Basic constraint abstraction used in Solver.
|
| DataStructureFactory
The aim of the factory is to provide a concrete implementation of clauses,
cardinality constraints and pseudo boolean consraints.
|
| ILits
That interface manages the solver's internal vocabulary.
|
| Class and Description |
|---|
| Constr
Basic constraint abstraction used in Solver.
|
| ILits
That interface manages the solver's internal vocabulary.
|
| Propagatable
This interface is to be implemented by the classes wanted to be notified of
the falsification of a literal.
|
| Undoable
Interface providing the undoable service.
|
| VarActivityListener
Interface providing the capability to increase the activity of a given
variable.
|
| Class and Description |
|---|
| Constr
Basic constraint abstraction used in Solver.
|
| DataStructureFactory
The aim of the factory is to provide a concrete implementation of clauses,
cardinality constraints and pseudo boolean consraints.
|
| ICDCL
Abstraction for Conflict Driven Clause Learning Solver.
|
| IOrder
Interface for the variable ordering heuristics.
|
| LearnedConstraintsDeletionStrategy
Strategy for cleaning the database of learned clauses.
|
| Learner
Provide the learning service.
|
| LearningStrategy
Implementation of the strategy design pattern for allowing various learning
schemes.
|
| Pair
Utility class to be used to return the two results of a conflict analysis.
|
| RestartStrategy
Abstraction allowing to choose various restarts strategies.
|
| SearchParams
Some parameters used during the search.
|
| Solver
The backbone of the library providing the modular implementation of a MiniSAT
(Chaff) like solver.
|
| SolverStats
Contains some statistics regarding the search.
|
| VarActivityListener
Interface providing the capability to increase the activity of a given
variable.
|
| Class and Description |
|---|
| IOrder
Interface for the variable ordering heuristics.
|
| IPhaseSelectionStrategy
The responsibility of that class is to choose the phase (positive or
negative) of the variable that was selected by the IOrder.
|
| Class and Description |
|---|
| Constr
Basic constraint abstraction used in Solver.
|