Class ConflictLearning

  • All Implemented Interfaces:
    SolverComponent

    public final class ConflictLearning
    extends java.lang.Object
    implements SolverComponent
    A solver component for conflict learning. (first UIP algorithm)
    Version:
    4.7
    • Method Summary

      All Methods Instance Methods Concrete Methods 
      Modifier and Type Method Description
      private void applyExplain​(MapClause explanationClause, int literal)
      performs one step of resolution for conflict explanation on given explanation clause.
      void applyExplainUIP​(MapClause explanationClause)
      It builds the explanation clause made of all literals that were involved in a conflict (ie which are in the clause and were asserted, or were asserted and triggered, in another clause, the propagation of a literal present in the current clause)
      private int findPositionTopLiteral​(MapClause explanationClause, int level, int startingPosition)
      It gets the position of last set literal of the clause.
      int getLevelToBackjump​(MapClause explanationClause)
      It computes to which level we should backjump to solve the conflict explained by @param explanationClause
      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

      • ConflictLearning

        public ConflictLearning()
    • Method Detail

      • getLevelToBackjump

        public int getLevelToBackjump​(MapClause explanationClause)
        It computes to which level we should backjump to solve the conflict explained by @param explanationClause
        Parameters:
        explanationClause - used for backjumping computation
        Returns:
        a level
      • applyExplainUIP

        public void applyExplainUIP​(MapClause explanationClause)
        It builds the explanation clause made of all literals that were involved in a conflict (ie which are in the clause and were asserted, or were asserted and triggered, in another clause, the propagation of a literal present in the current clause)
        Parameters:
        explanationClause - the SetClause we use, which must be initialized to the conflict clause
      • findPositionTopLiteral

        private final int findPositionTopLiteral​(MapClause explanationClause,
                                                 int level,
                                                 int startingPosition)
        It gets the position of last set literal of the clause.
        Parameters:
        explanationClause - the clause
        level - the level of selectable literals
        Returns:
        the last set literal of the clause, at current level, or 0 if none has been found
      • applyExplain

        private final void applyExplain​(MapClause explanationClause,
                                        int literal)
        performs one step of resolution for conflict explanation on given explanation clause.
        Parameters:
        explanationClause - the explanation clause
        literal - the literal that must be resolved
      • 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