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

HAL
open science

# The Satisfiability Problem in a Separation Logic of Relations

Nicolas Peltier

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

## To cite this version:

Nicolas Peltier. The Satisfiability Problem in a Separation Logic of Relations. Logic, Language, Information, and Computation - 31st International Workshop (Wollic 2025), 2025, Porto, Portugal. pp.260-277, 10.1007/978-3-031-99536-1_16. hal-05244161

HAL Id: hal-05244161

https://hal.science/hal-05244161v1

Submitted on 8 Sep 2025

HAL is a multi-disciplinary open access archive for the deposit and dissemination of scientific research documents, whether they are published 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_3.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# The Satisfiability Problem in a Separation Logic of Relations *

Nicolas Peltier

Univ. Grenoble Alpes, CNRS, LIG, F-38000 Grenoble France

**Abstract.** The separation logic of relations (SLR) is a generalization of separation logic (SL) which is useful to describe complex structures like graphs and relational databases. SLR extends SL by interpreting heaps as (multi)sets of relational atoms instead of partial functions. This paper addresses the satisfiability problem for SLR formulas with additional shape constraints (called *patterns*) expressing conditions such as uniqueness of atoms or functionality of relations. We show that the satisfiability problem is 2-EXPTIME-complete when (dis)equalities over existential variables are excluded from the considered patterns, and undecidable otherwise.

## 1 Introduction

Separation Logic (SL) [6,9] is widely employed in program verification to reason about code that manipulates dynamically allocated memory. SL formulas describe heaps, i.e., partial finite functions that map certain memory locations to tuples of other locations. SL formulas are built using atomic expressions like $x \mapsto (y_1, \dots, y_k)$, which assert that the location associated with $x$ is the sole allocated one (i.e., the heap domain is a singleton $\ell$, where $\ell$ is the value of $x$) and that this location points to the tuple $(y_1, \dots, y_k)$. To denote disjoint unions of heaps, SL introduces the separating conjunction $*$. Recently, an extension of SL has been introduced [7,2,1] to reason on more complex structures, based on arbitrary relations. This extended logic, known as Separation Logic of Relations (SLR), generalizes SL by allowing arbitrary (potentially non-functional) relations, where heaps are interpreted as sets of atomic expressions of the form $p(\ell_1, \dots, \ell_n)$, where $p$ is a relation and $\ell_1, \dots, \ell_n$ are locations. SLR offers a flexible framework for describing diverse data structures, such as graphs, hypergraphs, relational databases, and software or hardware architectures. SL is a specific instance of SLR, restricted to a single functional relation $\mapsto$. Like SL, SLR can be extended with inductively defined predicates and fixpoint semantics, enabling the description of unbounded structures. In this paper, we focus on testing the satisfiability of SLR formulas over multisets of atoms, under additional constraints (also called *patterns*) on the shape of the structure. These constraints may, for example, assert that certain atoms and/or locations appear at most $n$ times in a structure (for some fixed $n \in \mathbb{N}$), or that a relation satisfies some properties such as functionality. This problem generalizes the satisfiability problem for SL or for SLR over sets (as studied in [3,2]). In [3], it is proved that satisfiability is

<footnote>* This work has been partially funded by the French National Research Agency project ANR-21-CE48-0011.</footnote>
EXPTIME-complete for SL formulas, and in [2] it is shown that satisfiability belongs to 2-EXPTIME for a specific fragment of SLR that encodes reconfigurable architectures. Our work broadens these approaches by addressing more general classes of structures and arbitrary shape constraints. The shape constraints corresponding to SL [3] are related to the functional nature of the heap and assert that the same location cannot be allocated twice, whereas the configuration logic of [2] allows for structures defined as sets of relational atoms of some specific form. The structures we consider are arbitrary multisets of atoms $p(\ell_1, \dots, \ell_n)$, and the constraints we handle allow us to exclude structures that contain substructures of specific shapes, which strictly generalizes previous approaches (see Sect. 3 for more details). We demonstrate that the problem is 2-EXPTIME-complete when the shape constraints exclude disequalities over existential variables, and undecidable otherwise. Due to space constraints, some proofs are deferred to the appendix.

## 2 Definitions

We define the syntax and semantics of the logic SLR. We first briefly review some basic notations and definitions. For any function $f$, $dom(f)$ denotes the domain of $f$, and for any finite set $S$, $card(S)$ denotes the number of elements in $S$. A multiset $S$ is a function mapping elements to natural numbers, where $S(x)$ denotes the number of instances of $x$ in $S$ (called the multiplicity of $x$ in $S$). The sum of two multisets $S_1, S_2$ is defined as usual: $(S_1 + S_2)(x) = S_1(x) + S_2(x)$.

We consider 3 disjoint sets of symbols: a countably infinite set of variables $V$ and two sets of predicate symbols, $\mathcal{P}_H$ and $\mathcal{P}_I$, called heap predicates and inductive predicates, respectively. Each symbol $P \in \mathcal{P}_H \cup \mathcal{P}_I$ is associated with a unique arity $ar(P) \ge 0$. The predicates in $\mathcal{P}_H$ are used to define the relational structures on which the formulas are interpreted, whereas those in $\mathcal{P}_I$ denote inductively-defined structures of unbounded size. The set of SLR-formulas (or simply formulas) is inductively defined as follows:

$$ \mathbf{emp} \mid (x \approx y) \mid (x \not\approx y) \mid P(x_1, \dots, x_n) \mid \phi_1 \lor \phi_2 \mid \phi_1 * \phi_2 \mid \exists x \psi $$

where $x, y, x_1, \dots, x_n$ are variables, $P \in \mathcal{P}_H \cup \mathcal{P}_I$, $n = ar(P)$, and $\phi_1, \phi_2, \psi$ are SLR-formulas. As in SL, $\mathbf{emp}$ is a special atom denoting empty structures and $*$ is a special conjunction (called separating conjunction) denoting a union of structures. Negation and standard conjunction are not used (as in the usual fragment of SL called symbolic heaps). A formula of the form $\mathbf{emp}$ or $P(x_1, \dots, x_n)$ with $P \in \mathcal{P}_H \cup \mathcal{P}_I$ (resp. $x \approx y$ or $x \not\approx y$) is called a spatial atom (resp. an equational atom). An atom is a spatial atom or an equational atom. For all $S \subseteq \mathcal{P}_H \cup \mathcal{P}_I$, an $S$-atom is an atom of the form $P(x_1, \dots, x_n)$ with $P \in S$. For any formula $\phi$, we denote by $fv(\phi)$ the set of variables freely occurring in $\phi$. Formulas are taken up to all the usual properties of the logical symbols: associativity and commutativity of $*$, commutativity of $\approx$ and $\not\approx$, neutrality of $\mathbf{emp}$ for $*$, contraction of equational atoms for $*$ (i.e., $\phi * \phi = \phi$ if $\phi$ is an equational atom), $\alpha$-renaming, commutativity of $\exists$ (i.e. $\exists x \exists y \phi$ and $\exists x \exists y \phi$ are taken as identical) and up to transformation into prenex form. Any empty $*$-conjunction, e.g., $\phi_1 * \dots * \phi_n$ with $n = 0$, is taken as $\mathbf{emp}$. For any finite sequence of variables $x = (x_1, \dots, x_n)$, $\exists x \phi$
denotes the formula $∃x_1 ... ∃x_n φ$. A *substitution* is a total function from variables to variables. The *domain* of a substitution $σ$, denoted by $dom(σ)$, is the set of variables $x$ such that $σ(x) ≠ x$. A substitution of domain $\{x_1, ..., x_n\}$ with $σ(x_i) = y_i$ is denoted by $\{x_i ↦ y_i | i = 1, ..., n\}$. Formulas are interpreted over structures defined as follows:

**Definition 2.1.** Let $\mathcal{L}$ be a countably infinite fixed set of locations. A heap atom is an expression of the form $p(ℓ_1, ..., ℓ_n)$, where $p \in \mathcal{P}_{\text{H}}$, $n = \text{ar}(p)$ and $ℓ_1, ..., ℓ_n \in \mathcal{L}$. A structure is a pair $(s, \mathcal{h})$, where:

- $s$ is a store, i.e., a partial function from $\mathcal{V}$ to $\mathcal{L}$, with a finite domain.

- $\mathcal{h}$ is an $R$-heap (or simply a heap), i.e., a finite multiset of heap atoms.

We denote by $\mathcal{L}(\mathcal{h})$ the set of locations $ℓ$ that occur in some heap atom in $\mathcal{h}$, i.e.,
$\mathcal{L}(\mathcal{h}) = \{ℓ_i | p(ℓ_1, ..., ℓ_n) \in \mathcal{h}, 1 \le i \le n\}$.

Any store $s$ can be extended into a function mapping $\mathcal{P}_{\text{H}}$-atoms with variables in $dom(s)$ to heap atoms: $s(p(x_1, ..., x_n)) = p(s(x_1), ..., s(x_n))$.

**Remark 2.2.** Unlike [7,2], we define heaps as multisets rather than sets. This approach has the advantage of making the composition of heaps form a total function, while also broadening the applicability of the results to encompass multigraphs. Importantly, this generalization entails no loss of expressiveness, as we can enforce the condition that each atom appears at most once using a pattern within the language (see Sect. 3).

The semantics of predicates in $\mathcal{P}_I$ is defined by inductive rules:

**Definition 2.3.** A set of inductive definitions (SID) is a set of rules that are expressions of the form $P(x_1, ..., x_n) \Leftarrow \phi$, where $P \in \mathcal{P}_I$, $\text{ar}(P) = n$, $x_1, ..., x_n$ are pairwise distinct variables and $\phi$ is a formula with $fv(\phi) \subseteq \{x_1, ..., x_n\}$.

We write $P(y_1, ..., y_n) \Leftarrow_R \psi$ if $P(y_1, ..., y_n)$ can be transformed into $\psi$ using one of the rules in $R$, i.e., if $R$ contains a rule $P(x_1, ..., x_n) \Leftarrow \phi$ with $\psi = \phi\{x_i \mapsto y_i | i = 1, ..., n\}$.

