# A Framework for Hybrid Set-Theoretic and Numerical Problem Solving

Daniel Crowley, Daniel Le Berre, Olivier Roussel, Yakoub Salhi

► To cite this version:

Daniel Crowley, Daniel Le Berre, Olivier Roussel, Yakoub Salhi. A Framework for Hybrid Set-Theoretic and Numerical Problem Solving. ICTAI, Nov 2025, Athens, Greece. hal-05342317v2

HAL Id: hal-05342317

https://cnrs.hal.science/hal-05342317v2

Submitted on 7 Nov 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# A Framework for Hybrid Set-Theoretic and Numerical Problem Solving

**Daniel Crowley**

Univ. Artois, CNRS, UMR 8188,
Centre de Recherche en Informatique de Lens (CRIL)
F-62300 Lens, France
crowley@cril.fr

**Daniel Le Berre**

Univ. Artois, CNRS, UMR 8188,
Centre de Recherche en Informatique de Lens (CRIL)
F-62300 Lens, France
leberre@cril.fr

**Olivier Roussel**

Univ. Artois, CNRS, UMR 8188,
Centre de Recherche en Informatique de Lens (CRIL)
F-62300 Lens, France
roussel@cril.fr

**Yakoub Salhi**

Univ. Artois, CNRS, UMR 8188,
Centre de Recherche en Informatique de Lens (CRIL)
F-62300 Lens, France
salhi@cril.fr

**Abstract**—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.

**Index Terms**—propositional satisfiability, problem modeling, automated reasoning, qualitative reasoning

## I. INTRODUCTION

Set theory is a pervasive and rich branch of logic and mathematics. It is multifaceted and interesting problems can arise related to many of its aspects [1]. Here we focus on combining reasoning about relationships between sets and also their sizes. We propose a problem with constraints that can handle typical operations between sets, information about element inclusion or exclusion, and restrictions on the cardinalities of sets, with respect to other cardinalities, constants and other integer variables.

Such a framework could be used widely. We concentrate, however, on how helpful it can be for validity checking in the B method, wherein sets and arithmetic are central [2]–[5].

A helpful guide for our approach are qualitative calculi [6], [7]. This work starts with purely qualitative reasoning. Qual-

itative reasoning is limited in handling size constraints, and it is not ideal for set unions or intersections. To advance while staying inspired by a qualitative algebra, we introduce a new hybrid problem with qualitative aspects but without being bound to that framework by reasoning explicitly about sets' members while closely monitoring the interset standing.

We propose additionally our own solution to this new problem. This solution is SAT-based [8]. SAT encoding is a popular choice for dealing with hard combinatorial problems, including qualitative reasoning [9]. Again we take advantage of others' developments, but our encoding does not follow trivially from what has already been done. Totally within SAT, we encode cardinalities in such a way that many cardinalities can be enforced with one collection of constraints and auxiliary variables. Another novelty appears when composing set sizes with other scalar values. Difference graphs without negative cycles are traditionally models of such problems [10]. Incremental SAT solving is a known tactic for avoiding cycles [11]. In this work, we handle specific difference graphs with negative cycles to only solve a SAT instance once.

The rest of the article continues as follows. Section II introduces a concrete example of how the proposed framework can be applied to real-world problems, and Section III fleshes out the concepts required for the understanding of the contribution. Section IV revisits and introduces two set-theoretic frameworks, before Section V advances to describe their SAT encoding. Finally, before the paper concludes, Section VI presents some empirical results of using these frameworks.

## II. MOTIVATION

An important step in verifying system specifications using the B method [2]–[5] is that of discharging Proof Obligations (POs) generated from machines such as the simple example in Fig. 1.

Machines are verified by proving that every PO's goal is entailed by its hypotheses. A successful instantiation of the

<footnote>This work was funded by the project Enhancing B Language Reasoners Using SAT and SMT (BLaSST), ANR-21-CE25-0010.</footnote>
<figure><img src="image_2.png" /><figcaption>Fig. 1. Example of a B Machine</figcaption></figure>

conjunction of all the hypotheses and the negation of the goal is a counterexample to an invalid PO. Tools indicate which POs are not yet proved, but often do not show a counterexample to the user.

As concrete examples, let us look at two POs that are generated from the machine in Fig. 1 in order to guarantee that invariants hold after `AddToC1`. Both have the same set of hypotheses: $H = \{(CM \subseteq \mathbb{N}), (C_1 \subseteq CM), (C_2 \subseteq CM), (C_1 \cap C_2 = \emptyset), (ss \in CM), (ss \notin C_1)\}$, and the goals are $g_1 = C_1 \cup \{ss\} \subseteq CM$ and $g_2 = (C_1 \cup \{ss\}) \cap C_2 = \emptyset$. We confirm the validity of the first PO by determining the unsatisfiability of $(\bigwedge_{h \in H} (h)) \wedge \neg g_1$ and the invalidity of the second by producing a model of $(\bigwedge_{h \in H} (h)) \wedge \neg g_2$. There are denumerable countermodels of this second claim, wherever $C_1$ and $C_2$ are disjoint subsets of $CM$, itself a subset of $\mathbb{N}$, and $ss$ is in $C_2$; e.g., $CM = \{0, 1, 2, 3, 4, 5\}, C_1 = \{0, 1\}, C_2 = \{2, 3, 4\}, ss = 2$ is a countermodel because all $hs$ in $H$ are satisfied and $\{0, 1, 2\} \cap \{2, 3, 4\} \neq \emptyset$.

In the B method, POs are made up of expressions of set theory, functions, arithmetic, or first order logic. POs can be dealt with in different ways; atelierB [12] does so by applying native B method rewriting rules, ProB [13] benefits from Constraint Logic Programming (CLP) [14], and one can even translate POs to other languages such as SMT-LIB [15], the TPTP format [16], or Why3 [17] to use SMT or ATP software [18], [19]. SAT encodings too are widely used in formal methods. A notable example of this fact is its use for model checking [20].

Considering the requirements of the B method and the opportunities of SAT, we propose set-oriented constraint satisfaction problems that are encodable in SAT to check POs. Other frameworks have already been put forward to handle set constraints, such as Conjunto [21] and $\{\log\}$ [22]–[24]. The focus on set extensions in $\{\log\}$ is the closer of the two to this work’s approach, and it has even been conceived of applying it to B POs, but to animate them rather than to practically prove them [25]. It also differs in its outline and implementation as our problems will put more emphasis on relations between sets and our solution will utilize SAT instead of constraint logic programming. SAT has been used by [26] to reason about sets, but without qualitative inspiration, and with fewer numeric constraints.

### III. BACKGROUND

#### A. Boolean Satisfiability

The choice to solve a problem by encoding it as a Boolean Satisfiability Problem (SAT) follows that of many since it was discovered that SAT is NP-complete [27]–[29], and thanks to the advances in solvers’ performances, especially due to breakthroughs at the turn of the century [30], [31].

