Copy MBQI from the SAT paper

is invertible precisely if $k$ is odd.

is invertible precisely if $k$ is odd.

\section{Satisfiability of quantified bit-vector formulas}

\section{Satisfiability of quantified bit-vector formulas}

Todo.

Given a closed formula with quantifiers, the first step is to convert the

formula to the negation normal form and apply Skolemization to obtain

equisatisfiable formula of the form

\[

   \varphi ~\wedge~ \forall x_1, x_2, \dots, x_n\, (\psi[x_1, \dots, x_n]),

\]

where $\varphi$ and $\psi$ are quantifier-free formulas. Then the

\QFBV solver is invoked to check the satisfiability of the formula

$\varphi$. If $\varphi$ is unsatisfiable, then the entire formula is

unsatisfiable. If $\varphi$ is satisfiable, the \QFBV solver returns

its model $M$ and another call to the \QFBV solver is made to

determine whether $M$ is also a~model of

$\forall x_1, x_2, \dots, x_n \, (\psi)$. This is achieved by asking

the solver whether the formula $\neg \widehat{\psi}$ is satisfiable,

where $\widehat{\psi}$ is the formula $\psi$ with uninterpreted

constants replaced by their corresponding values in $M$. If

$\neg \widehat{\psi}$ is not satisfiable, then the structure $M$ is

indeed a model of the formula $\forall x_1, x_2, \dots, x_n\,(\psi)$,

therefore the entire formula is satisfiable and $M$ is its model. If

$\neg \widehat{\psi}$ is satisfiable, we get values $v_1, \dots, v_n$

such that $\neg\widehat{\psi}[v_1, \dots, v_n]$ holds.  To rule out

$M$ as a model, the instance $\psi[v_1, \dots, v_n]$ of the quantified

formula is added to the quantifier-free part, i.e.~the formula

$\varphi$ is modified to

\[

   \varphi' ~\equiv~ \varphi \wedge \psi[v_1, \dots, v_n],

\]

and the procedure is repeated.

\begin{exmp} Consider the formula

  % \[

  %   3 < a ~\wedge~ \forall x\,(\neg (a = 2 \times x)).

  % \]

  $3 < a ~\wedge~ \forall x\,(\neg (a = 2 \times x))$.  The subformula

  $3 < a$ is satisfiable and $a = 4$ is its model. However, it is not

  a model of the formula $\forall x \,(\neg (a = 2 \times x))$, since

  the \QFBV solver called on the formula

  $\neg (\neg (4 = 2 \times x))$ returns $x = 2$ as a model.

  %

  The next step is to decide the satisfiability of the formula

  $3 < a ~\wedge~ \neg (a = 2 \times 2)$. This formula is satisfiable

  and $a = 5$ is its model. Moreover, it is also a model of

  $\forall x \,(\neg (a = 2 \times x))$ as %, because the formula

  $\neg (\neg (5 = 2 \times x))$ is unsatisfiable. Hence, the input

  formula is satisfiable and $a = 5$ is its model.

\end{exmp}

This algorithm is trivially terminating, since there is only a finite

number of distinct models $M$ of $\varphi$. However, in some cases

exponentially many such models have to be ruled out before the solver

is able to find a correct model or decide unsatisfiability of the

whole formula. To overcome this issue, state-of-the-art SMT solvers do

not use just instances of the form $\psi[v_1, \dots, v_n]$ with

concrete values, but employ heuristics such as

E-matching~\cite{DNS05,MB07} or symbolic quantifier

instantiation~\cite{WHM13} to choose instances with ground terms which

can potentially rule out more spurious models and thus significantly

reduce the number of iterations of the algorithm. In practice,

suitable ground terms substituted for quantified variables are

selected only from subterms of the input formula.

\section{Computational complexity}

\section{Computational complexity}

The propositional satisfiability problem is well known from the

The propositional satisfiability problem is well known from the

\checkoddpage

\checkoddpage

\edef\side{\ifoddpage l\else r\fi}

\edef\side{\ifoddpage l\else r\fi}

\makebox[\textwidth][\side]{

\makebox[\textwidth][\side]{

\begin{minipage}[t]{\fullwidth}

\begin{minipage}[bt]{\fullwidth}

  \begin{subfigure}%{0.3\textwidth}

  \begin{subfigure}%{0.3\textwidth}

    \centering

    \centering

    \includegraphics{gfx/comparisonSmtlib.pdf}

    \includegraphics{gfx/comparisonSmtlib.pdf}

    \end{tabularx}

    \end{tabularx}

    \caption{Official results of quantified bit-vector category of

    \caption{Official results of quantified bit-vector category of

      \smt competition 2016 divided into the benchmarks with known

      \smt competition 2016 divided into the benchmarks with known

      status and benchmarks with a previously unknown status.}

      status and benchmarks with a previously unknown status. All

      times are in seconds.}

  \end{minipage}}

  \end{minipage}}

\end{table}

\end{table}

\usepackage{amssymb}

\usepackage{amssymb}

\usepackage{amsthm}

\usepackage[strict]{changepage}

\usepackage[strict]{changepage}

 No newline at end of file

\input{Includes/notation.tex}

\input{Includes/notation.tex}

\input{Includes/packages.tex}

\input{Includes/packages.tex}

\input{Includes/config.tex}

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

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