**Definition 2.4.** The satisfiability relation $\models_R$ is the least relation such that $(s, \mathcal{h}) \models_R \phi$ if $dom(s) \supseteqfv(\phi)$ and one of the following conditions holds:

- $\phi$ = emp and $\mathcal{h} = \emptyset$.

- $\phi = (t \approx s) (\text{resp. } t \not\approx s)$, $\mathcal{h} = \emptyset$ and $s(t) = s(s) (\text{resp. } s(t) \not\equiv s(s))$. Note that both formulas are satisfied only on empty heaps.

- $\phi$ is an $\mathcal{P}_{\text{H}}$-atom $p(x_1, ..., x_n)$ and $\mathcal{h} = \{p(s(x_1), ..., s(x_n))\}$. The formula asserts that $p(s(x_1), ..., s(x_n))$ is the only element in $\mathcal{h}$, with multiplicity 1.

- $\phi$ is a $\mathcal{P}_I$-atom and there exists a formula $\psi$ such that $\phi \Leftarrow_R \psi$ and $(s, \mathcal{h}) \models_R \psi$.

- $\phi = \phi_1 * \phi_2$ and there exist heaps $\mathcal{h}_1, \mathcal{h}_2$ such that $\mathcal{h} = \mathcal{h}_1 + \mathcal{h}_2$ and $(s, \mathcal{h}_i) \models_R \phi_i$ for all $i = 1, 2$. Note that, in contrast to SL, $\mathcal{h}_1, \mathcal{h}_2$ are not necessarily disjoint. The operator $+$ denotes the sum of the two multisets.

- $\phi = ∃x \psi$ and there exists a location $ℓ$ such that $(s', \mathcal{h}) \models_R \psi$, where $s'$ denotes a store of domain $dom(s') \cup \{x\}$ such that $s'(x) = ℓ$ and $s'(y) = s(y)$ if $y \in dom(s') \setminus \{x\}$.

A structure $(s, \mathcal{h})$ such that $(s, \mathcal{h}) \models_R \phi$ is an $R$-model of $\phi$. A formula is satisfiable if it has at least one $R$-model.
**Remark 2.5.** Note that equational atoms are true only in structures with an empty heap. This convention has the advantage of simplifying the syntax: equational constraints may be expressed without having to use the standard conjunction.

It is clear that the semantics of formulas does not depend on the name of the locations but only on the relations between these locations. Consequently, the locations occurring in a structure can be renamed arbitrarily without affecting the truth values of the formulas in the structure. This may be formalized by the proposition below. For any heap $\mathfrak{h}$ and mapping $\lambda : \mathcal{L} \to \mathcal{L}$, we denote by $\lambda(\mathfrak{h})$ the heap defined by the relations: $\lambda(\emptyset) = \emptyset$, $\lambda(p(\ell_1, \dots, \ell_n)) = p(\lambda(\ell_1), \dots, \lambda(\ell_n))$ and $\lambda(\mathfrak{h}_1 + \mathfrak{h}_2) = \lambda(\mathfrak{h}_1) + \lambda(\mathfrak{h}_2)$.

**Proposition 2.6.** Let $\lambda$ be any injective mapping from $\mathcal{L}$ to $\mathcal{L}$. Let $(s, \mathfrak{h})$ be a structure and let $\phi$ be a formula. Then: $(s, \mathfrak{h}) \models_R \phi \iff (\lambda \circ s, \lambda(\mathfrak{h})) \models_R \phi$.

*Proof.* By an immediate induction on the satisfiability relation.

### 3 The S-Satisfiability Problem

**Definition 3.1.** A pattern $\phi$ is a formula containing no predicate symbol in $\mathcal{P}_I$ and no disjunction. It is non-equational if, moreover, it contains no occurrence of $\approx$ or $\neq$, and $\exists$-restricted if for all atoms $x \approx y$ or $x \neq y$ occurring in $\phi$, neither $x$ nor $y$ occurs as an existentially quantified variable in $\phi$. The width of $\phi$ is defined as the number of occurrences of spatial atoms in $\phi$: $\text{width}(p(x_1, \dots, x_n)) = 1$, $\text{width}(x \approx y) = \text{width}(x \neq y) = 0$, $\text{width}(\phi_1 * \phi_2) = \text{width}(\phi_1) + \text{width}(\phi_2)$ and $\text{width}(\exists x \phi) = \text{width}(\phi)$.

Up to transformation into prenex form, a pattern of width $k$ may be written in the form: $\exists \mathbf{x} (*_{i=1}^m (y_i \approx y_i') *_{i=1}^n (z_i \neq z_i') *_{i=1}^k p_i(\mathbf{u}_i))$, where $m, n, k \ge 0$, $\mathbf{x}$ is a possibly empty sequence of variables, $y_i, y_i', z_i, z_i' \in \mathcal{V}$, $p_i \in \mathcal{P}_H$ and $\mathbf{u}_i$ is a sequence of variables.

**Definition 3.2.** A structure $(s, \mathfrak{h})$ is compatible with a set of patterns $S$ if there is no $\mathfrak{h}' \subseteq \mathfrak{h}$ and no $\phi \in S$ such that $(s, \mathfrak{h}') \models_R \phi$.

