Package eu.bandm.tools.dpll

Class Literal<P>

java.lang.Object
eu.bandm.tools.dpll.Literal<P>
Type Parameters:
P - the type of propositional variables
All Implemented Interfaces:
Proposition<P>
public final class Literal<P> extends Object implements Proposition<P>
Positive or negative occurrence of propositional variable.

Propositional variables are paired with a logical sign: true for positive and false for negative literals.

Propositional variables are represented by arbitrary objects, up to Object.equals(java.lang.Object). A null reference as a propositional variable is not supported.

  • Constructor Summary

    Constructors
    Constructor
    Description
    Literal(boolean sign, P variable)
    Creates a new instance.

  • Method Summary

    Modifier and Type
    Method
    Description
    boolean
    equals(Object o)
    boolean
    getSign()
    Returns the logical sign of this literal.
    P
    getVariable()
    Returns the propositional variable of this literal.
    int
    hashCode()
    static <P> boolean
    isConsistent(Collection<Literal<P>> literals)
    Checks whether the given literals are consistent.
    boolean
    isDisjunctionFree()
    Checks whether this proposition is free of disjunctions.
    boolean
    isFalse()
    Check whether this proposition is evidently false.
    boolean
    isSatisfiedBy(Set<Literal<P>> solution)
    Checks whether this proposition is satisfied by a given solution.
    boolean
    isTrue()
    Check whether this proposition is evidently true.
    Literal<P>
    negate()
    Return the negation of this literal.
    static <P> Literal<P>
    negative(P variable)
    Creates a new negative instance.
    static <P> Literal<P>
    positive(P variable)
    Creates a new positive instance.
    static <P> Set<Literal<P>>
    pure(Iterable<Literal<P>> literals)
    Finds the propositional variables occurring purely in some literals.
    int
    score()
    Returns a nonnegative measure of the syntactic complexity of this proposition.
    String
    toString()

    Methods inherited from class java.lang.Object

    clone, finalize, getClass, notify, notifyAll, wait, wait, wait

  • Constructor Details

    • Literal

      public Literal(boolean sign, P variable)
      Creates a new instance.
      Parameters:
      sign - the logical sign of the literal
      variable - the propositional variable
      Throws:
      NullPointerException - if variable is null

  • Method Details

    • positive

      public static <P> Literal<P> positive(P variable)
      Creates a new positive instance.
      Type Parameters:
      P - the type of propositional variables
      Parameters:
      variable - the propositional variable
      Returns:
      a positive literal with the given variable
      Throws:
      NullPointerException - if variable is null

    • negative

      public static <P> Literal<P> negative(P variable)
      Creates a new negative instance.
      Type Parameters:
      P - the type of propositional variables
      Parameters:
      variable - the propositional variable
      Returns:
      a negative literal with the given variable
      Throws:
      NullPointerException - if variable is null

    • isTrue

      public boolean isTrue()
      Check whether this proposition is evidently true.

      This implementation always returns false.

      Specified by:
      isTrue in interface Proposition<P>
      Returns:
      true if this proposition is immediately seen to be true; false otherwise.

    • isFalse

      public boolean isFalse()
      Check whether this proposition is evidently false.

      This implementation always returns false.

      Specified by:
      isFalse in interface Proposition<P>
      Returns:
      true if this proposition is immediately seen to be false; false otherwise.

    • score

      public int score()
      Returns a nonnegative measure of the syntactic complexity of this proposition.

      This implementation always returns 1.

      Specified by:
      score in interface Proposition<P>
      Returns:
      the number of literal occurrences in this proposition

    • isSatisfiedBy

      public boolean isSatisfiedBy(Set<Literal<P>> solution)
      Checks whether this proposition is satisfied by a given solution.

      This implementation is equivalent to solution.contains(this).

      Specified by:
      isSatisfiedBy in interface Proposition<P>
      Parameters:
      solution - the solution to check for satisfaction
      Returns:
      true if assuming that all literals in solution are true entails that this proposition is true; false otherwise.

    • isDisjunctionFree

      public boolean isDisjunctionFree()
      Checks whether this proposition is free of disjunctions.

      A disjunction-free proposition is satisfied by at most one solution that uses the same propositional variables.

      This implementation always returns false.

      Specified by:
      isDisjunctionFree in interface Proposition<P>
      Returns:
      true if this proposition is free of disjunctions

    • negate

      public Literal<P> negate()
      Return the negation of this literal.

      This operation is a guaranteed involution: l.negate().negate() == l always succeeds.

      Returns:
      a literal with opposite sign and identical variable.

    • equals

      public boolean equals(Object o)
      Overrides:
      equals in class Object

    • hashCode

      public int hashCode()
      Overrides:
      hashCode in class Object

    • toString

      public String toString()
      Overrides:
      toString in class Object

    • getSign

      public boolean getSign()
      Returns the logical sign of this literal.
      Returns:
      true for a positive, false for a negative literal

    • getVariable

      public P getVariable()
      Returns the propositional variable of this literal.
      Returns:
      the propositional variable of this literal

    • isConsistent

      public static <P> boolean isConsistent(Collection<Literal<P>> literals)
      Checks whether the given literals are consistent.

      A collection of literals is consistent if and only if it does not contain both a positive and a negative occurrence of the same propositional variable.

      Type Parameters:
      P - the type of propositional variables
      Parameters:
      literals - some literals
      Returns:
      true if there is some propositional variable p such that both positive(p) and negative(p) are contained in literals; false otherwise
      Throws:
      NullPointerException - is literals is null; behavior is unspecified if literals contains a null reference

    • pure

      public static <P> Set<Literal<P>> pure(Iterable<Literal<P>> literals)
      Finds the propositional variables occurring purely in some literals.

      A propositional variable occurs purely if there is either a positive or a negative occurrence, but not both.

      Type Parameters:
      P - the type of propositional variables
      Parameters:
      literals - some literals
      Returns:
      a set containing all propositional variables p such that either positive(p) or negative(p), but not both, are contained in literals
      Throws:
      NullPointerException - is literals is null; behavior is unspecified if literals contains a null reference