Package org.jacop.jasat.core

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.8

    • 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