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

Packages that use DataStructureFactory

Package	Description
org.sat4j.minisat
org.sat4j.minisat.constraints
org.sat4j.minisat.core
org.sat4j.minisat.learning
org.sat4j.pb.constraints
org.sat4j.pb.core

Uses of DataStructureFactory in org.sat4j.minisat

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

Modifier and Type	Method and Description
static ICDCL<DataStructureFactory>	SolverFactory.newBest17()
static ICDCL<DataStructureFactory>	SolverFactory.newBestHT()
static Solver<DataStructureFactory>	SolverFactory.newBestWL()
static ICDCL<DataStructureFactory>	SolverFactory.newDefaultAutoErasePhaseSaving()
static ICDCL<DataStructureFactory>	SolverFactory.newDefaultMS21PhaseSaving()
static Solver<DataStructureFactory>	SolverFactory.newGlucose()
static ICDCL<DataStructureFactory>	SolverFactory.newGlucose21()
static ICDCL<DataStructureFactory>	SolverFactory.newGreedySolver()
static Solver<DataStructureFactory>	SolverFactory.newMiniLearning(DataStructureFactory dsf, IOrder order)
static Solver<DataStructureFactory>	SolverFactory.newMiniLearningHeap()
static Solver<DataStructureFactory>	SolverFactory.newMiniLearningHeap(DataStructureFactory dsf)
static Solver<DataStructureFactory>	SolverFactory.newMiniLearningHeapExpSimp()
static ICDCL<DataStructureFactory>	SolverFactory.newMiniLearningHeapEZSimp()
static ICDCL<DataStructureFactory>	SolverFactory.newMiniLearningHeapEZSimpLongRestarts()
static ICDCL<DataStructureFactory>	SolverFactory.newMiniLearningHeapEZSimpNoRestarts()
static Solver<DataStructureFactory>	SolverFactory.newMiniLearningHeapRsatExpSimp()
static Solver<DataStructureFactory>	SolverFactory.newMiniLearningHeapRsatExpSimpBiere()
static ICDCL<DataStructureFactory>	SolverFactory.newMiniLearningHeapRsatExpSimpLuby()
static Solver<DataStructureFactory>	SolverFactory.newMiniSATHeap()
static Solver<DataStructureFactory>	SolverFactory.newMiniSATHeap(DataStructureFactory dsf)
static ICDCL<DataStructureFactory>	SolverFactory.newMiniSATHeapExpSimp()
static ICDCL<DataStructureFactory>	SolverFactory.newMiniSATHeapEZSimp()

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

Modifier and Type	Method and Description
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

Modifier and Type	Class and Description
class	AbstractCardinalityDataStructure
class	AbstractDataStructureFactory
class	CardinalityDataStructure
class	CardinalityDataStructureYanMax
class	CardinalityDataStructureYanMin
class	ClausalDataStructureWL
class	MixedDataStructureDanielHT Uses specific data structure for cardinality constraints.
class	MixedDataStructureDanielWL
class	MixedDataStructureSingleWL

Uses of DataStructureFactory in org.sat4j.minisat.core

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

Modifier and Type	Interface and Description
interface	ICDCL<D extends DataStructureFactory> Abstraction for Conflict Driven Clause Learning Solver.
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

Modifier and Type	Field and Description
protected D	Solver.dsfactory

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

Modifier and Type	Method and Description
DataStructureFactory	Solver.getDSFactory()

Uses of DataStructureFactory in org.sat4j.minisat.learning

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

Modifier and Type	Class and Description
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

Modifier and Type	Method and Description
void	MiniSATLearning.setDataStructureFactory(DataStructureFactory dsf)

Uses of DataStructureFactory in org.sat4j.pb.constraints

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

Modifier and Type	Class and Description
class	AbstractPBClauseCardConstrDataStructure
class	AbstractPBDataStructureFactory
class	CompetMinHTmixedClauseCardConstrDataStructureFactory
class	CompetResolutionMinPBLongMixedWLClauseCardConstrDataStructure
class	CompetResolutionPBLongMixedHTClauseCardConstrDataStructure
class	CompetResolutionPBLongMixedWLClauseCardConstrDataStructure
class	CompetResolutionPBMixedHTClauseCardConstrDataStructure
class	CompetResolutionPBMixedWLClauseCardConstrDataStructure
class	PBLongMaxClauseCardConstrDataStructure
class	PBLongMinClauseCardConstrDataStructure
class	PBMaxClauseAtLeastConstrDataStructure
class	PBMaxClauseCardConstrDataStructure
class	PBMaxDataStructure
class	PBMinClauseCardConstrDataStructure
class	PBMinDataStructure
class	PuebloPBMinClauseAtLeastConstrDataStructure
class	PuebloPBMinClauseCardConstrDataStructure
class	PuebloPBMinDataStructure

Uses of DataStructureFactory in org.sat4j.pb.core

Subinterfaces of DataStructureFactory in org.sat4j.pb.core

Modifier and Type	Interface and Description
interface	PBDataStructureFactory