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.
Learner	Provide the learning service.
LearningStrategy<L extends ILits>	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
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

DotSearchListener	Class allowing to express the search as a tree in the dot language.
Handle<T>	This class simply holds a reference to a object.
Heap	Heap implementation used to maintain the variables order in some heuristics.
IntQueue	Implementation of a queue.
LiteralsUtils	Utility methods to avoid using bit manipulation inside code.
SearchParams	Some parameters used during the search.
Solver<L extends ILits>	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.

Enum Summary

Lbool

That enumeration defines the possible truth value for a variable: satisfied, falsified or unknown/undefined.

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.