diff options
Diffstat (limited to 'chapters/background/03-satisfiability-modulo-theories.tex')
| -rw-r--r-- | chapters/background/03-satisfiability-modulo-theories.tex | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/chapters/background/03-satisfiability-modulo-theories.tex b/chapters/background/03-satisfiability-modulo-theories.tex index a55d54d..80e9932 100644 --- a/chapters/background/03-satisfiability-modulo-theories.tex +++ b/chapters/background/03-satisfiability-modulo-theories.tex @@ -1,7 +1,7 @@ \section{Satisfiability Modulo Theories} \label{sec:satisfiability-modulo-theories} -Satisfiability Modulo Theories (SMT) is the problem of determining whether a mathematical formula is +\textit{Satisfiability Modulo Theories} (SMT) is the problem of determining whether a mathematical formula is satisfiable within a certain formal theory in first-order logic. Barrett et al.~\cite{barrett2016smtlib} defined the SMT-LIB standard for input format and theory definitions. @@ -11,14 +11,13 @@ multiplication by constants, and equality/inequality relations: \begin{equation} \phi ::= t_1 \sim t_2 \mid \phi_1 \lor \phi_2 \mid \phi_1 \land \phi_2 \mid \neg \phi_1 \end{equation} -where $t_1, t_2$ are linear terms of the form $c_1 x_1 + \dots + c_k x_k + c_0$ (with $c_i \in \mathbb{R}$ and $x_i$ being real +where $t_1, t_2$ are linear terms of the form $c_1 \cdot x_1 + \dots + c_k \cdot x_k + c_0$ (with $c_i \in \mathbb{R}$ and $x_i$ being real variables), and $\sim \;\in \{=, \le, <, \ge, >\}$. To represent a ReLU activation $y = \max(0, x)$ in LRA, we must introduce a disjunction: \begin{equation} (x > 0 \land y = x) \lor (x \le 0 \land y = 0) \end{equation} -For a network with $N$ ReLU neurons, there are up to $2^N$ possible activation patterns. Solving the -verification property requires the SMT solver, such as Z3 presented by De Moura et al.~\cite{demoura2008z3}, -to implicitly explore this branching search space. - +For a network with $n$ ReLU neurons, there are up to $2^n$ possible activation patterns. Solving the +verification problem requires the SMT solver, such as Z3 presented by De Moura et +al.~\cite{demoura2008z3}, to implicitly explore this branching search space. |