Class BinaryClausesDatabase

    • Field Detail

      • clauses

        private int[] clauses
      • currentIndex

        private int currentIndex
      • numRemoved

        private int numRemoved
    • Constructor Detail

      • BinaryClausesDatabase

        public BinaryClausesDatabase()
    • Method Detail

      • addClause

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

        Watches require a very large array, but there maybe not so many binary clauses. Maybe a hashmap, connecting variable and list of watched clauses is more appropriate.

        Parameters:
        clause - the clause to add
        isModel - defined if the clause is model clause
        Returns:
        the unique ID referring to the clause
      • 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
      • 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().
      • 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
      • notifyClause

        private final int notifyClause​(int clauseIndex)
        when something changed, find the status of the clause
        Parameters:
        clauseIndex - index of the clause
        Returns:
        the state of the clause
      • 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