org.sat4j.minisat.learning
Class NoLearningButHeuristics<L extends ILits,D extends DataStructureFactory<L>>

java.lang.Object
  org.sat4j.minisat.learning.NoLearningButHeuristics<L,D>

All Implemented Interfaces:

java.io.Serializable, LearningStrategy<L,D>

public class NoLearningButHeuristics<L extends ILits,D extends DataStructureFactory<L>>
extends java.lang.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

Constructor Summary

NoLearningButHeuristics()

Method Summary

void	claBumpActivity(Constr reason)
void	init() hook method called just before the search begins.
void	learns(Constr reason)
void	setSolver(Solver<L,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

NoLearningButHeuristics

public NoLearningButHeuristics()

Method Detail

learns

public void learns(Constr reason)

setVarActivityListener

public void setVarActivityListener(VarActivityListener s)

Specified by:

setVarActivityListener in interface LearningStrategy<L extends ILits,D extends DataStructureFactory<L>>

setSolver

public void setSolver(Solver<L,D> s)

Specified by:

setSolver in interface LearningStrategy<L extends ILits,D extends DataStructureFactory<L>>

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<L extends ILits,D extends DataStructureFactory<L>>