diff options
| author | ericmarin <maarin.eric@gmail.com> | 2026-06-21 15:38:35 +0200 |
|---|---|---|
| committer | ericmarin <maarin.eric@gmail.com> | 2026-06-26 09:57:03 +0200 |
| commit | dbdd3ea807232b0be83d6a0eba9eb13011eb48e5 (patch) | |
| tree | 308e0778743428c62032c6df0acb90a8ec06a467 /chapters/background/03-satisfiability-modulo-theories.tex | |
| parent | 8d082714a1544de0c93f1963738b0db0e114df65 (diff) | |
| download | vein-dbdd3ea807232b0be83d6a0eba9eb13011eb48e5.tar.gz vein-dbdd3ea807232b0be83d6a0eba9eb13011eb48e5.zip | |
related work + conclusion
Diffstat (limited to 'chapters/background/03-satisfiability-modulo-theories.tex')
| -rw-r--r-- | chapters/background/03-satisfiability-modulo-theories.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/chapters/background/03-satisfiability-modulo-theories.tex b/chapters/background/03-satisfiability-modulo-theories.tex index bd90559..a55d54d 100644 --- a/chapters/background/03-satisfiability-modulo-theories.tex +++ b/chapters/background/03-satisfiability-modulo-theories.tex @@ -19,6 +19,6 @@ To represent a ReLU activation $y = \max(0, x)$ in LRA, we must introduce a disj (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 Demura et al.~\cite{demoura2008z3}, +verification property requires the SMT solver, such as Z3 presented by De Moura et al.~\cite{demoura2008z3}, to implicitly explore this branching search space. |