Class BinaryClausesDatabase

java.lang.Object
org.jacop.jasat.core.clauses.AbstractClausesDatabase
org.jacop.jasat.core.clauses.BinaryClausesDatabase
All Implemented Interfaces:
ClauseDatabaseInterface, SolverComponent

public final class BinaryClausesDatabase extends AbstractClausesDatabase
A database for binary clauses. It only accepts those.
Version:
4.10
  • Field Details

    • INITIAL_SIZE

      private static final int INITIAL_SIZE
      See Also:
    • clauses

      private int[] clauses
    • currentIndex

      private int currentIndex
    • numRemoved

      private int numRemoved
  • Constructor Details

    • BinaryClausesDatabase

      public BinaryClausesDatabase()
  • Method Details

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

      public int size()
      Description copied from class: AbstractClausesDatabase
      number of clauses in the database
      Specified by:
      size in interface ClauseDatabaseInterface
      Specified by:
      size in class AbstractClausesDatabase
      Returns:
      the number of clauses in the database
    • toCNF

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