Efficient Encodings of Conditional Cardinality Constraints
  In the encoding of many real-world problems to propositional satisfiability,
the cardinality constraint is a recurrent constraint that needs to be managed
effectively. Several efficient encodings have been proposed while missing that
such a constraint can be involved in a more general propositional formulation.
To avoid combinatorial explosion, Tseitin principle usually used to translate
such general propositional formula to Conjunctive Normal Form (CNF), introduces
fresh propositional variables to represent sub-formulas and/or complex
contraints. Thanks to Plaisted and Greenbaum improvement, the polarity of the
sub-formula $\Phi$ is taken into account leading to conditional constraints of
the form $y\rightarrow \Phi$, or $\Phi\rightarrow y$, where $y$ is a fresh
propositional variable. In the case where $\Phi$ represents a cardinality
constraint, such translation leads to conditional cardinality constraints
subject of the present paper. We first show that when all the clauses encoding
the cardinality constraint are augmented with an additional new variable, most
of the well-known encodings cease to maintain the generalized arc consistency
property. Then, we consider some of these encodings and show how they can be
extended to recover such important property. An experimental validation is
conducted on a SAT-based pattern mining application, where such conditional
cardinality constraints is a cornerstone, showing the relevance of our proposed
approach.