We will refer to Boolean variables with Roman letters such as $p, q$, or $s$. A formula $\phi$, if simple, is a constant $\top$ or $\bot$ or a variable $p$, or, if complex, a composition of direct subformulas $\psi$ and $\psi'$, $\neg\psi$ or $\psi \circ \psi'$ for a binary connective $\circ$ in $\{\top, \bot, \rightarrow, \leftrightarrow\}$. An interpretation $\omega$ assigns to each variable $p$ one value from the domain of either 1 or 0.

A literal is a variable $p$ or its negation $\neg p$. A disjunction of literals makes up a clause, and can be expressed as its literals’ set. A formula in Conjunctive Normal Form (CNF) is a conjunction of clauses, again treatable as a set. Any propositional formula can be tractably transformed into CNF while preserving its satisfiability [32]. We extend $\omega$ to formulas such that the assignment of a negative literal $\omega(\neg p)$ is 1 iff the assignment of the literal’s variable $\omega(p)$ is 0. A clause $c = \{l_1, \dots, l_n\}$ is satisfied iff at least one of its literals is assigned to 1, and the whole formula $\phi = \{c_1, \dots, c_m\}$ is satisfied by $\omega$ iff all of its clauses are satisfied. The goal of SAT—determining the satisfiability of $\phi$—amounts, then, to settling the existence of such an $\omega$.

#### B. Qualitative Spatial and Temporal Reasoning

Qualitative reasoning is a framework that descends from relation algebra discovered by De Morgan, Peirce, Schröder, and Tarski [33]. Given a Qualitative Constraint Network (QCN) of entities, a satisfiability problem consists of deciding whether a set $U$ of jointly exhaustive and pairwise disjoint relations can consistently hold among the entities [7], [34]. Every relation has an inverse relation, and every calculus is subject to a composition table [35] laying out the possible values for $xRz$ when $xPy \wedge yQz$ holds, limited to the base relations and tidily denoted $x(P \diamond Q)z$.

**Definition 1:** A QCN over a domain $D$ and a set $U$ of base relations is a couple $Q = \langle V, C \rangle$, where

* $V$ is a set of variables over $2^D$,

* $C: V \times V \rightarrow 2^U$ maps each pair of variables to the subset of $U$ allowed between them.

For instance, the Region Connection Calculus (RCC) [36] (with five relations (RCC5)) takes as entities topological regions in space, and relations determine how these regions interact with each other. Because of how well it models subsethood, RCC5 is also named “containment algebra” [37]. Its five base relations are equality (EQ), proper subsethood ($\subset$), proper supersethood ($\supset$), having a non-empty intersection (OV for overlap), and being disjoint (DR).<fnref n="1" /> We will refer to $\{EQ, \subset, \supset, OV, DR\}$ as $U_{RCC5}$. EQ, OV, and DR are each their own inverse, and $\subset$ and $\supset$ are the inverses of each other.

<footnote n="1">¹The symbols $\subset$, $\supset$, and OV are not typically used in the literature, but $\subset$ and $\supset$ make our intentions clear, and OV does not clash with B’s PO.</footnote>
RCC5's composition table can be found in [37] or [38]. In the style of [39], [40], RCC5 can be used along with further constraints of equality (=), strict inferiority (<) and strict superiority (>) on relative sizes. {$=, <, >$} will take the name $U_{\text{Card}}$. In the sequel, unless specified otherwise, such paired calculi are the QCNs we refer to, and the interdependencies between relations and size can be found in [41].

There are specific means for natively solving QCNs [42]–[47], but translating to SAT is also a popular approach [9].

## IV. SET-THEORETIC FRAMEWORKS

For handling sets, we first explore a purely qualitative approach, before turning our attention to a hybrid alternative which allows for more constraints regarding unions and intersections and comparison with integers but requires more care about domain size bounds.

### A. Purely Qualitative Reasoning-Based Approach

It is clear that a QCN can handle many basic set operations and relative cardinality comparison. Less obvious is the fact that there can also be constraints regarding elementhood. This can be seen by imagining a slightly different problem, a Membership-QCN (M-QCN) which extends a QCN without size pairing by allowing specific atoms to belong (or not) to sets.

**Definition 2:** An M-QCN over a domain D and base relations $U_{\text{RCC5}}$ is a tuple $\mathcal{M} = \langle V_s, V_e, C, M \rangle$, where

* $\langle V_s, C \rangle$ is a QCN over D and $U_{\text{RCC5}}$ ($V_s$ consists of set variables of $2^D$),

* $V_e$ is a set of variables over D ($V_e$ consists of element variables), and

* $M: V_e \times V_s \to 2^{\{\notin, \in\}} \setminus \{\emptyset\}$ is a mapping that specifies, for each $a \in V_e$ and for each variable $X \in V_s$, which membership relations are allowed between $a$ and $X$.

For all M-QCN there is an equisatisfiable QCN with more region variables and qualitative constraints and without $M$.

**Theorem 1:** Over some domain D and $U_{\text{RCC5}}$, an M-QCN $\mathcal{M}$ with constraints $C$ is consistent iff the QCN $\mathcal{N} = \langle V_s \cup \{X_a : a \in V_e\}, C' \rangle$ is consistent, where for all $a \in V_e$:

* $X_a$ is a fresh variable, distinct from all variables in $V_s$.

* For all $X \in V_s$:

$$ C'(X_a, X) = \begin{cases} \{\text{EQ}, \subset\} & \text{if } M(a, X) = \{\in\}, \\ \{\text{DR}\} & \text{if } M(a, X) = \{\notin\}, \\ \{\text{EQ}, \subset, \text{DR}\} & \text{if } M(a, X) = \{\in, \notin\}. \end{cases} \quad (1) $$

**Sketch 1:** The proof is omitted for lack of space. Intuitively, $a \in S$ is replaced by $X_a \subseteq S$ and $a \notin S$ by $X_a \cap S = \emptyset$. $X_a$ may contain other elements than $a$, but these are not relevant. □

RCC5, then, is quite apt for reasoning about interset containment and elementhood.

In B, there are also expressions about functions (e.g., asserting the existence of an injection between two sets). QCNs can partially encode some of these requirements, most notably regarding comparative sizes. For example, from the

existence of a bijection between sets X and Y we can deduce that $|X| = |Y|$.

