# Integrating Cardinality Constraints into Constraint Logic Programming with Sets

arXiv: https://arxiv.org/abs/2102.05422 · HTML: https://mlsanity.com/paper/2102.05422/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 10 Feb 2021.

## Built on by (most cited first, 1 of 1)

- [Complexity assessments for decidable fragments of Set Theory. IV: A quadratic reduction of constraints over nested sets to Boolean formulae](https://mlsanity.com/paper/2112.04797/) (2021)

## Abstract (arXiv)

Formal reasoning about finite sets and cardinality is an important tool for many applications, including software verification, where very often one needs to reason about the size of a given data structure and not only about what its elements are. The Constraint Logic Programming tool {log} provides a decision procedure for deciding the satisfiability of formulas involving very general forms of finite sets, without cardinality. In this paper we adapt and integrate a decision procedure for a theory of finite sets with cardinality into {log}. The proposed solver is proved to be a decision procedure for its formulas. Besides, the new CLP instance is implemented as part of the {log} tool. In turn, the implementation uses Howe and King's Prolog SAT solver and Prolog's CLP(Q) library, as an integer linear programming solver. The empirical evaluation of this implementation based on +250 real verification conditions shows that it can be useful in practice.