Package | Description |
---|---|
org.sat4j.minisat.core | |
org.sat4j.minisat.learning | |
org.sat4j.pb.core |
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.
|
void |
Solver.setLearningStrategy(LearningStrategy<D> strategy) |
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) |
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.
|