org.sat4j.minisat.learning
Class MiniSATLearning<L extends ILits>

java.lang.Object
  extended by org.sat4j.minisat.learning.MiniSATLearning<L>
All Implemented Interfaces:
java.io.Serializable, LearningStrategy<L>

public class MiniSATLearning<L extends ILits>
extends java.lang.Object

MiniSAT learning scheme. The Data Structure Factory is expected to be set thanks to the appropriate setter method before using it. It was not possible to set it in the constructor.

Author:
leberre
See Also:
Serialized Form

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

Constructor Detail

MiniSATLearning

public MiniSATLearning()
Method Detail

setDataStructureFactory

public void setDataStructureFactory(DataStructureFactory<L> dsf)

setSolver

public void setSolver(Solver<L> s)
Specified by:
setSolver in interface LearningStrategy<L extends ILits>

learns

public void learns(Constr constr)

toString

public java.lang.String toString()
Overrides:
toString in class java.lang.Object

setVarActivityListener

public void setVarActivityListener(VarActivityListener s)
Specified by:
setVarActivityListener in interface LearningStrategy<L extends ILits>

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>


Copyright © 2007 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.