For the first PO coming from the example in Fig. 1, we translate to a QCN with $V = \{C_1, C_1 \cup \{ss\}, C_2, CM, \{ss\}\}$ and $C = \{\langle C_1, CM \rangle \mapsto \{\text{EQ}, \subset\}, \langle C_1, C_1 \cup \{ss\} \rangle \mapsto \{\text{EQ}, \subset\}^*, \langle C_1, C_2 \rangle \mapsto \{\text{DR}\}, \langle C_1, CM \rangle \mapsto \{\text{EQ}, \subset\}, \langle C_1, \{ss\} \rangle \mapsto \{\text{DR}\}, \langle C_1 \cup \{ss\}, CM \rangle \mapsto \{\supset, \text{OV}, \text{DR}\}^\dagger, \langle C_1 \cup \{ss\}, \{ss\} \rangle \mapsto \{\text{EQ}, \supset\}^*, \langle C_2, CM \rangle \mapsto \{\text{EQ}, \subset\}, \langle CM, \{ss\} \rangle \mapsto \{\text{EQ}, \supset\}\}$

where constraints with * are approximations of required constraints and the one with $^\dagger$ negates $\subseteq$ by mapping to its complement in $U_{\text{RCC5}}$. Any pair of sets not yet specified is mapped to $U_{\text{RCC5}}$ by default, and because no cardinality comparisons appear in this example, all pairs of sets begin with all three size relations in their domains.

### B. Hybrid Qualitative-Numerical Framework

QCNs are already a start on proving POs. As expected, there are many POs that cannot be encoded using QCNs. Some of these, for example, regard comparing the cardinality of sets with constant or variable integers, and set operations such as unions and intersections are not yet handled perfectly. As a remedy, we drop the purely qualitative nature of QCNs. We include new integer variables that were unavailable to QCNs and define the Set Discovery Problem (SDP) for finding the content of sets satisfying constraints.

**Definition 3:** An SDP over D and U is defined as a tuple $Q = \langle V_s, V_i, \kappa, C, \Delta, \mathcal{P} \rangle$, where:

* $V_s$ (set variables) is a set of variables each ranging over $2^D$,

* $V_i$ (integer variables) is a set of variables each ranging over integers,

* $\kappa$ (constant sets) is a collection of finite subsets of D,

* $C$ is a partial mapping from $(V_s \cup \kappa) \times (V_s \cup \kappa)$ to $2^U$, representing the binary relations between sets,

* $\Delta$ is a collection of n-ary composition constraints with variables $s_i$ from $V_s \cup \kappa$ requiring either that $s_n = s_1 \cup \dots \cup s_{n-1}$ or that $s_n = s_1 \cap \dots \cap s_{n-1}$,

* $\mathcal{P}$ is a set of difference constraints (DC) involving combinations of integer variables from $V_i$ and/or cardinalities of set variables from $V_s$. These constraints are of form $v_1 - v_2 \le \alpha$, $0 - v \le \alpha$, or $v - 0 \le \alpha$, where a $v$ is either a variable in $V_i$ or $\text{card}(S)$, the cardinality of a set $S \in V_s$.

A solution to an SDP $\langle V_s, V_i, \kappa, C, \Delta, \mathcal{P} \rangle$ consists of an ordered pair of assignments $\sigma = \langle \sigma_s, \sigma_i \rangle$ with $\sigma_s : (V_s \cup \kappa) \to 2^D$ and $\sigma_i : V_i \to \mathbb{Z}$ such that:

* The assignment $\sigma_s$ must satisfy all the constraints in C and $\Delta$, meaning:

- For each pair of variables $x, y \in V_s \cup \kappa$, the relationship defined by $C(x, y)$ must hold between $\sigma_s(x)$ and $\sigma_s(y)$.

- For each n-tuple $\langle x_1, \dots, x_n \rangle \in (V_s \cup \kappa)^n$ that occurs in a constraint $\delta \in \Delta$, the sets $\sigma_s(x_1), \dots, \sigma_s(x_n)$
must satisfy rel, the relation called for by $\delta$. For example, if rel = union, then $\sigma_s(x_1) \cup \dots \cup \sigma_s(x_{n-1}) = \sigma_s(x_n)$.

* The set of constraints $\mathcal{P}$ must also be satisfied under $\sigma$, which implies:

- For each DC $x - y \le \alpha$, it must be true that $\tau(x) - \tau(y) \le \alpha$, where $\tau(z)$ denotes

$$ \left\{ \begin{array}{ll} \sigma_i(z), & \text{if } z \in V_i, \\ |\sigma_s(z')|, & \text{if } z \text{ is card}(z') \text{ and } z' \in V_s \cup \kappa, \text{ or} \\ 0, & \text{if } z \text{ is zero.} \end{array} \right. $$

As in the previous Subsection, we observe a translation of the first PO from Fig. 1. In this instance, $V_i$ and $\mathcal{P}$ can be empty, $V_s = \{C_1, C_2, CM, Un\}$ (Un representing the union of $C_1$ and $\{ss\}$), $\kappa = \{\{ss\}\}$, $C = \{(C_1, C_2) \mapsto \{DR\}, \langle C_1, CM \rangle \mapsto \{\subseteq\}, \langle C_1, \{ss\} \rangle \mapsto \{DR\}, \langle C_2, CM \rangle \mapsto \{\subseteq\}, \langle CM, Un \rangle \mapsto \{\subseteq\}, \langle CM, \{ss\} \rangle \mapsto \{\supseteq\}\}$, and $\Delta$ consists solely of $Un = C_1 \cup \{ss\}$.

## V. SAT ENCODINGS

Next we lay out a way to translate QCN and SDP into SAT instances.

When encoding a QCN into SAT, we treat the relations between sets as primitive. In the sequel, $V$ will denote $V$ in QCN and $V_s \cup \kappa$ in SDP. To break symmetries, we also fix an ordering on the elements of $V$, and in the case of SDP each element of $V_s$ precedes all those of $\kappa$. We refer then to the $i^{th}$ element of $V$ as $S_i$. As in the 1-D support encoding [9], we present each base relation $b$ between each pair $\langle S_i, S_j \rangle$, $i < j$, with a separate propositional variable $p_{ij}^b$.

To encode a QCN, each pair of sets has a $p_{ij}^b$ for each $v \in \mathcal{U}_{RCC5} \cup \mathcal{U}_{Card}$. For consistency, it would suffice that at least one relation hold in each part, but we follow [9] in seeking an exact instantiation of the network by enforcing that exactly one of the relations hold per calculus. We encode the following, assuming some order over both Us. Many encodings for cardinality constraints are known [48].

$$ \bigwedge_{1 \le i < j \le |V|} \left( \sum_{b \in \mathcal{U}} (p_{ij}^b) = 1 \right), \quad \text{for } \mathcal{U} \in \{\mathcal{U}_{RCC5}, \mathcal{U}_{Card}\} \quad (2) $$

The composition table and other constraints specific to the instance of QCN are encoded by a collection of conditions [9]. For $\mathcal{U}_{RCC5}$ and $\mathcal{U}_{Card}$ separately:

$$ \bigwedge_{1 \le i < j < k \le |V|} \left( \bigwedge_{b \in \mathcal{C}(S_i, S_j), b' \in \mathcal{C}(S_j, S_k)} \left( p_{ij}^b \wedge p_{jk}^{b'} \rightarrow \bigvee_{b'' \in \mathit{comp}} (p_{ik}^{b''}) \right) \right), \quad (3) $$

