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

Packages that use LearningStrategy

org.sat4j.minisat.core	Implementation of the MiniSAT solver skeleton.
org.sat4j.minisat.learning	Various learning strategies.
org.sat4j.pb.core

Uses of LearningStrategy in org.sat4j.minisat.core

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

void	Solver.setLearner(LearningStrategy<D> learner)

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

Solver(AssertingClauseGenerator acg, LearningStrategy<D> learner, D dsf, IOrder order, RestartStrategy restarter)
creates a Solver without LearningListener.

Solver(AssertingClauseGenerator acg, LearningStrategy<D> learner, D dsf, SearchParams params, IOrder order, RestartStrategy restarter)

Uses of LearningStrategy in org.sat4j.minisat.learning

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

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

PBSolver(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order, RestartStrategy restarter)

PBSolver(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, SearchParams params, IOrder order, RestartStrategy restarter)

PBSolverCautious(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order)

PBSolverCautious(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order, int bound)

PBSolverClause(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order)

PBSolverCP(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order)

PBSolverCP(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, SearchParams params, IOrder order)

PBSolverCP(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, SearchParams params, IOrder order, RestartStrategy restarter)

PBSolverMerging(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order)

PBSolverResCP(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order)

PBSolverResCP(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order, long bound)

PBSolverResCP(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, SearchParams params, IOrder order)

PBSolverResCP(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, SearchParams params, IOrder order, RestartStrategy restarter)

PBSolverResolution(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order, RestartStrategy restarter)

PBSolverResolution(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, SearchParams params, IOrder order, RestartStrategy restarter)

PBSolverWithImpliedClause(AssertingClauseGenerator acg, LearningStrategy<PBDataStructureFactory> learner, PBDataStructureFactory dsf, IOrder order)