Package org.sat4j.minisat.core

Implementation of the MiniSAT solver skeleton.

See:
Description

Interface Summary

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

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.

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.