Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Menu
Open sidebar
Martin Jonáš
DTEDI
Commits
99f3d906
Commit
99f3d906
authored
Sep 04, 2016
by
Martin Jonáš
Browse files
Strejda comments
parent
a53eba55
Changes
4
Hide whitespace changes
Inline
Sidebyside
Chapters/Chapter02.tex
View file @
99f3d906
...
...
@@ 355,13 +355,13 @@ solvers is to convert a \cnf formula to the corresponding \robdd and
check the root of the resulting
\bdd
. If the resulting
\bdd
has the
root 0, the formula is unsatisfiable, and it is satisfiable
otherwise. However, in order to keep the size of the
\bdd
small, it is
necessary to existentially quantify the variables
as soon as
possible
. This technique is known as
\emph
{
early
necessary to existentially quantify the variables
during the
computation
. This technique is known as
\emph
{
early
quantification
}
~
\cite
{
HKB96
}
. A simplified symbolic
\sat
algorithm
can be found for example in the survey of
\sat
solving by Darwiche and
Pipatsriswat~
\cite
{
DP09
}
.
Lookahead based algorithm, in contrast
with
the
\cdcl
, are employing
Lookahead based algorithm, in contrast
to
the
\cdcl
, are employing
expensive heuristics to guide the
\dpll
search to a satisfying
assignment instead of using cheap heuristics and learning from the
conflicts~
\cite
{
HD04
}
. Therefore, while
\cdcl
solvers are efficient on
...
...
@@ 379,9 +379,10 @@ theory~\cite{HKM16}.
\section
{
Satisfiability modulo theories
}
Similarly to
\sat
, the
\emph
{
satisfiability modulo theories problem
}
(
\smt
) is for a given a
\cnf
formula
$
\varphi
$
in a fixed theory
$
\mathcal
{
T
}$
decide whether it is
$
\mathcal
{
T
}$
satisfiable. Depending on the the theory
$
\mathcal
{
T
}$
,
the complexity of the
\smt
problem ranges from polynomial to
(
\smt
) is to decide for a given a
\cnf
formula
$
\varphi
$
in a fixed
theory
$
\mathcal
{
T
}$
whether it is
$
\mathcal
{
T
}$
satisfiable. Depending on the theory
$
\mathcal
{
T
}$
, the
complexity of the
\smt
problem ranges from polynomial to
undecidable. However, as the formula
$
\varphi
$
can contain Boolean
connectives, the
\smt
problem is at least
\NP
hard for nontrivial
theories.
...
...
@@ 441,13 +442,12 @@ infinite have been proposed~\cite{TZ05, RRZ05, JB10}.
\subsection
{
DPLL modulo theories
}
Most of the
\smt
approaches can be classified as
\emph
{
eager
}
or
\emph
{
lazy
}
~
\cite
{
BSST09
}
. The eager
\smt
approach consists in
directly translating the input formula to an equivalent propositional
formula and using an offtheshelf
\sat
solver to decide
satisfiability of this formula. The eager
\smt
approach is implemented
for example in the
\smt
solver
\uclid
, which supports the combination
of the theory of uninterpreted functions and the theory of Presburger
arithmetic with ordering~
\cite
{
LS04
}
.
\emph
{
lazy
}
~
\cite
{
BSST09
}
. In the eager
\smt
approach, input formula
is directly translated to an equivalent propositional formula and an
offtheshelf
\sat
solver is used to decide satisfiability of this
formula. The eager
\smt
approach is implemented for example in the
\smt
solver
\uclid
, which supports the combination of the theory of
uninterpreted functions and linear integer arithmetic~
\cite
{
LS04
}
.
On the other hand, the lazy
\smt
approach uses a
\sat
solver to reason
about the Boolean structure of the formula and a specialized
...
...
@@ 471,8 +471,8 @@ $\mathcal{T}$satisfiable. If the propositional model is not
$
\mathcal
{
T
}$
satisfiable, the corresponding theory lemma
$
\neg
M
^
p
$
is added to the formula and the procedure is repeated. This variant of
the lazy
\smt
approach is called offline, because it uses the
\sat
solver as a black box and employs the
\smt
solver only to
check
satisfiability of a complete Boolean assignment.
solver as a black box and employs the
$
\mathcal
{
T
}$

solver only to
check
satisfiability of a complete Boolean assignment.
\paragraph
{
Online approach
}
In contrast to the offline approach, the
\sat
and
\smt
solvers can
...
...
@@ 504,14 +504,13 @@ transition system~\cite{NOT06}. The \dpllt approach is used in the
majority of modern
\smt
solvers, including solvers
Barcelogic~
\cite
{
Barcelogic
}
, CVC4~
\cite
{
CVC4
}
,
MathSAT~
\cite
{
MathSAT
}
, OpenSMT~
\cite
{
OpenSMT
}
,
Simplify~
\cite
{
Simplify
}
, Yices~
\cite
{
Yices
}
, or
Z3~
\cite
{
Z3
}
.
Simplify~
\cite
{
Simplify
}
, Yices~
\cite
{
Yices
}
, and Z3~
\cite
{
Z3
}
.
\subsection
{
Natural domain
\smt
}
\label
{
ssec:natDomainSat
}
Although the separation of the
Boolean
and theory reasoning in
the
\dpll
approach allows the solver to be modular, it can be also
restricting in some cases. In particular,
\dpllt
based solvers can not
Although the separation of the
propositional
and theory reasoning in
the
\dpll
t
approach allows the solver to be modular, it can be also
restricting in some cases. In particular,
\dpllt

based solvers can not
directly reason about values of firstorder variables, but have to
rely on the
$
\mathcal
{
T
}$
solver guiding the search over Boolean
valuations. While there are some techniques like
\emph
{
splitting on
...
...
@@ 571,7 +570,7 @@ search, but in addition to assigning values of Boolean variables, it
can assign the value of theory variables and it can generate new
literals not occurring in the original formula. De Moura et al. have
implemented the
\mcsat
solver supporting linear real arithmetic and
uninterpreted function, which uses modeldriven FourierMotzkin
uninterpreted function
s
, which uses modeldriven FourierMotzkin
elimination~
\cite
{
Dan63
}
to learn new predicates from arithmetic
conflicts and modeldriven Ackermannization~
\cite
{
MB08, Ack54
}
to
learn new predicates from conflicts involving uninterpreted
...
...
@@ 589,7 +588,7 @@ for unsatisfiable formulas, or to compute \emph{Craig
interpolants
}
~
\cite
{
McM06, UltimateInterpol13, UltimateCores14
}
.
In the context of
\sat
and
\smt
solving, an unsatisfiable core is a
subset of clauses of a unsatisfiable formula that is already
subset of clauses of a
n
unsatisfiable formula that is already
unsatisfiable~
\cite
{
CGS07
}
. Three main approaches are used for the
unsatisfiable core computation in
\smt
~
\cite
{
BSST09
}
. In the first, if
a solver can compute resolution proofs for unsatisfiable formulas, the
...
...
@@ 623,19 +622,20 @@ to bitvectors of length $n$. The only predicate symbols in the \BV
theory are
$
=
$
,
$
\leq
_
u
$
, and
$
\leq
_
s
$
, interpreted as equality,
unsigned inequality of binaryencoded natural numbers, and signed
inequality of integers in
$
2
$
's complement representation,
respectively. Function symbols in the theory are
$
+
,
\times
,
\div
,
\&
,
\mid
,
\oplus
,
\ll
,
\gg
,
\cdot
,
\extract
{
n
}{
p
}$
,
interpreted as addition, multiplication, unsigned division, bitwise
and, bitwise or, bitwise exclusive or, leftshift, rightshift,
concatenation, and extraction of
$
n
$
bits starting from the position
$
p
$
, respectively. For the detailed description of the
\BV
theory
syntax and semantics, see for example Hadarean's PhD
thesis~
\cite
{
Had15
}
. This section focuses on the problem of
satisfiability of the quantifierfree fragment of the
\BV
theory,
denoted
\QFBV
. The the full
\BV
logic is treated in the next section.
respectively. Function symbols in the theory are
$
+
$
,
$
\times
$
,
$
\div
$
,
$
\&
$
,
$
\mid
$
,
$
\oplus
$
,
$
\ll
$
,
$
\gg
$
,
$
\cdot
$
,
$
\extract
{
n
}{
p
}$
, interpreted as addition, multiplication, unsigned
division, bitwise and, bitwise or, bitwise exclusive or,
leftshift, rightshift, concatenation, and extraction of
$
n
$
bits
starting from the position
$
p
$
, respectively. For the detailed
description of the
\BV
theory syntax and semantics, see for example
Hadarean's PhD thesis~
\cite
{
Had15
}
. This section focuses on the
problem of satisfiability of the quantifierfree fragment of the
\BV
theory, denoted
\QFBV
. The the full
\BV
logic is treated in the next
section.
Current stateoftheart
\smt
solvers for the
\QFBV
logic rely on
rewriting techniques
,
used to simplify the formula during the
rewriting techniques used to simplify the formula during the
preprocessing, and eager or lazy translation of the bitvector formula
to the equivalent propositional formula, which is subsequently solved
by a
\sat
solver. The transformation of a bitvector formula to the
...
...
@@ 646,7 +646,7 @@ bitblasting is beneficial when the theory combination is
required. For example, solvers Z3 and Yices apply bitblasting to all
operations except for the equality, which is handled by a specialized
solver, and dynamically add axioms of the array
theory~
\cite
{
Z3,Yices
}
, and
Boolector applies bitblasting to the
theory~
\cite
{
Z3,Yices
}
.
Boolector applies bitblasting to the
bitvector operations and lazily instantiates definitions of macros
and array axioms~
\cite
{
Boolector
}
. Furthermore, CVC4 uses lazy and
layered solver, which tries to decide the satisfiability using
...
...
@@ 660,8 +660,9 @@ generated by the subsolvers are added to the formula and a lazy
Although bitblasting is highly efficient for most of practical
problems, it can exhaust memory of the solver if the input formula
contains complex arithmetic or variables with large bitwidth. Several
techniques that avoid the bitblasting have been proposed to alleviate
this problem.
techniques that avoid the bitblasting and work directly on the level
of individual bitvectors (
\emph
{
wordlevel
}
) have been proposed to
alleviate this problem.
Some useful fragments of the bitvector theory can be solved by
specialized algorithms for deciding satisfiability. For example,
...
...
@@ 682,17 +683,17 @@ heuristics for generalizing explanations of bitvector conflicts. For
example, the solver
\mcsat
can perform the partial assignment
$
\extract
{
2
}{
0
}
(
x
)
\mapsto
10
$
, denoting that the two least
significant bits of
$
x
$
are
$
10
$
. To be able to efficiently use such
partial assignments, the solver
\mcbv
maintains two
overapproximations
of the set of models that are compatible with the
current partial
assignment  using
\emph
{
bitpatterns
}
and
\emph
{
arithmetic
intervals
}
. Bitpatterns are sequences of
$
0
$
,
$
1
$
and
$
u
$
, which
represents undefined bit,
and
constrain the values of
particular bits
in the assignment. On the other hand, arithmetic
intervals are pairs
of bitvector values representing lower and upper
bounds and constrain
integral values of bitvectors. Both bitpatterns
and arithmetic
intervals can be ordered to form a lattice in which the
solver
performs a search for a more general explanation if a conflict
is
detected.
partial assignments, the solver
\mcbv
maintains two
overapproximations
of the set of models that are compatible with the
current partial
assignment  using
\emph
{
bitpatterns
}
and
\emph
{
arithmetic
intervals
}
. Bitpatterns are sequences of
$
0
$
,
$
1
$
and
$
u
$
(
represents undefined bit
)
,
which
constrain the values of
particular bits
in the assignment. On the other hand, arithmetic
intervals are pairs
of bitvector values representing lower and upper
bounds and constrain
integral values of bitvectors. Both bitpatterns
and arithmetic
intervals can be ordered to form a lattice in which the
solver
performs a search for a more general explanation if a conflict
is
detected.
Another wordlevel approach for the full bitvector theory is
\emph
{
stochastic local search
}
(
\sls
), proposed for solving
...
...
@@ 709,10 +710,10 @@ necessary to satisfy randomly selected subformulas. The \sls based
solver has been shown to be able to decide several formulas not
decided by bitblasting solvers. To combine benefit of bitblasting
and
\sls
approaches, the latest version of Boolector, which have won
the 2016 SMT competition in category of quantifierfree
bitvectors,
uses a portfolio approach, which consists in first
running a
\sls
based solver for a short period of time and then
running a
bitblasting solver if the
\sls
solver fails to solve the
the 2016 SMT competition in
the
category of quantifierfree
bitvectors,
uses a portfolio approach, which consists in first
running a
\sls
based solver for a short period of time and then
running a
bitblasting solver if the
\sls
solver fails to solve the
formula~
\cite
{
BoolectorComp
}
.
\subsection
{
Preprocessing
}
...
...
@@ 741,9 +742,9 @@ relevant for software verification.
A variable
$
x
$
in a formula is called
\emph
{
unconstrained
}
if it
occurs only once in the formula. Brummayer~
\cite
{
Brum10
}
and
Bruttomesso~
\cite
{
Bru08
}
have independently observed that if an
unconstrained variable occurs as an argument to a function symbol
,
which
can be
\emph
{
inverted
}
with respect to this argument, replacing
this
function with a fresh variable yields an equisatisfiable
unconstrained variable occurs as an argument to a function symbol
that
can be
\emph
{
inverted
}
with respect to this argument, replacing
this
function with a fresh variable yields an equisatisfiable
formula. Moreover, unconstrained variables often occur in the
industrial benchmarks and especially in benchmarks produced during a
verification of programs in a single static assignment form, such as
...
...
@@ 766,22 +767,22 @@ in bitvectors precisely if $k$ is odd.
Although the bitvector theory admits quantifier elimination by
expanding all quantifiers with all possible bitvector values of the
corresponding bitwidth, this is rarely practical approach. Instead,
the formula is usually converted to a equisatisfiable formula by
corresponding bitwidth, this is rarely
a
practical approach. Instead,
the formula is usually converted to a
n
equisatisfiable formula by
Skolemization and then instances of the universally quantified
formulas are lazily added to the formula until a model is found or the
formula is found to be unsatisfiable by a
\QFBV
solver. There are
multiple ways to choose quantifier instances that are sufficient to
decide the satisfiability of the formula. For the bitvector theory,
the most widely used approach is the
\emph
{
modelbased quantifier
instantiation
}
approach
~
\cite
{
GM09
}
,
suppor
ted
by
Z3, CVC4, and
Yices,
combined by heuristics as Ematching or symbolic
quantifier
instantiation~
\cite
{
WHD13,Dut15
}
. Additionally, for
dealing with
quantifiers, CVC4 supports solving quantified formulas by
instantiation
}
~
\cite
{
GM09
}
,
implemen
ted
in
Z3, CVC4, and
Yices,
combined by heuristics as
\emph
{
Ematching
}
or
\emph
{
symbolic
quantifier
instantiation
}
~
\cite
{
WHD13,Dut15
}
. Additionally, for
dealing with
quantifiers, CVC4 supports solving quantified formulas by
\emph
{
counterexample guided quantifier instantiation
}
~
\cite
{
RDKT15
}
.
% and \emph{finite model finding}~\cite{RTG13}.
However, w
e describe only the modelbased quantifier instantiation in
detail,
as the counterexample guided quantifier considers all
W
e describe only the modelbased quantifier instantiation in
detail,
as the counterexample guided quantifier
instantiation
considers all
functions as uninterpreted during the conflict search, and therefore
its performance on bitvector formulas is limited.
...
...
@@ 807,9 +808,9 @@ 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 quantifierfree part, i.e.~the formula
$
\varphi
$
is modified to
$
M
$
as a model
as
the
formula
$
\varphi
$
, the instance
$
\psi
[
v
_
1
,
\dots
, v
_
n
]
$
of the quantified formula is added to the
quantifierfree part, i.e.~the formula
$
\varphi
$
is modified to
\[
\varphi
' ~
\equiv
~
\varphi
\wedge
\psi
[
v
_
1
,
\dots
, v
_
n
]
,
\]
...
...
@@ 877,7 +878,7 @@ quantifierfree fragments are denoted by the prefix QF\_, the
combination with the theory of uninterpreted functions is denoted by
the prefix UF, and the problems with unary and binary encoded
bitwidths 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 bitwidths. The completeness
results for these classes are summarized in table
\ref
{
tbl:complexity
}
, and briefly explained in the rest of this section.
...
...
@@ 914,8 +915,9 @@ polynomial time reduction from QF\_BV1 to \sat, showing that QF\_BV1
is in NP. A similar reduction from BV1 to
\qbf
can show that BV is in
\PSPACE
. For lower bounds,
\NP
hardness of QF
\_
BV1 follows from a
simple reduction from
\sat
, by encoding each propositional variable as
a bitvector of bitwidth 1, and similarly, BV1 can be shown to be
\PSPACE
hard.
a bitvector of bitwidth 1. Similarly, BV1 can be shown to be
\PSPACE
hard by considering every bitvector as a quantified variable
of bitwidth 1.
In quantifierfree formulas, uninterpreted functions can be eliminated
by the Ackermann expansion with only quadratic increase in the size of
...
...
@@ 927,8 +929,8 @@ fragment of the firstorder logic, which is well known to be
\NEXPTIME
complete~
\cite
{
WHD13
}
. The class of effectively
\marginpar
{
The class of effectively propositional formulas is also
known as the BernaysSchönfinkel class.
}
propositional formulas
consists only of formulas in form
$
\exists
^
*
\forall
^
*
\varphi
$
,
where
$
\varphi
$
does not contain any quantifiers or function symbols.
consists only of formulas in
the
form
$
\exists
^
*
\forall
^
*
\varphi
$
,
where
$
\varphi
$
does not contain any quantifiers or function symbols.
\paragraph
{
Binary encoded bitwidths
}
For formulas with binary encoded bitwidths, the bitblasting may
...
...
@@ 950,7 +952,7 @@ Similarly to the case with the unary encoding, the complexity of the
quantifierfree fragment stays the same when the uninterpreted
functions are added  QF
\_
UFBV2 can be shown to be in
\NEXPTIME
by
the Ackermann reduction and
\NEXPTIME
hard by the simple reduction
from QF
\_
UF
BV2. The complexity of the problem after adding quantifiers
from QF
\_
BV2. The complexity of the problem after adding quantifiers
and uninterpreted functions was investigated by Kovásznai et
al.~
\cite
{
KFB12
}
. Reencoding of all bitwidths to unary shows that
UFBV2 is in
\NNEXPTIME
. For the lower bound, Kovásznai et al. present
...
...
Chapters/Chapter03.tex
View file @
99f3d906
...
...
@@ 12,13 +12,13 @@ variable ordering based on dependencies in the input formula, which
can further reduce the size of
\bdds
, and approximations, which
partially alleviate infeasibility of representing multiplication with
a
\bdd
. This section summarizes all three of these components, which
were in detail described in our paper published at the SAT
conference
2016
~
\cite
{
JS16
}
.
were in detail described in our paper published at the SAT
2016
conference
~
\cite
{
JS16
}
.
The benefit of a
\bdd
based solver over the quantifier
instantiationbased one is the ability of representing all models of a
universally quantified formula even in cases in which finding a
suitable set quantifier instantiations would be infeasible. The
suitable set
of
quantifier instantiations would be infeasible. The
following formula, in which all variables have bitwith 32 bits, shows
this difference:
\[
...
...
@@ 28,14 +28,14 @@ this difference:
The
\bdd
based solver can quickly compute the
\bdd
for the quantified
subformula
$
\forall
(
x :
[
32
])
\,
(
a
\not
=
16
\cdot
x
)
$
, which shows
that the last 4 bits of the variable
$
a
$
ha
ve
to be
$
0
$
, i.e. the
value of
$
a
$
is divisible by
$
16
$
. After conjoining
this
\bdd
to the
\bdd
for
$
a
=
16
\cdot
b
\,
+
\,
16
\cdot
c
$
, the formula
is decided
unsatisfiable, as the resulting
\bdd
has root
$
0
$
. On the
other hand,
if one considers only quantifier instantiations by the
subterm of the
input formula, exponentially many quantifier instances
have to be
added to the formula to show its unsatisfiability, as there
is no
subterm of
$
\varphi
$
that can be instantiated as
$
x
$
to yield an
that
at least one of
the last 4 bits of the variable
$
a
$
ha
s
to be
$
0
$
, i.e. the
value of
$
a
$
is
not
divisible by
$
16
$
. After conjoining
this
\bdd
to the
\bdd
for
$
a
=
16
\cdot
b
\,
+
\,
16
\cdot
c
$
, the formula
is decided
unsatisfiable, as the resulting
\bdd
has root
$
0
$
. On the
other hand,
if one considers only quantifier instantiations by the
subterm of the
input formula, exponentially many quantifier instances
have to be
added to the formula to show its unsatisfiability, as there
is no
subterm of
$
\varphi
$
that can be instantiated as
$
x
$
to yield an
unsatisfiable quantifierfree formula.
\subsection
{
Simplifications
}
...
...
@@ 88,10 +88,10 @@ where $t$ is an arbitrary term that does not contain $x$.
\subsection
{
Variable ordering
}
Ordering of
\bdd
variables is crucial
to
efficiency. The size of a
Ordering of
\bdd
variables is crucial
for
efficiency. The size of a
\bdd
can differ exponentially when choosing a different
ordering. Therefore, besides well known methods dynamic variable
reordering during the computation
~
\cite
{
Rud93
}
, Q3B precomputes
ordering. Therefore, besides well known methods
of
dynamic variable
reordering during the computation, Q3B precomputes
initial variable ordering, which is based on the dependencies among
the variables in the formula.
...
...
@@ 103,13 +103,13 @@ which we denote $\leq_1, \leq_2, \leq_3$.
with the same significance are ordered by the order of the first
occurrences of the corresponding bitvector variables in the
formula. In this ordering, bit variables of the same significance
are
near
each other.
are
close to
each other.
\item
In
$
\leq
_
2
$
, bit variables are ordered by the order of the first
occurrences of the corresponding bitvector variables in the formula
and bit variables corresponding to the same bitvector variable are
ordered according to their significance (from the least to the most
significant). In this ordering, bit variables corresponding to the
same bitvector variable are
near
each other
same bitvector variable are
close to
each other
.
\item
In
$
\leq
_
3
$
, we first identify syntactically dependent
variables. Two variables are
\emph
{
syntactically dependent
}
if they
occur in the same atomic subformula. Then the set of variables is
...
...
@@ 117,10 +117,11 @@ which we denote $\leq_1, \leq_2, \leq_3$.
the syntactic dependence relation and each of these classes is
ordered according to
$
\leq
_
2
$
. Therefore, in this ordering, only
potentially dependent bit variables of the same significance are
near
each other.
close to
each other.
\end{itemize}
From these three orderings,
$
\leq
_
3
$
performs best on the set of our
benchmarks even if the dynamic variable reordering by sifting is used.
benchmarks even if the dynamic variable reordering by
\emph
{
sifting
}
~
\cite
{
Rud93
}
is used.
\subsection
{
Approximations
}
The size of the
\bdd
for multiplication is exponential regardless the
...
...
@@ 128,7 +129,7 @@ variable ordering~\cite{Bry91}. Therefore, to be able to decide
formulas with multiplication or complex arithmetic, Q3B uses
approximations of the input formula, which allow deciding a
satisfiability of the input formula by solving a simpler formula
instead. In the context of
\smt
solving, underapproximation of a
instead. In the context of
\smt
solving,
an
underapproximation of a
formula is a formula that logically entails the input formula and an
overapproximation of an input formula is a formula logically entailed
by the input formula. It can be easily seen that satisfiability of an
...
...
@@ 142,16 +143,16 @@ underapproximated by representing each bitvector variable by the
smaller number of bit variables than its original bitwidth. The
number of bits by which the bitvariable is represented is called the
\emph
{
effective bitwidth
}
. For reducing the effective bitwidth,
\uclid
offers multiple ways representa
tion the
variable by a smaller
number of bits

zero extension, oneextension, and
signextension. In all three
of these cases
, the effective bitwidth
is used
to represent the least significant bits of the bitvector
variable and
all other bits are set to 0, 1, or the value of the most
significant
effectively represented bit, respectively. To these
extensions, we
have proposed their right variants, which use
effectivebit width for
represent
ing
the most significant bits. Figure
xxx
illustrates left and right variants of zeroextension and
signextension
s
.
\uclid
offers multiple ways
to
represent
a variable by a smaller
number of bits
:
\emph
{
zero extension
}
,
\emph
{
oneextension
}
, and
\emph
{
signextension
}
. In all three, the effective bitwidth
is used
to represent the least significant bits of the bitvector
variable and
all other bits are set to 0, 1, or the value of the most
significant
effectively represented bit, respectively. To these
extensions, we
have proposed their right variants, which use
effectivebit width to
represent the most significant bits. Figure
\ref
{
fig:extensions
}
illustrates left and right variants of zeroextension and
signextension.
\begin{figure}
[tb]
\begin{tabularx}
{
\textwidth
}{
c X c
}
...
...
@@ 191,7 +192,7 @@ signextensions.
\label
{
fig:extensions
}
\end{figure}
In contrast to
\uclid
, we can use the same approach to perform
ing
In contrast to
\uclid
, we can use the same approach to perform
overapproximations, because we work with the quantified formulas. For
formulas in the negation normal form, underapproximations can be
achieved by reducing effective bitwidths of existentially quantified
...
...
@@ 202,22 +203,23 @@ In Q3B, approximations are used in a portfolio style. The solver
without approximations is run in parallel with the solver which
employs underapproximations and the solver which employs
overapproximations. Our experimental evaluation has shown that this
set up can help decide more formulas, especially formulas
containing
multiplication.
set up can help
to
decide more formulas, especially formulas
containing
multiplication.
\subsection
{
Experimental evaluation
}
Our experimental evaluation has shown that a
\bdd
based
\smt
solver
can decide more formulas of the set of quantified bitvector formulas
from the SMTLIB benchmark library~
\cite
{
BST10
}
. An addition to this
set of benchmarks, we have gathered quantified formulas produced by
the semisymbolic model checker
\SymDivine
~
\cite
{
BHB14
}
, which uses
quantified formulas to decide the equality of two symbolic states. On
this set of benchmarks, our solver Q3B also has better performance
than
\smt
solvers based on the quantifier instantiation and
bitblasting. Table
\ref
{
tbl:results
}
shows the numbers of formulas
solved by each solver and figure
\ref
{
fig:quantilePlots
}
presents a
quantile plot of CPU times needed to solve these formulas.
can decide more formulas than CVC4 and Z3, when the set of quantified
bitvector formulas in the SMTLIB benchmark library~
\cite
{
BST10
}
is
considered. Additionally, we have gathered quantified formulas
produced by the semisymbolic model checker
\SymDivine
~
\cite
{
BHB14
}
,
which uses quantified formulas to decide the equality of two symbolic
states. On this set of benchmarks, our solver Q3B also has better
performance than
\smt
solvers based on the quantifier instantiation
and bitblasting. Table
\ref
{
tbl:results
}
shows the numbers of
formulas solved by each solver and figure
\ref
{
fig:quantilePlots
}
presents the quantile plot of CPU times needed to solve these
formulas.
\begin{table}
\checkoddpage
...
...
@@ 297,20 +299,20 @@ quantile plot of CPU times needed to solve these formulas.
Recently, this results was confirmed by the
\smt
competition 2016 
our solver is the winner of the quantifiedbit vectors category. Table
\ref
{
tbl:smtcomp
}
shows official results for this category. The
benchmarks
are divided into two groups, with
\emph
{
known
}
and
\emph
{
unknown
}
status. A benchmark has a known status if at least two
solvers in the
previous year of the competition agreed whether the
benchmark is
satisfiable or unsatisfiable. The results show that Q3B
can solve as
many known benchmarks as other solvers, but solves
them in the
shortest time. Moreover, Q3B can solve more benchmarks
with unknown
status than any of the other solvers.
\ref
{
tbl:smtcomp
}
shows official results for this category. The
benchmarks
are divided into two groups, with
\emph
{
known
}
and
\emph
{
unknown
}
status. A benchmark has a known status if at least two
solvers in the
previous year of the competition agreed whether the
benchmark is
satisfiable or unsatisfiable. The results show that Q3B
can solve as
many known benchmarks as
the
other solvers, but solves
them in the
shortest time. Moreover, Q3B can solve more benchmarks
with unknown
status than any of the other solvers.
\section
{
Other areas of research
}
Outside the field of
\smt
solving, my research also consists in
software verification. In this field, I have coauthored the following
paper on the tool Symbiotic, which combines instrumentation, slicing
and symbolic execution to allow verification of a realworld
and
,
symbolic execution to allow verification of a realworld
code~
\cite
{
CJSSV16
}
.
...
...
Chapters/Chapter04.tex
View file @
99f3d906
...
...
@@ 5,13 +5,13 @@
\section
{
Objectives and Expected Results
}
\subsection
{
Symbolic solver for quantified bitvectors
}
I
will
continue developing the implemented symbolic
\smt
solver
Q3B,
which is aimed at solving quantified bitvector formulas. In
I
plan to
continue developing the implemented symbolic
\smt
solver
Q3B,
which is aimed at solving quantified bitvector 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 extraction of an
unsatisfiable core from the intermediate
\bdds
that were produced
during the computation
of the solver
.
during the computation.
Additionally, currently implemented approximations are very simple and
could benefit from better refinement in the case that the current
...
...
@@ 21,26 +21,27 @@ Moreover, I want to implement other variants of decision diagrams such
as zerosuppressed decision diagrams introduced by
Minato~
\cite
{
Min93
}
, binary moment diagrams introduced by Bryant and
Chen~
\cite
{
BC95
}
, 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
et al.~
\cite
{
BFGHMPS
}
. I plan to
experimentally evaluate their effect
on the
performance of the symbolic
\smt
solver for the quantified
bitvectors.
\subsection
{
Hybrid approach to quantified bitvectors
}
Although results of the symbolic
\smt
solver for quantified
bitvectors look promising, standard
\smt
solvers still perform
better
on queries containing multiplication and complex
bitvectors 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 bitvector formulas that combines strengths of
both of these approaches. For example, parts of the quantified
formula that do not contain multiplication can be converted to the
\bdd
, which can be used to guide the model search in the modelbased
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
overapproximations by bitpatterns and arithmetic
intervals. Moreover, a tighter cooperation is possible  if a
\mcsat
solver decides a value, it can be used to partially instantiate a
quantified part of the formula, for which the
\bdd
will be computed.
both of these approaches. For example, parts of the quantified formula
that do not contain multiplication can be converted to the
\bdd
, which
can be used to guide the model search in the modelbased quantifier
instantiation of the other parts of the formula. 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 overapproximations by bitpatterns and arithmetic
intervals. Moreover, a tighter cooperation is possible  if a value
of a variable is decided by during the
\mcbv
computation, it 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, an implementation of a solver using the
hybrid approach and its evaluation on the representative set of
...
...
@@ 53,9 +54,9 @@ 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 formulated a hypothesis that
describes
the necessary
condition for the quantified variable to be
describes
a sufficient
condition for the quantified variable to be
considered as unconstrained. Based on this hypothesis and a partial
proof of its validity, we have implemented a
n
proofofconcept
proof of its validity, we have implemented a proofofconcept
simplification procedure that can simplify quantified formulas that
contain unconstrained variables. Although the initial experimental
results, conducted on the formulas from the semisymbolic model
...
...
@@ 64,23 +65,23 @@ 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 unconstrained variable
$
x
$
has
bitwidth
$
n
$
, the
term
$
k
\times
x
$
can be rewritten to
$
extract
_
0
^{
n

i
}
(
x
)
\cdot
0
^
i
$
. This approach can be also extended to
the multiplication of two
variables from which one is unconstrained. I
plan to investigate
further extensions to the terms containing
division and remainder
operations and to publish a paper concerning
propagation of
unconstrained variables in quantified formulas and
extensions of
unconstrained variable simplification to multiplication
and
division. I will also experimentally evaluate the effect of such
$
k
\times
x
$
in which the variable
$
x
$
is unconstrained, this term can
be replaced by a simpler term regargless the parity of the value
$
k
$
. In
particular, if
$
i
$
is the largest number for which
$
2
^
i
$
divides the
constant
$
k
$
and the unconstrained variable
$
x
$
has
bitwidth
$
n
$
, the
term
$
k
\times
x
$
can be rewritten to
$
extract
_
0
^{
n

i
}
(
x
)
\cdot
0
^
i
$
.
.
This approach can be also extended to
the multiplication of two
variables from which one is unconstrained. I
plan to investigate
further extensions to the terms containing
division and remainder
operations and to publish a paper concerning
propagation of
unconstrained variables in quantified formulas and
extensions of
unconstrained variable simplification to multiplication
and
division. I will also experimentally evaluate the effect of such
simplifications on our solver Q3B and on stateof the art solvers such
as Boolector, CVC4, and Z3.
\subsection
{
Complexity of BV2
}
As was explained in
s
ection
\ref
{
sec:complexity
}
, the precise
As was explained in
S
ection
\ref
{
sec:complexity
}
, the precise
complexity of quantified bitvector formulas with binaryencoded
bitwidths and without uninterpreted functions is not known. It is
known to be in
\EXPSPACE
and to be
\NEXPTIME
hard. However, a class
...
...
@@ 93,13 +94,7 @@ BV2 is complete for the class of problems solvable by the
and
\emph
{
polynomial number of alternations
}
with respect to logspace
reduction. This class is usually denoted as
\AEXPTIMEp
and is known to
be in between
\NEXPTIME
and
\EXPSPACE
~
\cite
{
HKVV15, Luc16
}
. However,
whether any of the 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.
whether any of the inclusions is proper is not known.
\section
{
Progression Schedule
}
The plan of my future study and research activities is following:
...
...
classicthesisconfig.tex
View file @
99f3d906
...
...
@@ 98,7 +98,7 @@
%style=authoryearcomp, % Author 1999, 2010
%bibstyle=authoryear,dashed=false, % dashed: substitute rep. author with 
sorting=nyt,
% name, year, title
maxbibnames=
3
,
% default: 3, et al.
maxbibnames=
10
,
% default: 3, et al.
%backref=true,%
natbib=true
% natbib compatibility mode (\citep and \citet still work)
}{
biblatex
}
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment