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
beff0d37
Commit
beff0d37
authored
Oct 10, 2016
by
Martin Jonáš
Browse files
Minor changes
parent
21401a14
Changes
1
Hide whitespace changes
Inline
Side-by-side
Obhajoba/slides.tex
View file @
beff0d37
...
...
@@ -119,9 +119,14 @@
\newcommand
{
\QFBV
}{
\ensuremath
{
\mathcal
{
QFBV
}}}
\let\otp\titlepage
\renewcommand
{
\titlepage
}{
\otp\addtocounter
{
framenumber
}{
-1
}}
\begin{document}
\frame
{
\titlepage
}
\begin{frame}
[plain]
\titlepage
\end{frame}
\section
{
Propositional Satisfiability
}
\begin{frame}
...
...
@@ -188,17 +193,19 @@
\bigskip
Traditionally solved by
the
\alert
{
CDCL modulo theories
}
-- combination of
Traditionally solved by
\alert
{
CDCL modulo theories
}
-- combination of
CDCL and a specialized theory solver.
\pause
\begin{example}
Let
$
\varphi
=
(
x
+
y
=
3
)
\wedge
(
x >
1
)
\wedge
(
y
=
2
\vee
y
=
1
)
$
.
\begin{enumerate}
[<+->]
\item
Propositional model
$
\{
x
+
y
=
3
,~x >
1
,~y
=
2
\}
$
.
\item
Propositional model
$
\{
x
+
y
=
3
,~x >
1
,~y
=
2
,~
\neg
(
y
=
1
)
\}
$
.
\item
This model
\textbf
{
is not
}
consistent with the theory of integers.
\item
Conjoin
$
\neg
(
x
+
y
=
3
)
\vee
\neg
(
x >
1
)
\vee
\neg
(
y
=
2
)
$
to
$
\varphi
$
.
\item
Propositional model
$
\{
x
+
y
=
3
,~x >
1
,~y
=
1
\}
$
.
\item
Conjoin
$
\neg
(
x
+
y
=
3
)
\vee
\neg
(
x >
1
)
\vee
\neg
(
y
=
2
)
\vee
(
y
=
1
)
$
to
$
\varphi
$
.
\item
Propositional model
$
\{
x
+
y
=
3
,~x >
1
,~
\neg
(
y
=
2
)
,~
y
=
1
\}
$
.
\item
This model
\textbf
{
is
}
consistent with the theory of integers.
\item
$
\varphi
$
is satisfiable.
\end{enumerate}
...
...
@@ -260,15 +267,18 @@
Quantifier bit-vector formulas traditionally solved by
\alert
{
quantifier instantiation
}
.
\pause
\begin{example}
Let
$
\varphi
=
3
< a
~
\wedge
~
\forall
x
\,
(
a
\not
=
2
\
times
x
)
$
Let
$
\varphi
=
a >
3
~
\wedge
~
\forall
x
\,
(
a
\not
=
2
\
cdot
x
)
$
\pause
\begin{itemize}
[<+->]
\item
$
3
< a
$
is satisfiable with model
$
a
=
4
$
.
\item
$
a
=
4
$
not a model of
$
\forall
x
\,
(
a
\not
=
2
\
times
x
)
$
(corresponding counter-example is
$
x
=
2
$
)
.
\item
$
a >
3
$
is satisfiable with model
$
a
=
4
$
.
\item
$
a
=
4
$
not a model of
$
\forall
x
\,
(
a
\not
=
2
\
cdot
x
)
$
-- consider
$
x
=
2
$
.
\item
Add instance of the quantifier for
$
x
=
2
$
.
\item
$
3
< a
~
\wedge
~
(
a
\not
=
2
\
times
2
)
$
is satisfiable with model
$
a
=
5
$
.
\item
$
a
=
5
$
is a model of
$
\forall
x
\,
(
a
\not
=
2
\
times
x
)
$
.
\item
$
a >
3
~
\wedge
~
(
a
\not
=
2
\
cdot
2
)
$
is satisfiable with model
$
a
=
5
$
.
\item
$
a
=
5
$
is a model of
$
\forall
x
\,
(
a
\not
=
2
\
cdot
x
)
$
.
\item
$
\varphi
$
is satisfiable
\end{itemize}
\end{example}
...
...
@@ -319,13 +329,18 @@
Efficient algorithm are known for operations with BDDs (conjunction,
disjunction, quantifiers).
\
small
skip
\
big
skip
Quantification usually reduces the size of the BDD -- useful for
quantified bit-vectors.
\bigskip
Representation by (reduced and ordered) BDDs is canonical -- formula
is unsatisfiable iff the BDD has root false.
\end{frame}
\begin{frame}
We have implemented the solver Q3B, which
\begin{itemize}
\item
simplifies the formula,
...
...
@@ -334,7 +349,10 @@
too expensive.
\end{itemize}
Results show that Q3B is
\alert
{
more efficient
}
than standard SMT solvers.
\bigskip
Our results and results of SMT-COMP 2016 show that Q3B is
\alert
{
more efficient
}
than standard SMT solvers.
\end{frame}
\section
{
Aims of the Work
}
...
...
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