org.sat4j.minisat.learning
Class NoLearningNoHeuristics<D extends DataStructureFactory>

java.lang.Object
  extended by org.sat4j.minisat.learning.NoLearningNoHeuristics<D>
All Implemented Interfaces:
Serializable, LearningStrategy<D>

public final class NoLearningNoHeuristics<D extends DataStructureFactory>
extends Object

Allows MiniSAT to do backjumping without learning. The literals appearing in the reason do not see their activity increased. That solution looks the best for VLIW-SAT-1.0 benchmarks (1346s vs 1785s).

Author:
leberre
See Also:
Serialized Form

Constructor Summary
NoLearningNoHeuristics()
           
 
Method Summary
 void claBumpActivity(Constr reason)
           
 void init()
          hook method called just before the search begins.
 void learns(Constr reason)
           
 void setSolver(Solver<D> s)
           
 void setVarActivityListener(VarActivityListener s)
           
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

NoLearningNoHeuristics

public NoLearningNoHeuristics()
Method Detail

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 © 2012 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.