notxia/unibo-ai-notes
1
0
Fork 0
mirror of https://github.com/NotXia/unibo-ai-notes.git synced 2025-12-16 19:32:21 +01:00
Code Issues Packages Projects Releases Wiki Activity

Moved CDMO2 in year1

Browse Source
This commit is contained in:
Tian Cheng (Riccardo) Xia
2024-04-19 19:56:41 +02:00
parent ea45a504cf
commit 52495c241a
8 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

15
src/year1/combinatorial-decision-making-and-optimization/metadata.json Normal file
View File

@ -0,0 +1,15 @@
{
"name": "Combinatorial Decision Making and Optimization",
"year": 1,
"semester": 2,
"pdfs": [
{
"name": "CDMO module 1",
"path": "module1/cdmo1.pdf"
},
{
"name": "CDMO module 2",
"path": "module2/cdmo2.pdf"
}
]
}

1
src/year1/combinatorial-decision-making-and-optimization/module2/ainotes.cls Symbolic link
View File

@ -0,0 +1 @@
../../../ainotes.cls

15
src/year1/combinatorial-decision-making-and-optimization/module2/cdmo2.tex Normal file
View File

@ -0,0 +1,15 @@
\documentclass[11pt]{ainotes}
\title{Combinatorial Decision Making\\and Optimization\\(Module 2)}
\date{2023 -- 2024}
\def\lastupdate{{PLACEHOLDER-LAST-UPDATE}}
\def\calT{\mathcal{T}}
\begin{document}
\makenotesfront
\input{./sections/_smt.tex}
\end{document}

BIN
src/year1/combinatorial-decision-making-and-optimization/module2/img/_conflict_graph_example.pdf Normal file
View File

Binary file not shown.

BIN
src/year1/combinatorial-decision-making-and-optimization/module2/img/_layered_solvers.pdf Normal file
View File

Binary file not shown.

84
src/year1/combinatorial-decision-making-and-optimization/module2/img/conflict_graph_example.drawio Normal file
View File

@ -0,0 +1,84 @@
<mxfile host="Electron" modified="2024-04-18T18:52:18.767Z" agent="Mozilla/5.0 (Windows NT 10.0; Win64; x64) AppleWebKit/537.36 (KHTML, like Gecko) draw.io/23.1.5 Chrome/120.0.6099.109 Electron/28.1.0 Safari/537.36" etag="y8SOCJ19-c6V_RWc48bs" version="23.1.5" type="device">
<diagram name="Pagina-1" id="2E39NDmfMYuv_2c8OxZy">
<mxGraphModel dx="989" dy="577" grid="1" gridSize="10" guides="1" tooltips="1" connect="1" arrows="1" fold="1" page="1" pageScale="1" pageWidth="827" pageHeight="1169" math="0" shadow="0">
<root>
<mxCell id="0" />
<mxCell id="1" parent="0" />
<mxCell id="Nw_TqqoXpFTvkcw81iQf-3" value="c&lt;span style=&quot;font-style: normal;&quot;&gt;=&lt;/span&gt;b &lt;span style=&quot;font-style: normal;&quot;&gt;@ 0&lt;/span&gt;" style="ellipse;whiteSpace=wrap;html=1;fontSize=18;fontFamily=Computer modern;fontStyle=2;fillColor=#d5e8d4;strokeColor=#82b366;" vertex="1" parent="1">
<mxGeometry x="380" y="270" width="100" height="40" as="geometry" />
</mxCell>
<mxCell id="Nw_TqqoXpFTvkcw81iQf-4" value="h&lt;span style=&quot;font-style: normal;&quot;&gt;(&lt;/span&gt;a&lt;span style=&quot;font-style: normal;&quot;&gt;)&amp;nbsp;≠ &lt;/span&gt;h&lt;span style=&quot;font-style: normal;&quot;&gt;(&lt;/span&gt;c&lt;span style=&quot;font-style: normal;&quot;&gt;)&lt;/span&gt;&amp;nbsp;&lt;span style=&quot;font-style: normal;&quot;&gt;@ 1&lt;/span&gt;" style="ellipse;whiteSpace=wrap;html=1;fontSize=18;fontFamily=Computer modern;fontStyle=2;fillColor=#d5e8d4;strokeColor=#82b366;" vertex="1" parent="1">
<mxGeometry x="400" y="350" width="140" height="40" as="geometry" />
</mxCell>
<mxCell id="Nw_TqqoXpFTvkcw81iQf-5" value="a&lt;span style=&quot;font-style: normal;&quot;&gt; ≠ b&lt;/span&gt;&amp;nbsp;&lt;span style=&quot;font-style: normal;&quot;&gt;@ 1&lt;/span&gt;" style="ellipse;whiteSpace=wrap;html=1;fontSize=18;fontFamily=Computer modern;fontStyle=2" vertex="1" parent="1">
<mxGeometry x="250" y="350" width="100" height="40" as="geometry" />
</mxCell>
<mxCell id="Nw_TqqoXpFTvkcw81iQf-6" value="a&lt;span style=&quot;font-style: normal;&quot;&gt; = d&lt;/span&gt;&amp;nbsp;&lt;span style=&quot;font-style: normal;&quot;&gt;@ 1&lt;/span&gt;" style="ellipse;whiteSpace=wrap;html=1;fontSize=18;fontFamily=Computer modern;fontStyle=2" vertex="1" parent="1">
<mxGeometry x="350" y="470" width="100" height="40" as="geometry" />
</mxCell>
<mxCell id="Nw_TqqoXpFTvkcw81iQf-7" value="p&amp;nbsp;&lt;span style=&quot;font-style: normal;&quot;&gt;@ 1&lt;/span&gt;" style="ellipse;whiteSpace=wrap;html=1;fontSize=18;fontFamily=Computer modern;fontStyle=2" vertex="1" parent="1">
<mxGeometry x="425" y="410" width="90" height="40" as="geometry" />
</mxCell>
<mxCell id="Nw_TqqoXpFTvkcw81iQf-8" value="k&amp;nbsp;&lt;span style=&quot;font-style: normal;&quot;&gt;@ 1&lt;/span&gt;" style="ellipse;whiteSpace=wrap;html=1;fontSize=18;fontFamily=Computer modern;fontStyle=2;fillColor=#f8cecc;strokeColor=#b85450;" vertex="1" parent="1">
<mxGeometry x="220" y="450" width="90" height="40" as="geometry" />
</mxCell>
<mxCell id="Nw_TqqoXpFTvkcw81iQf-9" value="" style="endArrow=classic;html=1;rounded=0;exitX=0;exitY=1;exitDx=0;exitDy=0;" edge="1" parent="1" source="Nw_TqqoXpFTvkcw81iQf-3" target="Nw_TqqoXpFTvkcw81iQf-5">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="370" y="440" as="sourcePoint" />
<mxPoint x="420" y="390" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="Nw_TqqoXpFTvkcw81iQf-10" value="" style="endArrow=classic;html=1;rounded=0;exitX=0;exitY=0.5;exitDx=0;exitDy=0;entryX=1;entryY=0.5;entryDx=0;entryDy=0;" edge="1" parent="1" source="Nw_TqqoXpFTvkcw81iQf-4" target="Nw_TqqoXpFTvkcw81iQf-5">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="405" y="314" as="sourcePoint" />
<mxPoint x="318" y="362" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="Nw_TqqoXpFTvkcw81iQf-11" value="" style="endArrow=classic;html=1;rounded=0;exitX=0.5;exitY=1;exitDx=0;exitDy=0;entryX=0.5;entryY=0;entryDx=0;entryDy=0;" edge="1" parent="1" source="Nw_TqqoXpFTvkcw81iQf-4" target="Nw_TqqoXpFTvkcw81iQf-7">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="350" y="450" as="sourcePoint" />
<mxPoint x="400" y="400" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="Nw_TqqoXpFTvkcw81iQf-12" value="" style="endArrow=classic;html=1;rounded=0;exitX=0.5;exitY=1;exitDx=0;exitDy=0;entryX=0;entryY=0;entryDx=0;entryDy=0;" edge="1" parent="1" source="Nw_TqqoXpFTvkcw81iQf-5" target="Nw_TqqoXpFTvkcw81iQf-6">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="310" y="470" as="sourcePoint" />
<mxPoint x="360" y="420" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="Nw_TqqoXpFTvkcw81iQf-13" value="" style="endArrow=classic;html=1;rounded=0;exitX=0.5;exitY=1;exitDx=0;exitDy=0;entryX=1;entryY=0;entryDx=0;entryDy=0;" edge="1" parent="1" source="Nw_TqqoXpFTvkcw81iQf-7" target="Nw_TqqoXpFTvkcw81iQf-6">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="285" y="400" as="sourcePoint" />
<mxPoint x="405" y="500" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="Nw_TqqoXpFTvkcw81iQf-14" value="" style="endArrow=classic;html=1;rounded=0;exitX=0;exitY=1;exitDx=0;exitDy=0;entryX=0.5;entryY=0;entryDx=0;entryDy=0;" edge="1" parent="1" source="Nw_TqqoXpFTvkcw81iQf-5" target="Nw_TqqoXpFTvkcw81iQf-8">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="285" y="400" as="sourcePoint" />
<mxPoint x="405" y="500" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="Nw_TqqoXpFTvkcw81iQf-15" value="" style="endArrow=classic;html=1;rounded=0;exitX=0;exitY=0.5;exitDx=0;exitDy=0;entryX=0.957;entryY=0.756;entryDx=0;entryDy=0;entryPerimeter=0;" edge="1" parent="1" source="Nw_TqqoXpFTvkcw81iQf-6" target="Nw_TqqoXpFTvkcw81iQf-8">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="275" y="394" as="sourcePoint" />
<mxPoint x="275" y="460" as="targetPoint" />
</mxGeometry>
</mxCell>
<mxCell id="Nw_TqqoXpFTvkcw81iQf-16" value="" style="endArrow=none;dashed=1;html=1;rounded=0;fillColor=#dae8fc;strokeColor=#6c8ebf;strokeWidth=2;curved=1;" edge="1" parent="1">
<mxGeometry width="50" height="50" relative="1" as="geometry">
<mxPoint x="560" y="400" as="sourcePoint" />
<mxPoint x="350" y="280" as="targetPoint" />
<Array as="points">
<mxPoint x="420" y="400" />
<mxPoint x="390" y="390" />
<mxPoint x="360" y="360" />
</Array>
</mxGeometry>
</mxCell>
<mxCell id="Nw_TqqoXpFTvkcw81iQf-17" value="&lt;font style=&quot;font-size: 16px;&quot; face=&quot;Computer modern&quot;&gt;(1UIP)&lt;/font&gt;" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
<mxGeometry x="440" y="330" width="60" height="20" as="geometry" />
</mxCell>
</root>
</mxGraphModel>
</diagram>
</mxfile>

