Add more encodings for cardinality constraints

[Lipen]

As the title says, we need to provide more encodings for cardinality constraints (of the form k_min <= \sum(lit) <= k_max). Currently, only Totalizer [1] encoding is implemented, but are many others (e.g., sorting networks), which might be even more efficient (at least, for some problems).
[1] O. Bailleux and Y. Boufkhad, “Efficient CNF encoding of Boolean cardinality constraints,” in Principles and Practice of Constraint Programming, 2003, pp. 108–122. doi: 10.1007/978-3-540-45193-8_8.

The starting points for research:

• https://pysathq.github.io/docs/html/api/card.html
• https://github.com/liffiton/minicard