This is QMaxSAT with modulo totalizer using glucose2.0.
Modulo totalizer is a novel encoding for cardinality constraints.