Uses of Package
org.sat4j.minisat.core

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 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.

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.

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

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.

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.

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.core

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.

ICDCLLogger

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.

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.

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

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.