Package org.jacop.satwrapper

Class SatWrapper

    • Field Detail

      • empty

        boolean empty

      • core

        public Core core

      • boolVarToDomains

        public SatCPBridge[] boolVarToDomains

      • store

        public Store store

      • registeredVars

        public final java.util.Set<IntVar> registeredVars

      • levelToBackjumpTo

        public int levelToBackjumpTo

      • satToCpLevels

        public java.lang.Integer[] satToCpLevels

      • cpToSatLevels

        public java.lang.Integer[] cpToSatLevels

      • verbosity

        public int verbosity

      • trail

        private Trail trail

      • currentSatLevel

        private int currentSatLevel

      • modelClausesToAdd

        private final java.util.ArrayDeque<int[]> modelClausesToAdd

      • toAssertLiterals

        private IntQueue toAssertLiterals

      • clauseToLearn

        private MapClause clauseToLearn

      • mustBacktrack

        private boolean mustBacktrack

      • hasSolution

        private boolean hasSolution

    • Constructor Detail

      • SatWrapper

        public SatWrapper()
        creates everything in the right order

    • Method Detail

      • register

        public void register​(IntVar result)

      • register

        public void register​(IntVar variable,
                     boolean translate)
        registers the variable so that we can use it in SAT solver
        Parameters:
        variable - the CP IntVar variable
        translate - indicate whether to use == or <=

      • consistency

        public void consistency​(Store store)
        The point where all operations are effectively done in the SAT solver, until no operation remains or a conflict occurs
        Specified by:
        consistency in class Constraint
        Parameters:
        store - constraint store within which the constraint consistency is being checked.

      • processOneLiteral

        private void processOneLiteral()
        assert the next literal from toAssertLiterals

      • addSatLevel

        private void addSatLevel()
        adds one level for SAT side, and remembers the association between CP and SAT levels

      • onConflict

        public void onConflict​(MapClause clause,
                       int level)
        wrapper listens for conflicts.
        Specified by:
        onConflict in interface ConflictListener
        Parameters:
        clause - the conflict (unsatisfiable) clause
        level - the level at which the conflict occurred

      • onExplain

        public void onExplain​(MapClause explanation)
        wrapper listens for explanations, to know how deep to backtrack
        Specified by:
        onExplain in interface ExplanationListener
        Parameters:
        explanation - the explanation clause

      • onSolution

        public void onSolution​(boolean satisfiable)
        Description copied from interface: SolutionListener
        a handler called when a solution is found.
        Specified by:
        onSolution in interface SolutionListener
        Parameters:
        satisfiable - true when the solution is Satisfiable, false if it is Unsatisfiable.

      • removeLevel

        public void removeLevel​(int cpLevel)
        when the CP solver decides to remove a level, the wrapper must force the SAT solver to backtrack accordingly, to keep mappings between the two search trees consistent. This is also the place where the wrapper can decide that a conflict in the SAT solver has been solved.
        Specified by:
        removeLevel in interface Stateful
        Parameters:
        cpLevel - the level which is being removed.

      • queueVariable

        public void queueVariable​(int level,
                          Var var)
        Description copied from class: Constraint
        This is a function called to indicate which variable in a scope of constraint has changed. It also indicates a store level at which the change has occurred.
        Overrides:
        queueVariable in class Constraint
        Parameters:
        level - the level of the store at which the change has occurred.
        var - variable which has changed.

      • setBoolVariable

        private void setBoolVariable​(int variable,
                             boolean value)
        called when a boolean variable is set to some boolean value
        Parameters:
        variable - the boolean variable
        value - the value (true or false) of this variable

      • getConsistencyPruningEvent

        public int getConsistencyPruningEvent​(Var var)
        Description copied from class: Constraint
        It retrieves the pruning event which causes reevaluation of the constraint.
        Overrides:
        getConsistencyPruningEvent in class Constraint
        Parameters:
        var - variable for which pruning event is retrieved
        Returns:
        it returns the int code of the pruning event (GROUND, BOUND, ANY, NONE)

      • getMostActiveLiteral

        public int getMostActiveLiteral()
        asks the solver for which literal is the most active. It will return a literal, which can be transformed into a variable and a value from the variable domain. Useful when the CP solver does not know which variable to set to continue research
        Returns:
        a literal corresponding to some possible (variable,value)

      • showLiteralMeaning

        public java.lang.String showLiteralMeaning​(int literal)
        (for debug) show what a literal means
        Parameters:
        literal - literal for showing its meaning
        Returns:
        literal meaning

      • showClauseMeaning

        public java.lang.String showClauseMeaning​(java.lang.Iterable<java.lang.Integer> literals)

      • id

        public java.lang.String id()
        Description copied from class: Constraint
        It gives the id string of a constraint.
        Overrides:
        id in class Constraint
        Returns:
        string id of the constraint.

      • removeConstraint

        public void removeConstraint()
        Description copied from class: Constraint
        It removes the constraint by removing this constraint from all variables.
        Overrides:
        removeConstraint in class Constraint

      • satisfied

        public boolean satisfied()
        Description copied from interface: SatisfiedPresent
        It checks if the constraint is satisfied. It can return false even if constraint is satisfied but not all variables in its scope are grounded. It needs to return true if all variables in its scope are grounded and constraint is satisfied.

        Implementations of this interface for constraints that are not PrimitiveConstraint may require constraint imposition and consistency check as a requirement to work correctly.

        Specified by:
        satisfied in interface SatisfiedPresent
        Returns:
        true if constraint is possible to verify that it is satisfied.

      • toString

        public java.lang.String toString()
        Description copied from class: Constraint
        It produces a string representation of a constraint state.
        Overrides:
        toString in class Constraint

      • increaseWeight

        public void increaseWeight()
        Description copied from class: Constraint
        It increases the weight of the variables in the constraint scope.
        Overrides:
        increaseWeight in class Constraint

      • arguments

        public java.util.Set<Var> arguments()
        Description copied from class: Constraint
        It returns the variables in a scope of the constraint.
        Overrides:
        arguments in class Constraint
        Returns:
        variables in a scope of the constraint.

      • addSolverComponent

        public final void addSolverComponent​(SolverComponent module)
        to add some module to the solver
        Parameters:
        module - the module to add

      • addWrapperComponent

        public final void addWrapperComponent​(WrapperComponent module)
        add a component
        Parameters:
        module - the component

      • forget

        public final void forget()
        asks the solver to forget useless clauses, to free memory

      • addModelClause

        public final void addModelClause​(java.util.Collection<java.lang.Integer> clause)
        add model (globally valid) clause to solver, in a delayed fashion
        Parameters:
        clause - the clause to add

      • addModelClause

        public final void addModelClause​(int[] clause)

      • impose

        public final void impose​(Constraint constraint)
        add the constraint to the wrapper (ie, constraint.imposeToSat(this))
        Parameters:
        constraint - the constraint to add

      • impose

        public final void impose​(Store store)
        Description copied from class: Constraint
        It imposes the constraint in a given store.
        Overrides:
        impose in class Constraint
        Parameters:
        store - the constraint store to which the constraint is imposed to.

      • cpVarToBoolVar

        public final int cpVarToBoolVar​(IntVar variable,
                                int value,
                                boolean isEquality)
        given a CP variable and a value, retrieve the associated boolean literal for either 'variable = value' or either 'variable <= value'
        Parameters:
        variable - the CP variable
        value - a value in the range of this variable
        isEquality - a boolean, true if we want the literal that stands for 'x=d', false for 'x<=d'
        Returns:
        the corresponding literal, or 0 if it is out of bounds

      • boolVarToDomain

        public final SatCPBridge boolVarToDomain​(int literal)
        returns the CpVarDomain associated with this literal
        Parameters:
        literal - the boolean literal
        Returns:
        a range

      • boolVarToCpVar

        public final IntVar boolVarToCpVar​(int literal)
        get the IntVar back from a literal
        Parameters:
        literal - the literal
        Returns:
        IntVar represented by the literal

      • boolVarToCpValue

        public final int boolVarToCpValue​(int literal)
        transform a literal 'x=v' into a value 'v' for some CP variable
        Parameters:
        literal - literal to be transformed to value it represents
        Returns:
        the value represented by this literal

      • isEqualityBoolVar

        public final boolean isEqualityBoolVar​(int literal)
        checks if the boolean variable represents an assertion 'x=v' or 'x<=v'
        Parameters:
        literal - the boolean literal
        Returns:
        true if the literal represents a proposition 'x=v', false if it represents 'x<=v'

      • isVarLiteral

        public final boolean isVarLiteral​(int literal)
        checks if this literal corresponds to some CP variable
        Parameters:
        literal - the literal
        Returns:
        true if this literal stands for some 'x=v' or 'x<=v' proposition

      • log

        public boolean log​(java.lang.Object o,
                   java.lang.String format,
                   java.lang.Object... args)
        log method, similar to printf. Example: wrapper.log(this, "%s is %d", "foo", 42);
        Parameters:
        o - the object that logs something (use this)
        format - the format string (the message, if no formatting)
        args - the arguments to fill in the format
        Returns:
        always true

      • onStart

        public void onStart()
        Description copied from interface: StartStopListener
        called when the solver starts search. It will be called only once.
        Specified by:
        onStart in interface StartStopListener

      • 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

      • toCNF

        public void toCNF​(java.io.BufferedWriter output)
           throws java.io.IOException
        Throws:
        java.io.IOException