diff --git a/src/combinatorial-decision-making-and-optimization/module2/ainotes.cls b/src/combinatorial-decision-making-and-optimization/module2/ainotes.cls new file mode 120000 index 0000000..146fd3c --- /dev/null +++ b/src/combinatorial-decision-making-and-optimization/module2/ainotes.cls @@ -0,0 +1 @@ +../../ainotes.cls \ No newline at end of file diff --git a/src/combinatorial-decision-making-and-optimization/module2/cdmo2.tex b/src/combinatorial-decision-making-and-optimization/module2/cdmo2.tex new file mode 100644 index 0000000..2d48a88 --- /dev/null +++ b/src/combinatorial-decision-making-and-optimization/module2/cdmo2.tex @@ -0,0 +1,12 @@ +\documentclass[11pt]{ainotes} + +\title{Combinatorial Decision Making\\and Optimization\\(Module 2)} +\date{2023 -- 2024} +\def\lastupdate{{PLACEHOLDER-LAST-UPDATE}} + +\begin{document} + + \makenotesfront + \input{./sections/_smt.tex} + +\end{document} \ No newline at end of file diff --git a/src/combinatorial-decision-making-and-optimization/module2/sections/_smt.tex b/src/combinatorial-decision-making-and-optimization/module2/sections/_smt.tex new file mode 100644 index 0000000..19f0542 --- /dev/null +++ b/src/combinatorial-decision-making-and-optimization/module2/sections/_smt.tex @@ -0,0 +1,148 @@ +\chapter{Satisfiability modulo theory (SMT)} + + +\section{First-order logic for SMT} + + +\subsection{Syntax} + +\begin{remark} + Only quantifier-free fragments will be considered in this course. +\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$. + + \item[Formulas] \marginnote{Formulas} + The set of formulas over $\Sigma$ is denoted as $\mathbb{F}^\Sigma$. +\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 $\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} + + \begin{remark} + \texttt{ite} is an auxiliary function to capture the if-else construct. + \end{remark} +\end{description} + + +\subsection{$\mathbf{\Sigma}$-theory} + +\begin{description} + \item[Satisfiability] \marginnote{Satisfiability} + A model $\mathcal{M}$ satisfies a formula $\varphi \in \mathcal{F}^\Sigma$ if $\varphi^\mathcal{M} = \texttt{true}$. + + \item[$\mathbf{\Sigma}$-theory] \marginnote{$\Sigma$-theory} + Possibly infinite set $\mathcal{T}$ of $\Sigma$-models. + + \item[$\mathbf{\mathcal{T}}$-satisfiability] \marginnote{$\mathcal{T}$-satisfiability} + A formula $\varphi \in \mathbb{F}^\Sigma$ is $\mathcal{T}$-satisfiable if there exists a model $\mathcal{M} \in \mathcal{T}$ that satisfies it. + + \item[$\mathbf{\mathcal{T}}$-consistency] \marginnote{$\mathcal{T}$-consistency} + A set of formulas $\{ \varphi_1, \dots, \varphi_k \} \subseteq \mathbb{F}^\Sigma$ is $\mathcal{T}$-consistent iff + $\varphi_1 \land \dots \land \varphi_k$ is $\mathcal{T}$-satisfiable. + + \item[$\mathbf{\mathcal{T}}$-entailment] \marginnote{$\mathcal{T}$-entailment} + A set of formulas $\Gamma \subseteq \mathbb{F}^\Sigma$ $\mathcal{T}$-entails a formula $\varphi \in \mathbb{F}^\Sigma$ ($\Gamma \models_\mathcal{T} \varphi$) iff + in every model $\mathcal{M} \in \mathcal{T}$ that satisfies $\Gamma$, $\varphi$ is also satisfied. + + \begin{remark} + $\Gamma$ is $\mathcal{T}$-consistent iff $\Gamma \cancel{\models_\mathcal{T}} \bot$. + \end{remark} + + \item[$\mathbf{\mathcal{T}}$-validity] \marginnote{$\mathcal{T}$-validity} + A formula $\varphi \in \mathbb{F}^\Sigma$ is $\mathcal{T}$-valid iff $\varnothing \models_\mathcal{T} \varphi$. + + \begin{remark} + $\varphi$ is $\mathcal{T}$-consistent iff $\lnot\varphi$ is not $\mathcal{T}$-valid. + \end{remark} + + \begin{description} + \item[Theory lemma] \marginnote{Theory lemma} + $\mathcal{T}$-valid clause $c = l_1 \vee \dots \vee l_k$. + \end{description} + + \item[$\mathbf{\mathcal{T}}$-expansion] \marginnote{$\mathcal{T}$-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$ to $\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 $\mathcal{T}$, we implicitly consider the theory $\mathcal{T}'$ as: + \[ \mathcal{T}' = \{ \mathcal{M}' \mid \mathcal{M}' \text{ is an expansion of a $\Sigma$-model } \mathcal{M} \} \] + \end{remark} + + \item[Ground $\mathbf{\mathcal{T}}$-satisfiability] \marginnote{Ground $\mathcal{T}$-satisfiability} + Given a $\Sigma$-theory $\mathcal{T}$, determine if a ground formula is $\mathcal{T}$-satisfiable over a $\Sigma$-expansion $\mathcal{T}'$. + + \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 of $\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: + \[ 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 \] + + To determine if $p(g(x), f(d))$ is $\mathcal{M}$-satisfiable, we have to expand $\mathcal{M}$. + Let $\Sigma' = \Sigma \cup \{ x \}$. The expansion $\mathcal{M}'$ such that $x^{\mathcal{M}'} = \frac{\pi}{2}$ makes the formula satisfiable. +\end{example} + + +% \begin{description} +% \item[Satisfiability modulo theory (SMT)] \marginnote{Satisfiability modulo theory (SMT)} +% Satisfiability of a formula with respect to some background theory. + +% SMT extends SAT and exploits domain-specific reasoning (possibly with infinite domains). +% \end{description} \ No newline at end of file