Package org.jacop.jasat.core

Class ConflictLearning

java.lang.Object
org.jacop.jasat.core.ConflictLearning
All Implemented Interfaces:
SolverComponent
public final class ConflictLearning extends Object implements SolverComponent
A solver component for conflict learning. (first UIP algorithm)
Version:
4.10

  • Field Summary

    Fields
    Modifier and Type
    Field
    Description
    private Core
    core
     
    private DatabasesStore
    dbStore
     
    private Trail
    trail
     

  • Constructor Summary

    Constructors
    Constructor
    Description
    ConflictLearning()
     

  • Method Summary

    Modifier and Type
    Method
    Description
    private final 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 final 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

  • Field Details

  • Constructor Details

    • ConflictLearning

      public ConflictLearning()

  • Method Details

    • 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