Uses of Interface
org.sat4j.minisat.core.DataStructureFactory

Packages that use DataStructureFactory

org.sat4j.minisat	Implementation of the MiniSAT specification in Java.
org.sat4j.minisat.constraints	Implementations of various constraints for MiniSAT.
org.sat4j.minisat.core	Implementation of the MiniSAT solver skeleton.
org.sat4j.minisat.learning	Various learning strategies.

Uses of DataStructureFactory in org.sat4j.minisat

Methods in org.sat4j.minisat that return types with arguments of type DataStructureFactory

static Solver<DataStructureFactory>	SolverFactory.newBestHT()
static Solver<DataStructureFactory>	SolverFactory.newBestWL()
static Solver<DataStructureFactory>	SolverFactory.newGlucose()
static Solver<DataStructureFactory>	SolverFactory.newMiniLearning(DataStructureFactory dsf, IOrder order)
static Solver<DataStructureFactory>	SolverFactory.newMiniLearningCBWLPure()
static Solver<DataStructureFactory>	SolverFactory.newMiniLearningHeap()
static Solver<DataStructureFactory>	SolverFactory.newMiniLearningHeap(DataStructureFactory dsf)
static Solver<DataStructureFactory>	SolverFactory.newMiniLearningHeapExpSimp()
static Solver<DataStructureFactory>	SolverFactory.newMiniLearningHeapEZSimp()
static Solver<DataStructureFactory>	SolverFactory.newMiniLearningHeapEZSimpLongRestarts()
static Solver<DataStructureFactory>	SolverFactory.newMiniLearningHeapEZSimpNoRestarts()
static Solver<DataStructureFactory>	SolverFactory.newMiniLearningHeapRsatExpSimp()
static Solver<DataStructureFactory>	SolverFactory.newMiniLearningHeapRsatExpSimpBiere()
static Solver<DataStructureFactory>	SolverFactory.newMiniLearningHeapRsatExpSimpLuby()
static Solver<DataStructureFactory>	SolverFactory.newMiniLearningPure()
static Solver<DataStructureFactory>	SolverFactory.newMiniSATHeap()
static Solver<DataStructureFactory>	SolverFactory.newMiniSATHeap(DataStructureFactory dsf)
static Solver<DataStructureFactory>	SolverFactory.newMiniSATHeapExpSimp()
static Solver<DataStructureFactory>	SolverFactory.newMiniSATHeapEZSimp()

Methods in org.sat4j.minisat with parameters of type DataStructureFactory

static Solver<DataStructureFactory>	SolverFactory.newMiniLearning(DataStructureFactory dsf, IOrder order)
static Solver<DataStructureFactory>	SolverFactory.newMiniLearningHeap(DataStructureFactory dsf)
static Solver<DataStructureFactory>	SolverFactory.newMiniSATHeap(DataStructureFactory dsf)

Uses of DataStructureFactory in org.sat4j.minisat.constraints

Classes in org.sat4j.minisat.constraints that implement DataStructureFactory

class	AbstractCardinalityDataStructure
class	AbstractDataStructureFactory
class	CardinalityDataStructure
class	CardinalityDataStructureYanMax
class	CardinalityDataStructureYanMin
class	ClausalDataStructureCB
class	ClausalDataStructureCBWL
class	ClausalDataStructureWL
class	MixedDataStructureDanielCBWL
class	MixedDataStructureDanielHT Uses specific data structure for cardinality constraints.
class	MixedDataStructureDanielWL

Uses of DataStructureFactory in org.sat4j.minisat.core

Classes in org.sat4j.minisat.core with type parameters of type DataStructureFactory

interface	LearningStrategy<D extends DataStructureFactory> Implementation of the strategy design pattern for allowing various learning schemes.
class	Solver<D extends DataStructureFactory> The backbone of the library providing the modular implementation of a MiniSAT (Chaff) like solver.

Fields in org.sat4j.minisat.core declared as DataStructureFactory

protected D

Solver.dsfactory

Methods in org.sat4j.minisat.core that return DataStructureFactory

DataStructureFactory

Solver.getDSFactory()

Uses of DataStructureFactory in org.sat4j.minisat.learning

Classes in org.sat4j.minisat.learning with type parameters of type DataStructureFactory

class	ActiveLearning<D extends DataStructureFactory> Learn clauses with a great number of active variables.
class	ClauseOnlyLearning<D extends DataStructureFactory> The solver only records among all the constraints only the clauses.
class	FixedLengthLearning<D extends DataStructureFactory> A learning scheme for learning constraints of size smaller than a given constant.
class	LimitedLearning<D extends DataStructureFactory> Learn only clauses which size is smaller than a percentage of the number of variables.
class	MiniSATLearning<D extends DataStructureFactory> MiniSAT learning scheme.
class	NoLearningButHeuristics<D extends DataStructureFactory> Allows MiniSAT to do backjumping without learning.
class	NoLearningNoHeuristics<D extends DataStructureFactory> Allows MiniSAT to do backjumping without learning.
class	PercentLengthLearning<D extends DataStructureFactory> Selects the constraints to learn according to its length as a percentage of the total number of variables in the solver universe.

Methods in org.sat4j.minisat.learning with parameters of type DataStructureFactory

void	MiniSATLearning.setDataStructureFactory(DataStructureFactory dsf)