The problem we are considering in this paper (termed the *S-satisfiability problem*) is to determine, given a formula $\phi$, a set of rules $\mathcal{R}$ and a set of patterns $S$, whether there exists an $\mathcal{R}$-model of $\phi$ that is compatible with $S$. Note that the formulas in $S$ are interpreted negatively, i.e., assert conditions that *cannot* be satisfied by any sub-structure. In particular, the standard satisfiability problem in Separation Logic may be encoded as follows: the set $\mathcal{P}_H$ contains a unique symbol $H$ denoting the heap, with arity $k+1$, where $k$ denotes a number of record fields. An atom $H(x_0, \dots, x_k)$ asserts that location $x_0$ is allocated and refers to the tuple of locations $(x_1, \dots, x_k)$. The set $S$ contains a unique formula which guarantees that the same location cannot be allocated twice: $\exists x_1, y_1, \dots, y_k, z_1, \dots, z_k (H(x, y_1, \dots, y_k) * H(x, z_1, \dots, z_k))$. The *configuration logic* of [2] is encoded by considering a set $\mathcal{P}_H$ containing a monadic predicate $x \mapsto [x]$ (asserting that $x$ denotes a component in the architecture), a family of $n$-ary predicates $x_1, \dots, x_n \mapsto \langle x_1, p_1, \dots, x_n, p_n \rangle$ (denoting interactions, for every $n \in \mathbb{N}$ and ports $p_1, \dots, p_n$) and predicates $x \mapsto x@q$ (asserting that component $x$ is in state $q$). The set $S$ contains the formulas $\exists x ([x] * [x])$ and $\exists x_1, \dots, x_n (\langle x_1, p_1, \dots, x_n, p_n \rangle *$
(x₁:p₁, ..., xₙ:pₙ)), which assert that each component or interaction occurs only once, as well as the formulas ∃x (x@q * x@q') for all distinct states q, q' (asserting that each component is in only one state). Numerous variations are possible. For instance we may consider structures encoding multigraphs, then S will contain a formula of the form ∃x (node(x) * node(x)) (as nodes occur at most once in a graph) but no formula ∃x, y (edge(x, y) * edge(x, y)) (as multiple edges are permitted). We may also consider sets S containing formulas with equality. For instance assume that $P_H$ contains two predicates next and prev denoting pointers in a doubly linked list, then the formula ∃x, y, z (next(x, y) * prev(y, z) * x ≠ z) asserts that these pointers are well-defined, in the sense that the previous element of the next element of x is necessarily x. However, the latter formula is not ∃-restricted, and as we shall demonstrate, the satisfiability problem is undecidable in this case.

# 4 Decision Procedure

In the present section, we devise an algorithm to solve the S-satisfiability problem, assuming that all the patterns in S are ∃-restricted (but the input formula may be arbitrary). We show that this algorithm operates in doubly exponential time. The algorithm follows a standard technique (see, e.g., [3,8]), which consists in constructing an abstraction of the set of models of the input formula. This abstraction is finite (which ensures termination) and contains enough information to determine if the abstracted model is compatible with S. The information stored in the abstraction includes the set of free variables V, an equivalence relation ~, denoting the equality relation over these variables, and a finite set Σ of non-equational patterns satisfied over subparts of the heap.

To formalize this notion of abstraction, we need to introduce some notations. Let < be any total order on variables (fixed throughout this paper). For every equivalence relation ~ on some set of variables V (which will always be clear from the context), we denote by x↓_~ the smallest (w.r.t. <) variable y ∈ V such that x ~ y. For every formula φ such thatfv(φ) ⊆ V, we denote by φ↓_~ the formula φσ, where σ = {x ↦ x↓_|x ∈ V}. The formula φ is ~-normalized if φ↓_~= φ.

**Definition 4.1.** A abstraction is a tuple (V, ~, Σ) where V is a finite set of variables, ~ is an equivalence relation on V, and Σ is a finite set of non-equational ~-normalized patterns.

Definition 4.4 yields a simple criterion to check that the structures that are captured by a given abstraction satisfy a given $\exists$-restricted pattern. To this purpose, we first introduce a notion of subsumption, which captures a very simple restricted form of entailment:

**Definition 4.2.** A formula *φ* subsumes a formula *ψ* if *φ* and *ψ* are respectively of the form: ∃y₁, ..., yₘ (*φ'* *σ*). and ∃x₁, ..., xₙ ∃y₁, ..., yₘ *φ'*, where *σ* is any substitution of domain {x₁, ..., xₙ}.

As explained before, formulas are taken modulo α-renaming and commutativity of Θ:
for instance the formula ∃x p(x, y) subsumes the formula ∃u ∃v p(u, v) because these
formulas may be written ∃x p(x, v)σ and ∃v ∃x p(x, v) (respectively), with σ = {v ↦ y}.
The following proposition is immediate to prove:
**Proposition 4.3.** If $\phi$ subsumes $\psi$ and $(s, \mathfrak{h}) \models_R \phi$ then $(s, \mathfrak{h}) \models_R \psi$.

**Definition 4.4.** Let $\phi$ be an $\exists$-restricted pattern. We write $(V, \sim, \Sigma) \triangleright \phi$ if $\phi$ is of the form $\exists z (*_{i=1}^n (x_i \approx x'_i) *_{i=1}^m (y_i \not\approx y'_i) * \phi')$ and:

- For all $i \in \{1, \dots, n\}$, $x_i, x'_i \in V$ and $x_i \sim x'_i$.

- For all $i \in \{1, \dots, m\}$, $y_i, y'_i \in V$ and $y_i \not\sim y'_i$.

- The set $\Sigma$ contains a formula subsuming $\exists z \phi'$.

Note that, because $\phi$ is $\exists$-restricted, the variables $x_i, x'_i, y_i, y'_i$ cannot occur in $z$.

We define an algorithm to construct, given a formula $\phi$, a set of abstractions which capture all the models of $\phi$ (in a sense that will be specified later). This set is constructed by structural induction on $\phi$, using a fixpoint computation to handle inductive predicates (see Def. 4.5). In what follows, we often denote an equivalence relation $\sim$ by giving a set of equations $x \sim y$, with the implicit meaning that $\sim$ is the smallest reflexive, symmetric and transitive relation on $V$ such that $(x \sim y) \in S \implies x \sim y$ (where $V$ is fixed by the context). For instance $\emptyset$ denotes the relation $\sim$ such that $x \sim y \iff (x = y \land x \in V)$. To simplify notations, we assume that the equality $fv(\phi_1) = fv(\phi_2)$ holds for all disjunctions $\phi_1 \lor \phi_2$ (this property can easily be enforced by replacing each formula $\phi_i$ by $\phi_i * *_{x \in fv(\phi_{3-i}) \setminus fv(\phi_i)} \phi'$) (x $\approx$ x)). Similarly, we also assume that the equality $fv(\phi) = fv(p(x))$ holds for all rules $p(x) \leftarrow \phi$ (again, this property can be enforced by adding dummy equations $x \approx x$ into $\phi$).

**Definition 4.5.** For every formula $\phi$, we denote by $\mathcal{A}_k(\phi)$ the set of abstractions defined inductively as follows.

- If $\phi = \mathbf{emp}$ then $\mathcal{A}_k(\phi) = \{(\emptyset, \emptyset, \{\mathbf{emp}\})\}$.

- If $\phi = x \approx y$ then $\mathcal{A}_k(\phi) = \{(\{x, y\}, \{x \sim y\}, \{\mathbf{emp}\})\}$.

- If $\phi = x \not\approx y$ then $\mathcal{A}_k(\phi) = \{(\{x, y\}, \emptyset, \{\mathbf{emp}\})\}$.

- If $\phi = p(x_1, \dots, x_n)$ with $p \in \mathcal{P}_H$ then $\mathcal{A}_k(\phi)$ is the set of abstractions of the form $((x_1, \dots, x_n), \sim, \{\mathbf{emp}, \phi \downarrow^\sim\})$, where $\sim$ is an equivalence relation on $\{x_1, \dots, x_n\}$.

- If $\phi = P(x_1, \dots, x_n)$ with $P \in \mathcal{P}_I$ then $\mathcal{A}_k(\phi) = \bigcup_{\phi \in \mathcal{R}\psi} \mathcal{A}_k(\psi)$.

- If $\phi = \phi_1 \lor \phi_2$ then $\mathcal{A}_k(\phi) = \mathcal{A}_k(\phi_1) \cup \mathcal{A}_k(\phi_2)$.

- If $\phi = \phi_1 * \phi_2$, $(V_i, \sim_i, \Sigma_i) \in \mathcal{A}_k(\phi_i)$ (for all $i \in \{1, 2\}$) and $\sim$ is any equivalence relation on $V_1 \cup V_2$ that agrees with $\sim_i$ on $V_i$, then $\mathcal{A}_k(\phi)$ contains the abstraction:

$$ (V_1 \cup V_2, \sim, \{ (\phi_1 * \phi_2) \downarrow \mid \phi_i \in \Sigma_i, \text{width}(\phi_1) + \text{width}(\phi_2) \le k \}) $$

- If $\phi = \exists x \psi$ and $(V', \sim', \Sigma') \in \mathcal{A}_k(\psi)$ then $\mathcal{A}_k(\phi)$ contains the abstraction $(V, \sim, \Sigma)$ where $V = V' \setminus \{x\}$, $\sim$ is the restriction of $\sim'$ to $V$ and $\Sigma = \{\exists x \xi \mid \xi \in \Sigma'\}$. We assume, by $\alpha$-renaming, that $y < x$ for all $y \in fv(\phi)$.

Lemmata 4.6 and 4.7 relate the set of abstractions $\mathcal{A}_k(\phi)$ to the models of $\phi$. More precisely, Lem. 4.6 states that every abstraction $A \in \mathcal{A}_k(\phi)$ can be associated with a model of $\phi$ which satisfies all the properties stated in A (as defined in Def. 4.4). For all $V \subseteq \mathcal{V}$ and for all $k \in \mathbb{N}$, we denote by $\mathrm{Pt}(V, k)$ the set of non-equational patterns $\phi$ such that $fv(\phi) \subseteq V$ and $\mathrm{width}(\phi) \le k$.
**Lemma 4.6.** For every formula $\phi$ and for every abstraction $A = (V, \sim, \Sigma)$ in $\mathcal{A}_k(\phi)$ there exists a structure $(s, \mathfrak{h})$ satisfying the following properties:

1. $(s, \mathfrak{h}) \models_R \phi$.

2. For all $x, y \in V$, $x \sim y \iff s(x) = s(y)$.

3. If $\psi \in \mathrm{Pt}(V, k)$, $(s, \mathfrak{h}') \models_R \psi$ and $\mathfrak{h}' \subseteq \mathfrak{h}$ then $\Sigma$ contains a formula subsuming $\psi \downarrow$.

Conversely, Lem. 4.7 states a form of completeness: for every model $(s, \mathfrak{h})$ of $\phi$, $\mathcal{A}_k(\phi)$ contains some abstraction containing the properties fulfilled by $(s, \mathfrak{h})$.

**Lemma 4.7.** Let $\phi$ be a formula with $V = \mathrm{fv}(\phi)$ and $(s, \mathfrak{h})$ be an $\mathcal{R}$-model of $\phi$, with $\mathrm{dom}(s) = V$. The set $\mathcal{A}_k(\phi)$ contains an abstraction $A = (V, \sim, \Sigma)$ such that:

1. For all $x, y \in V$, $x \sim y \iff s(x) = s(y)$.

2. For all $\psi \in \Sigma$, there exists $\mathfrak{h}' \subseteq \mathfrak{h}$ such that $(s, \mathfrak{h}') \models_R \psi$.

Theorem 4.8 gives the decision procedure for testing $\mathcal{S}$-satisfiability and Corollary 4.9 states the main results of this section.

**Theorem 4.8.** Let $\phi$ be a formula, with $V = \mathrm{fv}(\phi)$, and let $S$ be a set of $\exists$-restricted patterns such that $\mathrm{width}(\psi) \le k$, for all $\psi \in S$. The two following statements are equivalent.

- The formula $\phi$ admits an $\mathcal{R}$-model $(s, \mathfrak{h})$ that is compatible with $S$.

- The set $\mathcal{A}_k(\phi)$ contains an abstraction $A$ of domain $V$ such that $A \nvdash \psi$, for all $\psi \in S$.

**Corollary 4.9.** The $\mathcal{S}$-satisfiability problem is in 2-EXPTIME for sets of restricted patterns $S$. If the size of the formulas in $S$ is bounded by a constant, then the problem is EXPTIME-complete.

**5 Lower Bound**

In this section, we show that $\mathcal{S}$-satisfiability is 2-EXPTIME-hard (for $\exists$-restricted patterns). The proof is based on a reduction from the membership problem for alternating Turing machines.

**Definition 5.1.** An Alternating Turing Machine (ATM) is a tuple $M = (Q, \Gamma, \delta, q_0, g)$ where:

- $Q$ is a finite set of states.

- $\Gamma$ is a finite alphabet, containing a special symbol $\mathbf{b}$, called the blank symbol.

- $\delta \subseteq Q \times \Gamma \times Q \times \Gamma \times \{\leftarrow, \rightarrow\}$ is the transition relation. The transition $(q, a, q', b, \mu) \in \delta$ specifies that, in state $q$, upon reading symbol $a$, the machine may move to state $q'$, write $b$ to the tape and move the head by one to the left (if $\mu = \leftarrow$) or to the right (if $\mu = \rightarrow$).

- $q_0 \in Q$ is the initial state.

- $g: Q \rightarrow \{\lor, \land\}$ partitions the set of states into existential ($g(q) = \lor$) and universal ($g(q) = \land$) states.
A configuration of an ATM $M = (Q, \Gamma, \delta, q_0, g)$ is a tuple $(q, w, i)$ where $q \in Q$ is the current state, $w : \mathbb{N} \to \Gamma$ is a tape, encoding a finite word on $\Gamma$, denoted by a function giving the symbol $w(j)$ stored in every cell $j \in \mathbb{N}$, where the set $\{j \in \mathbb{N} | w(j) \neq \text{B}\}$ is finite, and $i \in \mathbb{N}$ is the current position of the head on the tape. For any tape $w$ and integer $i$, we denote by $w[i \leftarrow a]$ the tape $w'$ which satisfies $w'(i) = a$ and $w'(j) = w(j)$ for all $j \neq i$. Let $i \stackrel{\text{def}}{=} i - 1$ if $i > 0$ (where $0^{-}$ is undefined) and $i \stackrel{\text{def}}{=} i + 1$. We assume that, since $0$ denotes the leftmost position on the tape, no transition moves the head left of $0$. The step relation of $M$ is a relation between configurations, defined as follows: $(q, w, i) \to (q', w', j)$ iff there exists a transition $(q, a, q', b, \mu) \in \delta$ such that $w(i) = a$, $w' = w[i \leftarrow b]$ and $j = i^{\mu}$ (assuming $i^{\mu}$ is defined, i.e., either $i > 0$ or $\mu = -\to$). The set of accepting configurations is defined inductively as follows. A configuration $(q, w, i)$ is accepting if one of the following conditions holds: (i) $g(q) = \lor$ and there exists a configuration $(q', w', j)$ such that $(q, w, i) \to (q', w', j)$ and $(q', w', j)$ is accepting. (ii) $g(q) = \land$ and all configurations $(q', w', j)$ such that $(q, w, i) \to (q', w', j)$ are accepting. In particular, if $g(q) = \land$ (resp. $g(q) = \lor$) and $\delta$ contains no transition of the form $(q, a, q', b, \mu)$ then $(q, w, i)$ is always (resp. never) accepting. A standard (non deterministic) Turing machine is an ATM where there are no transitions from universal states, which are thus accepting states. An ATM accepts a word $a_0...a_n \in (\Gamma \setminus \{\text{B}\})^*$ if the configuration $(q_0, w_0, 0)$ is accepting, with $w_0(i) = a_i$ if $0 \le i \le n$ and $w_0(i) = \text{B}$ otherwise. The membership problem ($M, w$) asks the following: given an ATM $M = (Q, \Gamma, \delta, q_0, g)$ and a word $w$ does $M$ accept $w$?

For any tape $w$, we denote by $|w|$ the length of $w$: $|w| = \text{card}(\{j \in \mathbb{N} | w(j) \neq \text{B}\})$. The ATM $M$ is exponential-space bounded if there exists a constant $c$ such that for every configuration $(q, w, i)$ with $(q_0, w_0, 0) \to^* (q, w, i)$, $|w| \le c \cdot 2^{p(|w_0|)}$, for some constant $c$ and polynomial function $p$. The complexity class AEXPSPACE is the class of membership problems where $M$ is exponential-space bounded. It is known that AEXPSPACE = co-AEXPSPACE = 2-EXPTIME [4], where co-AEXPSPACE is the complement class of AEXPSPACE<fnref n="1" />.

In the following, we shall consider the membership problem ($M, \epsilon$), where $\epsilon$ denotes the empty word. This is without loss of generality; indeed, let ($M, w$) be any instance of the membership problem, and let $c$ and $p$ be the constant and polynomial function witnesses the fact that $M$ is exponential-space bounded. Let $M_w$ be an ATM that produces $w$ starting from input $\epsilon$. Clearly, $M_w$ uses at most $|w|$ working space, thus the machine $M_w$; $M$, which runs $M_w$ on the empty word and then continues with $M$, runs in space $c \cdot 2^{p(|w|)}$ and accepts $\epsilon$ if and only if $M$ accepts $w$. If $N$ denotes any natural number with $N \ge \log_2(c) + p(w)$, then $M_w$; $M$ runs in space $2^N$ and moreover, $(M, w)$ and $(M_w, \epsilon)$ have the same answer. Therefore, we assume from now on that $M = (Q, \Gamma, \delta, q_0, g)$ is an ATM started in the configuration $(q_0, w_0, 0)$ with $w_0(j) = \text{B}$ for all $j \in \mathbb{N}$ and that $M$ runs in space at most $2^N$ on the empty input word, where $N$ is bounded by a polynomial in the length of $w$. We define a formula $\phi$ and a set of patterns $S$ (of polynomial size w.r.t. $M$ and $N$) such that $\phi$ is $S$-satisfiable iff the configuration $(q_0, w_0, 0)$ is accepting. This reduction ensures that any problem in AEXPSPACE is polynomially reducible to the $S$-satisfiability problem, thus that the latter problem is 2-EXPTIME-hard.

<footnote n="1">¹ Every ATM can be complemented in linear time, by simply interchanging the existential with the universal states, thus all alternating classes are closed under complement.</footnote>
All symbols $x \in \Gamma \cup \{0, 1, \leftarrow, \rightarrow\}$ are associated with pairwise distinct variables in $\mathcal{V}$, also denoted by $x$ to simplify notations and improve readability. These variables occur freely in the formula $\phi$ and in the set of patterns $\mathcal{S}$ and must be passed as parameters to every predicate in $\mathcal{P}_I$. For readability, we take this as implicit in the rules given below, i.e., any atom $P(x)$ with $P \in \mathcal{P}_I$ should be read $P(x, y)$ where $y$ is the sequence of variables in $\Gamma \cup \{0, 1, \leftarrow, \rightarrow\}$ (with any fixed order).

We first define a predicate $P$ which generates heaps denoting tapes of exponential size. The tape is encoded using a symbol $t \in \mathcal{P}_H$. Each cell in the tape is associated with a number encoded in binary and the atom $t(x, y_1, \dots, y_N, z)$ is used to assert that the cell numbered $y_1, \dots, y_N$ in the tape $x$ contains the symbol $z$. We also use a predicate $h \in \mathcal{P}_H$ to denote the position of the head in the tape: $h(x, y_1, \dots, y_N)$ states that the head of tape $x$ points to the cell number $(y_1, \dots, y_N)$. The predicate $P$ positions the head arbitrarily and call a predicate $P'$ which generates the content of each cell in the tape, starting from the one numbered $0, \dots, 0$.

$$ P(x) \leftarrow \exists y_1, \dots, y_N (h(x, y_1, \dots, y_N) * P'(x, 0, \dots, 0) * \overset{N}{\underset{i=1}{\ast}} d(y_i)) \\ d(x) \leftarrow x \approx 0 \qquad d(x) \leftarrow x \approx 1 $$

The atom $P'(x, y_1, \dots, y_N)$ chooses the content $z \in \Gamma$ of the cell numbered $y_1, \dots, y_N$ and allocates the corresponding atom $t(x, y_1, \dots, y_N, z)$. If $y_1, \dots, y_N$ is not $(1, \dots, 1)$ then it recursively calls $P'$ on the next cell. To this purpose, one needs to increase $y_1, \dots, y_N$ by 1. This can be done by adding different rules for each $i \in \{1, \dots, N\}$, where $i$ denotes the index of the rightmost digit in $y_1, \dots, y_N$ that is equal to 0. In each of these rules, we add conditions stating that $y_i$ is 0 and that $y_{i+1}, \dots, y_N = 1$, so that the next cell is necessarily numbered $(y_1, \dots, y_{i-1}, 1, 0, \dots, 0)$. Note that, in all cases, one rule is required for each $z \in \Gamma$.

$$ P'(x, y_1, \dots, y_N) \leftarrow (t(x, y_1, \dots, y_N, z) * P'(x, y_1, \dots, y_{i-1}, 1, 0, \dots, 0) \\ \qquad * y_i \approx 0 * \overset{N}{\underset{j=i+1}{\ast}} (y_j \approx 1)) \quad \text{for all } z \in \Gamma \text{ and } i \in \{1, \dots, N\} $$

$$ P'(x, y_1, \dots, y_N) \leftarrow t(x, y_1, \dots, y_N, z) * \overset{n}{\underset{j=1}{\ast}} (y_j \approx 1) \quad \text{for all } z \in \Gamma $$

We introduce a predicate $a \in \mathcal{P}_H$ which will encode the actions applied on the tapes: $a(x, y, u, v, w)$ states that the tape $y$ is obtained from a tape $x$ by replacing the symbol $u$ occurring at the head position by $v$, then by applying the move $w$ on the head. We then introduce a predicate $q \in \mathcal{P}_I$ for every state $q \in \mathcal{Q}$, generating potential derivations from state $q$. More precisely, the atom $q(x)$ allocates the action applied on a tape $x$ at state $q$ and the new tape $y$, then calls the predicate $q'(y)$ corresponding to the target state. If $g(q) = \lor$ then one transition is chosen undeterministically in every rule, yielding one action and one tape, whereas if $g(q) = \land$ then all transitions corresponding to the state $q$ and some (arbitrarily chosen) symbol $a$ must be applied, yielding several actions and tapes in the same rule. Note that, at this point, we do not check that the content of the tape $x$ is coherent with the selected transition (such conditions will be asserted later, by formulas in $\mathcal{S}$).

$$ q(x) \leftarrow \exists y (a(x, y, a, b, \mu) * P(y) * q'(y)) \\ \qquad \text{for all } q, a, q', b, \mu \text{ such that } g(q) = \lor \text{ and } (q, a, q', b, \mu) \in \delta $$
$$q(x) \leftarrow \exists y_1, \dots, y_N *_{i=1}^n (a(x, y_i, a, b_i, \mu_i) * P(y_i) * q_i(y_i))$$

for all $q$ such that $g(q) = \wedge$, for all $a \in \Gamma$

where $\{(q, a, q_i, b_i, \mu_i) | i \in \{1, \dots, n\}\}$ is the set of transitions of the form $(q, a, q', b, \mu)$

We then define a set of patterns $S$ which assert various constraints ensuring that the derivation encoded by the construction above is valid, i.e., that the applied transitions are in coherence with the tape content. The first formula states that the initial tape $x_0$ is empty. To this purpose it suffices to check that it contains no cell of the form $t(x_0, y_1, \dots, y_N, z)$ with $z \notin \mathbf{B}$, which is asserted by adding the following pattern in $S$ (remind that $S$-satisfiability is defined by excluding all structures containing a subheap satisfying one of the patterns in $S$):

$$\exists y_1, \dots, y_N t(x_0, y_1, \dots, y_N, z) \quad \text{for all } z \neq \mathbf{B}$$

Similarly, to encode the fact that the head initially points to $(0, \dots, 0)$, we introduce patterns ruling out all atoms $h(x_0, y_1, \dots, y_N)$ where $y_i = 1$ for some $i \in \{1, \dots, N\}$:

$$\exists y_1, \dots, y_{N-1} h(x_0, y_1, \dots, y_{i-1}, 1, y_i, y_{N-1}) \quad \text{for all } i \in \{1, \dots, N\}$$

We then encode the relation between tapes and actions. We first check that, if the structure contains an atom $a(x, x', u, v, w)$ (meaning that tape $x'$ is obtained from $x$ by replacing $a$ by $b$ and applying move $w$), then necessarily the cell corresponding to the head position in $x$ must contain $a$ in $x$ and $b$ in $x'$. As the head position in encoded by an atom $h(x, y_1, \dots, y_N)$, this yields the following pattern:

$$\exists x, x', y_1, \dots, y_N (a(x, x', u, v, w) * h(x, y_1, \dots, y_N))$$

$$* t(x, y_1, \dots, y_N, z) * t(x', y_1, \dots, y_N, z')$$

for all $u, v \in \Gamma$, for all $w \in \{\leftarrow, \rightarrow\}$ and for all $z, z' \in \Gamma$ with $z \neq u$ or $z' \neq v$

By excluding structures containing heaps satisfying the above pattern, we ensure that the head of $x$ points to a cell containing $u$ in $x$ and $v$ in $x'$. To state that all the cells other than the one numbered $y_1, \dots, y_N$ are unaffected by the above action, we introduce the following formulas:

$$\exists x, x', y_1, \dots, y_{N-1}, y'_1, \dots, y'_{N-1} (a(x, x', u, v, w) * h(x, y_1, \dots, y_i, y, y_{i+1}, \dots, y_{N-1}))$$

$$* t(x, y_1, \dots, y_i, y', y_{i+1}, \dots, y_{N-1}, z) * t(x, y_1, \dots, y_i, y', y_{i+1}, \dots, y_{N-1}, z')$$

for all $i \in \{0, \dots, N-1\}$, for all $y, y' \in \{0, 1\}$ and for all $z, z' \in \Gamma$ with $y \neq y'$ and $z \neq z'$

Here the head points to the cell numbered $(y_1, \dots, y_i, y, y_{i+1}, \dots, y_{N-1})$ (where $y$ is some particular distinguished digit, that is fixed in each rule). The pattern rules out structures in which a cell numbered $y_1, \dots, y_i, y', y_{i+1}, \dots, y_{N-1}$ (where $y'$ is some digit distinct from $y$) has distinct content in $x$ and $x'$. This is stated by allocating atoms of the form $t(x, y_1, \dots, y_i, y', y_{i+1}, \dots, y_{N-1}, z)$ and $t(x, y_1, \dots, y_i, y', y_{i+1}, \dots, y_{N-1}, z')$ (with $z, z' \in \Gamma$ and $z \neq z'$). One such formula is added for all $i \in \{0, \dots, N-1\}$ and for all distinct digits $y, y'$ and symbols $z, z'$, and ruling out all these patterns ensures that the content of any cell other than that of head of $x$ is the same in $x$ and $x'$.
The next two formulas encode the effect of a move to the right. They state that if the current head position is numbered ($y_1, \dots, y_i, 0, 1, \dots, 1$) then the position after the move should be ($y_1, \dots, y_i, 1, 0, \dots, 0$). As the constraints are expressed negatively, this is stated by discarding positions that differ from the latter sequence of digits. To state that the positions are not identical, we ensure that they differ by at least one digit (the last one that is distinct in both sequence). To this purpose, we assume that $j$ denotes the index of the rightmost faulty digit. The first formula covers the case where this digit occurs inside the suffix $1, 0, \dots, 0$. The case $j = i + 1$ covers the case where the first digit in the sequence is 0 instead of 1, while the case $j > i + 1$ occurs when one of the 0 is 1 instead of 0.

$$ \exists x, x', y_1, \dots, y_{j-1} (a(x, x', u, v, \rightarrow) * h(x, y_1, \dots, y_i, 0, 1, \dots, 1) \\ * h(x', y_1, \dots, y_i, y_{i+1}, \dots, y_{j-1}, u, 0, \dots, 0)) \\ \text{for all } u, v \in \Gamma \text{ and } i, j \in \{1, \dots, N\} \text{ where } j > i \\ \text{and either } j = i + 1 \text{ and } u = 0 \text{ or } j > i + 1 \text{ and } u = 1 $$

The formula below covers the case where the suffix is correct, but the faulty digit occurs inside the prefix $y_1, \dots, y_i$.

$$ \exists x, x', y_1, \dots, y_i, y'_1, \dots, y'_{j-1} (a(x, x', u, v, \rightarrow) * h(x, y_1, \dots, y_{j-1}, y, y_{j+1}, \dots, y_i, 0, 1, \dots, 1) \\ * h(x', y'_1, \dots, y'_{j-1}, y', y_{j+1}, \dots, y_i, 1, 0, \dots, 0) \\ \text{for all } u, v \in \Gamma, y, y' \in \{0, 1\} \text{ and } i, j \in \{1, \dots, N-1\}, \text{ where } j \le i \text{ and } y \ne y' $$

