Class LongClausesDatabase

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

public final class LongClausesDatabase extends AbstractClausesDatabase
A pool of long clauses, implemented with two watched an blocking literals to minimize cache misses.
Version:
4.10
  • Field Details

    • DEFAULT_INITIAL_NUMBER_OF_CLAUSES

      private static final int DEFAULT_INITIAL_NUMBER_OF_CLAUSES
      See Also:
    • SIZE_OF_CLAUSE_CACHE

      private static final int SIZE_OF_CLAUSE_CACHE
      See Also:
    • currentIndex

      private int currentIndex
    • clauses

      private int[][] clauses
    • literalsCache

      private int[][] literalsCache
    • generator

      Random generator
      Put it one place so there is only one Random generator for the whole SAT solver. TODO: Radek.
  • Constructor Details

    • LongClausesDatabase

      public LongClausesDatabase()
  • Method Details

    • 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 clauseIndex, 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:
      clauseIndex - 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
    • 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
    • ensureSize

      public void ensureSize(int size)
      be sure that the database can contain numberOfClauses clauses
      Parameters:
      size - the size of the database to be ensured
    • isSatisfied

      private final boolean isSatisfied(int literal)
      is the literal at position @param literalPos satisfied in current trail ?
    • isActiveOrSatisfied

      private final boolean isActiveOrSatisfied(int literal)
      is the literal at position @param literalPos satisfied or active ?
    • isActive

      private final boolean isActive(int literal)
      is the literal at position @param literalPos satisfied or active ?
    • 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