2024-11-26 Encoding Cardinality Constraints in Automated Reasoning