Similar patterns can be added to encode the effect of the moves to the left (they are omitted for conciseness). The next formula ensures that all the tapes are pairwise distinct:

$$ \exists x (h(x, 0, \dots, 0) * h(x, 0, \dots, 0)) $$

It is easy to check that the formula $P(x_0) * q_0(x_0)$ admits a model compatible with the above patterns iff the configuration $(q_0, w_0, 0)$ is accepting. This yields the following:

**Theorem 5.2.** *The S-satisfiability problem is 2-EXPTIME-hard for $\exists$-restricted sets of patterns S.*

# 6 Undecidability Result

We now show that the S-satisfiability problem is undecidable if the patterns under consideration are not $\exists$-restricted, i.e., if disequations<fnref n="2" /> containing existential variables are allowed inside formulas in S. The proof goes by a reduction from the halting problem on ATM (TM are sufficient but the reduction is given for ATM for the sake of uniformity). The encoding we use is similar to that of Sect. 5, except that cell numbers are represented as locations (linked by a predicate next) rather than sequences of digits. Because disequalities on existential variables are now allowed, we can assert that two cell numbers (denoted by locations) x and y are distinct using the formula $x \neq y$. This

<footnote n="2">² Note that the equations containing existential variables are not problematic as they can always be eliminated using the equivalence: $\exists x (x \approx y * \phi) \equiv \phi\{x \mapsto y\}$.</footnote>
eliminates the need to explicitly instantiate $x$ and $y$ with distinct sequences of digits, as was done in Sect. 5 and greatly simplifies the encoding.

