Class 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.7
    • Field Detail

      • propagationCauses

        private int[] propagationCauses
    • Constructor Detail

      • DomainClausesDatabase

        public DomainClausesDatabase()
    • Method Detail

      • 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
      • 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
      • 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 java.lang.String toString​(java.lang.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
      • toCNF

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