Spell check

The \emph{theory of fixed sized bit-vectors (\BV)} is a multi-sorted

The \emph{theory of fixed sized bit-vectors (\BV)} is a multi-sorted

first-order theory with infinitely many sorts $\sort{n}$ corresponding

first-order theory with infinitely many sorts $\sort{n}$ corresponding

to bit-vectors of length $n$. The only predicate symbols in the \BV

to bit-vectors of length $n$. The only predicate symbols in the \BV

theory are $=$, $\leq_u$, and $\leq_s$, interpretead as equality,

theory are $=$, $\leq_u$, and $\leq_s$, interpreted as equality,

unsigned inequality of binary-encoded natural numbers, and signed

unsigned inequality of binary-encoded natural numbers, and signed

inequality of integers in $2$'s complement representation,

inequality of integers in $2$'s complement representation,

respectively. Function symbols in the theory are

respectively. Function symbols in the theory are

equivalent propositional formula is traditionally called

equivalent propositional formula is traditionally called

\emph{bit-blasting}~\cite{Kro08}.  \marginpar{TODO: Nepřidat odstavec

\emph{bit-blasting}~\cite{Kro08}.  \marginpar{TODO: Nepřidat odstavec

  o propagating-complete \cnf encodings?} More lazy approach to the

  o propagating-complete \cnf encodings?} More lazy approach to the

bit-blasting is benefitial when the theory combination is

bit-blasting is beneficial when the theory combination is

required. For example, solvers Z3 and Yices apply bit-blasting to all

required. For example, solvers Z3 and Yices apply bit-blasting to all

operations except for the equality, which is handled by a specialized

operations except for the equality, which is handled by a specialized

solver, and dynamically add axioms of the array

solver, and dynamically add axioms of the array

generated by the sub-solvers are added to the formula and a lazy

generated by the sub-solvers are added to the formula and a lazy

\dpllt bit-blasting solver is employed~\cite{HBJBT14}.

\dpllt bit-blasting solver is employed~\cite{HBJBT14}.

\subsection{Word-level techinques}

\subsection{Word-level techniques}

Although bit-blasting is highly efficient for most of practical

Although bit-blasting is highly efficient for most of practical

problems, it can exhaust memory of the solver if the input formula

problems, it can exhaust memory of the solver if the input formula

contains complex arithmetic or variables with large bit-width. Several

contains complex arithmetic or variables with large bit-width. Several

example, the solver \mcsat can perform the partial assignment

example, the solver \mcsat can perform the partial assignment

$\extract{2}{0}(x) \mapsto 10$, denoting that the two least

$\extract{2}{0}(x) \mapsto 10$, denoting that the two least

significant bits of $x$ are $10$. To be able to efficiently use such

significant bits of $x$ are $10$. To be able to efficiently use such

partial assignments, the solver \mcbv mantains two over-approximations

partial assignments, the solver \mcbv maintains two over-approximations

of the set of models that are compatible with the current partial

of the set of models that are compatible with the current partial

assignment -- using \emph{bit-patterns} and \emph{arithmetic

assignment -- using \emph{bit-patterns} and \emph{arithmetic

  intervals}. Bit-patterns are sequences of $0$, $1$ and $u$, which

  intervals}. Bit-patterns are sequences of $0$, $1$ and $u$, which

Another word-level approach for the full bit-vector theory is

Another word-level approach for the full bit-vector theory is

\emph{stochastic local search} (\sls), proposed for solving

\emph{stochastic local search} (\sls), proposed for solving

bit-vectors by Frohlich et al.~\cite{FBWH15} and subsequently improved

bit-vectors by Fröhlich et al.~\cite{FBWH15} and subsequently improved

by Niemetz et al.~\cite{NPBF15,NPB16}. In the \sls approach, the

by Niemetz et al.~\cite{NPBF15,NPB16}. In the \sls approach, the

solver randomly chooses initial values of bit-vector variables and

solver randomly chooses initial values of bit-vector variables and

tries to find a satisfying assignment by performing random bit flips,

tries to find a satisfying assignment by performing random bit flips,