We consider any $\mathbf{ATM} M = (Q, \Gamma, \delta, q_0, g)$ and encode accepting derivations starting from an empty tape. The rules of the predicate $P$ are adapted as follows. Instead of generating a tape of exponential size, they generate a tape of arbitrary size, in which the cell numbers are encoded as locations, chained using **next**. The variables $y_0$ and $y_f$ denote the first and last cell numbers, respectively, and $t(x, y, z)$ asserts that the cell numbered $y$ in tape $x$ contains the symbol $z$.

$$ 
\begin{align*}
P(x, y_0, y_f) &\Leftarrow \exists y (h(x, y) * P'(x, y_0, y_f)) \\
P'(x, y, y_f) &\Leftarrow \exists y' (t(x, y, z) * P'(x, y', y_f) * \mathbf{next}(y, y') * y \neq y_f) \quad \text{for all } z \in \Gamma \\
P(x, y, y_f) &\Leftarrow (t(x, y, z) * y \approx y_f) \quad \text{for all } z \in \Gamma
\end{align*}
$$

The predicates corresponding to states are defined as in Sect. 5. The definition of the set of patterns $S$ is adapted as follows. In contrast to Sect. 5, we also need to ensure that there is no move to the right of the last cell and that the predicate **next** is functional (note that the same atom **next**($x, y$) may occur several times in the structure).

$$ 
\begin{align*}
\exists y t(x_0, y, z) \quad &\text{for all } z \neq \mathbf{B} \qquad \exists y (h(x_0, y) * y \neq y_0) \\
&\exists x, x', y (a(x, x', u, v, w) * h(x, y) * t(x, y, z) * t(x', y, z')) \\
&\quad \text{for all } u, v \in \Gamma, w \in \{\leftarrow, \rightarrow\} \text{ and } z, z' \in \Gamma \text{ with } z \neq u \text{ or } z' \neq v \\
\exists x, x', y, y' (a(x, x', u, v, w) * h(x, y) * y \neq y' * t(x, y', z) * t(x', y', z')) \\
&\quad \text{for all } u, v \in \Gamma, w \in \{\leftarrow, \rightarrow\} \text{ and } z, z' \in \Gamma \text{ such that } z \neq z' \\
\exists x, x', y, y' (a(x, x', u, v, \rightarrow) * h(x, y) * \mathbf{next}(y, y') * h(x', y'') * y'' \neq y') \quad \forall u, v \in \Gamma \\
&\quad \exists x (h(x, y_0) * h(x, y_0)) \\
\exists x, x' (a(x, x', u, v, \rightarrow) * h(x, y_f)) \quad &\text{\% no move to the right of the last cell} \\
\exists y, y_1, y_2 (\mathbf{next}(y, y_1) * \mathbf{next}(y, y_2) * y_1 \neq y_2) \quad &\text{next is functional}
\end{align*}
$$

The formula $P(x_0) * q_0(x_0)$ admits a model compatible with the above patterns iff the configuration $(q_0, \epsilon, 0)$ is accepting. As $M$ is arbitrary, we get:

**Theorem 6.1.** *The S-satisfiability problem is undecidable for non $\exists$-restricted sets of patterns S.*

# 7 Conclusion

We developed a doubly exponential algorithm to check the satisfiability of formulas in the separation logic of relations, under additional constraints defined by sets of patterns of a specific form that are excluded from the structures. We proved that this algorithm is optimal and that the problem becomes undecidable when a more general class of patterns is considered. These results significantly advance existing satisfiability testing algorithms for certain variants of separation logic and provide a clearer boundary for the types of properties that can be imposed on structures without losing the decidability of the satisfiability problem. Importantly, unlike [5] (which focuses on a decidable fragment of the entailment problem in SLR), our approach imposes no restrictions on the inductive rules defining the semantics of the predicate symbols; the only limitations apply to the patterns. We plan to extend this algorithm to target more expressive languages. Specifically, we aim to broaden the logic to represent structures that include data interpreted over fixed theories, such as arithmetic.
## References

