Package org.jacop.jasat.core.clauses

Class DefaultClausesDatabase

  • All Implemented Interfaces:
    ClauseDatabaseInterface, SolverComponent
    public final class DefaultClausesDatabase
extends AbstractClausesDatabase
    A standard database of clauses, implemented in an efficient way such that insertion or removal of clauses works fast.

    Two-watched literals are used for fast unit propagation. The two first literals of each clauses are the watches.

    Version:
    4.8

    • Field Detail

      • DEFAULT_INITIAL_NUMBER_OF_CLAUSES

        private static final int DEFAULT_INITIAL_NUMBER_OF_CLAUSES
        See Also:
        Constant Field Values

      • clauses

        private int[][] clauses

      • currentIndex

        private int currentIndex

      • numRemoved

        private int numRemoved

    • Constructor Detail

      • DefaultClausesDatabase

        public DefaultClausesDatabase()

    • Method Detail

      • assertLiteral

        public void assertLiteral​(int literal)
        Notify the watches that this literal is set, updating the watched clauses and propagating literals if pertinent. If a conflict occurs, the solver conflict Event will be triggered. This is the main part of unit propagation for the solver.

        It always creates a list of new watched list (newWatchedList).

        Parameters:
        literal - the literal that is being set

      • addClause

        public int addClause​(int[] clause,
                     boolean isModel)
        Description copied from interface: ClauseDatabaseInterface
        It adds a clause to the database. This can change the state of the solver, for example if the clause is unsatisfiable in the current trail affectation, the solver will get in the conflict state.
        Parameters:
        clause - the clause to add
        isModel - defined if the clause is model clause
        Returns:
        the unique ID referring to the clause

      • removeClause

        public void removeClause​(int clauseIndex)
        Description copied from interface: ClauseDatabaseInterface
        It removes the clause which unique ID is @param clauseId.
        Parameters:
        clauseIndex - clause id

      • canRemove

        public boolean canRemove​(int clauseId)
        Description copied from interface: ClauseDatabaseInterface
        It tells if the implementation of ClausesDatabase can remove clauses or not
        Parameters:
        clauseId - the unique Id of the clause
        Returns:
        true iff removal of clauses is possible

      • resolutionWith

        public MapClause resolutionWith​(int clauseId,
                                MapClause explanation)
        Description copied from interface: ClauseDatabaseInterface
        It returns the clause obtained by resolution between clauseIndex and clause. It will also modify in place the given SetClause (avoid allocating).
        Parameters:
        clauseId - the unique id of the clause
        explanation - an explanation clause that is modified by resolution
        Returns:
        the clause obtained by resolution

      • rateThisClause

        public int rateThisClause​(int[] clause)
        Description copied from class: AbstractClausesDatabase
        Indicates how much this database is optimized for this clause. The Database that gives the higher rank will get the clause.
        Specified by:
        rateThisClause in class AbstractClausesDatabase
        Parameters:
        clause - a clause to rate
        Returns:
        a non negative integer indicating how much the database is interested in this clause

      • backjump

        public void backjump​(int level)
        returns to the given level
        Parameters:
        level - the level to return to. Must be < solver.getCurrentLevel().

      • checkWatches4Clause

        private java.lang.String checkWatches4Clause​(int clauseIndex)
        (used for debug) checks if the 2 first literals of the clauses are exactly the set of literals that watch this clause
        Parameters:
        clauseIndex - the index of the clause

      • checkWatches4var

        private java.lang.String checkWatches4var​(int var)
        (used for debug) checks if the 2 first literals of the clauses are exactly the set of literals that watch this clause
        Parameters:
        clauseIndex - the index of the clause

      • putAt0And1

        private final void putAt0And1​(int[] clause,
                              int i,
                              int j)
        assuming i != j, this modifies clause so that the elements that were at position i and j will now be at position 0 and 1 (i.e. clause[i] becomes clause[0] and clause[j] becomes clause[1])
        Parameters:
        clause - the clause to modify
        i - the first index
        j - the second index

      • ensureSize

        public void ensureSize​(int size)
        be sure that the database can contain @param size clauses
        Parameters:
        size - the number of clauses

      • toCNF

        public void toCNF​(java.io.BufferedWriter output)
           throws java.io.IOException
        Description copied from class: AbstractClausesDatabase
        It creates a CNF description of the clauses stored in this database.
        Specified by:
        toCNF in interface ClauseDatabaseInterface
        Specified by:
        toCNF in class AbstractClausesDatabase
        Parameters:
        output - it specifies the target to which the description will be written.
        Throws:
        java.io.IOException - execption from java.io package