Adding cardinality constraints to integer programs with applications to maximum satisfiability