where $comp = b \diamond b' \cap \mathcal{C}(S_i, S_k)$.

The effect of RCC5 on size is encoded with $p_{ij}^c \rightarrow p_{ij}^<, p_{ij}^> \rightarrow p_{ij}^>$, and $p_{ij}^{\text{EQ}} \rightarrow p_{ij}^{\equiv}$. In the other direction, each size relation rules out some RCC5 relations. Although derivable from (2) and from the first direction, to facilitate propagation

by the SAT solver, we also encode $p_{ij}^< \rightarrow \neg p_{ij}^>$, $p_{ij}^> \rightarrow \neg p_{ij}^c$, and $p_{ij}^{\equiv} \rightarrow \neg p_{ij}^> \wedge \neg p_{ij}^c$.

To encode an SDP, each pair of sets requires five $p_{ij}^b$ (with $b \in \mathcal{U}_{RCC5}$), and (2) is enforced on them. To reason directly about membership, for each set $S_i$ in $V$ we introduce $|D|$ propositional variables $q_j^i$, each true iff the $j^{th}$ element $D$ is a member of $S_i$. The elements of pairs of sets are constrained to reflect the required RCC5 relations.

Subsets and supersets mirror each other. The relation of being a proper subset is encoded with:

$$ p_{ij}^{\le} \rightarrow \left( \bigwedge_{k=1}^{|D|} (q_k^i \rightarrow q_k^j) \wedge \left( \bigvee_{k=1}^{|D|} (\neg q_k^i \wedge q_k^j) \right) \right) \quad (4) $$

This rule can be interpreted as saying that whenever a set $S_i$ is a proper subset of another $S_j$, every one of its elements is an element of $S_j$ and $S_j$ has at least one other element.

The encoding of equal sets requires that every element of the domain occurs in the first set iff it occurs in the second, that is,

$$ p_{ij}^{\text{EQ}} \rightarrow \left( \bigwedge_{k=1}^{|D|} (q_k^i \leftrightarrow q_k^j) \right). \quad (5) $$

When there is an overlap between sets, the intersection must be non-empty and the two relative complements likewise.

$$ p_{ij}^{\text{OV}} \rightarrow \left( \left( \bigvee_{k=1}^{|D|} (q_k^i \wedge q_k^j) \right) \wedge \left( \bigvee_{k=1}^{|D|} (q_k^i \wedge \neg q_k^j) \right) \right) \wedge \left( \bigvee_{k=1}^{|D|} (\neg q_k^i \wedge q_k^j) \right) \quad (6) $$

Finally, disjointness is encoded by specifying that the sets have no element in common, and that neither be empty, as in:

$$ p_{ij}^{\text{DR}} \rightarrow \left( \bigwedge_{k=1}^{|D|} (\neg q_k^i \vee \neg q_k^j) \wedge \bigvee_{k=1}^{|D|} (q_k^i) \wedge \bigvee_{k=1}^{|D|} (q_k^j) \right) \quad (7) $$

The encodings of the two types of n-ary constraints in $\Delta$ differ from one another in whether one side has a conjunction or a disjunction:

$$ \begin{align} S_n &= S_1 \cup \dots \cup S_{n-1} \rightarrow \bigwedge_{k=1}^{|D|} \left( q_k^n \leftrightarrow \bigvee_{i=1}^{n-1} (q_i^k) \right) \tag{8} \\ S_n &= S_1 \cap \dots \cap S_{n-1} \rightarrow \bigwedge_{k=1}^{|D|} \left( q_k^n \leftrightarrow \bigwedge_{i=1}^{n-1} (q_i^k) \right) \nonumber \end{align} $$

## A. Single Sequential Counter

Finally, we need also to encode the difference constraints (DCs) in $\mathcal{P}$. When it comes to the cardinality of sets, thanks to the unary encoding of elements, we can apply techniques for calculating cardinality constraints on propositional variables. There are many ways to encode such constraints [48], but we elect the sequential counter encoding [49]. As originally put forth, this encoding ensures that the cardinality does not
exceed a known amount $\alpha$ by means of $2|D|\alpha + |D| + \alpha - 1$ clauses and $|D|^2 - |D|$ auxiliary variables. For each considered $\alpha$, a whole new encoding is required. We modify this encoding so that there is an equivalence instead of a unidirectional implication between variables and cardinalities, and it is sufficient to add unary clauses to the encoding in order to enforce different bounds.

This encoding requires the introduction of fresh propositional variables. Every set $S_i$ gets $\frac{|D|^2+|D|}{2} - 1$ variables $s_{j,k}^i$, each of which is true iff $S_i$ includes at least $k$ of the first $j$ elements of $D$. The elements are then bound to their cardinalities with the following rules:

$$ (s_{1,1}^i \leftrightarrow q_1^i) \wedge \bigwedge_{k=1}^{|D|-1} (\neg s_{k,k+1}^i), \quad \bigwedge_{j=2}^{|D|} (s_{j,1}^i \leftrightarrow (q_j^i \lor s_{j-1,1}^i)), \\ \text{and} \\ \bigwedge_{j=2}^{|D|} \left( \bigwedge_{k=2}^j \left( s_{j,k}^i \leftrightarrow \left( (q_j^i \land s_{j-1,k-1}^i) \lor s_{j-1,k}^i \right) \right) \right). $$

