Commit beacfd2d authored by Martin Jonas's avatar Martin Jonas
Browse files

Few changes to slides.

parent beff0d37
\documentclass[aspectratio=169]{beamer}
%\documentclass[aspectratio=169]{beamer}
\documentclass{beamer}
%\usepackage[czech]{babel}
\usepackage[utf8]{inputenc}
%balíček na A4
......@@ -128,58 +129,6 @@
\titlepage
\end{frame}
\section{Propositional Satisfiability}
\begin{frame}
\frametitle{Propositional Satisfiability}
Propositional satisfiability problem (SAT) -- decide whether a
propositional formula is satisfiable.
\bigskip
For example
$\varphi = (y \vee z)~\wedge~(\neg y \vee z)~\wedge~(y \vee x
\vee z)~\wedge~(y \vee \neg x \vee \neg z)$ is satisfiable.
\bigskip
Usually solved by a \alert{conflict driven clause learning} algorithm (CDCL), which relies on:
\begin{itemize}
\item preprocessing,
\item variable assignment (with heuristics),
\item unit propagation,
\item conflict analysis,
\item clause learning,
\item backtracking,
\item restarts.
\end{itemize}
% \begin{example}
% $\varphi = (\neg y \vee z)~\wedge~(\neg y \vee z)~\wedge~(y \vee x \vee z)~\wedge~(y \vee \neg x \vee \neg z)$.
% \bigskip
% \begin{tikzpicture}[every node/.style={draw}]
% \node (e) at (5,4) {decide};
% \node [visible on=<2->] (x) at (2,3) {decide};
% \node [visible on=<3->] (xy) at (0,2) {propagate};
% \node [visible on=<4->] (xyz) at (0,0.5) {conflict (learn $\neg y$)};
% \node [visible on=<5->] (-y) at (9,3) {decide};
% \node [visible on=<6->] (-yz) at (7,2) {propagate};
% \node [visible on=<7->] (-yz-x) at (7,0.5) {sat};
% \path[auto, every node/.style={}, above]
% (e) edge [visible on=<2->] node {$x$} (x)
% (x) edge [visible on=<3->] node {$y$} (xy)
% (xy) edge [visible on=<4->, left] node {$z$} (xyz)
% (e) edge [visible on=<5->] node {$\neg y$} (-y)
% (-y) edge [visible on=<6->] node {$z$} (-yz)
% (-yz) edge [visible on=<7->, left] node {$\neg x$} (-yz-x);
% \end{tikzpicture}
% \end{example}
\end{frame}
\section{Satisfiability Modulo Theories}
\begin{frame}
\frametitle{Satisfiability Modulo Theories}
......@@ -189,33 +138,32 @@
\smallskip
Function symbols are given interpretations by the theory.
Function and relation symbols are given interpretations by the theory.
\bigskip
Traditionally solved by \alert{CDCL modulo theories} -- combination of
CDCL and a specialized theory solver.
\pause
\begin{example}
Let $\varphi = (x + y = 3) \wedge (x > 1) \wedge (y = 2 \vee y = 1)$.
For example
\begin{itemize}
\item $x + y = 3~\wedge~x > 1~\wedge~y > x$ is satisfiable over the
integers,
\item $3 = x + x$ is unsatisfiable over the integers,
\item $3 = x + x$ is satisfiable over the rationals.
\end{itemize}
\begin{enumerate}[<+->]
\item Propositional model $\{ x + y = 3,~x > 1,~y = 2,~\neg(y = 1) \} $.
\item This model \textbf{is not} consistent with the theory of integers.
\item Conjoin $\neg (x + y = 3) \vee \neg (x > 1) \vee \neg (y = 2) \vee (y = 1)$ to $\varphi$.
\item Propositional model $\{ x + y = 3,~x > 1,~\neg(y=2),~y = 1\} $.
\item This model \textbf{is} consistent with the theory of integers.
\item $\varphi$ is satisfiable.
\end{enumerate}
\end{example}
\end{frame}
\section{Theory of Bit-Vectors}
\begin{frame}
\frametitle{Theory of Bit-Vectors}
Hardware and programming languages do not work over integers.
The formula
\[
(x > 0)~\wedge~(y > 0)~\wedge~(x + y < 0)
\]
should be satisfiable due to overflows.
Theory of bit-vectors describes bounded integers (or vectors of
bits) with:
\begin{itemize}
......@@ -224,16 +172,9 @@
\item comparison.
\end{itemize}
Often used in modelling of software.
\bigskip
Different from mathematical integers -- for example the formula
\[
\varphi = (x^{[32]} >_s 0)~\wedge~(y^{[32]} >_s 0)~\wedge~(x^{[32]} + y^{[32]} = 0)
\]
\smallskip
is \alert{satisfiable}.
Often used in modelling of software.
\end{frame}
\section{Quantifier-free Bit-Vector Logic}
......@@ -267,21 +208,6 @@
Quantifier bit-vector formulas traditionally solved by
\alert{quantifier instantiation}.
\pause
\begin{example}
Let $\varphi = a > 3 ~\wedge~ \forall x\,(a \not = 2 \cdot x)$
\pause
\begin{itemize}[<+->]
\item $a > 3$ is satisfiable with model $a = 4$.
\item $a = 4$ not a model of $\forall x \,(a \not = 2 \cdot x)$ -- consider $x = 2$.
\item Add instance of the quantifier for $x = 2$.
\item $a > 3 ~\wedge~ (a \not = 2 \cdot 2)$ is satisfiable with model $a = 5$.
\item $a = 5$ is a model of $\forall x \,(a \not = 2 \cdot x)$.
\item $\varphi$ is satisfiable
\end{itemize}
\end{example}
\end{frame}
\section{Symbolic Approach to Quantified Bit-Vectors}
......@@ -341,7 +267,9 @@
\end{frame}
\begin{frame}
We have implemented the solver Q3B, which
\frametitle{Symbolic Approach to Quantified Bit-Vectors}
I have implemented the solver Q3B, which
\begin{itemize}
\item simplifies the formula,
\item converts the formula to the BDD,
......@@ -351,8 +279,7 @@
\bigskip
Our results and results of SMT-COMP 2016 show that Q3B is
\alert{more efficient} than standard SMT solvers.
Q3B is the \alert{winner} of SMT Competition 2016 in the category of quantified bit-vectors.
\end{frame}
\section{Aims of the Work}
......@@ -371,7 +298,8 @@
\begin{itemize}
\item Determining a computational complexity of quantified bit-vector logic with
bit-widths represented in binary.
\item Extending simplifications using unconstrained variables
\item Extending known syntactic simplifications of quantified
bit-vector formulas.
\end{itemize}
\end{frame}
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment