Class Core

java.lang.Object
org.jacop.jasat.core.Core
All Implemented Interfaces:
SolverComponent

public final class Core extends Object implements SolverComponent
The main solver structure, to be used either by a search component or by another program that uses it for conflict learning and detection.

This implements interfaces for being manipulated from the outside, and from its components

Version:
4.8
  • Field Details

    • toPropagate

      public IntQueue toPropagate
    • explanationClause

      public MapClause explanationClause
    • assignmentNum

      public long assignmentNum
    • mustForget

      private boolean mustForget
    • maxVariable

      private int maxVariable
    • timeMap

      private Map<String,Long> timeMap
    • isStopped

      public boolean isStopped
    • timer

      public Timer timer
    • pool

      public MemoryPool pool
    • dbStore

      public DatabasesStore dbStore
    • trail

      public Trail trail
    • config

      public Config config
    • verbosity

      public int verbosity
    • logStream

      public PrintStream logStream
    • currentLevel

      public int currentLevel
    • currentState

      public int currentState
    • conflictLearning

      public ConflictLearning conflictLearning
    • assertionModules

      public AssertionListener[] assertionModules
    • backjumpModules

      public BackjumpListener[] backjumpModules
    • conflictModules

      public ConflictListener[] conflictModules
    • propagateModules

      public PropagateListener[] propagateModules
    • solutionModules

      public SolutionListener[] solutionModules
    • forgetModules

      public ForgetListener[] forgetModules
    • clauseModules

      public ClauseListener[] clauseModules
    • explanationModules

      public ExplanationListener[] explanationModules
    • startStopModules

      public StartStopListener[] startStopModules
    • restartModules

      public BackjumpListener[] restartModules
    • numAssertionModules

      public int numAssertionModules
    • numBackjumpModules

      public int numBackjumpModules
    • numConflictModules

      public int numConflictModules
    • numPropagateModules

      public int numPropagateModules
    • numSolutionModules

      public int numSolutionModules
    • numForgetModules

      public int numForgetModules
    • numClauseModules

      public int numClauseModules
    • numExplanationModules

      public int numExplanationModules
    • numStartStopModules

      public int numStartStopModules
    • numRestartModules

      public int numRestartModules
  • Constructor Details

    • Core

      public Core(Config config)
      creates the solver, which in turn creates all inner components and connect them together.
      Parameters:
      config - configuration for the solver
    • Core

      public Core()
      initializes the solver with a default configuration.
  • Method Details

    • addModelClause

      public int addModelClause(IntVec clause)
      adds a clause to the solver
      Parameters:
      clause - the clause to add
      Returns:
      the unique ID of the clause
    • addModelClause

      public int addModelClause(int[] clause)
      same as previous, add the clause as a model clause
      Parameters:
      clause - the clause to add
      Returns:
      the unique ID of this clause, or -1 if it is trivial
    • addClause

      private int addClause(int[] clause, boolean isModelClause)
      add @param clause to the pool of clauses
    • canRemove

      public boolean canRemove(int clauseId)
      predicate : can we remove the clause without breaking the correctness of the solver ?
      Parameters:
      clauseId - the unique Id of the clause
      Returns:
      true if removing the clause is allowed
    • removeClause

      public boolean removeClause(int clauseId)
      removes the clause with unique Id, if possible
      Parameters:
      clauseId - the unique Id of the clause to remove
      Returns:
      true if success, false if failure
    • assertLiteral

      public void assertLiteral(int literal, int newLevel)
      decides a single step of search by setting the value of a variable
      Parameters:
      literal - the literal to set true
      newLevel - the current search level
    • backjumpToLevel

      public void backjumpToLevel(int level)
      tells the SAT-solver to backtrack to the given level. The level must be lower or equal to the solver's current level.
      Parameters:
      level - the level to return to
    • restart

      public void restart()
      make a restart, that is, restart search from level 0.
    • start

      public void start()
      notify all modules that we start
    • stop

      public void stop()
      notify all modules that we stop
    • forget

      public void forget()
      removes the less useful learnt clauses to free memory
    • getLevelToBackjump

      public int getLevelToBackjump()
      Computes at which level we should backjump to solve the conflict. The solver must be in CONFLICT state.
      Returns:
      a level lower than the current level, in which the solver state would no longer be CONFLICT.
    • getLevelToBackjump

      public int getLevelToBackjump(MapClause explanationClause)
    • getFreshVariable

      public int getFreshVariable()
      gets a fresh variable that one can use for example for lazy clause generation. If used, every clause added must use only the variables get by this way, or a variable collision could occur.
      Returns:
      a fresh variable
    • getManyFreshVariables

      public int getManyFreshVariables(int number)
      get several new variables at once, more efficiently than running getFreshVariable() @param number times. The variables range from the returned int to the returned int + @param number - 1
      Parameters:
      number - the number of fresh variables we want
      Returns:
      The first variable in the range of new variables
    • setMaxVariable

      public void setMaxVariable(int maxVariable)
      Tells the solver what is the greatest variable in the problem
      Parameters:
      maxVariable - the new maximum variable. Must not be lower than solver.getMaxVariable().
    • getMaxVariable

      public int getMaxVariable()
      Returns:
      the current max variable
    • addComponent

      public void addComponent(SolverComponent module)
      give the module access to the whole class, even if the solver is only known as a ISatSolver
      Parameters:
      module - the module to add to the solver
    • unitPropagate

      public final void unitPropagate()
      performs propagation on all unit clauses until either : - no unit clause remains - a conflict occurs
    • triggerForgetEvent

      private void triggerForgetEvent()
      triggers an event of forget()
    • triggerAssertEvent

      private void triggerAssertEvent(int literal, int newLevel)
      triggers an event for assertion of a literal
      Parameters:
      literal - the literal asserted
      newLevel - the new level, after assertion. It must be strictly greater than currentLevel.
    • triggerIdleEvent

      public void triggerIdleEvent()
      tells the SAT-solver to return to a normal state after a conflict has been solved (backjump or restart)
    • triggerLearnEvent

      public void triggerLearnEvent(MapClause clauseToLearn)
      triggers an event of learning
      Parameters:
      clauseToLearn - the clause which is learnt
    • triggerConflictEvent

      public void triggerConflictEvent(MapClause clause)
      triggers a conflict. The next step of the research should be conflict learning and then backjumping.
      Parameters:
      clause - an unsatisfiable clause.
    • triggerPropagateEvent

      public void triggerPropagateEvent(int literal, int unitClauseId)
      triggers a unit propagation event. This keeps the same level.
      Parameters:
      literal - the unique unset literal, which must be true for the clause to be satisfied
      unitClauseId - the unique id of the unit clause that propagates
    • triggerBackjumpEvent

      public void triggerBackjumpEvent(int level)
      triggers an event to backjump
      Parameters:
      level - the level to backjump to
    • triggerRestartEvent

      public void triggerRestartEvent()
      triggers an event of restart
    • triggerSatEvent

      public void triggerSatEvent()
      to trigger if the problem is found to be satisfiable
    • triggerUnsatEvent

      public void triggerUnsatEvent()
      to trigger if the problem is found to be not satisfiable
    • markTime

      public final void markTime(String s)
      remembers that @param s is associated with the current time (in ms)
      Parameters:
      s - the mark of current time
    • getTime

      public final long getTime(String s)
      get the time associated with given mark, or 0 if none
      Parameters:
      s - the mark
      Returns:
      the time associated with given mark, or 0 if none
    • getTimeDiff

      public final long getTimeDiff(String s)
      gets the time difference (in ms) between now and the mark
      Parameters:
      s - the mark
      Returns:
      the time elapsed since mark, in ms
    • logc

      public final void logc(String s, Object... args)
      logs important messages in comments
      Parameters:
      s - the message
      args - the arguments for the message
    • logc

      public final void logc(int level, String s, Object... args)
      logs less important messages, in comments
      Parameters:
      level - verbosity level
      s - the message
      args - the arguments for the message
    • hasSolution

      public final boolean hasSolution()
      Returns:
      true if the solver reached a solution
    • printSolution

      public final void printSolution()
      prints the current solution on standard output
    • getReturnCode

      public final int getReturnCode()
      before exiting, we must know which return code we must give
      Returns:
      the return code to exit with
    • toString

      public String toString()
      Overrides:
      toString in class Object
    • 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