of termination, and define $s$ to be the mapping where $s(a) =S_a$ for all $a\in A$. Let $a \in A$ and $b \in s(a)$. By the definition of the algorithm, the pair $([{\mathbf{A}}, \{a_1\},\ldots,\{a_n\},\{a\}],\allowbreak[{\mathbf{B}}, S_{a_1},\ldots, S_{a_n},\{b\}])$ has the ACC, and thus the desired homomorphism $h_{a,b}$ exists.

Now, suppose that the instance $({\mathbf{A}}, {\mathbf{B}})$ has the SACC, and let $s$ be a mapping with the described properties. We show that throughout the execution of the algorithm, it holds that $s(a)\subseteq S_a$ for all $a\in A$. First, $S_a$ is initialized with $B$ for every $a\in A$. Next, we show that when $a \in A$ and $b \in s(a)$, then $b$ is never removed from $S_a$ by the algorithm. This is because by definition of SACC, there exists a homomorphism $h_{a,b}: {\mathbf{A}}\rightarrow {\wp}({\mathbf{B}})$ with $h_{a,b}(a)=\{b\}$ such that for all $a' \in A$, it holds that $h_{a,b}(a') \subseteq s(a')$. Since $s(a')\subseteq S_{a'}$ by the inductive assumption, $([{\mathbf{A}}, \{a_1\},\ldots,\{a_n\},\{a\}],[{\mathbf{B}}, S_{a_1},\ldots, S_{a_n},\{b\}])$ has the ACC and hence the algorithm does not remove $b$ from $S_a$.

\[def:sac-solves\] Let ${\mathbf{B}}$ be a structure. We say that singleton arc consistency *solves* ${{\mathsf{CSP}}}({\mathbf{B}})$ if for all structures ${\mathbf{A}}$, the following holds: $({\mathbf{A}}, {\mathbf{B}})$ has the SACC implies that there is 