Class TernaryClausesDatabase

  • All Implemented Interfaces:
    ClauseDatabaseInterface, SolverComponent

    public final class TernaryClausesDatabase
    extends AbstractClausesDatabase
    A database for ternary clauses. It only accepts those.

    It does not work with watched literals. All literals are watching and if any of them changes then clause is being checked for unit propagation.

    Pros : no need to change watches. Cons : need to check the clause every time any literal changes.

    TODO, check if this the efficient way of dealing with ternary clauses.

    Version:
    4.8
    • Field Detail

      • clauses

        private int[] clauses
      • curValues

        private int[] curValues
      • curLit

        private int[] curLit
      • currentIndex

        private int currentIndex
      • numRemoved

        private int numRemoved
    • Constructor Detail

      • TernaryClausesDatabase

        public TernaryClausesDatabase()
    • Method Detail

      • 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
      • 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