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

Packages that use LearningStrategy

Package	Description
org.sat4j.minisat.core	Implementation of the MiniSAT solver skeleton.
org.sat4j.minisat.learning	Various learning strategies.
org.sat4j.pb.core	Implementations of pseudo boolean solvers

Uses of LearningStrategy in org.sat4j.minisat.core

Methods in org.sat4j.minisat.core with parameters of type LearningStrategy

Modifier and Type	Method and Description
void	ICDCL.setLearner(LearningStrategy<D> learner) Deprecated. renamed into setLearningStrategy()
void	Solver.setLearner(LearningStrategy<D> strategy)
void	ICDCL.setLearningStrategy(LearningStrategy<D> strategy) Allow to change the learning strategy, i.e. to decide which clauses/constraints should be learned by the solver after conflict analysis.
void	Solver.setLearningStrategy(LearningStrategy<D> strategy)

Constructors in org.sat4j.minisat.core with parameters of type LearningStrategy

Constructor and Description
Solver(LearningStrategy<D> learner, D dsf, IOrder order, RestartStrategy restarter) creates a Solver without LearningListener.
Solver(LearningStrategy<D> learner, D dsf, SearchParams params, IOrder order, RestartStrategy restarter)
Solver(LearningStrategy<D> learner, D dsf, SearchParams params, IOrder order, RestartStrategy restarter, ILogAble logger)

Uses of LearningStrategy in org.sat4j.minisat.learning

Classes in org.sat4j.minisat.learning that implement LearningStrategy

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.

Uses of LearningStrategy in org.sat4j.pb.core

Constructors in org.sat4j.pb.core with parameters of type LearningStrategy

Constructor and Description
PBSolver(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order, RestartStrategy restarter)
PBSolver(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, SearchParams params, IOrder order, RestartStrategy restarter)
PBSolverCautious(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order)
PBSolverCautious(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order, int bound)
PBSolverClause(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order)
PBSolverCP(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order)
PBSolverCP(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, SearchParams params, IOrder order)
PBSolverCP(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, SearchParams params, IOrder order, RestartStrategy restarter)
PBSolverResCP(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order)
PBSolverResCP(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order, long bound)
PBSolverResCP(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, SearchParams params, IOrder order)
PBSolverResCP(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, SearchParams params, IOrder order, RestartStrategy restarter)
PBSolverResolution(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order, RestartStrategy restarter)
PBSolverResolution(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, SearchParams params, IOrder order, RestartStrategy restarter)
PBSolverWithImpliedClause(LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order)