Core-guided MaxSAT with soft cardinality constraints