A Framework for Hybrid Set-Theoretic and Numerical Problem Solving

In formal methods, checking the validity of some proof obligations results in reasoning about sets, and particularly their interrelations and their cardinalities. Motivated by this interest, we investigate hybrid problems that combine constraints from both aspects. In this context, we consider two approaches: one purely qualitative and one explicitly representing membership. We propose SAT-based encodings for solving these problems. First we encode qualitative constraints on relations between sets and their cardinalities. Afterwards, we deal with richer constraints on set elements and with numerical constraints on both cardinalities and integer variables, assuming a fixed domain. In this setting, we identify a domain size bound for the version with explicit membership, beyond which increasing the domain cannot affect satisfiability. We evaluate the proposed encodings on real-world B language specifications. The proposed approaches allow the validation of proofs not yet decided by several existing approaches, and so could be used in addition to the others in order to automate the validation of even more proofs.