Package org.tweetyproject.logics.pl.util

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 Summary

Constructors

Constructor	Description
CardinalityConstraintEncoder(Collection<Proposition> atoms, int atMost)	Create a new at-most-n cardinality constraint with the given set of atoms and the given n.

Method Summary

Modifier and Type	Method	Description
boolean	equals(Object obj)
static PlBeliefSet	getBinomialEncoding(Collection<Proposition> atoms, int atMost)	Returns a naive SAT encoding of the given cardinality constraint.
static Conjunction	getNaiveAtMostOneEncoding(Collection<Proposition> atoms)	Returns a naive at-most-1 encoding for the given set of atoms.
PlBeliefSet	getSatEncoding()	Returns a SAT encoding of this cardinality constraint.
PlBeliefSet	getSatEncoding(String name)	Returns a SAT encoding of this cardinality constraint.
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.
int	hashCode()
String	toString()

Methods inherited from class java.lang.Object

getClass, notify, notifyAll, wait, wait, wait

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