Intuitively, the first part ensures that a variable $s_{1,1}^i$ is true iff $S_i$ includes the first element of the domain, and that it is impossible for the cardinality of a single element to be greater than 1. From the second part, $s_{j,1}^i$ is true iff $s_{j',1}^i$ is for some earlier $j'$ or the $j^{th}$ element itself is included. The third commands that $s_{j,k}^i$ is true iff at least $k$ of the previous $j-1$ elements were already included or at least $k-1$ were included and the $j^{th}$ is included.

DCs between the size of a set $v_i$ and zero can be enforced with unary clauses with a positive literal for at least and the subsequent negative literal for at most 2:

$$ \mathrm{card}(v_i) \ge k \rightsquigarrow s_{|D|,k}^i, \quad \mathrm{card}(v_i) \le k \rightsquigarrow \neg s_{|D|,k+1}^i. \qquad (9) $$

A DC on two cardinalities for a non-negative $k$ below $|D|$ can be asserted without loss of generality with the following.

$$ \mathrm{card}(v_i) - \mathrm{card}(v_j) \le k \rightsquigarrow \bigwedge_{l=k+1}^{|D|} \left( s_{|D|,l}^i \rightarrow s_{|D|,l-k}^j \right) \quad (10) $$

For $S_{|D|}$, there are $|D|$ variables, $s_{|D|,k}^i$, and for all $S_j$ from 1 to $|D| - 1$, there are $j + 1$. The $2|D|^2 + 6|D| - 2$ clauses in this adaption of [49] are more numerous than those required for the original sequential encoding, but still of the same order (when $\alpha = |D|$) and fortunately they can be reused for any cardinality as per (9).

## B. One-Shot Negative Cycle Prevention

What remains is to encode DCs with elements of $V_i$. These constraints together are encountered in Difference Logic (see, e.g., [10], [39], [50]–[52]). The accepted means of solving such problems is to consider instances as a directed Difference Graph (DG), wherein the variables are nodes and the edges are the differences in the constraints, and $x_0$ denotes zero. We also treat the set sizes as constant parts of the degree, manipulating relevant DCs so that the cardinalities are on the same side as $\alpha$ and the integer variable is subtracted from or by zero — that is, $\mathrm{card}(S) - x_i \le \alpha$ becomes

$x_0 - x_i \le \alpha - \mathrm{card}(S)$, say. As an example, take the following constraints: $x_2 - x_1 \le 3$, $x_3 - x_2 \le -2$, $x_1 - x_3 \le 4$, $x_4 - x_1 \le 1$, $x_4 - x_0 \le 5$, $x_1 - \mathrm{card}(S) \le -1$, $\mathrm{card}(S') - x_3 \le 2$, where all $x_i$ come from $V_i$ and $S, S'$ are set variables. These constraints are depicted in Fig. 2.

<figure><img src="image_3.png" /><figcaption>Fig. 2. Example of a DG. Solid edges represent constraints between integer variables, while dashed edges represent constraints involving set cardinalities.</figcaption></figure>

On a first pass, we ignore DCs with a cardinality and check the consistency of the sub-instance regarding solely elements of $V_i$ by the usual means: calculating shortest paths and finding the graph to be free of negative cycles by means of the Bellman-Ford or Floyd-Warshall algorithms [53]–[56]. Deriving contradiction at this point of course makes the entire instance unsatisfiable. Otherwise, the DG must be handled during the resolution by the SAT solver. A traditional approach is to incrementally check for satisfiability with the SAT solver before asserting new constraints to block negative cycles [57]. Instead we block negative cycles once before one solver call by means of bringing back the mixed DC, viz., with one set variable and one integer variable.

Because the DG represents a consistent situation up to this point, a potential negative cycle would have to involve the size of some set $S \in V_s$ in some mixed DC. Conceived thus, a negative cycle would have to take one of the following three possible forms, with each $\alpha_i$ a constant integer:

1) $x_0 \xrightarrow{\alpha_0-\mathrm{card}(S)} x_1 \xrightarrow{\alpha_1} x_2 \xrightarrow{\alpha_2} \dots \xrightarrow{\alpha_{k-1}} x_k \xrightarrow{\alpha_k} x_0,$

2) $x_0 \xrightarrow{\alpha_0} x_1 \xrightarrow{\alpha_1} x_2 \xrightarrow{\alpha_2} \dots \xrightarrow{\alpha_{k-1}} x_k \xrightarrow{\alpha_k+\mathrm{card}(S')} x_0,$

3) $x_0 \xrightarrow{\alpha_0-\mathrm{card}(S)} x_1 \xrightarrow{\alpha_1} \dots \xrightarrow{\alpha_{k-1}} x_k \xrightarrow{\alpha_k+\mathrm{card}(S')} x_0.$

The reason why the operator card cannot occur more than twice in a cycle is that each constraint involving a set cardinality corresponds to an edge connected to $x_0$ after our manipulation, and $x_0$ has only one incoming edge and only one outgoing edge in a cycle.

We bind, then, the SAT encoding with the difference graph by blocking differences of any of the three forms by means of negating or enforcing $s_{|D|}$ variables like in (9) in cases 1) and 2), and comparing arrays of variables as in (10) in case 3). The appropriate constraints are chosen by running a variant of the Bellman-Ford algorithm wherein edge weights may involve cardinalities, and are compared in the following way.

A distance $d$ is treated as at least as short as a distance $d'$ only if $\sigma(d) \le \sigma(d')$ for all $\sigma$. When no cardinalities are

<footnote n="2">²Here and in the sequel, “$\phi \rightsquigarrow \psi$” means that $\phi$ is encoded with $\psi$.</footnote>
involved in either of $d$ or $d'$, the metric is the same as before, e.g., $5 \le 9$. Because all cardinalities are in $\mathbb{N}$, if distances differ only on one cardinality, $\mathrm{card}(S)$, the distance with a lower coefficient for $\mathrm{card}(S)$ is shorter, e.g., $5 \le 5+\mathrm{card}(S)$. In these two cases, when relaxing distances, the shorter is kept for the next iteration, and the longer is discarded. When distances $d$ and $d'$ differ on more than one cardinality (the null cardinality, the pure integers, included), unless each coefficient in $d$ is less than or equal to the corresponding coefficient in $d'$, $d$ and $d'$ are incommensurable. Both then are held onto for the next iteration, and both cases must be considered. For example, we cannot tell whether $5$ or $3+\mathrm{card}(S)$ is shorter without knowing the value of $\mathrm{card}(S)$, so both distances survive.

After the usual number of iterations for Bellman-Ford, constraints are derived from each of the distances representing that from the zero node to itself so that each value remain non-negative.

Some benefits of this approach are that the numbers of solver calls and encoded clauses are reduced since, although not all distances with set sizes are comparable, some can be known to be less than others independently of the size of the relevant sets. Hence, subsumed clauses need not be encoded into the SAT instance.

### C. Domain Size and Unsatisfiability

For a QCN, only the relations between sets are encoded and so the satisfiability of an encoding is not dependent on any domain. In the case of an SDP, a SAT encoding will depend also on the size of $D$. In the case of abstract B machines, there is no evident restriction on the size of $D$, but in practice we must set a finite domain. In general, a SAT encoding can be unsatisfiable not due to the validity of the original machine but owing to the domain chosen for the SAT encoding being too tight.

For a subset of possible SDPs, we find a sufficient bound for $|D|$ such that an unsatisfiable instance over it cannot become satisfiable by increasing the domain size.

**Theorem 2:** Given an SDP $\mathcal{X} = \langle V_s, \emptyset, \kappa, C, \Delta, \mathcal{P} \rangle$ over $D$ such that every constraint in $\mathcal{P}$ is a DC of the form $0 - \mathrm{card}(S) \le \alpha$ or $\mathrm{card}(S) - 0 \le \alpha$, if $\mathcal{X}$ is unsatisfiable and

$$|D| \ge \max \left( \begin{array}{l} \left( \bigcup \kappa_i + \sum_{\substack{i,j \in V_s, \\ i < j}} (\nu_{\chi}(\lambda(C(i,j)))) \right) \\ + \sum_{\substack{i \in V_s, \\ k \in \kappa}} (\nu_{\kappa}(\lambda(C(i,k)))) + \mu, 1 \end{array} \right), \quad (11)$$

