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

Packages that use DataStructureFactory

org.sat4j.csp	Classes needed for CSP to SAT translation.
org.sat4j.maxsat	MAXSAT and Weighted Max SAT framework.
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.
org.sat4j.pb.constraints	Implementation of data structures for pseudo boolean constraints.
org.sat4j.pb.core	Implementations of pseudo boolean solvers

Uses of DataStructureFactory in org.sat4j.csp

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

static <L extends ILits> Solver<DataStructureFactory>

SolverFactory.newMiniSAT(DataStructureFactory dsf)

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

static <L extends ILits> Solver<DataStructureFactory>

SolverFactory.newMiniSAT(DataStructureFactory dsf)

Uses of DataStructureFactory in org.sat4j.maxsat

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

static Solver<DataStructureFactory>

SolverFactory.newMiniMaxSAT() Builds a SAT solver for the MAX sat evaluation.

Uses of DataStructureFactory in org.sat4j.minisat

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

static ICDCL<DataStructureFactory>	SolverFactory.newBest17()
static ICDCL<DataStructureFactory>	SolverFactory.newBestHT()
static ICDCL<DataStructureFactory>	SolverFactory.newBestSingleWL()
static Solver<DataStructureFactory>	SolverFactory.newBestWL()
static ICDCL<DataStructureFactory>	SolverFactory.newDefaultAutoErasePhaseSaving()
static ICDCL<DataStructureFactory>	SolverFactory.newDefaultMS21PhaseSaving()
static Solver<DataStructureFactory>	SolverFactory.newGlucose()
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 ICDCL<DataStructureFactory>	SolverFactory.newMiniLearningPure()
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

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	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

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

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)

Uses of DataStructureFactory in org.sat4j.pb.constraints

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

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

interface

PBDataStructureFactory