Uses of Package
org.sat4j.minisat.core

Packages that use org.sat4j.minisat.core

org.sat4j.minisat	Implementation of the MiniSAT specification in Java.
org.sat4j.minisat.constraints	Implementations of various constraints for MiniSAT.
org.sat4j.minisat.constraints.card	Implementations of cardinality constraints.
org.sat4j.minisat.constraints.cnf	Implementations of clausal contraints.
org.sat4j.minisat.core	Implementation of the MiniSAT solver skeleton.
org.sat4j.minisat.learning	Various learning strategies.
org.sat4j.minisat.orders	Various heuristics to select the next variable to branch on.
org.sat4j.minisat.restarts	Various restart strategies.
org.sat4j.minisat.uip	Various ways to compute an asserting clause (containing one Unique Implication Point).

Classes in org.sat4j.minisat.core used by org.sat4j.minisat

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.

ILits2
Specific vocabulary taking special care of binary clauses.

ILits23
Specific vocabulary taking special care of binary and ternary clauses.

IOrder
Interface for the variable ordering heuristics.

Solver
The backbone of the library providing the modular implementation of a MiniSAT (Chaff) like solver.

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.constraints

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.

ILits2
Specific vocabulary taking special care of binary clauses.

ILits23
Specific vocabulary taking special care of binary and ternary clauses.

Learner
Provide the learning service.

Propagatable
This interface is to be implemented by the classes wanted to be notified of the falsification of a literal.

UnitPropagationListener
Interface providing the unit propagation capability.

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.constraints.card

Constr
Basic constraint abstraction used in Solver.

ILits
That interface manages the solver's internal vocabulary.

Propagatable
This interface is to be implemented by the classes wanted to be notified of the falsification of a literal.

Undoable
Interface providing the undoable service.

UnitPropagationListener
Interface providing the unit propagation capability.

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.constraints.cnf

Constr
Basic constraint abstraction used in Solver.

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.

Propagatable
This interface is to be implemented by the classes wanted to be notified of the falsification of a literal.

Undoable
Interface providing the undoable service.

UnitPropagationListener
Interface providing the unit propagation capability.

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.core

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.

ILits2
Specific vocabulary taking special care of binary clauses.

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.

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

Learner
Provide the learning service.

LearningStrategy
Implementation of the strategy design pattern for allowing various learning schemes.

Pair
Utility class to be used to return the two results of a conflict analysis.

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.

SearchParams
Some parameters used during the search.

Solver
The backbone of the library providing the modular implementation of a MiniSAT (Chaff) like solver.

SolverStats
Contains some statistics regarding the search.

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.

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.learning

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.

LearningStrategy
Implementation of the strategy design pattern for allowing various learning schemes.

Solver
The backbone of the library providing the modular implementation of a MiniSAT (Chaff) like solver.

VarActivityListener
Interface providing the capability to increase the activity of a given variable.

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.orders

Heap
Heap implementation used to maintain the variables order in some heuristics.

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.

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.restarts

RestartStrategy
Abstraction allowing to choose various restarts strategies.

SearchParams
Some parameters used during the search.

Classes in org.sat4j.minisat.core used by org.sat4j.minisat.uip

AssertingClauseGenerator
An assertingClauseGenerator is responsible for the creation of an asserting clause during conflict analysis.