Uses of Package
org.sat4j.minisat.core

Packages that use org.sat4j.minisat.core

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.
org.sat4j.specs	Those classes are intended for users dealing with SAT solvers as black boxes.

Classes in org.sat4j.minisat.core used by org.sat4j.minisat

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.

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.constraints

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.

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.constraints.card

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.

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.constraints.cnf

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.

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.core

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.

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.learning

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.

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.orders

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.

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.restarts

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.

Classes in org.sat4j.minisat.core used by org.sat4j.specs

Class and Description
Constr Basic constraint abstraction used in Solver.