Changes

\chapter{Introduction}\label{ch:introduction}

\chapter{Introduction}\label{ch:introduction}

% ************************************************

% ************************************************

During the last decades, the area of solving \emph{propositinal

During the last decades, the area of solving \emph{propositional

  satisfiability} (\sat)~\cite{DP09} and consequently the related area

  satisfiability} (\sat)~\cite{DP09} and consequently the related area

of solving \emph{satisfiability modulo theories} (\smt)~\cite{BSST09}

of solving \emph{satisfiability modulo theories} (\smt)~\cite{BSST09}

has undergone steep development in both theory and practice. Achieved

has undergone steep development in both theory and practice. Achieved

analysis and verification, where \smt solvers are now seen as standard

analysis and verification, where \smt solvers are now seen as standard

tools.

tools.

The task for an \smt solver is for a given first-order formula in a

The task for an \smt solver is to decide for a given first-order

given first-order theory decide, whether the formula is

formula in a given first-order theory whether the formula is

satisfiable. Usually, if the formula is satisfiable, the \smt solver

satisfiable. Usually, if the formula is satisfiable, the \smt solver

also has the ability to provide its model. Modern \smt solvers support

also has the ability to provide its model. Modern \smt solvers support

wide range of different first-order theories -- for example, theories

wide range of different first-order theories -- for example, theories

of integers, real numbers, floating-point numbers, arrays, strings,

of integers, real numbers, floating-point numbers, arrays, strings,

inductively defined data types, bit-vectors and various combinations

inductively defined data types, bit-vectors and various combinations

and framgents of these theories. From the software analysis and

and fragments of these theories. From the software analysis and

verification point of view, a particularly important of these theories

verification point of view, a particularly important of these theories

is the theory of bit-vectors, which can be used to describing

is the theory of bit-vectors, which can be used to describing

properties of computer programs, since they usually use data-types of

properties of computer programs, since they usually use data-types of

formulas is twofold. Formulas in the bit-vector theory allow to model

formulas is twofold. Formulas in the bit-vector theory allow to model

the program's behavior precisely including possible arithmetic

the program's behavior precisely including possible arithmetic

overflows and underflows. Furthermore, in contrast to the theory of

overflows and underflows. Furthermore, in contrast to the theory of

integers, the satisfiability of bit-vector theory is decidable even if

integers, the satisfiability of the bit-vector theory is decidable

the multiplication is allowed.

even if the multiplication is allowed.

Therefore, quantifier-free bit-vector formulas are used in tools for

Therefore, quantifier-free bit-vector formulas are used in tools for

symbolic execution, bounded model checking, analysis of hardware

symbolic execution, bounded model checking, analysis of hardware

circuits, static analysis, or test generation. Most of the current

circuits, static analysis, or test generation. Most of the current

\smt solvers for the quantifier-free bit-vector formulas eagerly or

\smt solvers for quantifier-free bit-vector formulas eagerly or lazily

lazily translate the formula to the propositional logic

translate the formula to the propositional logic (so called

(\emph{bit-blasting}) and use an efficient \sat solver to decide its

\emph{bit-blasting}) and use an efficient \sat solver to decide its

satisfiability. Therefore, the efficiency of most of the \smt solvers

satisfiability. Therefore, the efficiency the majority of \smt solvers

for such formulas is tightly connected to the efficiency of the \sat

for such formulas is tightly connected to the efficiency of the \sat

solvers. Plenty of solvers for the quantifier-free bit-vector formulas

solvers. Plenty of solvers for the quantifier-free bit-vector formulas

exist: Beaver~\cite{Beaver}, Boolector~\cite{Boolector},

exist: for example Beaver~\cite{Beaver}, Boolector~\cite{Boolector},

CVC4~\cite{CVC4}, MathSAT5~\cite{MathSAT}, OpenSMT~\cite{OpenSMT},

CVC4~\cite{CVC4}, MathSAT5~\cite{MathSAT}, OpenSMT~\cite{OpenSMT},

Sonolar~\cite{Sonolar}, Spear~\cite{Spear}, STP~\cite{STP},

Sonolar~\cite{Sonolar}, Spear~\cite{Spear}, STP~\cite{STP},

UCLID~\cite{LS04}, Yices~\cite{Yices}, or Z3~\cite{Z3}.

UCLID~\cite{LS04}, Yices~\cite{Yices}, or Z3~\cite{Z3}.

In some cases, quantifier-free formulas are not succint enough and

In some cases, quantifier-free formulas are not succinct enough and

quantified formulas are necessary. Bit-vector quantified formulas

using quantification is necessary to keep a reasonable size of the

arise naturally for example in applications that generate loop

formula. Bit-vector quantified formulas arise naturally for example in

