A method, apparatus and product for encoding a cardinality constraint in Conjunctive Normal Form (CNF). The method comprising: having a Boolean formula comprising a cardinality constraint, wherein the cardinality constraint relating to a set of Boolean variables, the set of variables consisting of N variables, the cardinality constraint given in a non-Conjunctive Normal Form; and encoding the cardinality constraint in Conjunctive Normal Form based on a mapping by a Perfect Hash Family, whereby said memory is modified to retain the CNF encoded cardinality constraint.