Package org.jacop.jasat.core.clauses

Interface ClauseDatabaseInterface

    • Method Summary

      All Methods Instance Methods Abstract Methods 
      Modifier and Type Method Description
      int addClause​(int[] clause, boolean isModelClause)
      It adds a clause to the database.
      void assertLiteral​(int literal)
      It informs the ClausesDatabase that this literal is set, so that it can perform unit propagation.
      void backjump​(int level)
      Do everything needed to return to the given level.
      boolean canRemove​(int clauseId)
      It tells if the implementation of ClausesDatabase can remove clauses or not
      void removeClause​(int clauseId)
      It removes the clause which unique ID is @param clauseId.
      MapClause resolutionWith​(int clauseIndex, MapClause clause)
      It returns the clause obtained by resolution between clauseIndex and clause.
      int size()
      size of the database
      void toCNF​(java.io.BufferedWriter output)
      It writes the clauses of the databases in cnf format to the specified writer.

    • Method Detail

      • addClause

        int addClause​(int[] clause,
              boolean isModelClause)
        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
        isModelClause - defined if the clause is model clause
        Returns:
        the unique ID referring to the clause

      • assertLiteral

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

      • removeClause

        void removeClause​(int clauseId)
        It removes the clause which unique ID is @param clauseId.
        Parameters:
        clauseId - clause id

      • canRemove

        boolean canRemove​(int clauseId)
        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

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

      • backjump

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

      • size

        int size()
        size of the database
        Returns:
        the number of clauses in the database

      • toCNF

        void toCNF​(java.io.BufferedWriter output)
    throws java.io.IOException
        It writes the clauses of the databases in cnf format to the specified writer.
        Parameters:
        output - the output writer to which all the clauses will be written to.
        Throws:
        java.io.IOException - execption from java.io package