org.sat4j.minisat.learning
Class NoLearningButHeuristics<D extends DataStructureFactory>
java.lang.Object
org.sat4j.minisat.learning.NoLearningButHeuristics<D>
- All Implemented Interfaces:
- Serializable, LearningStrategy<D>
public final class NoLearningButHeuristics<D extends DataStructureFactory>
- extends Object
Allows MiniSAT to do backjumping without learning. The literals appearing in
the reason have their activity increased. That solution does not look good
for VLIW-SAT-1.0 benchmarks (1785s vs 1346s).
- Author:
- leberre
- See Also:
- Serialized Form
Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
NoLearningButHeuristics
public NoLearningButHeuristics()
learns
public void learns(Constr reason)
setVarActivityListener
public void setVarActivityListener(VarActivityListener s)
- Specified by:
setVarActivityListener
in interface LearningStrategy<D extends DataStructureFactory>
setSolver
public void setSolver(Solver<D> s)
- Specified by:
setSolver
in interface LearningStrategy<D extends DataStructureFactory>
claBumpActivity
public final void claBumpActivity(Constr reason)
init
public void init()
- Description copied from interface:
LearningStrategy
- hook method called just before the search begins. Useful to compute
metrics/parameters based on the input formula.
- Specified by:
init
in interface LearningStrategy<D extends DataStructureFactory>
Copyright © 2010 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.