Class Core

  • All Implemented Interfaces:
    SolverComponent

    public final class Core
    extends java.lang.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.7
    • Field Detail

      • toPropagate

        public IntQueue toPropagate
      • explanationClause

        public MapClause explanationClause
      • assignmentNum

        public long assignmentNum
      • mustForget

        private boolean mustForget
      • maxVariable

        private int maxVariable
      • timeMap

        private java.util.Map<java.lang.String,​java.lang.Long> timeMap
      • isStopped

        public boolean isStopped
      • timer

        public java.util.Timer timer
      • trail

        public Trail trail
      • config

        public Config config
      • verbosity

        public int verbosity
      • logStream

        public java.io.PrintStream logStream
      • currentLevel

        public int currentLevel
      • currentState

        public int currentState
      • 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 Detail

      • 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 Detail

      • 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​(java.lang.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​(java.lang.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​(java.lang.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​(java.lang.String s,
                               java.lang.Object... args)
        logs important messages in comments
        Parameters:
        s - the message
        args - the arguments for the message
      • logc

        public final void logc​(int level,
                               java.lang.String s,
                               java.lang.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 java.lang.String toString()
        Overrides:
        toString in class java.lang.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