Class DomainClausesDatabase

java.lang.Object
org.jacop.jasat.core.clauses.AbstractClausesDatabase
org.jacop.satwrapper.translation.DomainClausesDatabase
All Implemented Interfaces:
ClauseDatabaseInterface, SolverComponent, WrapperComponent

public final class DomainClausesDatabase extends AbstractClausesDatabase implements WrapperComponent
clause database designed to handle efficiently CP domain constraints, with the interface of boolean clauses databases.

This database must be added in the SAT solver (ideally at first position) and linked to the wrapper; it can then propagate literals that have a CP semantic with respect to their meaning about domains.

Version:
4.10
  • Field Details

    • wrapper

      private SatWrapper wrapper
    • propagationCauses

      private int[] propagationCauses
  • Constructor Details

    • DomainClausesDatabase

      public DomainClausesDatabase()
  • Method Details

    • assertLiteral

      public void assertLiteral(int assertedLiteral)
      this is responsible for propagating literals within the SAT solver to keep domain constraints coherent. It is informed by the SAT solver that some literal has been set, and propagate other variable literals.
      Specified by:
      assertLiteral in interface ClauseDatabaseInterface
      Parameters:
      assertedLiteral - the literal that is set
    • propagate

      public void propagate(int literal, int assertedLiteral)
      propagates the literal directly in the SAT solver
      Parameters:
      literal - the literal to propagate
      assertedLiteral - the literal that has been the origin of the propagation
    • clear

      private void clear()
      clear everything (no more propagations or ignored literals)
    • resolutionWith

      public MapClause resolutionWith(int clauseIndex, MapClause clause)
      to get a real clause to resolve with, we seek for the clause at the origin of the propagation.
      Specified by:
      resolutionWith in interface ClauseDatabaseInterface
      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.
      Specified by:
      backjump in interface ClauseDatabaseInterface
      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
    • 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.
      Specified by:
      addClause in interface ClauseDatabaseInterface
      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.
      Specified by:
      removeClause in interface ClauseDatabaseInterface
      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
      Specified by:
      canRemove in interface ClauseDatabaseInterface
      Parameters:
      clauseId - the unique Id of the clause
      Returns:
      true iff removal of clauses is possible
    • 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
    • initialize

      public void initialize(SatWrapper wrapper)
      Description copied from interface: WrapperComponent
      connect the component to the wrapper
      Specified by:
      initialize in interface WrapperComponent
      Parameters:
      wrapper - the wrapper
    • 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