then $\mathcal{X}$ is unsatisfiable over any domain $D'$, where $\lambda(r)$ returns a single base relation $b$ from the set $r$ such that $b \in r$ and for all $b' \in r$ and $b \ne b'$, $b \prec b'$ in $\langle \mathrm{OV}, \mathrm{DR}, \supset, \subset, \mathrm{EQ} \rangle$, $\nu_{\chi}(b)$ maps $\{\mathrm{OV} \mapsto 3, \mathrm{DR} \mapsto 2, \supset \mapsto 1, \subset \mapsto 1, \mathrm{EQ} \mapsto 0\}$, $\nu_{\kappa}(b)$ maps $\{\mathrm{OV} \mapsto 1, \mathrm{DR} \mapsto 1, \supset \mapsto 1, \subset \mapsto 0, \mathrm{EQ} \mapsto 0\}$, and $\mu = \sum_{S_i \in V_s} (\max(\{\alpha : (\mathrm{card}(S_i) \ge \alpha) \in \mathcal{P}\} \cup \{0\}))$.

**Sketch 2:** This bound is obtained from using a semantic tableau on a translation into first-order logic [58], [59]. Inuitively, $\nu_{\chi}$'s values come from the number of existential quantifiers introducing fresh variables. On the qualitative side, OV overshadows any other base relation because one element in the intersection and one in each of the two relative complements must be accounted for. Where there is no OV, but there is a DR, we need a fresh variable for both sets. Then, if there is neither OV nor DR, but there is $\subset$ (inclusive) or $\supset$, there is an existential qualifier on the larger side. For EQ, all quantifiers are universal and so have no effect. The case is similar for $\nu_{\kappa}$ but some variables are already introduced by the definition of the elements of $\kappa$. For constraints on cardinality of a set $s$, it is unsurprising that at least $\alpha$ variables must be available in order to ensure that the safety of constraints such as $\mathrm{card}(s) \ge \alpha$. On the other hand, those like $\mathrm{card}(s) \le \alpha$ do not require the introduction of variables. Even if the tableau introduces no variables, the domain cannot be empty, so the bound is at least one. $\square$

Thanks to this, if we calculate such a bound $k^*$ for fragments of instances and the SAT encoding persists in being unsatisfiable with an adequate $|D| = k^*$, we can conclude that the unsatisfiability is not due to the bound.

## VI. EXPERIMENTATION

This section records some empirical observations on the performance of these SAT encodings, serving as a proof of concept for the considered approach in general and as a comparison between the purely qualitative and the hybrid versions.

### A. Experimental Design

a) **Dataset:** We convert and run on SAT translations of both QCN and SDP versions of real-world B method POs made available by the safety security company CLEARSY<fnref n="3" />. These are read as POG files, which are descriptions of POs generated from B machines by atelierB. These provided POs are all expected to be valid, so we augment the dataset and run also on a modified version of each PO with its goal negated. This does not ensure that the new PO will be invalid, but some of them should be in practice.

b) **Variations of Considered Hypotheses and Meanings of Outcomes:** On both halves of the dataset, the encoding is identical for the QCN approach; as many hypotheses as possible are encoded along with the negation of the goal. It is noted if there are expressions encoded incompletely (such as, for example, the relative sizes of the domain and range of functions). Whenever the answer to a purely qualitative instance is UNSATISFIABLE, then we conclude the PO to be validated because domain size is not an issue.

For SDP, an answer of UNSATISFIABLE can indeed originate from having encoded a valid PO, but also from using too small a domain to encode a counterexample. When running on the original instances, only constraints considered by Theorem 2 were encoded, and the domain size was set to the bound given by this theorem. Unsatisfiability being found here permits claiming validity, but for the encodings of the

<footnote n="3">³Instances: https://zenodo.org/records/7050797. Results: https://zenodo.org/records/17197860. Code: [60]</footnote>
modified POs with arbitrary domain size, unsatisfiability is unconvincing.

When the SAT solver outputs SATISFIABLE, there are two possible meanings depending on the completeness of the encoding. When either the purely qualitative or SDP framework handles each of the PO's hypotheses and its goal accurately, then a model of the SAT encoding is a counterexample to the PO. If there are some unhandled hypotheses, then a satisfiable encoding is inconclusive seeing as the skipped hypotheses could be key in making the PO valid.

c) Running: Each job included the conversion of the POG file to SAT and the resolution of the instance by CaDi-CaL [61], and was run on a core of an Intel Xeon Gold 6248 2.5GHz with 768GB of RAM and a timeout of 64 seconds.

d) Juxtaposition: As well as testing these qualitative approaches, it has previously been checked how well known tools for handling PO perform while verifying these instances. Two forces of atelierB were run directly. Forces in this context are versions of atelierB's automated prover with increasing proof power. A force is stronger when it has more rules and has a better chance of proving the PO. On the other hand, it can be more costly and ascending through the forces increases the possibility of not terminating. After translation with ppTransPOG [62], cvc5 [63] and Z3 [64] were run on SMT instances and Vampire [65] and iProver [66] on TPTP instances with the aim to validate the original POs. It is not our goal to replace these foregoing strategies. Indeed, many POs must be encoded in first-order logic, which is undecidable in general. We cannot encode everything, and do not decide as many POs as the other approaches. Yet we are able to verify some instances that other solvers did not decide.

## B. Results

A summary of the comparison of the results can be found in Table I. This table shows the counts of cases that are settled by one or both of the approaches. Unhelpful results (timeouts, SATISFIABLE without complete characterization, UNSATISFIABLE without certainty regarding the bound size) are not shown.

<table><caption>TABLE I
COMPARISON OF RESULTS BY NUMBER OF INSTANCES ANSWERED DEFINITIVELY</caption><thead><tr><th></th><th>Purely Qual.</th><th>Both</th><th>SDP Only</th></tr></thead><tbody><tr><td>Counterexamples</td><td>13</td><td>103</td><td>11</td></tr><tr><td>Verified</td><td>10030</td><td>36</td><td>23748</td></tr><tr><td>Of which verified only by this work</td><td>34</td><td>6</td><td>150</td></tr></tbody></table>

These results show that there is room to use these approaches. In the final row are the numbers of POs verified by the respective columns and also included in the second row but not verified by the previous approaches. Of the POs verified by our approaches, 190 were not verified by any of the others. Hereby we see that the two qualitative approaches are not redundant with respect to each other nor with respect to the state-of-the-art, and both could be useful for automating

the discharging of POs. Especially promising is the fact that there are POs validated that were not decided by the others.

## VII. CONCLUSION