1. E. Ahrens, M. Bozga, R. Iosif, and J. Katoen. Reasoning about distributed reconfigurable systems. *Proc. ACM Program. Lang.*, 6(OOPSLA2):145–174, 2022.

2. M. Bozga, L. Bueri, and R. Iosif. Decision problems in a logic for reasoning about reconfigurable distributed systems. In J. Blanchette, L. Kovács, and D. Pattinson, editors, *Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings*, volume 13385 of *Lecture Notes in Computer Science*, pages 691–711. Springer, 2022.

3. J. Brotherston, C. Fuhs, J. A. N. Pérez, and N. Gorogiannis. A decision procedure for satisfiability in separation logic with inductive predicates. In T. A. Henzinger and D. Miller, editors, *Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 25:1–25:10. ACM, 2014.

4. A. K. Chandra, D. Kozen, and L. J. Stockmeyer. Alternation. *J. ACM*, 28(1):114–133, 1981.

5. M. Echenim and N. Peltier. A direct procedure to test entailment in a separation logic of relations. Research report (under review), 2024. https://lig-membres.imag.fr/peltier/RSL.pdf.

6. S. S. Ishtiaq and P. W. O'Hearn. Bi as an assertion language for mutable data structures. In *ACM SIGPLAN Notices*, volume 36, pages 14–26, 2001.

7. V. Kuncak and M. C. Rinard. Generalized records and spatial conjunction in role logic. In R. Giacobazzi, editor, *Static Analysis, 11th International Symposium, SAS 2004, Verona, Italy, August 26-28, 2004, Proceedings*, volume 3148 of *Lecture Notes in Computer Science*, pages 361–376. Springer, 2004.

8. N. Peltier. An exptime-complete entailment problem in separation logic. In G. Metcalfe, T. Studer, and R. J. G. B. de Queiroz, editors, *Logic, Language, Information, and Computation - 30th International Workshop, WoLLIC 2024, Bern, Switzerland, June 10-13, 2024, Proceedings*, volume 14672 of *Lecture Notes in Computer Science*, pages 157–174. Springer, 2024.

9. J. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In *Proc. of LICS'02*, 2002.

## A Proof of Lemma 4.6

The proof proceeds by induction on the set $\mathcal{A}_k(\phi)$.

