| Package | Description |
|---|---|
| org.sat4j.minisat |
Implementation of the MiniSAT specification in Java.
|
| org.sat4j.minisat.constraints |
Implementations of various constraints for MiniSAT.
|
| org.sat4j.minisat.constraints.card |
Implementations of cardinality constraints.
|
| org.sat4j.minisat.constraints.cnf |
Implementations of clausal constraints.
|
| org.sat4j.minisat.core |
Implementation of the MiniSAT solver skeleton.
|
| org.sat4j.minisat.learning |
Various learning strategies.
|
| org.sat4j.minisat.orders |
Various heuristics to select the next variable to branch on.
|
| org.sat4j.minisat.restarts |
Various restart strategies.
|
| 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.
|
| UnitPropagationListener
Interface providing the unit propagation capability.
|
| 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.
|
| UnitPropagationListener
Interface providing the unit propagation capability.
|
| 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.
|
| UnitPropagationListener
Interface providing the unit propagation capability.
|
| 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.
|
| UnitPropagationListener
Interface providing the unit propagation capability.
|
| 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.
|
Copyright © 2013 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.