This paper described a hybrid combination of qualitative and numerical reasoning, SDP, for formulating problems originating from set theory. On top of this, a means of solving these problems was defined. This definition necessitated tailoring an adaption of a SAT encoding of cardinalities over variables without entire re-encodings for each considered cardinality and treatment of difference constraints that could block negative cycles in a difference graph without making numerous calls to shortest-path seekers or SAT solvers. As a particular example of its usefulness, experiments showed that such reasoning can be used to verify real-world B POs that are unverified by other common approaches. This approach can also totally encode some invalid POs and provide counterexamples.

A next step is to take this approach into SMT. There exists a non-standard SMT logic QF_UFLIAFS (quantifier free, uninterpreted functions, linear integer arithmetic, finite sets) [67] implemented in the solver cvc, and based on including the set membership operation with Boolean Algebra and Presburger Arithmetic [68], [69]. A comparison with our approach is a significant work that is in progress.

## REFERENCES

[1] M. R. Garey and D. S. Johnson, *Computers and Intractability*. freeman San Francisco, 1979, vol. 174.

[2] J.-R. Abrial, A. Hoare, and P. Chapron, *The B-Book*. Cambridge university press, 1996.

[3] S. Schneider, *The B-Method: An Introduction*. Palgrave Oxford, 2001.

[4] D. Cansell and D. Méry, "Foundations of the B Method," *Computing and informatics*, vol. 22, no. 3-4, pp. 221-256, 2003.

[5] J.-R. Abrial, *Modeling in Event-B: System and Software Engineering*. Cambridge University Press, 2010.

[6] G. Ligozat, *Qualitative Spatial and Temporal Reasoning*. John Wiley & Sons, 2013.

[7] G. Ligozat and J. Renz, "What is a Qualitative Calculus? A General Framework," in *Pacific Rim International Conference on Artificial Intelligence*. Springer, 2004, pp. 53-64.

[8] A. Biere, M. Heule, and H. van Maaren, *Handbook of Satisfiability*. IOS press, 2021, vol. 336.

[9] D. N. Pham, J. Thornton, and A. Sattar, "Modelling and solving temporal reasoning as propositional satisfiability," *Artificial Intelligence*, vol. 172, no. 15, pp. 1752-1782, 2008.

[10] S. Cotton and O. Maler, "Fast and Flexible Difference Constraint Propagation for DPLL (T)," in *International Conference on Theory and Applications of Satisfiability Testing*. Springer, 2006, pp. 170-183.

[11] T. Soh, D. Le Berre, S. Roussel, M. Banbara, and N. Tamura, "Incremental SAT-Based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem," in *Logics in Artificial Intelligence: 14th European Conference, JELIA 2014, Funchal, Madeira, Portugal, September 24-26, 2014. Proceedings 14*. Springer, 2014, pp. 684-693.

[12] CLEARSY, "atelierB," https://www.atelierb.eu.

[13] M. Leuschel and M. Butler, "ProB: A model checker for B," in *International symposium of formal methods europe*. Springer, 2003, pp. 855-874.

[14] K. Marriott, P. J. Stuckey, and M. Wallace, "Constraint Logic Programming," *Foundations of Artificial Intelligence*, vol. 2, pp. 409-452, 2006.

[15] C. Barrett, P. Fontaine, and C. Tinelli, "The Satisfiability Modulo Theories Library (SMT-LIB)," www.SMT-LIB.org, 2016.

[16] G. Sutcliffe, "The Logic Languages of the TPTP World," *Logic Journal of the IGPL*, 2022.

[17] J.-C. Filliâtre and A. Paskevich, "Why3—Where Programs Meet Provers," in *European symposium on programming*. Springer, 2013, pp. 125-128.
[18] D. Déharbe, "Integration of SMT-Solvers in B and Event-B Development Environments," *Science of Computer Programming*, vol. 78, no. 3, pp. 310–326, 2013.

[19] D. Mentré, C. Marché, J.-C. Filliátre, and M. Asuka, "Discharging Proof Obligations from Atelier B using Multiple Automated Provers," in *International Conference on Abstract State Machines, Alloy, B, VDM, and Z*. Springer, 2012, pp. 238–251.

[20] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu, "Symbolic Model Checking without BDDs," in *Tools and Algorithms for the Construction and Analysis of Systems: 5th International Conference*. Springer, 1999, pp. 193–207.

[21] C. Gervet, "Conjunto: Constraint Logic Programming with Finite Set Domains," in *ILPS*, 1994.

[22] A. Dovier, E. G. Omodeo, E. Pontelli, and G. Rossi, "{log}: A Language for Programming in Logic with Finite Sets," *The Journal of logic programming*, vol. 28, no. 1, pp. 1–44, 1996.

[23] A. Dovier, C. Piazza, E. Pontelli, and G. Rossi, "Sets and Constraint Logic Programming," *ACM Transactions on Programming Languages and Systems (TOPLAS)*, vol. 22, no. 5, pp. 861–931, 2000.

[24] M. Cristiá and G. Rossi, "{log}: Set Formulas as Programs," *arXiv preprint arXiv:2104.08130*, 2021.

[25] M. Cristiá, "From B Specifications to {log} Forgrams," *arXiv preprint arXiv:2407.03283*, 2024.

[26] F. Lardeux, E. Monfroy, B. Crawford, and R. Soto, "Set constraint model and automated encoding into SAT: application to the social golfer problem," *Annals of Operations Research*, vol. 235, no. 1, pp. 423–452, 2015.

[27] S. A. Cook, "The Complexity of Theorem-Proving Procedures," in *Logic, automata, and computational complexity: The works of Stephen A. Cook*, 2023, pp. 143–152.

[28] R. M. Karp, "Reducibility among Combinatorial Problems," *The Journal of Symbolic Logic*, vol. 40, no. 4, 1972.

[29] L. A. Levin, "Universal Search Problems," pp. 399–400, 1984.

[30] J. P. Marques-Silva and K. A. Sakallah, "GRASP: A Search Algorithm for Propositional Satisfiability," *IEEE Transactions on Computers*, vol. 48, no. 5, pp. 506–521, 1999.

[31] M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik, "Chaff: Engineering an Efficient SAT Solver," in *Proceedings of the 38th annual Design Automation Conference*, 2001, pp. 530–535.

[32] G. S. Tseitin, "On the Complexity of Derivation in Propositional Calculus," *Automation of reasoning: 2: Classical papers on computational logic 1967–1970*, pp. 466–483, 1983.

[33] A. Tarski, "On the Calculus of Relations," *The journal of symbolic logic*, vol. 6, no. 3, pp. 73–89, 1941.

[34] A. Inants and J. Euzenat, "So, what exactly is a qualitative calculus?" *Artificial intelligence*, vol. 289, p. 103385, 2020.

[35] J. F. Allen, "Maintaining Knowledge about Temporal Intervals," *Communications of the ACM*, vol. 26, no. 11, pp. 832–843, 1983.

