Package org.sat4j.minisat.core

Implementation of the MiniSAT solver skeleton.

See: Description

Interface Summary

Interface	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<D extends DataStructureFactory>	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.
Learner	Provide the learning service.
LearningStrategy<D extends DataStructureFactory>	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	Abstraction allowing to choose various restarts strategies.
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 Summary

Class	Description
ActivityComparator	Utility class to sort the constraints according to their activity.
CircularBuffer	Create a circular buffer of a given capacity allowing to compute efficiently the mean of the values storied.
ConflictTimerAdapter	Perform a task when a given number of conflicts is reached.
ConflictTimerContainer	Agregator for conflict timers (composite design pattern).
Counter
Heap	Heap implementation used to maintain the variables order in some heuristics.
IntQueue	Implementation of a queue.
Pair	Utility class to be used to return the two results of a conflict analysis.
SearchParams	Some parameters used during the search.
Solver<D extends DataStructureFactory>	The backbone of the library providing the modular implementation of a MiniSAT (Chaff) like solver.
SolverStats	Contains some statistics regarding the search.

Enum Summary

Enum	Description
LearnedConstraintsEvaluationType	List the available strategies to evaluate learned clauses.
SimplificationType	List the available simplification techniques available.

Package org.sat4j.minisat.core Description

Implementation of the MiniSAT solver skeleton. This is the place to go for looking more deeply into a SAT solver. All of the abstractions needed to customize a solver are defined here.