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.



Copyright © 2010 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.