<html><head><meta name="color-scheme" content="light dark"></head><body><pre style="word-wrap: break-word; white-space: pre-wrap;">
\begin{slide}{Anwendungsaufgabe}

Motivation: (Un)gleichungssysteme Ã¼ber 
\begin{itemize}
\item $(\{-\infty\}\cup \NN,\max,+)$ 
  (arktischer Halbring)
\item $(\NN\cup\{+\infty\},\min,\max)$ 
  (\glqq fuzzy\grqq\ Halbring)
\end{itemize}


\begin{itemize}
\item Term $\to$ 
  Variable $\mid$ Zahl 
  $\mid \max(t_1,t_2) \mid \min(t_1,t_2) \mid t_1+t_2$
\item Formel $\to$ Gleichung. 
  (Ungl. nicht nÃ¶tig, warum?)  
\end{itemize}

(auch fÃ¼r reelle Zahlen) \emph{nicht} 
auf lineares Ungl.sys. reduzierbar (sonst P$=$NP).


Anwendung: Terminationsbeweise mit 
arktischen/fuzzy Matrizen

\end{slide}

\begin{slide}{Ordnungsconstraints fÃ¼r Matrizen}

Wortersetzungssystem $R$ Ã¼ber $\Sigma$, 

Bsp: $R=\{aa \to aba\}$ Ã¼ber $\Sigma=\{a,b\}$

\bigskip

Matrix-Interpretation (Halbring $D$, Dimension $n$)

$[\cdot]: \Sigma\to D^{n\times n}$
fÃ¼r Buchstaben 

fÃ¼r WÃ¶rter durch Multiplikation: 
$[x_1,\ldots,x_k]=[x_1]\circ\ldots\circ{}[x_k]$

\bigskip
zulÃ¤ssig: $\forall x\in\Sigma: [x]_{1,1} \neq 0_D$

kompatibel: 
$\forall (l,r)\in R: \forall i,j: [l]_{i,j} &gt;_0 [r]_{i,j}$

wobei $p&gt;_0 q \iff (p=0_D=q) \vee (p&gt;q)$

\bigskip

Beispiel: \( D=(\NN\cup\{+\infty\},\min,\max), \)

\([a] = \left(\begin{array}{ccc}
2 &amp; +\infty &amp; 0 \\
1 &amp; +\infty &amp; 0 \\
+\infty &amp; +\infty &amp; +\infty
\end{array}\right),
[b] = \left(\begin{array}{ccc}
0 &amp; 0 &amp; 0 \\
0 &amp; 0 &amp; 0 \\
0 &amp; 0 &amp; 0
\end{array}\right).
\)


\end{slide}
  
\begin{slide}{LÃ¶sungsansÃ¤tze}
($=$ Projektthemen)
\begin{itemize}
\item simulieren als MIP, dann lÃ¶sen mit glpk oder scip
\item SMT/QFLRA, QFLIA, dann lÃ¶sen mit (z. B.) Z3.2
\item (\glqq bitblasting\grqq, 
  SMT/QFBV oder direkt nach SAT)
\end{itemize}
\bigskip
Literatur:
\begin{itemize} \itemsep 2pt
\item Definition, Competition (SMT/LIB, /COMP, /EXEC)
\url{http://www.smtexec.org/exec/?jobs=311}
\item
\glqq SMT als Buch\grqq: 
Daniel Kroening und Oliver Strichman:
\emph{Decision Procedures---an Algorithmic Point of View,}
\begin{small}
Springer 2008.
\url{http://www.decision-procedures.org/}
\end{small}
\end{itemize}

\end{slide}
</pre></body></html>