919
src/year1/combinatorial-decision-making-and-optimization/module2/sections/_smt.tex Normal file
View File

@ -0,0 +1,919 @@
\chapter{Satisfiability modulo theory}
\begin{description}
\item[Satisfiability modulo theory (SMT)] \marginnote{Satisfiability modulo theory (SMT)}
Satisfiability of a formula with respect to some background formal theory/theories.
SMT extends SAT and exploits domain-specific reasoning (possibly with infinite domains).
\end{description}
\section{First-order logic for SMT}
\subsection{Syntax}
\begin{remark}
Only quantifier-free formulas (q.f.f.) are considered in SMT.
\end{remark}
\begin{description}
\item[Functions] \marginnote{Functions}
The set of all the functions is denoted as $\Sigma^F = \bigcup_{k \geq 0} \Sigma^F_k$
where $\Sigma^F_k$ denotes the set of $k$-ary functions.
\begin{description}
\item[Constants] $\Sigma^F_0$
\end{description}
\item[Predicates] \marginnote{Predicates}
The set of all the predicates is denoted as $\Sigma^P = \bigcup_{k \geq 0} \Sigma^P_k$
where $\Sigma^P_k$ denotes the set of $k$-ary predicates.
\begin{description}
\item[Propositional symbols] $\Sigma^P_0$
\end{description}
\item[Signature] \marginnote{Signature}
The set of the non-logical symbols of FOL is denoted as:
\[ \Sigma = \Sigma^F \cup \Sigma^P \]
\item[Terms] \marginnote{Terms}
The set of terms over $\Sigma$ is denoted as $\mathbb{T}^\Sigma$:
\[
\begin{split}
\mathbb{T}^\Sigma = &\,
\Sigma^F_0 \,\cup \\
& \{ f(t_1, \dots, t_k) \mid f \in \Sigma^F_k \land t_1, \dots, t_k \in \mathbb{T}^\Sigma \} \,\cup \\
& \{ \texttt{ite}(\varphi, t_1, t_2) \mid \varphi \in \mathbb{F}^\Sigma \land t_1, t_2 \in \mathbb{T}^\Sigma \}
\end{split}
\]
\begin{remark}
\texttt{ite} is an auxiliary function to capture the if-then-else construct.
\end{remark}
\item[Formulas] \marginnote{Formulas}
The set of formulas over $\Sigma$ is denoted as $\mathbb{F}^\Sigma$:
\[
\begin{split}
\mathbb{F}^\Sigma = &\,
\{ \bot, \top \} \,\cup\, \Sigma^P_0 \,\cup \\
&\{ t_1 = t_2 \mid t_1, t_2 \in \mathbb{T}^\Sigma \} \,\cup \\
& \{ p(t_1, \dots, t_k) \mid p \in \Sigma^P_k \land t_1, \dots, t_k \in \mathbb{T}^\Sigma \} \,\cup \\
& \{ \lnot \varphi \mid \varphi \in \mathbb{F}^\Sigma \} \,\cup \\
& \{ (\varphi_1 \Rightarrow \varphi_2), (\varphi_1 \iff \varphi_2), (\varphi_1 \land \varphi_2), (\varphi_1 \vee \varphi_2) \mid \varphi_1, \varphi_2 \in \mathbb{F}^\Sigma \}
\end{split}
\]
\end{description}
\subsection{Semantics}
\begin{description}
\item[$\mathbf{\Sigma}$-model] \marginnote{$\Sigma$-model}
Pair $\mathcal{M} = \langle M, (\cdot)^\mathcal{M} \rangle$ defined on a given signature $\Sigma$ where:
\begin{itemize}
\item $M$ is the universe of $\mathcal{M}$.
\item $(\cdot)^\mathcal{M}$ is a mapping such that:
\begin{itemize}
\item $\forall f \in \Sigma^F_k: f^\mathcal{M} \in \{ \varphi \mid \varphi: M^k \rightarrow M \}$.
\item $\forall p \in \Sigma^P_k: p^\mathcal{M} \in \{ \varphi \mid \varphi: M^k \rightarrow \{ \texttt{true}, \texttt{false} \} \}$.
\end{itemize}
\end{itemize}
\item[Interpretation] \marginnote{Interpretation}
Extension of the mapping function $(\cdot)^\mathcal{M}$ to terms and formulas:
\begin{itemize}
\item $\top^\mathcal{M} = \texttt{true}$ and $\bot^\mathcal{M} = \texttt{false}$.
\item $(f(t_1, \dots, t_k))^\mathcal{M} = f^\mathcal{M}(t_1^\mathcal{M}, \dots, t_k^\mathcal{M})$ and
$(p(t_1, \dots, t_k))^\mathcal{M} = p^\mathcal{M}(t_1^\mathcal{M}, \dots, t_k^\mathcal{M})$.
\item $\texttt{ite}(\varphi, t_1, t_2)^\mathcal{M} = \begin{cases}
t_1^\mathcal{M} & \text{if $\varphi^\mathcal{M} = \texttt{true}$} \\
t_2^\mathcal{M} & \text{if $\varphi^\mathcal{M} = \texttt{false}$}
\end{cases}$.
\end{itemize}
\end{description}
\subsection{$\mathbf{\Sigma}$-theory}
\begin{description}
\item[Satisfiability] \marginnote{Satisfiability}
A model $\mathcal{M}$ satisfies a formula $\varphi \in \mathbb{F}^\Sigma$ if $\varphi^\mathcal{M} = \texttt{true}$.
\item[$\mathbf{\Sigma}$-theory] \marginnote{$\Sigma$-theory}
Possibly infinite set $\calT$ of $\Sigma$-models.
\item[$\mathbf{\calT}$-satisfiability] \marginnote{$\calT$-satisfiability}
A formula $\varphi \in \mathbb{F}^\Sigma$ is $\calT$-satisfiable if there exists a model $\mathcal{M} \in \calT$ that satisfies it.
\item[$\mathbf{\calT}$-consistency] \marginnote{$\calT$-consistency}
A set of formulas $\{ \varphi_1, \dots, \varphi_k \} \subseteq \mathbb{F}^\Sigma$ is $\calT$-consistent iff
$\varphi_1 \land \dots \land \varphi_k$ is $\calT$-satisfiable.
\item[$\mathbf{\calT}$-entailment] \marginnote{$\calT$-entailment}
A set of formulas $\Gamma \subseteq \mathbb{F}^\Sigma$ $\calT$-entails a formula $\varphi \in \mathbb{F}^\Sigma$ ($\Gamma \models_\calT \varphi$) iff
in every model $\mathcal{M} \in \calT$ that satisfies $\Gamma$, $\varphi$ is also satisfied.
\begin{remark}
$\Gamma$ is $\calT$-consistent iff $\Gamma \cancel{\models_\calT} \bot$.
\end{remark}
\item[$\mathbf{\calT}$-validity] \marginnote{$\calT$-validity}
A formula $\varphi \in \mathbb{F}^\Sigma$ is $\calT$-valid iff $\varnothing \models_\calT \varphi$.
\begin{remark}
$\varphi$ is $\calT$-consistent iff $\lnot\varphi$ is not $\calT$-valid.
\end{remark}
\begin{description}
\item[Theory lemma] \marginnote{Theory lemma}
$\calT$-valid clause $c = l_1 \vee \dots \vee l_k$.
\end{description}
\item[$\Sigma$-expansion] \marginnote{$\Sigma$-expansion}
Given a $\Sigma$-model $\mathcal{M} = \langle M, (\cdot)^\mathcal{M} \rangle$ and $\Sigma' \supseteq \Sigma$,
an expansion $\mathcal{M}' = \langle M', (\cdot)^{\mathcal{M}'} \rangle$ over $\Sigma'$ is any $\Sigma'$-model such that:
\begin{itemize}
\item $M' = M$.
\item $\forall s \in \Sigma: s^{\mathcal{M}'} = s^\mathcal{M}$
\end{itemize}
\begin{remark}
Given a $\Sigma$-theory $\calT$, we implicitly consider it to be the theory $\calT'$ defined as:
\[ \calT' = \{ \mathcal{M}' \mid \mathcal{M}' \text{ is an expansion of a $\Sigma$-model } \mathcal{M} \text{ in } \calT\} \]
\end{remark}
\item[Ground $\mathbf{\calT}$-satisfiability] \marginnote{Ground $\calT$-satisfiability}
Given a $\Sigma$-theory $\calT$, determine if a ground formula is $\calT$-satisfiable over a $\Sigma$-expansion $\calT'$.
\item[Axiomatically defined theory] \marginnote{Axiomatically defined theory}
Given a minimal set of formulas (axioms) $\Lambda \subseteq \mathbb{F}^\Sigma$,
its corresponding theory is the set of all the models that respect $\Lambda$.
\end{description}
\begin{example}
Let $\Sigma$ be defined as:
\[ \Sigma^F_0 = \{ a, b, c, d \} \hspace{2em} \Sigma^F_1 = \{ f, g \} \hspace{2em} \Sigma^P_2 = \{ p \} \]
A $\Sigma$-model $\mathcal{M} = \langle [0, 2\pi[, (\cdot)^\mathcal{M} \rangle$ can be defined as follows:
\begin{gather*}
a^\mathcal{M} = 0 \hspace{2em} b^\mathcal{M} = \frac{\pi}{2} \hspace{2em} c^\mathcal{M} = \pi \hspace{2em} d^\mathcal{M} = \frac{3\pi}{2} \\
f^\mathcal{M} = \sin \hspace{2em} g^\mathcal{M} = \cos \hspace{2em} p^\mathcal{M}(x, y) \iff x > y
\end{gather*}
To determine if $p(g(x), f(d))$ is $\mathcal{M}$-satisfiable, we have to expand $\mathcal{M}$ as there are free variables ($x$).
Let $\Sigma' = \Sigma \cup \{ x \}$. The expansion $\mathcal{M}'$ such that $x^{\mathcal{M}'} = \frac{\pi}{2}$ makes the formula satisfiable.
\end{example}
\subsection{Theories of interest}
\begin{description}
\item[Equality with Uninterpreted Functions theory (EUF)] \marginnote{Equality with Uninterpreted Functions theory (EUF)}
Theory $\calT_\text{EUF}$ containing all the possible $\Sigma$-models.
\begin{remark}
Also called empty theory as its axiom set is $\varnothing$ (i.e. allows any model).
\end{remark}
\begin{remark}
Useful to deal with black-box functions (i.e. prove satisfiability without a specific theory).
\begin{example}
The following formula can be proved to be unsatisfiable by only using syntactic manipulations of basic FOL concepts:
\begin{gather*}
\big( a * (f(b) + f(c)) = d \big) \land \big( b * (f(a) + f(c)) \neq d \big) \land \underline{\big( a = b \big)} \\
\big( \underline{a * (f(a) + f(c))} = d \big) \land \big( \underline{a * (f(a) + f(c))} \neq d \big) \\
\big( g(a, c) = d \big) \land \big( g(a, c) \neq d \big)
\end{gather*}
\end{example}
\end{remark}
\item[Arithmetic theories] \marginnote{Arithmetic theories}
Theories with $\Sigma = (0, 1, +, -, \leq)$.
\begin{description}
\item[Presburger arithmetic]
Theory $\calT_\mathbb{Z}$ that interprets $\Sigma$-symbols over integers.
\begin{itemize}
\item Ground $\calT_\mathbb{Z}$-satisfiability is \textbf{NP}-complete.
\item Extended with multiplication, $\calT_\mathbb{Z}$-satisfiability becomes undecidable.
\end{itemize}
\item[Real arithmetic]
Theory $\calT_\mathbb{R}$ that interprets $\Sigma$-symbols over reals.
\begin{itemize}
\item Ground $\calT_\mathbb{R}$-satisfiability is in \textbf{P}.
\item Extended with multiplication, $\calT_\mathbb{R}$-satisfiability becomes doubly-exponential.
\end{itemize}
\end{description}
\begin{remark}
In floating points, commutativity still holds, but associativity and distributivity are not guaranteed.
\end{remark}
\item[Array theory] \marginnote{Array theory}
Let $\Sigma_\mathcal{A}$ be the signature containing two functions:
\begin{descriptionlist}
\item[$\texttt{read}(a, i)$] Reads the value of $a$ at index $i$.
\item[$\texttt{write}(a, i, v)$] Returns an array $a'$ where the value $v$ is at the index $i$ of $a$.
\end{descriptionlist}
The theory $\calT_\mathcal{A}$ is the set of all models respecting the following axioms:
\begin{itemize}
\item $\forall a\, \forall i\, \forall v: \texttt{read}(\texttt{write}(a, i, v), i) = v$.
\item $\forall a\, \forall i\, \forall j\, \forall v: (i \neq j) \Rightarrow \Big( \texttt{read}\big( \texttt{write}(a,i,v), j \big) = \texttt{read}(a, j) \Big)$.
\item $\forall a\, \forall a': \big( \forall i: \texttt{read}(a, i) = \texttt{read}(a', i) \big) \Rightarrow (a = a')$.
\end{itemize}
\begin{remark}
The full $\calT_\mathcal{A}$ theory is undecidable but there are decidable fragments.
\end{remark}
\item[Bit-vectors theory] \marginnote{Bit-vectors theory}
Theory $\calT_\mathcal{BV}$ with vectors of bits of fixed length as constants and
operations such as:
\begin{itemize}
\item String-like operations (e.g. slicing, concatenation, \dots).
\item Logical operations (e.g. bit-wise operators).
\item Arithmetic operations (e.g. $+$, $-$, \dots).
\end{itemize}
\item[String theory] \marginnote{String theory}
Theory to handle strings of unbounded length.
\begin{description}
\item[Theory of word equations]
Given an alphabet $\mathcal{S}$, a word equation has form $L = R$
where $L$ and $R$ are concatenations of string constants over $\mathcal{S}^*$.
\begin{remark}
The general theory of word equations is undecidable.
\end{remark}
\begin{remark}
The quantifier-free theory of word equations is decidable.
\end{remark}
\end{description}
\end{description}
\begin{remark}
In practice, many theories are often combined.
\end{remark}
\section{Encoding to SAT}
\subsection{Eager approaches}
All the information on the formal theory is used from the beginning to encode an SMT formula $\varphi$ into an equisatisfiable SAT formula $\varphi'$
(i.e. SMT is compiled into SAT).
\begin{descriptionlist}
\item[Equisatisfiability] \marginnote{Equisatisfiability}
Given a $\Sigma$-theory $\calT$, two formulas $\varphi$ and $\varphi'$ are equisatisfiable iff:
\[ \varphi \text{ is $\calT$-satisfiable } \iff \varphi' \text{ is $\calT$-satisfiable } \]
\end{descriptionlist}
Eager approaches have the following advantages:
\begin{itemize}
\item Does not require an SMT solver.
\item Once encoded, whichever SAT solver can be used.
\end{itemize}
Eager approaches have the following disadvantages:
\begin{itemize}
\item An ad-hoc encoding is needed for all the theories.
\item The resulting SAT formula might be huge.
\end{itemize}
\begin{description}
\item[Algorithm]
Given an EUF formula $\varphi$, to determine if it is $\calT_\text{EUF}$-satisfiable,
the following steps are taken:
\begin{enumerate}
\item Replace functions and predicates with constant equalities.
Given the terms $f(t_1), \dots, f(t_k)$, possible approaches are:
\begin{descriptionlist}
\item[Ackermann approach] \marginnote{Ackermann approach}
\begin{itemize}
\item Each $f(t_i)$ is encoded into a new constant $A_i$.
\item Add the constraints $(t_i = t_j) \Rightarrow (A_i = A_j)$ for each $i < j$.
\end{itemize}
\item[Bryant approach] \marginnote{Bryant approach}
\begin{itemize}
\item $f(t_1)$ is encoded as $A_1$.
\item $f(t_2)$ is encoded as $\texttt{ite}(t_2 = t_1, A_1, A_2)$.
\item $f(t_3)$ is encoded as $\texttt{ite}\big( t_3 = t_1, A_1, \texttt{ite}(t_3 = t_2, A_2, A_3) \big)$.
\item $f(t_i)$ is encoded as:
\[ \texttt{ite}\Big( t_i = t_1, A_1, \texttt{ite}\Big( t_i = t_2, A_2, \texttt{ite}\big( \dots, \texttt{ite}(t_i = t_{i-1}, A_{i-1}, A_i) \big) \Big) \Big) \]
\end{itemize}
\end{descriptionlist}
\item Remove equalities to reduce $\varphi$ into propositional logic.
Possible encodings are:
\begin{descriptionlist}
\item[Small-domain encoding]
If $\varphi$ has $n$ distinct variables $\{ c_1, \dots, c_n \}$,
a possible model $\mathcal{M} = \langle M, (\cdot)^\mathcal{M} \rangle$ that satisfies it must have $\vert M \vert \leq n$.
Therefore, each $c_i^\mathcal{M}$ can be associated to a value in $\{ 1, \dots, n \}$.
In SAT, this mapping from $c_i^\mathcal{M}$ to $\{ 1, \dots, n \}$ can be encoded using $O(\log n)$ bits.
Finally, an equality $c_i = c_j$ (or $c_i \neq c_j$) can be encoded by adding bitwise constraints.
\item[Direct encoding]
Encode each equality $a = b$ with a propositional symbol $P_{a,b}$
and add transitivity constraints of form $(P_{a,b} \land P_{b,c}) \Rightarrow P_{a,c}$.
\end{descriptionlist}
\end{enumerate}
\end{description}
\subsection{Lazy approaches}
Integrate SAT solvers with theory-specific decision procedures.
These approaches are more flexible and modular and avoid an explosion of SAT clauses.
On the other hand, the search becomes SAT-driven and not theory-driven.
\begin{remark}
Most SMT solvers follow a lazy approach.
\end{remark}
\begin{description}
\item[Algorithm] \phantom{}
Let $\calT$ be a theory.
Given a conjunction of $\calT$-literals $\varphi = \varphi_1 \land \dots \land \varphi_n$,
to determine its $\calT$-satisfiability, a generic lazy solver does the following:
\begin{enumerate}
\item Each SMT literal $\varphi_i$ is encoded (abstracted) into a SAT literal $l_i$ to form the abstraction $\Phi = \{ l_1, \dots, l_n \} $ of $\varphi$.
\item The $\calT$-solver sends $\Phi$ to the SAT-solver.
\begin{itemize}
\item If the SAT-solver determines that $\Phi$ is unsatisfiable, then $\varphi$ is $\calT$-unsatisfiable.
\item Otherwise, the SAT-solver returns a model $\mathcal{M} = \{ a_1, \dots, a_n \}$ (an assignment of the literals, possibly partial).
\end{itemize}
\item The $\calT$-solver determines if $\mathcal{M}$ is $\calT$-consistent.
\begin{itemize}
\item If it is, then $\varphi$ is $\calT$-satisfiable.
\item Otherwise, update $\Phi = \Phi \cup \lnot \mathcal{M}$ and go to Point 2.
\end{itemize}
\end{enumerate}
\begin{example}
Consider the EUF formula $\varphi$:
\[ \big( g(a) = c \big) \land \big( (f(g(a)) \neq f(c)) \vee (g(a) = d) \big) \land \big( c \neq d \big) \]
\begin{itemize}
\item $\varphi$ abstracted into SAT is:
\begin{gather*}
\underbrace{ \big( g(a) = c \big) }_{l_1} \land
\big(
\lnot\underbrace{ (f(g(a)) = f(c)) }_{l_2} \vee
\underbrace{ (g(a) = d) }_{l_3}
\big) \land
\lnot\underbrace{ \big( c = d \big) }_{l_4} \\
l_1 \land (\lnot l_2 \vee l_3) \land \lnot l_4
\end{gather*}
Therefore, $\Phi = \{ l_1, (\lnot l_2 \vee l_3), \lnot l_4 \}$
\item The $\calT$-solver sends $\Phi$ to the SAT-solver.
Let's say that it return $\mathcal{M} = \{ l_1, \lnot l_2, \lnot l_4 \}$.
\item The $\calT$-solver checks if $\mathcal{M}$ is consistent. Let's say it is not.
Let $\Phi' = \Phi \cup \lnot \mathcal{M} = \{ l_1, (\lnot l_2 \vee l_3), \lnot l_4, (\lnot l_1 \vee l_2 \vee l_4) \}$.
\item The $\calT$-solver sends $\Phi'$ to the SAT-solver.
Let's say that it return $\mathcal{M}' = \{ l_1, l_2, l_3, \lnot l_4 \}$.
\item The $\calT$-solver checks if $\mathcal{M}'$ is consistent. Let's say it is not.
Let $\Phi'' = \Phi' \cup \lnot \mathcal{M}' = \{ l_1, (\lnot l_2 \vee l_3), \lnot l_4, (\lnot l_1 \vee l_2 \vee l_4), (\lnot l_1 \vee \lnot l_2 \vee \lnot l_3 \vee l_4) \}$.
\item The $\calT$-solver sends $\Phi''$ to the SAT-solver and it detects the unsatisfiability.
Therefore, $\varphi$ is $\calT$-unsatisfiable.
\end{itemize}
\end{example}
\item[Optimizations] \phantom{}
\begin{itemize}
\item Check $\calT$-consistency on partial assignments.
\item Given a $\calT$-inconsistent assignment $\mu$,
find a smaller $\calT$-inconsistent assignment $\eta \subseteq \mu$ and add $\lnot \eta$ to $\Phi$ instead of $\lnot \mu$.
\item When reaching $\calT$-inconsistency, backjump to a $\calT$-consistent point in the computation.
\end{itemize}
\end{description}
\section{CDCL($\calT$)}
\marginnote{CDCL($\calT$)}
Lazy solver based on CDCL for SAT extended with a $\calT$-solver.
The $\calT$-solver does the following:
\begin{itemize}
\item Checks the $\calT$-consistency of a conjunction of literals.
\item Performs deduction of unassigned literals.
\item Explains $\calT$-inconsistent assigments.
\item Allows to backtrack.
\end{itemize}
\begin{description}
\item[State transition] \marginnote{State transition}
Transition system to describe the reasoning of SAT or SMT solvers.
A transition has form:
\[ (\mu \Vert \varphi) \rightarrow (\mu' \Vert \varphi') \]
where:
\begin{itemize}
\item $\varphi$ and $\varphi'$ are $\calT$-formulas.
\item $\mu$ and $\mu'$ are (partial) boolean assignments to atoms of $\varphi$ and $\varphi'$, respectively.
\item $(\mu \Vert \varphi)$ and $(\mu' \Vert \varphi')$ are states.
\end{itemize}
\begin{description}
\item[Transition rule] Determine the possible transitions.
\item[Derivation] Sequence of transitions.
\item[Initial state] $(\varnothing \Vert \varphi)$.
\item[$\calT$-consistency]
Given a $\calT$-formula $\varphi$ and a full assignment $\mu$ of $\varphi$,
$\varphi$ is $\calT$-consistent ($\mu \models_{\calT} \varphi$)
if there is a derivation from $(\varnothing \Vert \varphi)$ to $(\mu \Vert \varphi)$.
\end{description}
\item[$\calT$-propagation] \marginnote{$\calT$-propagation}
Deduce the assignment of an unassigned literal $l$ using some knowledge of the theory.
\begin{description}
\item[$\calT$-consequence] \marginnote{$\calT$-consequence}
If:
\begin{itemize}
\item $\mu \models_\calT l$,
\item $l$ or $\lnot l$ occur in $\varphi$,
\item $l$ and $\lnot l$ do not occur in $\mu$,
\end{itemize}
then:
\[ (\mu \Vert \varphi) \rightarrow (\mu \cup \{ l \} \Vert \varphi) \]
\end{description}
\begin{example}
Given the formula $\varphi$:
\[ \big( g(a) = c \big) \land \Big( \big( f(g(a)) \neq f(c) \big) \vee \big( g(a) = d \big) \Big) \land \big( c \neq d \big) \]
A possible derivation for some theory $\calT$ (i.e. $\calT$-propagation are decided arbitrarily) is:
\begin{enumerate}
\item $\varnothing \Vert \varphi$ (initial state).
\item $\varnothing \Vert \varphi \rightarrow \{ l_1 \} \Vert \varphi$ (Unit propagation).
\item $\{ l_1 \} \Vert \varphi \rightarrow \{ l_1, l_2 \} \Vert \varphi$ ($\calT$-propagation).
\item $\{ l_1, l_2 \} \Vert \varphi \rightarrow \{ l_1, l_2, l_3 \} \Vert \varphi$ (Unit propagation).
\item $\{ l_1, l_2, l_3 \} \Vert \varphi \rightarrow \{ l_1, l_2, l_3, l_4 \} \Vert \varphi$ ($\calT$-propagation).
\item $\{ l_1, l_2, l_3, l_4 \} \Vert \varphi \rightarrow \texttt{fail}$ (Failure).
\end{enumerate}
As we are at decision level 0 (as no decision literal has been fixed), we can conclude that $\varphi$ is unsatisfiable.
\begin{remark}
Unit and theory propagation are alternated (see algorithm description).
\end{remark}
\end{example}
\item[Algorithm]
Given a $\calT$-formula $\varphi$ and a (partial) $\calT$-assignment $\mu$ (i.e. initial decisions),
CDCL($\calT$) does the following:
\begin{algorithm}
\caption{CDCL($\calT$)}
\begin{lstlisting}[mathescape=true]
def cdclT($\varphi$, $\mu$):
if preprocess($\varphi$, $\mu$) == CONFLICT: return UNSAT
$\varphi^p$, $\mu^p$ = SMT_to_SAT($\varphi$), SMT_to_SAT($\mu$)
level = 0
$l$ = None
while True:
status = propagate($\varphi^p$, $\mu^p$, $l$)
if status == SAT:
return SAT_to_SMT($\mu^p$)
elif status == UNSAT:
$\eta^p$, jump_level = analyzeConflict($\varphi^p$, $\mu^p$)
if jump_level < 0: return UNSAT
backjump(jump_level, $\varphi^p \land \lnot\eta^p$, $\mu^p$)
elif status == UNKNOWN:
$l$ = decideNextLiteral($\varphi^p$, $\mu^p$)
level += 1
\end{lstlisting}
\end{algorithm}
Where:
\begin{descriptionlist}
\item[\texttt{preprocess}]
Preprocesses $\varphi$ with $\mu$ through operations such as simplifications, $\calT$-specific rewritings, \dots
\item[\texttt{SMT\_TO\_SAT}]
Provides the boolean abstraction of an SMT formula.
\item[\texttt{SAT\_TO\_SMT}]
Reverses the boolean abstraction of an SMT formula.
\item[\texttt{propagate}]
Iteratively apply:
\begin{itemize}
\item Unit propagation,
\item $\calT$-consistency check,
\item $\calT$-propagation.
\end{itemize}
Returns \texttt{SAT}, \texttt{UNSAT} or \texttt{UNKNOWN} (when no deductions are possible and there are still free variables).
\item[\texttt{analyzeConflict}]
Performs conflict analysis:
\begin{itemize}
\item If the conflict is detected by SAT boolean propagation ($\mu^p \land \varphi^p \models_p \bot$),
a boolean conflict set $\eta^p$ is outputted (as in standard CDCL).
\item If the conflict is detected by $\calT$-propatation ($\mu \land \phi \models_\calT \bot$),
a theory conflict $\eta$ is produced and its boolean abstraction $\eta^p$ is outputted.
\end{itemize}
Moreover, the earliest decision level at which a variable of $\eta^p$ is unassigned is returned.
As in standard CDCL, $\lnot \eta^p$ is added to $\varphi^p$ and the algorithm backjumps to a previous decision level (if possible).
\item[\texttt{decideNextLiteral}]
Decides the assignment of an unassigned variable (as in standard CDCL).
Theory information might be exploited.
\end{descriptionlist}
\item[Implication graph] \marginnote{Implication graph}
As in the standard CDCL algorithm, an implication graph is used to explain conflicts.
\begin{descriptionlist}
\item[Nodes] Decisions, derived literals or conflicts.
\item[Edges] If $v$ allows to unit/theory propagate $w$, then there is an edge $v \rightarrow w$.
\end{descriptionlist}
\end{description}
\begin{example}
Given the $\calT$-formula $\varphi$:
\[ \big( h(a) = h(c) \vee p \big) \land \big( a = b \vee \lnot p \vee a = d \big) \land \big( a \neq d \vee a = b \big) \]
and an initial decision $(c = b) \in \mu$,
CDCL($\calT$) does the following:
\begin{enumerate}
\item As no propagation is possible, the decision $h(a) \neq h(c)$ is added to $\mu$.
\item Unit propagate $p$ due to the clause $\big( h(a) = h(c) \vee p \big)$ and the decision at the previous step.
\item $\calT$-propagate $(a \neq b)$ due to the current assigments: $\{ c = b, h(a) \neq h(c) \} \models_\calT a \neq b$.
\item Unit propagate $(a = d)$ due to the clause $\big( a = b \vee \lnot p \vee a = d \big)$ and the current knowledge base ($p$ and $a \neq b$).
\item There is a conflict between $(a \neq d)$ and $(a = d)$.
\end{enumerate}
By building the conflict graph, one can identify the 1UIP as the decision $h(a) \neq h(c)$.
\begin{center}
\includegraphics[width=0.35\linewidth]{./img/_conflict_graph_example.pdf}
\end{center}
A cut in front of the 1UIP that separates decision nodes and the conflict node (as in standard CDCL) is made
to obtain the conflict set $\eta = \{ h(a) \neq h(c), c = b \}$.
$\big( (h(a) = h(c)) \vee (c \neq b) \big)$ is added as a clause and the algorithm backjumps at the decision level 0.
\end{example}
\section{Theory solvers}
Decide satisfiability of theory-specific formulas.
\subsection{EUF theory}
\begin{description}
\item[Congruence closure] \marginnote{Congruence closure}
Given a conjunction of EUF literals $\Phi$,
its satisfiability can be decided in polynomial time as follows:
\begin{enumerate}
\item Add a new variable $c$ and replace each $p(t_1, \dots, t_k)$
with $f_p(t_1, \dots, t_k) = c$.
\item Partition input literals into the sets of equalities $E$ and disequalities $D$.
\item Define $E^*$ as the congruence closure of $E$.
It is the smallest equivalence relation $\equiv_E$ over terms such that:
\begin{itemize}
\item $(t_1 = t_2) \in E \Rightarrow (t_1 \equiv_E t_2)$.
\item For each $f(s_1, \dots, s_k)$ and $f(t_1, \dots, t_k)$ occurring in $E$,
if $s_i \equiv_E t_i$ for each $i \in \{ 1, \dots, k \}$, then $f(s_1, \dots, s_k) \equiv_E f(t_1, \dots, t_k)$.
\end{itemize}
\item $\Phi$ is satisfiable iff $\forall (t_1 \neq t_2) \in D \Rightarrow (t_1 \,\cancel{\equiv}_E\, t_2)$.
\end{enumerate}
\begin{remark}
In practice, congruence closure is usually implemented using a DAG to represent terms and union-find for the $E^*$ class.
\end{remark}
\end{description}
\subsection{Arithmetic theories}
\begin{description}
\item[Linear real arithmetic]
LRA theory has signature $\Sigma_\text{LRA} = (\mathbb{Q}, +, -, *, \leq)$
where the multiplication $*$ is only linear.
\begin{description}
\item[Fourier-Motzkin elimination] \marginnote{Fourier-Motzkin elimination}
Given an LRA formula, its satisfiability can be decided as follows:
\begin{enumerate}
\item Replace:
\begin{itemize}
\item $(t_1 \neq t_2)$ with $(t_1 < t_2) \vee (t_2 < t_1)$.
\item $(t_1 \leq t_2)$ with $(t_1 < t_2) \vee (t_1 = t_2)$.
\end{itemize}
\item Eliminate equalities and apply the Fourier-Motzkin elimination\footnote{\url{https://en.wikipedia.org/wiki/Fourier\%E2\%80\%93Motzkin_elimination}}
method on all variables to determine satisfiability.
\end{enumerate}
\begin{remark}
Not practical on a large number of constraints.
The simplex algorithm is more suited.
\end{remark}
\end{description}
\item[Linear integer arithmetic]
LIA theory has signature $\Sigma_\text{LRA} = (\mathbb{Z}, +, -, *, \leq)$
where the multiplication $*$ is only linear.
Fourier-Motzkin can be applied to check satisfiability.
Simplex and branch \& bound is usually better.
\end{description}
\subsection{Difference logic theory}
Difference logic (DL) atomic formulas have form $(x - y \leq k)$
where $x$, $y$ are variables and $k$ is a constant.
\begin{remark}
Constraints with form $(x - y \bowtie k)$
where $\bowtie \,\in \{ =, \neq, <, \geq, > \}$ can be rewritten using $\leq$.
\end{remark}
\begin{remark}
Unary constraints $x \leq k$ can be rewritten as $x - z_0 \leq k$
with the assignment $z_0 = 0$.
\end{remark}
\begin{theorem}
By allowing $\neq$ and with domain in $\mathbb{Z}$,
deciding satisfiability becomes NP-hard.
\begin{proof}
Any graph $k$-coloring instance can be poly-reduced to a difference logic formula.
\end{proof}
\end{theorem}
\begin{description}
\item[Graph consistency] \marginnote{Graph consistency}
Given DL literals $\Phi$, it is possible to build a weighted graph $\mathcal{G}_\Phi$ where:
\begin{descriptionlist}
\item[Nodes] Variables occurring in $\Phi$.
\item[Edges] $x \xrightarrow{k} y$ for each $(x - y \leq k) \in \Phi$.
\end{descriptionlist}
\begin{theorem}
$\Phi$ is inconsistent $\iff$ $\mathcal{G}_\Phi$ has a negative cycle
(i.e. cycle whose cost is negative).
\end{theorem}
\begin{remark}
A negative cycle acts as an inconsistency explanation (not necessarily minimal).
\end{remark}
\begin{remark}
From the consistency graph, if there is a path from $x$ to $y$ with cost $k$,
then $(x - y \leq k)$ can be deduced.
\end{remark}
\end{description}
\section{Combining theories}
Given $\calT_i$-solvers for theories $\calT_1, \dots, \calT_n$,
a general approach to combine them into a $\bigcup_i^n \calT_i$-solver is the following:
\begin{enumerate}
\item Purify the formula so that each literal belongs to a single theory. New constants can be introduced.
\begin{description}
\item[Interface equalities] Equalities involving shared constants across solvers should be the same for all solvers.
\end{description}
\item Iteratively run the following:
\begin{enumerate}
\item Each $\calT_i$-solver checks the satisfiability of $\calT_i$-formulas. If one detects unsatisfiability, the whole formula is unsatisfiable.
\item When a $\calT_i$-solver deduces a new literal, it sends it to the other solvers.
\end{enumerate}
\end{enumerate}
\begin{example}
Consider the formula:
\[ \Big( f\big( f(x) - f(y) \big) = a \Big) \land \Big( f(a) = a+2 \Big) \land \Big( x = y \Big) \]
where the theories of EUF and linear arithmetic (LA) are involved.
To determine satisfiability, the following steps are taken:
\begin{enumerate}
\item The formula is purified to obtain the literals:
\begin{center}
\small
\begin{tabular}{c|c}
\toprule
\textbf{LA} & \textbf{EUF} \\
\midrule
\makecell{
$e_1 = e_2 - e_3$ \\
$e_4 = 0$ \\
$e_5 = a+2$
} &
\makecell{
$f(e_1) = a$ \\
$e_2 = f(x)$ \\
$e_3 = f(y)$ \\
$f(e_4) = e_5$ \\
$x = y$
} \\
\bottomrule
\end{tabular}
\end{center}
where $e_1, \dots, e_5$ are new constants.
\item Both EUF-solver and LA-solver determine \texttt{SAT}.
Moreover, the EUF-solver deduces that $\{ x=y, f(x)=e_2, f(y)=e_3 \} \models_{EUF} (e_2 = e_3)$ and sends it to the LA-solver.
\begin{center}
\small
\begin{tabular}{c|c}
\toprule
\textbf{LA} & \textbf{EUF} \\
\midrule
\makecell{
$e_1 = e_2 - e_3$ \\
$e_4 = 0$ \\
$e_5 = a+2$ \\
$\underline{e_2 = e_3}$
} &
\makecell{
$f(e_1) = a$ \\
$e_2 = f(x)$ \\
$e_3 = f(y)$ \\
$f(e_4) = e_5$ \\
$x = y$
} \\
\bottomrule
\end{tabular}
\end{center}
\item Both EUF-solver and LA-solver determine \texttt{SAT}.
Moreover, the LA-solver deduces that $\{ e_2-e_3=e_1, e_4=0, e_2=e_3 \} \models_{LA} (e_1 = e_4)$ and sends it to the EUF-solver.
\begin{center}
\small
\begin{tabular}{c|c}
\toprule
\textbf{LA} & \textbf{EUF} \\
\midrule
\makecell{
$e_1 = e_2 - e_3$ \\
$e_4 = 0$ \\
$e_5 = a+2$ \\
$e_2 = e_3$
} &
\makecell{
$f(e_1) = a$ \\
$e_2 = f(x)$ \\
$e_3 = f(y)$ \\
$f(e_4) = e_5$ \\
$x = y$ \\
$\underline{e_1 = e_4}$
} \\
\bottomrule
\end{tabular}
\end{center}
\begin{center}
$\vdots$
\end{center}
\item The EUF-solver determines \texttt{SAT} but the LA-solver determines \texttt{UNSAT}.
Therefore, the formula is unsatisfiable.
\end{enumerate}
\end{example}
\subsection{Deterministic Nelson-Oppen}
\marginnote{Deterministic Nelson-Oppen}
Let $\calT_1$ be a $\Sigma_1$-theory and $\calT_2$ be a $\Sigma_2$-theory.
$(\calT_1 \cup \calT_2)$-satisfiability can be checked with the deterministic Nelson-Oppen if $\calT_1$ and $\calT_2$ are:
\begin{descriptionlist}
\item[Signature-disjoint] $\Sigma_1 \cap \Sigma_2 = \varnothing$.
\item[Stably-infinite] $\calT_i$ is stably-infinite iff every $\calT_i$-satisfiable formula $\varphi$ has a corresponding
$\calT_i$-model with a universe of infinite cardinality that satisfies it.
\item[Convex] For each set of $\calT_i$-literals $S$, it holds that:
\[ \big( S \models_{\calT_i} (a_1 = b_1) \vee \dots \vee (a_n = b_n) \big) \Rightarrow \big( S \models_{\calT_i} (a_k = b_k) \big) \text{ for some $k \in \{ 1, \dots, n \}$ } \]
\begin{example}
$\calT_\mathbb{Z}$ is not convex. Consider the following formula $\varphi$:
\[ (1 \leq z) \land (z \leq 2) \land (u = 1) \land (v = 2) \]
We have that:
\[ \varphi \models_{\calT_\mathbb{Z}} (z = u) \vee (z = v) \]
But it is not true that:
\[ \varphi \cancel{\models}_{\calT_\mathbb{Z}} z = u \hspace{3em} \varphi \cancel{\models}_{\calT_\mathbb{Z}} z = v \]
\end{example}
\end{descriptionlist}
\begin{description}
\item[Algorithm]
Given a $(\calT_1 \cup \calT_2)$-formula $S$,
the deterministic Nelson-Oppen algorithm works as follows:
\begin{enumerate}
\item Purify $S$ into $S_1$ and $S_2$.
Let $E$ be the set of interface equalities between $S_1$ and $S_2$ (i.e. it contains all the equalities that involve shared constants).
\item If $S_1 \models_{\calT_1} \bot$ or $S_2 \models_{\calT_2} \bot$, then $S$ is unsatisfiable.
\item If $S_1 \models_{\calT_1} (x = y)$ with $(x = y) \in (E \smallsetminus S_2)$, then $S_2 \leftarrow S_2 \cup \{ x = y \}$. Go to Point 2.
\item If $S_2 \models_{\calT_2} (x = y)$ with $(x = y) \in (E \smallsetminus S_1)$, then $S_1 \leftarrow S_1 \cup \{ x = y \}$. Go to Point 2.
\item $S$ is satisfiable.
\end{enumerate}
\end{description}
\subsection{Non-deterministic Nelson-Oppen}
\marginnote{Non-deterministic Nelson-Oppen}
Extension of the deterministic Nelson-Oppen algorithm to non-convex theories.
Works by doing case splitting on pairs of shared variables and has exponential time complexity.
\section{SMT extensions}
\subsection{Layered solvers}
\marginnote{Layered solvers}
Stratify the problem into layers of increasing complexity.
The satisfiability of each layer is determined by a different solver of increasing expressivity and complexity.
\begin{figure}[H]
\centering
\includegraphics[width=0.7\linewidth]{./img/_layered_solvers.pdf}
\caption{Example of layered solvers}
\end{figure}
\subsection{Case splitting}
\marginnote{Case splitting}
Case reasoning on free variables.
\begin{example}
Given the formula:
\[ y = \texttt{read}\big( \texttt{write}(A, i, x), j \big) \]
A solver can explore the case when $i = j$ and $i \neq j$.
\end{example}
\begin{description}
\item[$\calT$-solver case reasoning]
The $\calT$solver internally detects inconsistencies through case reasoning.
\item[SAT solver case reasoning]
The $\calT$-solver encodes the case reasoning and sends it to the SAT solver.
\begin{example}
Given the formula:
\[ y = \texttt{read}\big( \texttt{write}(A, i, x), j \big) \]
The $\calT$-solver sends to the SAT solver the following:
\[
\begin{split}
y = \texttt{read}\big( \texttt{write}(A, i, x), j \big) \land (i = j) &\Rightarrow y = x \\
y = \texttt{read}\big( \texttt{write}(A, i, x), j \big) \land (i \neq j) &\Rightarrow y = \texttt{read}(A, j)
\end{split}
\]
\end{example}
\end{description}
\subsection{Optimization modulo theory}
\marginnote{Optimization modulo theory}
Extension of SMT so that it finds a model that simultaneously satisfies the input formula $\varphi$ and optimizes an objective function $f_\text{obj}$.
$\varphi$ belongs to a theory $\calT = \calT_{\preceq} \cup \calT_1 \cup \dots \cup \calT_n$
where $\calT_{\preceq}$ contains a predicate $\preceq$ (e.g. $\leq$) representing a total order.
\begin{description}
\item[Offline OTM($\mathcal{LRA}$)]
Approach that does not require to modify the SMT solver.
\begin{description}
\item[Linear search]
Repeatedly solve the problem and, at each iteration, add the constraint $\texttt{cost} < c_i$ where $c_i$ is the cost found at the $i$-th iteration.
\item[Binary search]
Given the cost domain $[l_i, u_i]$,
repeatedly pick a pivot $p_i \in [l_i, u_i]$ and add the constraint $\texttt{cost} < p_i$.
If a model is found, recurse in the domain $[l_i, p_i]$, otherwise recurse in $[p_i, u_i]$.
\end{description}
\item[Inline OTM($\mathcal{LRA}$)]
SMT solver that integrates an optimization procedure.
\end{description}