Multiple changes

  pages     = {245--257},

  year      = {1979}

}

@article{Luc16,

  author    = {Martin L{\"{u}}ck},

  title     = {Complete Problems of Propositional Logic for the Exponential Hierarchy},

  journal   = {CoRR},

  volume    = {abs/1602.03050},

  year      = {2016}

}

 No newline at end of file

\section{Objectives and Expected Results}

\subsection{Unconstrained variable propagation for quantified

  bit-vectors}

Simplifications using unconstrained variables can be extended to

quantified formulas. However, in the quantified setting, constraints

can be induced also by the order of the quantified variables. We have

hypothesis of the necessary condition for the quantified variable to

be unconstrained and we have implemented an proof-of-concept

simplification procedure using unconstrained variables for the

quantified bit-vector formulas. Although the initial experimental

results, conducted on the formulas from the semi-symbolic model

checker \SymDivine look promissing, the formal proof of the correctnes

is not yet complete.

Furthermore, we suggest simplifications even for term in the form

$k \times x$ with odd values of $x$. If $x$ has bit-width $n$, $i$ is

the largest number such that $2^i$ which divides the constant $k$ and

the value $x$ is unconstrained, the term $k \times x$ can be rewritten

to $extract_0^{n-i}(x) \cdot 0^i$. This approach can possibly be

extended to the multiplication of two variables from one is

unconstrained and further generalized. We plan to prove the

correctness of these rules and develop a formal framework to classify

such rewrite rules.

\subsection{Symbolic solver for quantified bit-vectors}

I plan to continue developing the implemented symbolic \smt solver for

quantified bit-vecors Q3B. Besides implementing the proposed

simplifiactions for quantified formulas containing unconstrained

variables, I plan to add support of uninterpreted functions and theory

of arrays, which are highly desirable for the usage in program

verification. I also want to implement a support for extracting

unsatisfiable cores from the intermediate \bdds, which were produced

I will continue developing the implemented symbolic \smt solver Q3B,

which is aimed for solving quantified bit-vector formulas. In

particular, I plan to add support for uninterpreted functions and the

theory of arrays, which is highly desirable for applications in the

program verification. I also want to implement an extraction of an

unsatisfiable core from the intermediate \bdds that were produced

during the computation of the solver.

Additionally, approximations implemented are right now very simple and

could benefit from better refinement of the approximation in the case

that the current approximation is too coarse.

Additionally, currently implemented approximations are very simple and

could benefit from better refinement in the case that the current

approximation is too coarse.

Moreover, we want to implement other variants of decision diagrams

such as zero-suppressed decision diagrams introduced by

Minato~\cite{Min93} and algebraic decision diagrams introduced by

Bahar et al.~\cite{BFGHMPS} and experimentally evaluate their effect

on the performance of the \smt solver.

Moreover, I want to implement other variants of decision diagrams such

as zero-suppressed decision diagrams introduced by Minato~\cite{Min93}

and algebraic decision diagrams introduced by Bahar et

al.~\cite{BFGHMPS} and experimentally evaluate their effect on the

performance of the symbolic \smt solver for the quantified

bit-vectors.

\subsection{Hybrid approach to quantified bit-vectors}

Although our results with the symbolic \smt solver for quantified

bit-vectors look promissing, standard \smt solvers still perform

better on simple queries and on queries containing

multiplication. Therefore, I want to develop a hybrid approach to \smt

solving of quantified bit-vector formulas, which combines strengths of

both of these approaches. For example, a part of the quantified

formula without multiplication can be converted to the \bdd, which can

be used to guide the model search in the model-based quantifier

instantiation. One possible way of achieving this is adding \bdd based

representation of sets of assignments to the \mcbv solver developed by

Zeljić et al. The \bdd representation can be added to the current

over-approximations by bit-patterns and arithmetic intervals.

Although results of the symbolic \smt solver for quantified

bit-vectors look promising, standard \smt solvers still perform

better on queries containing multiplication and complex

arithmetic. Therefore, I plan to develop a hybrid approach to \smt

solving of quantified bit-vector formulas that combines strengths of

both of these approaches. For example, parts of the quantified

formula, which do not contain multiplication, can be converted to the

\bdd that can be used to guide the model search in the model-based

quantifier instantiation. One possible way of achieving this is adding

support for \bdds to the solver \mcbv developed by Zeljić et al. The

\bdd representation can be added to the currently used

over-approximations by bit-patterns and arithmetic

intervals. Moreover, a tighter cooperation is possible -- if a \mcsat

solver decides a value, this can be used to partially instantiate a

quantified part of the formula, for which the \bdd will be computed.

As the part of my PhD study, also an implementation of a proposed

As the part of my PhD study, an implementation of a solver using the

hybrid approach and its evaluation on the representative set of

benchmark is expected.

benchmark is expected. The hybrid approach to quantified bit-vectors

is the main aim of my PhD study.

\subsection{Unconstrained variable propagation for quantified

  bit-vectors}

Simplifications using unconstrained variables can be extended to

quantified formulas. However, in the quantified setting, constraints

among variables can be introduced also by the order in which the

variables are quantified. We have hypothesis that describes the

necessary condition for the quantified variable to be considered as

unconstrained. Based on this hypothesis and a partial proof of its

validity, we have implemented an proof-of-concept simplification

procedure that can simplify quantified formulas which contain

unconstrained variables. Although the initial experimental results,

conducted on the formulas from the semi-symbolic model checker

\SymDivine, look promising, the formal proof of the correctness is not

yet complete.

Moreover, the simplifications of formulas with unconstrained variables

can be further extended. For example, if a formula contains a term

$k \times x$ with an odd values of $k$ and the variable $x$ is

unconstrained, this term can be replaced by a simpler term. In

particular, if $i$ is the largest number for which $2^i$ divides the

constant $k$ and the variable $x$ has bit-width $n$, the term

$k \times x$ can be rewritten to $extract_0^{n-i}(x) \cdot 0^i$. In

turn, this approach can be also extended to the multiplication of two

variables from one is unconstrained. I plan to investigate further

extensions of to the terms containing division and remainder

operations and publish all described extension to the unconstrained

variable propagation. I will also experimentally evaluate the effect

of such simplifications on our solver Q3B and on state-of the art

solvers such as Boolector, CVC4, and Z3.

\subsection{Complexity of BV2}

As was explained in section \ref{sec:complexity}, the precise

known to be in \EXPSPACE and to be \NEXPTIME-hard. However, a class

for which the problem is complete is not known.

Acording to our investigation, it is probably complete for neither of

According to our investigation, it is probably complete for neither of

those complexity classes. We are working on a proof which shows that

BV2 is complete for the class of problems solvable by the

\emph{alternating Turing machine} (\atm) with the exponential space

and \emph{polynomial number of alternations} with respect to log-space

reduction. This class is usually denoted as \AEXPTIMEp and is known to

be in between \EXPSPACE and \NEXPTIME. However, whether any of the

inclusions is proper is not known.

inclusions is proper is not known. The \AEXPTIMEp-hardness of the BV2

can be shown by reducing the problem of satisfiability of

\emph{quantified second order boolean formulas}, which was recently

proven to be \AEXPTIMEp-hard by Lück~\cite{Luc16}.

Expected result is a paper published at an international conference or

in a journal.

\newpage

\section{Progression Schedule}

The plan of my future study and research activities is following:

\begin{description}[style=nextline,leftmargin=0.8cm]

\item [now -- January 2017] Extending unconstrained variable

  propagation to quantified formulas and to non-linear multiplication.

\item [now -- January 2019] Improvements and mantaining of the

\item [now -- January 2019] Improvements and maintaining of the

  developed symbolic \smt solver Q3B.

\item [January 2017] Doctoral exam and defence of this thesis proposal.

\item [January 2017 -- May 2017] Proving a precise complexity class of

  the quantfied bit-vector formulas without uninterpreted functions

  and with binary encoded bit-widths.

\item [May 2017 -- January 2018] Development of a hybrid approach to

\item [January 2017] Doctoral exam and defense of this thesis proposal.

\item [February 2017 -- April 2017] Proving a precise complexity class

  of the quantified bit-vector formulas without uninterpreted functions

  and with binary encoded bit-widths. Preparing a paper on this topic.

\item [May 2017 -- December 2017] Development of a hybrid approach to

  \smt solving of quantified bit-vector formulas combining symbolic

  representation of formulas with \dpllt or \mcsat.

\item [January 2018 -- August 2018] Implementing a hybrid \smt solver

\item [August 2018 -- January 2019] Text of the Ph.D. thesis.

\item [September 2018 -- January 2019] Text of the PhD thesis.

\item [January 2019] The final version of the thesis.

\end{description}

        \hfill

        \vfill

        \bigskip \bigskip

        \begingroup

            \color{Maroon}\spacedallcaps{\myTitle} \\ \bigskip

            \Large{\color{Maroon}\spacedallcaps{\myTitle}} \\ \bigskip

        \endgroup

        \spacedlowsmallcaps{\myName}

        \vfill

        \includegraphics[width=6cm]{gfx/fi_logo} \\ \bigskip

        \includegraphics[width=5cm]{gfx/fi_logo}

        \vfill

        \mySubtitle \\ \medskip

        \mySubtitle \\

        %\myDegree \\

        %\myDepartment \\

        %\myFaculty \\

        %\myUni \\ \bigskip

        \smallskip

        \myTime

        \vfill

      \end{center}

      \noindent \myFaculty, \myUni \\

      \noindent Supervisor: \myProf

  \end{addmargin}

\end{titlepage}

\newcommand{\sls}{\textsc{sls}\xspace}

\newcommand{\mcbv}{\textsc{mcbv}\xspace}

\newcommand{\nnf}{\textsc{nnf}\xspace}

\newcommand{\qsbf}{\textsc{qsbf}\xspace}

\newcommand{\true}{\ensuremath{\texttt{true}}}

\newcommand{\false}{\ensuremath{\texttt{false}}}

\newcommand{\myProf}{doc. RNDr. Jan Strejček, Ph.D.\xspace}

%\newcommand{\myOtherProf}{Put name here\xspace}

%\newcommand{\mySupervisor}{Put name here\xspace}

\newcommand{\myFaculty}{Faculty of informatics\xspace}

\newcommand{\myFaculty}{Faculty of Informatics\xspace}

%\newcommand{\myDepartment}{Put data here\xspace}

\newcommand{\myUni}{Masaryk University\xspace}

\newcommand{\myLocation}{Brno\xspace}

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

% Using PDFLaTeX

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

%\usepackage{tikz}

%\usetikzlibrary{backgrounds,calc}

%\usepackage{graphicx,lipsum}

\PassOptionsToPackage{pdftex,hyperfootnotes=false,pdfpagelabels}{hyperref}

    \usepackage{hyperref}  % backref linktocpage pagebackref

\pdfcompresslevel=9

\pdfadjustspacing=1

\PassOptionsToPackage{pdftex}{graphicx}

    \usepackage{graphicx}

%    \usepackage{eso-pic}

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

% Hyperreferences