invariants, ranking functions, loop summaries, or that test equality

applications that generate loop invariants, ranking functions, loop

of two symbolic states. However, the \smt solvers' support of

summaries, or that test equality of two symbolic states. However, the

quantified bit-vector logic is much more modest -- CVC4, Yices, and Z3

\smt solvers' support of quantified bit-vector logic is much more

officially support quantifiers in bit-vector formulas. Recently,

modest -- only CVC4, Yices, and Z3 officially support quantifiers in

quantifiers have been also implemented in an development version of

bit-vector formulas. Recently, quantifiers have been also implemented

Boolector. All of these \smt solvers solve quantified bit-vector

in an development version of Boolector~\cite{BoolectorComp}. All of

formulas by some variant of quantifier-instantiation and using a

these \smt solvers solve quantified bit-vector formulas by some

solver for quantifier-free formulas as an oracle.

variant of quantifier-instantiation and using a solver for

quantifier-free formulas as an oracle.

In the last year, we have proposed a different approach. We have

In the last year, we have proposed a different approach. We have

implemented a symbolic solver Q3B, which is based on binary decision

implemented a symbolic solver Q3B, which is based on binary decision

verification.

verification.

The thesis proposal is organized as follows. Chapter~\ref{ch:sota}

The thesis proposal is organized as follows. Chapter~\ref{ch:sota}

summarizes the state of the art and is divided into six sections. The

summarizes the state of the art and is divided into six

first section introduces necessary background and notations from

sections. Section~\ref{sec:prelim} introduces necessary background and

propositional logic and first-order logic. The second section

notations from propositional logic and first-order

describes approaches to solving propositional satisfiability problem

logic. Section~\ref{sec:sat} describes approaches to solving

and the third section describes approaches to solving satisfiability

propositional satisfiability problem and Section~\ref{sec:smt}

modulo theories. The fourth and fifth sections are devoted to solving

describes approaches to solving satisfiability modulo

quantifier-free and quantifed formulas over the theory of bit-vectors,

theories. Sections \ref{sec:qfbv} and \ref{sec:bv} are devoted to

respectively. The final, sixth, section describes results about the

solving quantifier-free and quantified formulas over the theory of

computational complexity of bit-vector

bit-vectors, respectively. Finally, Section~\ref{sec:complexity}

logics. Chapter~\ref{ch:achieved} describes results, which we have

section describes results about the computational complexity of

achieved during the first two years of my PhD

bit-vector logics. Chapter~\ref{ch:achieved} describes results, which

we have achieved during the first two years of my PhD

study. Chapter~\ref{ch:aims} presents the aim of the thesis and states

study. Chapter~\ref{ch:aims} presents the aim of the thesis and states

plans remaining part of the PhD study.

plans remaining part of the PhD study.

%*****************************************

%*****************************************

\section{Preliminaries}

\section{Preliminaries}

\label{sec:prelim}

This section introduces the notation used in the rest of this

This section introduces the notation used in the rest of this

chapter. The exposition of the propositional logic is mainly based on

chapter. The exposition of the propositional logic is mainly based on

is clear from the context, we drop the respective $\Sigma$- or

is clear from the context, we drop the respective $\Sigma$- or

$\mathcal{T}$- prefixes.

$\mathcal{T}$- prefixes.

% In the following text, we suppose the knowledge of a standard

% first-order logic and model theory, which is given for example by

% Enderton~\cite{End01}.

% Definitions for the first-order quantifier-free formulas are similar

% to those from subsection \ref{prelim:prop}, except that the set $\P$

% now contains a fixed finite set of first-order atoms that do not

% contain free variables. For example, if we consider a set of atoms

% $\P = \{ x \geq y + 1, x = 4 \}$, where $x, y, 1$, and $4$ are

% constant symbols, $x \geq y + 1~\vee~\neg (x = 4)$ is a clause.

% A \emph{theory} $\mathcal{T}$ is a set of first-order structures.  A formula

% $\varphi$ is $\mathcal{T}$-\emph{satisfiable} or $\mathcal{T}$-\emph{consistent} if there

% is a structure $M \in T$ in which the formula $F$ holds in the

% standard first-order sense. The formula $\varphi$ is

% $\mathcal{T}$-\emph{unsatisfiable} or $\mathcal{T}$-\emph{inconsistent} otherwise. If the

% distinction is necessary, we call literals over a specific background

% theory $\mathcal{T}$-literals. In the rest of this chapter, we consider only

% theories for which the satisfiability of conjunctions of literals is

% decidable and we call any decision procedure for conjunctions of

% $\mathcal{T}$-literals a $\mathcal{T}$-\emph{solver}.

% Using the same notation as in the propositional logic, a partial