solver has been shown to be able to decide several formulas not

solver has been shown to be able to decide several formulas not

decided by bit-blasting solvers. To combine benefit of bit-blasting

decided by bit-blasting solvers. To combine benefit of bit-blasting

and \sls approaches, the latest version of Boolector, which have won

and \sls approaches, the latest version of Boolector, which have won

the 2016 SMT competition in category of unquantified bit-vectors, uses

the 2016 SMT competition in category of quantifier-free bit-vectors,

a protfolio approach, which consists in first running a \sls based

uses a portfolio approach, which consists in first running a \sls

solver for a short period of time and then running a bit-blasting

based solver for a short period of time and then running a

solver if the \sls solver fails to solve the

bit-blasting solver if the \sls solver fails to solve the

formula~\cite{BoolectorComp}.

formula~\cite{BoolectorComp}.

\subsection{Preprocessing}

\subsection{Preprocessing}

uninterpreted functions, allowing quantifiers, and in encoding of the

uninterpreted functions, allowing quantifiers, and in encoding of the

bit-widths (unary vs. binary). In the following, we follow the

bit-widths (unary vs. binary). In the following, we follow the

notation of Kováznai et al~\cite{KFB16} -- decision problems for

notation of Kováznai et al~\cite{KFB16} -- decision problems for

quantifer-free fragments are dentoted by the prefix QF\_, the

quantifier-free fragments are denoted by the prefix QF\_, the

combination with the theory of uninterpreted functions is denoted by

combination with the theory of uninterpreted functions is denoted by

the prefix UF, and the problems with unary and binary encoded

the prefix UF, and the problems with unary and binary encoded

bit-widths are denoted by suffixes 1 and 2, respectively. For example,

bit-widths are denoted by suffixes 1 and 2, respectively. For example,

QF\_UFBV2 is the decision problem for quantifier free formulas with

QF\_UFBV2 is the decision problem for quantifier free formulas with

uninterpreted functions and binary encoded bit-withs. The completeness

uninterpreted functions and binary encoded bit-widths. The completeness

results for these classes are summarized in table

results for these classes are summarized in table

\ref{tbl:complexity}, and briefly explained in the rest of this section.

\ref{tbl:complexity}, and briefly explained in the rest of this section.

exponential with respect to the size of the formula. Therefore,

exponential with respect to the size of the formula. Therefore,

bit-blasting shows that QF\_BV2 is in \NEXPTIME. On the other hand,

bit-blasting shows that QF\_BV2 is in \NEXPTIME. On the other hand,

Kovásznai et al. have presented a polynomial time reduction of

Kovásznai et al. have presented a polynomial time reduction of

satisfiability of \emph{dependent quantified boolean formulas} (\dqbf)

satisfiability of \emph{dependent quantified Boolean formulas} (\dqbf)

to QF\_BV2. Since \dqbf is well known to be \NEXPTIME-complete, this

to QF\_BV2. Since \dqbf is well known to be \NEXPTIME-complete, this

reduction shows \NEXPTIME-hardness of QF\_BV2~\cite{KFB12}. In

reduction shows \NEXPTIME-hardness of QF\_BV2~\cite{KFB12}. In

contrast, the precise complexity after adding quantifiers is not

contrast, the precise complexity after adding quantifiers is not

formulas from QF\_BV2, it is also \NEXPTIME-hard.

formulas from QF\_BV2, it is also \NEXPTIME-hard.

Similarly to the case with the unary encoding, the complexity of the

Similarly to the case with the unary encoding, the complexity of the

quantifier-fre fragment stays the same when the uninterpreted

quantifier-free fragment stays the same when the uninterpreted

functions are added -- QF\_UFBV2 can be shown to be in \NEXPTIME by

functions are added -- QF\_UFBV2 can be shown to be in \NEXPTIME by

the Ackermann reduction and \NEXPTIME-hard by the simple reduction

the Ackermann reduction and \NEXPTIME-hard by the simple reduction

from QF\_UFBV2. The complexity of the problem after adding quantifiers

from QF\_UFBV2. The complexity of the problem after adding quantifiers