Interface ClauseDatabaseInterface

All Known Implementing Classes:
AbstractClausesDatabase, BinaryClausesDatabase, DatabasesStore, DefaultClausesDatabase, DomainClausesDatabase, LongClausesDatabase, TernaryClausesDatabase, UnaryClausesDatabase

public interface ClauseDatabaseInterface
Interface for clause databases or database stores. Any entity that contains clauses and can perform different operations on them.
Version:
4.8
  • Method Summary

    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.
    resolutionWith(int clauseIndex, MapClause clause)
    It returns the clause obtained by resolution between clauseIndex and clause.
    int
    size of the database
    void
    It writes the clauses of the databases in cnf format to the specified writer.
  • Method Details

    • 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(BufferedWriter output) throws 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:
      IOException - execption from java.io package