For many classes of constraints (e.g., non-linear constraints over the integers, array constraints with quantifiers), it is undecidable whether a constraint from the given class is satisfiable (i.e., has a solution). However, one can make the problem trivially decidable by restricting all variables to finite sets, where the corresponding decision procedure can simply try all possibilities. This works well, if the cardinality of the restricting sets is small, but does not scale well to sets of bigger cardinality. The task of the thesis topic is to develop decision procedures that scale better in such a situation.