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<L extends ILits>	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.
IMarkableLits	Vocabulary in which literals can be marked.
IOrder<L extends ILits>	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<L extends ILits,D extends DataStructureFactory<L>>	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.
SearchListener	Interface to the solver main steps.
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
DotSearchListener	Class allowing to express the search as a tree in the dot language.
Heap	Heap implementation used to maintain the variables order in some heuristics.
IntQueue	Implementation of a queue.
Lbool	That enumeration defines the possible truth value for a variable: satisfied, falsified or unknown/undefined.
Pair	Utility class to be used to return the two results of a conflict analysis.
SearchParams	Some parameters used during the search.
Solver<L extends ILits,D extends DataStructureFactory<L>>	The backbone of the library providing the modular implementation of a MiniSAT (Chaff) like solver.
SolverStats	Contains some statistics regarding the search.
TextOutputListener	Debugging Search Listener allowing to follow the search in a textual way.

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.