[36] D. A. Randell, Z. Cui, and A. G. Cohn, "A Spatial Logic based on Regions and Connection," *KR*, vol. 92, pp. 165–176, 1992.

[37] P. B. Ladkin and R. D. Maddux, "On Binary Constraint Problems," *Journal of the ACM (JACM)*, vol. 41, no. 3, pp. 435–469, 1994.

[38] I. Düntsch, "Relation Algebras and their Application in Temporal and Spatial Reasoning," *Artificial Intelligence Review*, vol. 23, no. 4, pp. 315–357, 2005.

[39] A. Gerevini, M. Cristani et al., "On Finding a Solution in Temporal Constraint Satisfaction Problems," in *IJCAI*, vol. 97, 1997, pp. 1460–1465.

[40] D. Wolter and J. H. Lee, "Connecting Qualitative Spatial and Temporal Representations by Propositional Closure," in *IJCAI International Joint Conference on Artificial Intelligence*, 2016.

[41] A. Gerevini and J. Renz, "Combining topological and size information for spatial reasoning," *Artificial Intelligence*, vol. 137, no. 1-2, pp. 1–42, 2002.

[42] P. Van Beek and D. W. Manchak, "The Design and Experimental Analysis of Algorithms for Temporal Reasoning," *Journal of Artificial Intelligence Research*, vol. 4, pp. 1–18, 1996.

[43] J. Renz and B. Nebel, "Efficient Methods for Qualitative Spatial Reasoning," *Journal of Artificial Intelligence Research*, vol. 15, pp. 289–318, 2001.

[44] J. Renz et al., "Qualitative Spatial and Temporal Reasoning: Efficient Algorithms for Everyone," in *IJCAI*, 2007, pp. 526–531.

[45] Z. Gantner, M. Westphal, and S. Wölfli, "GQR-A Fast Reasoner for Binary Qualitative Constraint Calculi," in *AAAI Workshop on Spatial and Temporal Reasoning*. AAAI Chicago (IL), 2008, p. 6.

[46] M. Sioutis and M. Koubarakis, "Consistency of Chordal RCC-8 Networks," in *2012 IEEE 24th International Conference on Tools with Artificial Intelligence*, vol. 1. IEEE, 2012, pp. 436–443.

[47] M. Sioutis, "Triangulation versus Graph Partitioning for Tackling Large Real World Qualitative Spatial Networks," in *2014 IEEE 26th International Conference on Tools with Artificial Intelligence*. IEEE, 2014, pp. 194–201.

[48] O. Roussel and V. Manquinho, "Pseudo-Boolean and Cardinality Constraints," in *Handbook of Satisfiability - Second Edition*, ser. Frontiers in Artificial Intelligence and Applications, A. Biere, M. Heule, H. van Maaren, and T. Walsh, Eds. *IOS Press*, 2021, vol. 336, pp. 1087–1129.

[49] C. Sinz, "Towards an Optimal CNF Encoding of Boolean Cardinality Constraints," in *International conference on principles and practice of constraint programming*. Springer, 2005, pp. 827–831.

[50] R. Dechter, I. Meiri, and J. Pearl, "Temporal constraint networks," *Artificial intelligence*, vol. 49, no. 1-3, pp. 61–95, 1991.

[51] O. Strichman, S. A. Seshia, and R. E. Bryant, "Deciding Separation Formulas with SAT," in *Computer Aided Verification: 14th International Conference, CAV 2002 Copenhagen, Denmark, July 27–31, 2002 Proceedings 14*. Springer, 2002, pp. 209–222.

[52] S. Cotton, E. Asarin, O. Maler, and P. Niebert, "Some Progress in Satisfiability Checking for Difference Logic," in *International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems*. Springer, 2004, pp. 263–276.

[53] R. Bellman, "On a Routing Problem," *Quarterly of applied mathematics*, vol. 16, no. 1, pp. 87–90, 1958.

[54] R. W. Floyd, "Algorithm 97: Shortest Path," *Communications of the ACM*, vol. 5, no. 6, pp. 345–345, 1962.

[55] S. Warshall, "A Theorem on Boolean Matrices," *Journal of the ACM (JACM)*, vol. 9, no. 1, pp. 11–12, 1962.

[56] T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein, *Introduction to Algorithms*. MIT press, 2022.

[57] C. Wang, F. Ivančić, M. Ganai, and A. Gupta, "Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination," in *LPAR*. Springer, 2005, pp. 322–336.

[58] R. M. Smullyan and R. M. Smullyan, *First-Order Logic*. Springer, 1968.

[59] M. Fitting, *First-Order Logic and Automated Theorem Proving*. Springer Science & Business Media, 2012.

[60] "sdp-solver." [Online]. Available: https://archive.softwareheritage.org/swh:1:dir:0692070184d805b6f122328d7a6bf3a8f445c3a2

[61] A. Biere, T. Faller, K. Fazekas, M. Fleury, N. Froleyks, and F. Pollitt, "CaDiCaL 2.0," in *Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I*, ser. Lecture Notes in Computer Science, A. Gurfinkel and V. Ganesh, Eds., Springer, 2024, pp. 133–152.

[62] *CLEARSY*, "pptranspog." [Online]. Available: https://github.com/CLEARSY/pptranspog

[63] H. Barbosa, C. Barrett, M. Brain, G. Kremer, H. Lachnitt, M. Mann, A. Mohamed, M. Mohamed, A. Niemetz, A. Nötzli et al., "cvc5: A Versatile and Industrial-Strength SMT Solver," in *International Conference on Tools and Algorithms for the Construction and Analysis of Systems*. Springer, 2022, pp. 415–442.

[64] L. De Moura and N. Bjørner, "Z3: An efficient SMT solver," in *International conference on Tools and Algorithms for the Construction and Analysis of Systems*. Springer, 2008, pp. 337–340.

[65] L. Kovács and A. Voronkov, "First-Order Theorem Proving and VAM-PIRE," in *International Conference on Computer Aided Verification*. Springer, 2013, pp. 1–35.

[66] K. Korovin, "iProver–An Instantiation-Based Theorem Prover for First-Order Logic (System Description)," in *International Joint Conference on Automated Reasoning*. Springer, 2008, pp. 292–298.

[67] K. Bansal, C. Barrett, A. Reynolds, and C. Tinelli, "Reasoning with Finite Sets and Cardinality Constraints in SMT," *Logical Methods in Computer Science*, vol. 14, 2018.

[68] V. Kuncak, H. H. Nguyen, and M. Rinard, "Deciding Boolean Algebra with Presburger Arithmetic," *Journal of Automated Reasoning*, vol. 36, pp. 213–239, 2006.

[69] V. Kuncak and M. Rinard, "Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic," in *International Conference on Automated Deduction*. Springer, 2007, pp. 215–230.