% assignment is a set of literals and can be therefore seen as a

% conjunction of literals, i.e. a formula. If a partial assignment $M$

% is a propositional model of a given formula $\varphi$ and the partial

% assignment $M$ is $\mathcal{T}$-consistent, we say that $M$ is a

% $\mathcal{T}$-\emph{model} of $\varphi$. If $\varphi$ and $\psi$ are formulas

% such that $\varphi \wedge \neg \psi$ is $\mathcal{T}$-inconsistent, we say that

% \emph{$\varphi$ entails $\psi$ in $\mathcal{T}$} and write it as

% $\varphi \models_T \psi$.

% \subsection{First-order quantified formulas}

% As the first-order formulas containing quantifiers are concerned, we

% impose no restrictions on their form. We again suppose the knowledge

% and definitions from the standard first-order logic and model theory.

% A first-order formula $\varphi$ is in a \emph{negation normal form},

% if the only logical connectives in $\varphi$ are negations,

% conjunctions, and disjunctions and all negations in $\varphi$ occur in

% front of a literal. Every first-order formula can be transformed to a

% formula without existential quantifiers by introducing uninterpreted

% functions; this process is known as \emph{Skolemization}.

\subsection{Many-sorted logic}

\subsection{Many-sorted logic}

For some theories, it can be convinient to distinguish several types

For some theories, it can be convinient to distinguish several types

in Enderton~\cite{End01}.

in Enderton~\cite{End01}.

\section{Propositional satisfiability}

\section{Propositional satisfiability}

\label{sec:sat}

A \emph{propositional satisfiability problem} (\sat) is, for a given

A \emph{propositional satisfiability problem} (\sat) is, for a given

formula $\varphi$ in \cnf, to decide whether it is satisfiable. The

formula $\varphi$ in \cnf, to decide whether it is satisfiable. The

remain, the formula is satisfiable. The main problem of \dppr is its

remain, the formula is satisfiable. The main problem of \dppr is its

space complexity, since the number of the clauses may grow

space complexity, since the number of the clauses may grow

exponentially even for simple formulas. To alleviate this problem, the

exponentially even for simple formulas. To alleviate this problem, the

refinement of \dppr algorithm was introduced in 1962 by Davis, Putnam,

refinement of \dppr algorithm was introduced in 1962 by Davis,

Logemann and Loveland~\cite{DPLL62}.

Logemann and Loveland~\cite{DPLL62}.

The Davis--Putnam--Logemann--Loveland \quotegraffito{If you don't know

The Davis--Putnam--Logemann--Loveland \quotegraffito{If you don't know

theory~\cite{HKM16}.

theory~\cite{HKM16}.

\section{Satisfiability modulo theories}

\section{Satisfiability modulo theories}

\label{sec:smt}

Similarly to \sat, the \emph{satisfiability modulo theories problem}

Similarly to \sat, the \emph{satisfiability modulo theories problem}

(\smt) is to decide for a given a \cnf formula $\varphi$ in a fixed

(\smt) is to decide for a given a \cnf formula $\varphi$ in a fixed

in bit-vectors precisely if $k$ is odd.

in bit-vectors precisely if $k$ is odd.

\section{Satisfiability of quantified bit-vector formulas}

\section{Satisfiability of quantified bit-vector formulas}

\label{sec:bv}

Although the bit-vector theory admits quantifier elimination by

Although the bit-vector theory admits quantifier elimination by

expanding all quantifiers with all possible bit-vector values of the

expanding all quantifiers with all possible bit-vector values of the

\item TACAS 2016, April 2016, Eindhoven, The Netherlands

\item TACAS 2016, April 2016, Eindhoven, The Netherlands

\end{itemize}

\end{itemize}

\section{Teaching}

\section{Teaching}

I have tutored seminar groups for the following courses:

At my faculty, I have tutored seminar groups for the following

courses:

\begin{itemize}

\begin{itemize}

\item Automata, Grammars, and Complexity (2014--now)

\item Automata, Grammars, and Complexity (2014--now)

\item Formal Languages and Automata (2016--now)

\item Formal Languages and Automata (2016--now)

\item Non-Imperative Programming (2015--now)

\item Non-Imperative Programming (2015--now)

\end{itemize}

\end{itemize}

\smallskip

\smallskip

\noindent I have also been a reader of the following bachelor theses:

\noindent I have also been an official reader of the following

bachelor theses:

\begin{itemize}

\begin{itemize}

\item Jan Mrázek -- Caching SMT Queries in SymDivine

\item Jan Mrázek -- Caching SMT Queries in SymDivine

\item Jakub Lédl -- Many-sorted equational logic

\item Jakub Lédl -- Many-sorted equational logic