- Assume that $\phi = \mathbf{emp}$ and $A = (\emptyset, \emptyset, \{\mathbf{emp}\})$, i.e., $V = \emptyset = \text{fv}(\phi)$, $\sim$ is empty and $\Sigma = \{\mathbf{emp}\}$. Let $s$ be an arbitrary store, and let $b = \emptyset$. By definition, $(s, b) \models_R \phi$, hence Assertion 1 holds. Assertion 2 trivially holds because $V = \emptyset$. Moreover, the only formula $\psi \in \text{Pt}(V, k)$ such that $(s, b') \models_R \psi$ for some $b' \subseteq b$ is $\mathbf{emp}$ (as the only atoms in formulas in $\text{Pt}(V, k)$ are $\mathcal{P}_H$-atoms or $\mathbf{emp}$, and no $\mathcal{P}_H$-atom can be satisfied on an empty heap), thus Assertion 3 holds (as $\mathbf{emp}$ subsumes itself).

- Assume that $\phi = (x \approx y)$ and $A = (\{x, y\}, \{x \sim y\}, \{\mathbf{emp}\})$, i.e., $V = \{x, y\} = \text{fv}(\phi)$, $u \sim v$ holds for all $u, v \in V$ (remember that $\sim$ is closed under reflexivity, symmetry and transitivity) and $\Sigma = \{\mathbf{emp}\}$. Let $s$ be an arbitrary store such that $s(x) = s(y)$ and let $b = \emptyset$. It is clear that Assertions 1 and 2 hold. As in the previous case, the only formula $\psi \in \text{Pt}(V, k)$ such that $(s, b') \models_R \psi$ for some $b' \subseteq b$ is $\mathbf{emp}$, thus Assertion 3 holds.
- Assume that $\phi = (x \neq y)$ and $A = (\{x, y\}, \emptyset, \{\text{emp}\})$, i.e., $V = \{x, y\} = \text{fv}(\phi)$, $u \sim v$ holds iff $u = v$ and $\Sigma = \{\text{emp}\}$. Let $s$ be an arbitrary store such that $s(x) \neq s(y)$ and let $h = \emptyset$. As in the previous cases, it is straightforward to check that Assertions 1, 2, and 3 hold.

- Assume that $\phi = p(x_1, \dots, x_n)$ with $p \in \mathcal{P}_H$ and that the abstraction $\mathcal{A}_k(\phi)$ is of the form $(\{x_1, \dots, x_n\}, \sim, \{\text{emp}, \phi \downarrow_{\sim}\})$, where $\sim$ is an equivalence relation on $\{x_1, \dots, x_n\}$. Then $V = \{x_1, \dots, x_n\} = \text{fv}(\phi)$ and $\Sigma = \{\text{emp}, \phi \downarrow_{\sim}\}$. Let $s$ be any store such that $s(x_i) = s(x_j)$ iff $x_i \sim x_j$ (such a store always exists as $\mathcal{L}$ is infinite). Assertion 2 holds by definition of $s$. Let $h$ be the heap $\{p(s(x_1), \dots, s(x_n))\}$. By definition of $h$, $(s, h) \models_R \phi$, i.e., Assertion 1 holds. Now, consider any formula $\psi \in \text{Pt}(V, k)$ such that $(s, h') \models_R \psi$, for some $h' \subseteq h$. We show that $\psi$ is subsumed by a formula in $\Sigma$. The result is immediate if $h' = \emptyset$, as necessarily $\psi = \text{emp}$ in this case, and $\text{emp}$ occurs in $\Sigma$. Otherwise, we must have $h' = h$. Since $\psi \in \text{Pt}(V, k)$, $\psi$ is of the form $\exists y *_{i=1}^m p_i(z_i^1, \dots, z_i^{n_i})$ with $p_i \in \mathcal{P}_H$. As $h$ is of cardinality 1 and $(s, h) \models_R \psi$, we must have $m = 1$ (as every atom $p_i(z_i)$ is satisfied only on heaps of cardinality 1). Thus, there exists a store $s'$, coinciding with $s$ on all variables not occurring in $y$ such that $(s', h) \models_R p_1(z_1^1, \dots, z_1^{n_1})$. By definition of $h$, this entails that $p_1 = p$, $n_1 = n$ and that $s'(z_1^i) = s(x_i)$ for all $i \in \{1, \dots, n\}$. Consequently, $z_1^i \downarrow_{\sim} = x_i \downarrow_{\sim}$ for all $i$ such that $z_1^i \in \{x_1, \dots, x_n\}$. Let $\sigma$ be a substitution mapping every variable $z_1^i$ occurring in $y$ to $x_i \downarrow_{\sim}$. We get $p(z_1^1, \dots, z_1^n) \downarrow_{\sim} \sigma = \phi \downarrow_{\sim}$, so that $\psi \downarrow_{\sim}$ is subsumed by the formula $\phi \downarrow_{\sim}$ that occurs in $\Sigma$. Hence Assertion 3 holds.

- Assume that $\phi = P(x_1, \dots, x_n)$ and $A \in \mathcal{A}_k(\xi)$ for some $\xi$ such that $\phi \Leftarrow_R \xi$. By the induction hypothesis, there exists a model $(s, h)$ of $\xi$ such that Assertions 2 and 3 hold. As every model of $\xi$ is also a model of $\phi$, Assertion 1 is also satisfied.

- Assume that $\phi = \phi_1 \lor \phi_2$ and $A \in \mathcal{A}_k(\phi_i)$ for some $i \in \{1, 2\}$. By the induction hypothesis, there exists a model $(s, h)$ of $\phi_i$ such that Assertions 2 and 3 hold. As every model of $\phi_i$ is also a model of $\phi$, we get the result.

- Assume that $\phi = \phi_1 * \phi_2$ and that $\mathcal{A}_k(\phi_i)$ contains abstractions $(V_i, \sim_i, \Sigma_i) \in \mathcal{A}_k(\phi_i)$ (for all $i \in \{1, 2\}$), where $V = V_1 \cup V_2$, $\sim$ agrees with $\sim_i$ on $V_i$, and $\Sigma$ is the tuple $\{(\phi_1 * \phi_2) \downarrow_{\sim} | \phi_i \in \Sigma_i, \text{width}(\phi_1) + \text{width}(\phi_2) \le k\}$. By the induction hypothesis, there exist structures $(s_i, h_i)$ such that $(s_i, h_i) \models_R \phi_i; x \sim_i y \iff s_i(x) = s_i(y)$ (for all $x, y \in V_i$); and if $\psi \in \text{Pt}(V_i, k)$ and $(s_i, h') \models_R \psi$ for some $h' \subseteq h_i$ then $\Sigma_i$ contains a formula subsuming $\psi \downarrow_{\sim_i}$. Let $s$ be any store such that the equivalence $x \sim y \iff s(x) = s(y)$ holds for all $x, y \in V$. By definition, Assertion 2 is satisfied. Let $\mathcal{L}_1, \mathcal{L}_2$ be disjoint infinite subsets of $\mathcal{L}$, which are also disjoint from $s(V)$. As $\sim$ agrees with $\sim_i$ on all variables in $V_i$, we get $s(x) = s(y) \iff s_i(x) = s_i(y)$ for all $x, y \in V_i$. Thus one can construct an injective mapping $\lambda_i$ from $s_i(V_i) \cup \mathcal{L}(h_i)$ to $s(V_i) \cup \mathcal{L}_i$ such that $\lambda_i(s_i(x)) = s(x)$, for all $x \in V_i$, and $\lambda_i(\ell) \in \mathcal{L}_i$ if $\ell \notin s(V_i)$. By Prop. 2.6 we have $(\lambda_i \circ s_i, \gamma(h_i)) \models_R \phi_i$, thus (as $s$ coincides with $\lambda_i \circ s_i$ on every variable occurring in $V_i = \text{fv}(\phi_i)$), we get $(s, \lambda_i(h_i)) \models_R \phi_i$. Let $h = \lambda_1(h_1) + \lambda_2(h_2)$. By definition, we have $(s, h) \models_R \phi_1 * \phi_2 = \phi$, hence Assertion 1 holds. It only remains to show that Assertion 3 is satisfied. Consider a formula $\psi \in \text{Pt}(V, k)$ such that $(s, h') \models_R \psi$ for some $h' \subseteq h$. We must show that $\Sigma$ contains a formula subsuming $\psi \downarrow_{\sim}$. By definition of $h$, $h'$ must be of the form $h'_1 + h'_2$ where $h'_i \subseteq \lambda_i(h_i)$. Moreover, the formula $\psi$ is of the form $\exists y *_{i=1}^n p_i(z_i)$ with $p_i \in \mathcal{P}_H$. We assume by $\alpha$-renaming that $y$ contains no variable in $V$. As $(s, h') \models_R \psi$, there exists a store $s'$, coinciding with $s$ on all variables not occurring in $y$, such that $(s', h') \models_R \xi$. Let $\sigma$ be any substitution mapping every variable $y$ in $y$ to an arbitrary chosen variable $y' \in V$ such that $s(y') = s'(y)$, if such a variable exists, otherwise $y\sigma = y$. By definition,
(s', b') ⊨_R ξσ, and for all variables y occurring in y and ξσ, we must have s'(y) ∉ s(V). As each atom p_i(z_i) is satisfied only on heaps of size 1, one can partition the set {1, ..., n} into sets I_1, I_2 such that i ∈ I_j iff the part of the heap that corresponds to p_i(z_i) is in I_j. Let ξ_j = *_{i∈I_j} p_i(x_i), we get (s', b'_j) ⊨_R ξ_jσ and ξ = ξ_1 * ξ_2 (up to AC of *). Let y_j be the sequence of the variables in y that occur in ξ_jσ, we get (s, b'_j) ⊨_R ∃y_j ξ_jσ. Since ψ ∈ Pt(V, k), necessarily width(ψ) ≤ k, i.e., n ≤ k, so that width(∃y_j ξ_j) = card(I_j) ≤ k. As (s', b'_j) ⊨_R ξ_jσ, for every variable x ∈ fv(ξ_j), we have s'(x) ∈ L(b'_j) ⊆ L(λ_j(b_j)). Thus if moreover x ∈ V \ V_j, then by definition of λ_j (since L(λ_j(b_j)) ⊆ s(V_j) ∪ L_j and L_j ∪ s(V) = ∅) there must exist some variable x' ∈ V_j such that s(x) = s(x'). Let θ_j be a substitution mapping every such variable x ∈ (V ∩ fv(ξ_j)) \ V_j to a variable x' ∈ V_j with the same value in s. We get (s, b'_j) ⊨_R ∃y_j ξ_jσθ_j, thus (as fv(∃y_j ξ_jθ_j) ⊆ V_j) (λ ∘ s_j, b'_j) ⊨_R ∃y_j ξ_jσθ_j. Using Prop. 2.6, we deduce that (s_j, b_j) ⊨_R ∃y_j ξ_jσθ_j, so that (by the induction hypothesis) Σ_j contains a formula ψ'_j subsuming ∃y_j ξ_jσθ_j ↓_~, By definition of the subsumption relation, the formula ψ'_j is of the form ∃y'_j ξ'_jσθ'_jη'_j ↓_~, where η_j is a substitution and y'_j is the subsequence of the variables in y_j that do not occur in the domain of η_j. Then Σ necessarily contains the formula (ψ'_1 * ψ'_1) ↓_~. Up to prenex form, and using the fact that ~_1 and ~_2 are included in ~, the formula (ψ'_1 * ψ'_2) ↓_~ may be written on the form: ∃y'_1 ∃y'_2 (ξ_1σθ_1η_1 * ξ_2σθ_2η_2) ↓_~. By definition xθ_i ↓_~ = x ↓_~ (as x ~ xθ_i) thus (ψ'_1 * ψ'_2) ↓_~ is of the form: ∃y'_1 ∃y'_2 (ξ_1 * ξ_2)ση ↓_~, where xη = xη_1η_2 ↓_~, i.e., of the form ∃y'_1 ∃y'_2 (ξ_1 * ξ_2) ↓_~ σ', with xσ' = xση ↓_~. Therefore, (ψ'_1 * ψ'_2) ↓_~ subsumes the formula ψ ↓_~.

- Assume that $\phi = \exists x \phi'$ and that there exists $(V', \sim', \Sigma') \in \mathcal{A}_k(\phi')$ such that $V = V' \setminus \{x\}$,
  ~ is the restriction of $\sim'$ to $V$ and $\Sigma = \{\exists x \xi \mid \xi \in \Sigma'\}$. By the induction hypothesis there
  exists a structure $(s, \mathfrak{h})$ such that $(s, \mathfrak{h}) \models_R \phi', x \sim' y \iff s(x) = s(y)$ (for all $x, y \in V'$)
  and for all formulas $\psi \in \mathrm{Pt}(V', k)$ and heaps $\mathfrak{h}' \subseteq \mathfrak{h}$, if $(s, \mathfrak{h}') \models_R \psi$ then $\Sigma'$ contains
  a formula subsuming $\psi \downarrow$. This entails that Assertions 1 and 2 hold (as $\phi$ is a logical
  consequence of $\phi'$ and $V \subseteq V'$). Consider a formula $\psi \in \mathrm{Pt}(V, k)$ and a heap $\mathfrak{h}' \subseteq \mathfrak{h}$
  such that $(s, \mathfrak{h}') \models_R \psi$. As $V \subseteq V'$, we deduce that $\psi \in \mathrm{Pt}(V', k)$, so that $\Sigma'$ contains
  a formula $\xi$ subsuming $\psi \downarrow$. By definition, $\psi$ must be of the form $\exists y \exists z \psi'$ and there
  exists a substitution $\sigma$ of domain $y$ such that $\xi = \exists z (\psi' \downarrow, \sigma)$. We may assume by $\alpha$-
  renaming that $y$ and $z$ contain no variable in $V'$ (hence $x$ does not occur in $y$ or $z$). Then
  $\Sigma$ contains the formula $\exists x \xi$. Since (by the assumption in Def. 4.5), $y < x$ holds for all
  $y \in \mathrm{fv}(\phi)$, we have $u \downarrow = u \downarrow$ for all variables $u \neq x$. Since $x$ cannot occur in $\mathrm{fv}(\psi')$ (as
  $\psi \in \mathrm{Pt}(V, k)$, thus $\mathrm{fv}(\psi) \subseteq V$, and $x$ does not occur in $y$ or $z$), we get $\xi = \exists z (\psi' \downarrow, \sigma)$.
  If $x \notin \mathrm{fv}(\xi)$ then $\exists x \xi = \xi$ subsumes $\psi \downarrow$ and the proof is completed. Otherwise, $y$
  contains a variable $y$ such that $y\sigma = x$, then $y$ is of the form $(y', y)$. Up to $\alpha$-renaming,
  $\exists x \xi$ is of the form $\exists y \xi\{x \mapsto y\}$ and we get $\exists y \xi\{x \mapsto y\} = \exists y \exists z (\psi' \downarrow, \sigma')$, where $\sigma'$ is
  the restriction of $\sigma'$ to the variables distinct from $y$, with $\psi \downarrow = \exists y' \exists y \exists z \psi' \downarrow$, so that
  $\exists x \xi$ subsumes $\psi \downarrow$.

B Proof of Lemma 4.7

The proof is by induction on the satisfiability relation.

- If $\phi = \text{emp}$, then by Def. 4.5, $\mathcal{A}_k(\phi)$ contains an abstraction $(\emptyset, \emptyset, \{\text{emp}\})$. By definition, $V = \emptyset$ and $\mathfrak{h} = \emptyset$, so that the two assertions of the lemma trivially hold.
- If $\phi = (x \approx y)$, then, by Def. 4.5, $\mathcal{A}_k(\phi)$ contains an abstraction $(\{x, y\}, \{x \sim y\}, \{\text{emp}\})$. By definition, $V = \{x, y\}$, $s(x) = s(y)$ and $h = \emptyset$, so that we get $u \sim v \iff s(u) = s(v)$ (for all $u, v \in V$) and $(s, h) \models_R \text{emp}$.

- If $\phi = (x \not\approx y)$, then, by Def. 4.5, $\mathcal{A}_k(\phi)$ contains an abstraction $(\{x, y\}, \emptyset, \{\text{emp}\})$. By definition, $V = \{x, y\}$, $s(x) \neq s(y)$ and $h = \emptyset$, so that $u \sim v \iff s(u) = s(v)$ (for all $u, v \in V$) and $(s, h) \models_R \text{emp}$.

- If $\phi = p(x_1, \dots, x_n)$ with $p \in \mathcal{P}_H$ then $V = \{x_1, \dots, x_n\}$ and, by Def. 4.5, $\mathcal{A}_k(\phi)$ contains an abstraction $(\{x_1, \dots, x_n\}, \sim, \{\text{emp}, \phi \downarrow\})$, where $\sim$ is the equivalence relations of $V$ such that $u \sim v \iff s(u) = s(v)$ (for all $u, v \in V$). By Def. 2.4, $h = \{p(s(x_1), \dots, s(x_n))\}$, so that $(s, h) \models_R \phi$, and therefore $(s, h) \models_R \phi \downarrow$. Moreover, we also have $(s, \emptyset) \models_R \text{emp}$, with $\emptyset \subseteq h$.

- If $\phi$ is a $\mathcal{P}_I$-atom, then by definition $(s, h) \models_R \psi$ for some formula $\psi$ such that $\phi \Leftarrow_R \psi$. Note that (as the right-hand side of inductive rules contains all the variables in the left-hand side) necessarily $fv(\psi) = fv(\phi) = V$. By the induction hypothesis, $\mathcal{A}_k(\psi)$ contains an abstraction $A = (V, \sim, \Sigma)$ such that $x \sim y \iff s(x) = s(y)$ (for all $x, y \in V$) and for all $\psi \in \Sigma$, there exists $h' \subseteq h$ such that $(s, h') \models_R \psi$. By Def. 4.5, $A \in \mathcal{A}_k(\phi)$.

- If $\phi = \phi_1 \lor \phi_2$, then by definition $(s, h) \models_R \phi_i$ for some $i \in \{1, 2\}$. By the above assumption on disjunctions, $fv(\phi_i) = V$. By the induction hypothesis, $\mathcal{A}_k(\phi_i)$ contains an abstraction $A = (V, \sim, \Sigma)$ such that $x \sim y \iff s(x) = s(y)$ (for all $x, y \in V$) and for all $\psi \in \Sigma$, there exists $h' \subseteq h$ such that $(s, h') \models_R \psi$. By Def. 4.5, $A \in \mathcal{A}_k(\phi)$.

- If $\phi = \phi_1 * \phi_2$, then by definition, there exist heaps $h_1, h_2$ such that $(s, h_i) \models_R \phi_i$ for all $i \in \{1, 2\}$, and $h = h_1 + h_2$. Let $V_i = fv(\phi_i)$. By the induction hypothesis, $\mathcal{A}_k(\phi_i)$ contains an abstraction $A_i = (V_i, \sim_i, \Sigma_i)$ such that $x \sim_i y \iff s(x) = s(y)$ (for all $x, y \in V_i$) and for all $\psi \in \Sigma_i$, there exists $h'_i \subseteq h_i$ such that $(s, h'_i) \models_R \psi$. Let $\sim$ be the equivalence relation such that $x \sim y \iff s(x) = s(y)$ (for all $x, y \in V$). By definition, $\sim$ coincides with $\sim_i$ on $V_i$. Moreover, $V = V_1 \cup V_2$. By Def. 4.5, $\mathcal{A}_k(\phi)$ contains the abstraction $(V, \sim, \Sigma)$ with $\Sigma = \{(\phi_1 * \phi_2) \downarrow | \phi_i \in \Sigma_i, \text{width}(\phi_1) + \text{width}(\phi_2) \le k\}$. Let $\psi \in \Sigma$. By definition, $\psi = (\psi_1 * \psi_2) \downarrow$ with $\psi_i \in \Sigma_i$, so that there exists $h'_i$ with $h'_i \subseteq h_i$ and $(s, h'_i) \models_R \psi_i$ (for all $i \in \{1, 2\}$). This entails that $(s, h'_1 + h'_2) \models_R (\psi_1 * \psi_2) \downarrow = \psi$ with $h'_1 + h'_2 \subseteq h_1 + h_2 = h$.

- If $\phi = \exists x \psi$ then by definition there exists a store $s'$ coinciding with $s$ on any variable other than $x$ such that $(s', h) \models_R \psi$. By the induction hypothesis, we deduce that $\mathcal{A}_k(\psi)$ contains an abstraction $(V', \sim', \Sigma')$ such that $V' = fv(\psi)$, $u \sim v \iff s'(u) = s'(v)$ (for all $u, v \in V'$) and $\forall \psi \in \Sigma' \exists h' \subseteq h$ s.t. $(s', h') \models_R \psi$. By Def. 4.5, $\mathcal{A}_k(\phi)$ contains an abstraction $(V' \setminus \{x\}, \sim, \Sigma)$, where $\sim$ is the restriction of $\sim'$ to $V' \setminus \{x\}$ and $\Sigma = \{\exists x \xi | \xi \in \Sigma'\}$. We have $V' \setminus \{x\} = fv(\psi) \setminus \{x\} = fv(\phi) = V$. Moreover, if $x \in V$ then $s(u) = s'(u)$, so that the equivalence $u \sim v \iff s(u) = s(v)$ holds for all $u, v \in V$. Finally, if $\psi \in \Sigma$, then $\psi = \exists x \xi$ with $\xi \in \Sigma'$, so that there exists $h' \subseteq h$ with $(s', h') \models_R \xi$. This entails that $(s, h') \models_R \exists x \xi = \psi$.

### C Proof of Theorem 4.8

We establish the two implications.

⇒ Let $(s, h)$ be a model of $\phi$ that is compatible with $S$, i.e., $(s, h') \not\models_R \psi$ for all $\psi \in S$ and for all $h' \subseteq h$. By Lem. 4.7, $\mathcal{A}_k(\phi)$ contains an abstraction $A = (V, \sim, \Sigma)$ such that
$x \sim y \iff s(x) = s(y)$ (for all $x, y \in V$) and $\forall \psi \in \Sigma, \exists b' \subseteq b, (s, b') \models_R \psi$. Assume that there exists $\psi \in S$ such that $A \triangleright \psi$. By definition, this entails that $\psi$ is of the form $\exists z (*_{i=1}^n (x_i \approx x'_i) *_{i=1}^m (y_i \not\approx y'_i) * \xi)$ where $x_i, x'_i, y_i, y'_i \in V, x_i \sim x'_i$ (for all $i \in \{1, \dots, n\}$), $y_i \not\sim y'_i$ (for all $i \in \{1, \dots, m\}$), and $\Sigma$ contains a formula $\xi'$ subsuming $\exists z \xi$. Using the above equivalence, we deduce that $s(x_i) = s(x'_i)$ (for all $i \in \{1, \dots, n\}$), and $s(y_i) \neq s(y'_i)$ (for all $i \in \{1, \dots, m\}$), so that $(s, \emptyset) \models_R *_{i=1}^n (x_i \approx x'_i) * *_{i=1}^m (y_i \not\approx y'_i)$. Moreover, as $\xi' \in \Sigma$, there exists $b' \subseteq b$ such that $(s, b') \models_R \xi'$. By Prop. 4.3, we deduce that $(s, b') \models_R \exists z \xi$. Consequently, we get: $(s, b') \models_R \exists z (*_{i=1}^n (x_i \approx x'_i) * *_{i=1}^m (y_i \not\approx y'_i) * \xi)$, i.e. $(s, b') \models_R \psi$, thus leading to a contradiction of the assumption that $(s, b)$ is compatible with $S$.

$\Leftarrow$ Assume that $\mathcal{A}_k(\phi)$ contains an abstraction $A = (V, \sim, \Sigma)$ of domain $V$ such that $A \not\triangleright \psi$, for all $\psi \in S$. By Lem. 4.6, we deduce that there exists a structure $(s, b)$ such that $(s, b) \models_R \phi, x \sim y \iff s(x) = s(y)$ (for all $x, y \in V$) and for all $\psi \in \mathrm{Pt}(V, k)$, if $(s, b') \models_R \psi$ for some $b' \subseteq b$ then $\psi$ is subsumed by some formula in $\Sigma$. Assume that $(s, b)$ is not compatible with $S$, i.e., that there exist $\psi \in S$ and $b' \subseteq b$ such that $(s, b') \models_R \psi$. By definition, $\psi$ must be of the form $\exists z (*_{i=1}^n (x_i \approx x'_i) *_{i=1}^m (y_i \not\approx y'_i) * \xi)$ with $n \ge 0, m \ge 0$ and $\xi$ contains no equational atom. As $S$ is $\exists$-restricted, $x_i, x'_i, y_i, y'_i$ occur in $V$. Therefore we get by the above equivalence: $x_i \sim x'_i$ (for all $i \in \{1, \dots, n\}$) and $y_i \not\sim y'_i$ (for all $i \in \{1, \dots, m\}$). Moreover, $(s, b') \models_R \exists z \xi$. By the hypothesis of the lemma, $\mathrm{width}(\psi) \le k$, so that $\mathrm{width}(\xi) \le k$ and thus $\exists z \xi \in \mathrm{Pt}(V, k)$. By the implication above, we deduce that there exists a formula $\xi' \in \Sigma$ that subsumes $\exists z \xi$, so that $A \triangleright \psi$, which contradicts our hypothesis.

## D Proof of Corollary 4.9

By Th. 4.8, to test whether a formula $\phi$ is $S$-satisfiable, it is sufficient to compute the set $\mathcal{A}_k(\phi)$ (for $k = \mathrm{width}(S)$) and verify whether it contains an abstraction $A$ such that $A \not\triangleright \psi$ for all $\psi \in S$. To achieve this, one needs to compute all the sets $\mathcal{A}_k(\phi' \sigma)$, where $\phi'$ is a formula occurring in $\phi$ or $R$, and $\sigma$ is a substitution. Up to a renaming of variables, the number of such formulas is simply exponential w.r.t. the size of $\phi$ and $R$. It is clear that the size of the formulas in $\mathrm{Pt}(V, k)$ is polynomial w.r.t. the size of $\phi$ and $S$. Consequently, the number of formulas in $\mathrm{Pt}(V, k)$ is exponential, and the number of subsets of $\mathrm{Pt}(V, k)$ is doubly exponential. Since the number of equivalence relations ~ over a set $V$ is simply exponential w.r.t. $\mathrm{card}(V)$, we deduce that the number of abstractions to consider is doubly exponential w.r.t. the size of $\phi$, $S$, and $R$. Meanwhile, the size of these abstractions is simply exponential. Therefore, the algorithm runs in doubly exponential time.

If the size of the formulas in $S$ is bounded, then $k$ is also bounded, and the size of the formulas in $\mathrm{Pt}(V, k)$ is bounded as well. Consequently, the number of abstractions becomes simply exponential, and the algorithm runs in exponential time. Hence, the problem is EXPTIME-complete, as EXPTIME-hardness follows from the EXPTIME-hardness of the satisfiability problem in standard SL [3].