Class UnaryClausesDatabase

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

public final class UnaryClausesDatabase extends AbstractClausesDatabase
A database for unit clauses (length 1). It only accepts those.
Version:
4.8
  • Field Details

    • INITIAL_SIZE

      private static final int INITIAL_SIZE
      TODO: Radek, just curious

      how is the conflict raised by this database? how is the propagation done? After clauses are added, how is the unit propagation taking place?

      => conflicts are only raised when a clause is added, because either we propagate the only literal of the clause, either it is false (=> conflict) However, a good question is: what if we add such a clause at level > 0 and some backjump goes under this level, maybe we should watch literals after all. ==> FIXME

      Is the addClause a right place to do above? Would it cause troubles for consistency of state of different components?

      See Also:
    • clauses

      private int[] clauses
    • currentIndex

      private int currentIndex
    • numRemoved

      private int numRemoved
  • Constructor Details

    • UnaryClausesDatabase

      public UnaryClausesDatabase()
  • Method Details

    • addClause

      public int addClause(int[] clause, boolean isModel)
      TODO: Radek,

      why would you bother with having any code for removal when nothing is being actually removed. Why not disallow removal altogether and call it StaticUnaryClausesDatabase?

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

      public String toString(String prefix)
      Description copied from class: AbstractClausesDatabase
      prints the content of the database in a nice way, each line being prefixed with
      Overrides:
      toString in class AbstractClausesDatabase
      Parameters:
      prefix - prefix for printed line
      Returns:
      a String representation of the database
    • 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