Package org.jacop.jasat.core.clauses

Class UnaryClausesDatabase

    • Field Detail

      • INITIAL_SIZE

        private static final int INITIAL_SIZE
        TODO: Radek, just curious

        how is the conflict raised by this database? how is the propagation done? After clauses are added, how is the unit propagation taking place?

        => conflicts are only raised when a clause is added, because either we propagate the only literal of the clause, either it is false (=> conflict) However, a good question is: what if we add such a clause at level > 0 and some backjump goes under this level, maybe we should watch literals after all. ==> FIXME

        Is the addClause a right place to do above? Would it cause troubles for consistency of state of different components?

        See Also:
        Constant Field Values

      • clauses

        private int[] clauses

      • currentIndex

        private int currentIndex

      • numRemoved

        private int numRemoved

    • Constructor Detail

      • UnaryClausesDatabase

        public UnaryClausesDatabase()

    • Method Detail

      • addClause

        public int addClause​(int[] clause,
                     boolean isModel)
        TODO: Radek,

        why would you bother with having any code for removal when nothing is being actually removed. Why not disallow removal altogether and call it StaticUnaryClausesDatabase?

        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 clauseId)
        Description copied from interface: ClauseDatabaseInterface
        It removes the clause which unique ID is @param clauseId.
        Parameters:
        clauseId - 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 clause)
        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
        clause - an explanation clause that is modified by resolution
        Returns:
        the clause obtained by resolution

      • backjump

        public void backjump​(int level)
        Description copied from interface: ClauseDatabaseInterface
        Do everything needed to return to the given level.
        Parameters:
        level - the level to return to. Must be < solver.getCurrentLevel().

      • assertLiteral

        public void assertLiteral​(int literal)
        Description copied from interface: ClauseDatabaseInterface
        It informs the ClausesDatabase that this literal is set, so that it can perform unit propagation.
        Parameters:
        literal - the literal that is set

      • 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

      • toString

        public java.lang.String toString​(java.lang.String prefix)
        Description copied from class: AbstractClausesDatabase
        prints the content of the database in a nice way, each line being prefixed with
        Overrides:
        toString in class AbstractClausesDatabase
        Parameters:
        prefix - prefix for printed line
        Returns:
        a String representation of the database

      • 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