| Modifier and Type | Class and Description |
|---|---|
class |
ConflictLearning
A solver component for conflict learning.
|
class |
Core
The main solver structure, to be used either by a search component or by
another program that uses it for conflict learning and detection.
|
class |
Trail
It stores the current variables status (affected or not, with which value and explanation).
|
| Modifier and Type | Field and Description |
|---|---|
List<SolverComponent> |
Config.mainComponents
the list of components the solver must add
|
| Modifier and Type | Method and Description |
|---|---|
void |
Core.addComponent(SolverComponent module)
give the module access to the whole class, even if the solver is only
known as a ISatSolver
|
| Modifier and Type | Class and Description |
|---|---|
class |
AbstractClausesDatabase
This class specifies an abstract class for clauses pools.
|
class |
BinaryClausesDatabase
A database for binary clauses.
|
class |
DatabasesStore
This provides a unique interface to several databases.
|
class |
DefaultClausesDatabase
A standard database of clauses, implemented in an efficient way such that insertion
or removal of clauses works fast.
|
class |
LongClausesDatabase
A pool of long clauses, implemented with two watched an blocking literals
to minimize cache misses.
|
class |
TernaryClausesDatabase
A database for ternary clauses.
|
class |
UnaryClausesDatabase
A database for unit clauses (length 1).
|
| Modifier and Type | Class and Description |
|---|---|
class |
ActivityModule
counts the activity of literals
|
class |
DebugModule
module used for debug : it logs every event it is informed of
|
class |
HeuristicAssertionModule
module used to guide research by selecting the next literal to assert
|
class |
HeuristicForgetModule
A component that selects clauses to forget when solver.forget() is called.
|
class |
HeuristicRestartModule
A module that indicates if a restart would be useful now.
|
class |
SearchModule
A basic searching component, which controls the solver to solve the problem
|
class |
StatModule
collects statistics about the solver
|
| Modifier and Type | Interface and Description |
|---|---|
interface |
AssertionListener
A class that can register to the Solver, to be notified when some events
occur.
|
interface |
BackjumpListener
interface for components that listen for backjumps, or restarts
|
interface |
ClauseListener
module that listens to add/removal of clauses
|
interface |
ConflictListener
module that listens to conflicts that are discovered.
|
interface |
ExplanationListener
module used when an explanation is found
|
interface |
ForgetListener
called when the solver forget() method is called.
|
interface |
PropagateListener
module called when a propagate event is called
|
interface |
SolutionListener
module called when solution is found.
|
interface |
StartStopListener
called when the solver starts or stops.
|
| Modifier and Type | Class and Description |
|---|---|
class |
MemoryPool
Class containing int[] of different lengths, to avoid allocating/deallocating too much.
|
| Modifier and Type | Class and Description |
|---|---|
class |
SatChangesListener
this class listens to changes in literals in SAT solver, and reminds
what changes this implies for CP variables
|
class |
SatWrapper
wrapper to communicate between SAT solver and CP solver.
|
class |
WrapperDebugModule
a class used to debug, but with additional data
|
| Modifier and Type | Method and Description |
|---|---|
void |
SatWrapper.addSolverComponent(SolverComponent module)
to add some module to the solver
|
| Modifier and Type | Class and Description |
|---|---|
class |
DomainClausesDatabase
clause database designed to handle efficiently CP domain constraints, with
the interface of boolean clauses databases.
|
Copyright © 2022. All rights reserved.