In this paper we present Cardinal, a general finite sets constraint solver just made publicly available in ECLiPSe Constraint System, suitable for combinatorial problem solving by exploiting inferences over sets cardinality. In fact, to deal with set variables and set constraints, existing set constraint solvers are not adequate to handle a number of problems, as they do not actively use important information about the cardinality of the sets, a key feature in such problems.Cardinal is formally presented as a set of rewriting rules on a constraint store and we illustrate its efficiency with experimental results. We show the importance of propagating constraints on sets cardinality, by comparingCardinalwith other solvers. Another contribution of this paper is on modelling: we focus essentially on digital circuits problems, for which we present new modelling approaches and prove that sets alone can be used to model these problems in a clean manner and solve them efficiently using Cardinal. Results on a set of diagnostic problems show that Cardinal obtains a speed up of about two orders of magnitude over Conjunto, a previous available set constraint solver, which uses a more limited amount of constraint propagation on cardinalities. Additionally, to further extend modelling capabilities and efficiency, we generalized Cardinal to actively consider constraints over set functions other than cardinality. The Cardinal version just released allows declaring union, minimum and maximum functions on set variables, and easily constraining those functions, letting Cardinal especial inferences efficiently take care of different problems. We describe such extensions and discuss its potentialities, which promise interesting research directions.