|
||||||||||
PREV NEXT | FRAMES NO FRAMES |
Packages that use org.sat4j.minisat.core | |
---|---|
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 contraints. |
org.sat4j.minisat.constraints.cnf | Implementations of clausal contraints. |
org.sat4j.minisat.constraints.pb | Implementations of pseudo boolean contraints. |
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 | |
org.sat4j.minisat.uip | Various ways to compute an asserting clause (containing one Unique Implication Point). |
Classes in org.sat4j.minisat.core used by org.sat4j.minisat | |
---|---|
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. |
|
ILits2
Specific vocabulary taking special care of binary clauses. |
|
ILits23
Specific vocabulary taking special care of binary and ternary clauses. |
|
IOrder
Interface for the variable ordering heuristics. |
|
Solver
The backbone of the library providing the modular implementation of a MiniSAT (Chaff) like solver. |
Classes in org.sat4j.minisat.core used by org.sat4j.minisat.constraints | |
---|---|
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. |
|
ILits2
Specific vocabulary taking special care of binary clauses. |
|
ILits23
Specific vocabulary taking special care of binary and ternary clauses. |
|
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. |
Classes in org.sat4j.minisat.core used by org.sat4j.minisat.constraints.card | |
---|---|
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. |
Classes in org.sat4j.minisat.core used by org.sat4j.minisat.constraints.cnf | |
---|---|
Constr
Basic constraint abstraction used in Solver. |
|
ILits
That interface manages the solver's internal vocabulary. |
|
ILits2
Specific vocabulary taking special care of binary clauses. |
|
ILits23
Specific vocabulary taking special care of binary and ternary clauses. |
|
IMarkableLits
Vocabulary in which literals can be marked. |
|
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. |
Classes in org.sat4j.minisat.core used by org.sat4j.minisat.constraints.pb | |
---|---|
AssertingClauseGenerator
An assertingClauseGenerator is responsible for the creation of an asserting clause during conflict analysis. |
|
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. |
|
Handle
This class simply holds a reference to a object. |
|
ILits
That interface manages the solver's internal vocabulary. |
|
IOrder
Interface for the variable ordering heuristics. |
|
Learner
Provide the learning service. |
|
LearningStrategy
Implementation of the strategy design pattern for allowing various learning schemes. |
|
Propagatable
This interface is to be implemented by the classes wanted to be notified of the falsification of a literal. |
|
RestartStrategy
|
|
SearchParams
Some parameters used during the search. |
|
Solver
The backbone of the library providing the modular implementation of a MiniSAT (Chaff) like solver. |
|
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. |
Classes in org.sat4j.minisat.core used by org.sat4j.minisat.core | |
---|---|
AssertingClauseGenerator
An assertingClauseGenerator is responsible for the creation of an asserting clause during conflict analysis. |
|
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. |
|
Handle
This class simply holds a reference to a object. |
|
ILits
That interface manages the solver's internal vocabulary. |
|
ILits2
Specific vocabulary taking special care of binary clauses. |
|
IOrder
Interface for the variable ordering heuristics. |
|
Lbool
That enumeration defines the possible truth value for a variable: satisfied, falsified or unknown/undefined. |
|
Learner
Provide the learning service. |
|
LearningStrategy
Implementation of the strategy design pattern for allowing various learning schemes. |
|
Propagatable
This interface is to be implemented by the classes wanted to be notified of the falsification of a literal. |
|
RestartStrategy
|
|
SearchListener
Interface to the solver main steps. |
|
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. |
|
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. |
Classes in org.sat4j.minisat.core used by org.sat4j.minisat.learning | |
---|---|
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. |
Classes in org.sat4j.minisat.core used by org.sat4j.minisat.orders | |
---|---|
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. |
Classes in org.sat4j.minisat.core used by org.sat4j.minisat.restarts | |
---|---|
RestartStrategy
|
|
SearchParams
Some parameters used during the search. |
Classes in org.sat4j.minisat.core used by org.sat4j.minisat.uip | |
---|---|
AssertingClauseGenerator
An assertingClauseGenerator is responsible for the creation of an asserting clause during conflict analysis. |
|
||||||||||
PREV NEXT | FRAMES NO FRAMES |