org.sat4j.minisat.learning
Class NoLearningNoHeuristics

java.lang.Object
  org.sat4j.minisat.learning.NoLearningNoHeuristics

All Implemented Interfaces:

java.io.Serializable, LearningStrategy

public class NoLearningNoHeuristics
extends java.lang.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	setVarActivityListener(VarActivityListener s)

Methods inherited from class java.lang.Object

equals, 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

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