Class CardinalityConstraintEncoder

java.lang.Object
org.tweetyproject.logics.pl.util.CardinalityConstraintEncoder

public class CardinalityConstraintEncoder extends Object
This class generates SAT encodings for cardinality constraints. A cardinality constraint is a constraint of the form "at most n out of {a1,...,ak} are true", where a1 ... ak are propositions and n is an integer.
Author:
Anna Gessler
  • Constructor Details

    • CardinalityConstraintEncoder

      public CardinalityConstraintEncoder(Collection<Proposition> atoms, int atMost)
      Create a new at-most-n cardinality constraint with the given set of atoms and the given n.
      Parameters:
      atoms - the atoms
      atMost - n
  • Method Details

    • getSatEncoding

      public PlBeliefSet getSatEncoding(String name)
      Returns a SAT encoding of this cardinality constraint.
      Parameters:
      name - prefix for auxiliary variables
      Returns:
      encoding
    • getSatEncoding

      public PlBeliefSet getSatEncoding()
      Returns a SAT encoding of this cardinality constraint.
      Returns:
      encoding
    • getBinomialEncoding

      public static PlBeliefSet getBinomialEncoding(Collection<Proposition> atoms, int atMost)
      Returns a naive SAT encoding of the given cardinality constraint.
      Parameters:
      atoms - the atoms
      atMost - the maximal number of true atoms
      Returns:
      sat encoding
    • getSequentialCounterEncoding

      public static PlBeliefSet getSequentialCounterEncoding(Collection<Proposition> atoms, int atMost, String name)
      Returns a SAT encoding of the given cardinality constraint based on the method of [Sinz. "Towards an Optimal {CNF} Encoding of Boolean Cardinality Constraints." Principles and Practice of Constraint Programming, Springer 2005].
      Parameters:
      atoms - the atoms
      atMost - the maximal number of true atoms
      name - for auxiliary variables
      Returns:
      SAT encoding of constraint
    • getNaiveAtMostOneEncoding

      public static Conjunction getNaiveAtMostOneEncoding(Collection<Proposition> atoms)
      Returns a naive at-most-1 encoding for the given set of atoms.
      Parameters:
      atoms - the atoms
      Returns:
      at-most-1 encoding
    • equals

      public boolean equals(Object obj)
      Overrides:
      equals in class Object
    • hashCode

      public int hashCode()
      Overrides:
      hashCode in class Object
    • toString

      public String toString()
      Overrides:
      toString in class Object