Package org.tweetyproject.logics.pl.syntax

Class CardinalityConstraint

java.lang.Object

org.tweetyproject.logics.pl.syntax.PlFormula

org.tweetyproject.logics.pl.syntax.CardinalityConstraint

All Implemented Interfaces:

Formula, ClassicalFormula, Conjunctable, Disjunctable, Invertable, ProbabilityAware, SimpleLogicalFormula

public class CardinalityConstraint
extends PlFormula

This class represents a cardinality constraint, i.e. a constraint of the form "at most n out of {a1,...,ak} are true", where a1 ... ak are propositions and n is an integer. It also includes methods that generate SAT encodings for cardinality constraints.

Author:

Anna Gessler

Constructor Summary

Constructors

Constructor	Description
CardinalityConstraint(java.util.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
PlFormula	clone()	Creates a deep copy of this formula
PlFormula	collapseAssociativeFormulas()	This method collapses all associative operations appearing in this term, e.g.
boolean	equals(java.lang.Object obj)
java.util.Set<Proposition>	getAtoms()	Processes the set of all atoms which appear in this formula
static PlBeliefSet	getBinomialEncoding(java.util.Collection<Proposition> atoms, int atMost)	Returns a naive SAT encoding of the given cardinality constraint.
java.util.Set<PlFormula>	getLiterals()	Returns all literals, i.e.
java.util.Set<PossibleWorld>	getModels(PlSignature sig)	Returns the set of models of this formula wrt.
static Conjunction	getNaiveAtMostOneEncoding(java.util.Collection<Proposition> atoms)	Returns a naive at-most-1 encoding for the given set of atoms.
java.util.Set<PlPredicate>	getPredicates()	Processes the set of all predicates which appear in this formula
PlBeliefSet	getSatEncoding()	Returns a SAT encoding of this cardinality constraint.
PlBeliefSet	getSatEncoding(java.lang.String name)	Returns a SAT encoding of this cardinality constraint.
static PlBeliefSet	getSequentialCounterEncoding(java.util.Collection<Proposition> atoms, int atMost, java.lang.String name)	Returns a SAT encoding of the given cardinality constraint based on the method of [Sinz.
int	hashCode()
int	numberOfOccurrences(Proposition p)	Returns the number of occurrences of the given proposition within this formula
CardinalityConstraint	replace(Proposition p, PlFormula f, int i)	Replaces the ith instance of the proposition p by f.
Conjunction	toCnf()	This method returns this formula in conjunctive normal form (CNF).
PlFormula	toNnf()	This method returns this formula in negation normal form (NNF).
java.lang.String	toString()
PlFormula	trim()	Removes duplicates (identical formulas) from conjunctions and disjunctions and removes duplicate negations.

Methods inherited from class org.tweetyproject.logics.pl.syntax.PlFormula

combineWithAnd, combineWithOr, complement, getModels, getPredicateCls, getPrimeImplicants, getSignature, getUniformProbability, isClause, isConjunctiveClause, isLiteral, resolvableWith, resolveWith, toBlakeCanonicalForm, toDnf

Methods inherited from class java.lang.Object

getClass, notify, notifyAll, wait, wait, wait

Constructor Detail

CardinalityConstraint

public CardinalityConstraint(java.util.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 Detail

getSatEncoding

public PlBeliefSet getSatEncoding(java.lang.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(java.util.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(java.util.Collection<Proposition> atoms,
                                                       int atMost,
                                                       java.lang.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(java.util.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

getAtoms

public java.util.Set<Proposition> getAtoms()

Description copied from interface: SimpleLogicalFormula

Processes the set of all atoms which appear in this formula

Specified by:

getAtoms in interface SimpleLogicalFormula

Specified by:

getAtoms in class PlFormula

Returns:

The set of all atoms

getLiterals

public java.util.Set<PlFormula> getLiterals()

Description copied from class: PlFormula

Returns all literals, i.e. all formulas of the form "a" or "!a" where "a" is a proposition, that appear in this formula.

Specified by:

getLiterals in class PlFormula

Returns:

all literals appearing in this formula.

collapseAssociativeFormulas

public PlFormula collapseAssociativeFormulas()

Description copied from class: PlFormula

This method collapses all associative operations appearing in this term, e.g. every a||(b||c) becomes a||b||c.

Specified by:

collapseAssociativeFormulas in class PlFormula

Returns:

the collapsed formula.

getPredicates

public java.util.Set<PlPredicate> getPredicates()

Description copied from interface: SimpleLogicalFormula

Processes the set of all predicates which appear in this formula

Specified by:

getPredicates in interface SimpleLogicalFormula

Specified by:

getPredicates in class PlFormula

Returns:

all predicates that appear in this formula

trim

public PlFormula trim()

Description copied from class: PlFormula

Removes duplicates (identical formulas) from conjunctions and disjunctions and removes duplicate negations. Simplifies equivalences and implications with equivalent formulas (A=>A, A<=>A) to tautologies.

Specified by:

trim in class PlFormula

Returns:

an equivalent formula without duplicates.

toNnf

public PlFormula toNnf()

Description copied from class: PlFormula

This method returns this formula in negation normal form (NNF). A formula is in NNF iff negations occur only directly in front of a proposition.

Specified by:

toNnf in class PlFormula

Returns:

the formula in NNF.

toCnf

public Conjunction toCnf()

Description copied from class: PlFormula

This method returns this formula in conjunctive normal form (CNF). A formula is in CNF iff it is a conjunction of disjunctions and in NNF. The CNF generated by this method is not necessarily minimal.

Specified by:

toCnf in class PlFormula

Returns:

the formula in CNF.

getModels

public java.util.Set<PossibleWorld> getModels(PlSignature sig)

Description copied from class: PlFormula

Returns the set of models of this formula wrt. the given signature.

Specified by:

getModels in class PlFormula

Parameters:

sig - some propositional signature

Returns:

the set of models of this formula wrt. the given signature.

numberOfOccurrences

public int numberOfOccurrences(Proposition p)

Description copied from class: PlFormula

Returns the number of occurrences of the given proposition within this formula

Specified by:

numberOfOccurrences in class PlFormula

Parameters:

p - some proposition

Returns:

the number of occurrences of the given proposition within this formula

replace

public CardinalityConstraint replace(Proposition p,
                                     PlFormula f,
                                     int i)

Description copied from class: PlFormula

Replaces the ith instance of the proposition p by f.

Specified by:

replace in class PlFormula

Parameters:

p - some proposition

f - some formula

i - the index of the proposition

Returns:

a new formula with the ith instance of the proposition p replaced by f.

equals

public boolean equals(java.lang.Object obj)

Specified by:

equals in interface SimpleLogicalFormula

Specified by:

equals in class PlFormula

hashCode

public int hashCode()

Specified by:

hashCode in interface SimpleLogicalFormula

Specified by:

hashCode in class PlFormula

clone

public PlFormula clone()

Description copied from interface: SimpleLogicalFormula

Creates a deep copy of this formula

Specified by:

clone in interface SimpleLogicalFormula

Specified by:

clone in class PlFormula

Returns:

the cloned formula

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object