Class HeuristicAssertionModule

  • All Implemented Interfaces:
    SolverComponent

    public final class HeuristicAssertionModule
    extends java.lang.Object
    implements SolverComponent
    module used to guide research by selecting the next literal to assert
    Version:
    4.8
    • Method Summary

      All Methods Instance Methods Concrete Methods 
      Modifier and Type Method Description
      int findNextVar()
      this is the main heuristic function, which tries to guess which literal is the most interesting to set now.
      void initialize​(Core core)
      initializes the component with the given solver.
      • Methods inherited from class java.lang.Object

        clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
    • Constructor Detail

      • HeuristicAssertionModule

        public HeuristicAssertionModule​(ActivityModule activity)
    • Method Detail

      • findNextVar

        public int findNextVar()
        this is the main heuristic function, which tries to guess which literal is the most interesting to set now. Can trigger SAT if no unset variable is found.
        Returns:
        a literal with no current value. Polarity counts.
      • initialize

        public void initialize​(Core core)
        Description copied from interface: SolverComponent
        initializes the component with the given solver. May be called only once. This method must register the component to the solver for the run.
        Specified by:
        initialize in interface SolverComponent
        Parameters:
        core - core component to initialize