Commit bc0a4271 authored by Martin Jonas's avatar Martin Jonas
Browse files

Small fixes

parent 976ee06b
......@@ -7,12 +7,11 @@
This section introduces the notation used in the rest of this
chapter. The exposition of the propositional logic is mainly based on
the work of Nieuwenhuis et al.~\cite{NOT06}. The exposition of the
first-order logic is partly based on the same source, but the
definition of a first-order theory is different. In particular,
instead of defining theory as a set of first-order sentences, the
theory is defined as a set of first-order \emph{structures}, as this
definition is more suitable for the bit-vector theory, which is
introduced in the later parts of this chapter.
first-order logic is based on works of Enderton~\cite{End01} and of
Barrett et al.~\cite{BSST09}. Note that instead of following the
approach of Enderton, we follow the approach of Barrett et al. and
define the theory as a set of first-order \emph{structures}, rather
than a set of first-order sentences.
\subsection{Propositional formulas, assignments, and satisfaction}
\label{prelim:prop}
......@@ -64,7 +63,7 @@ if $\varphi$ is satisfiable precisely if $\psi$ is satisfiable.
A \emph{signature} $\Sigma$ consists of a set of \emph{function
symbols} $\Sigma^f$, a set of \emph{predicate symbols} $\Sigma^p$
and for each of these symbols a non-negative number called its
and a non-negative number for each of these symbols called its
\emph{arity}. Given a signature $\Sigma$, \emph{$\Sigma$-terms},
\emph{$\Sigma$-atoms}, \emph{$\Sigma$-literals},
\emph{$\Sigma$-clauses}, and \emph{$\Sigma$-formulas} are defined as
......@@ -83,32 +82,32 @@ arity $n$ assigns a function $f^\mathcal{A} \colon A^n \rightarrow A$,
and to each predicate symbol $P \in \Sigma^p$ of arity $n$ assigns a
relation $P^\mathcal{A} \subseteq A^n$. Given a $\Sigma$-structure
$\mathcal{A}$, there exists a unique homomorphic extension of
$(\_)^\mathcal{A}$, which to each ground term $t$ assigns an element
$t^\mathcal{A} \in A$, and which can be further extended in a standard
way to assign a truth value
$\varphi^\mathcal{A} \in \{ \true, \false \}$ to each ground formula
$\varphi$. A $\Sigma$-structure $\mathcal{A}$ is said to
\emph{satisfy} a ground $\Sigma$-formula $\varphi$ if
$(\_)^\mathcal{A}$ to terms, which to each term $t$ assigns an element
$t^\mathcal{A} \in A$. In turn, using standard definitions, the
assignment $(\_)^\mathcal{A}$ can be further extended to assign a
truth value $\varphi^\mathcal{A} \in \{ \true, \false \}$ to each
formula $\varphi$. A $\Sigma$-structure $\mathcal{A}$ is said to
\emph{satisfy} a $\Sigma$-formula $\varphi$ if
$\varphi^\mathcal{A} = \true$. In such case, the structure
$\mathcal{A}$ is also called a \emph{model} of the
formula $\varphi$.
$\mathcal{A}$ is also called a \emph{model} of the formula $\varphi$.
A \emph{$\Sigma$-theory} $\mathcal{T}$ is a class of
$\Sigma$-structures closed under isomorphisms and variable
reassignment. A ground $\Sigma$-formula is said to be satisfiable in
the $\Sigma$-theory $\mathcal{T}$, or $\mathcal{T}$-satisfiable, if
there exists a $\Sigma$-structure $\mathcal{A} \in \mathcal{T}$ such
that $\mathcal{A}$ satisfies $\varphi$. The structure $\mathcal{A}$ is
then called a \emph{$\mathcal{T}$-model} of $\varphi$. If $\varphi$ is
a ground $\Sigma$-formula and $\Gamma$ is a set of ground
$\Sigma$-formulas, we say that \emph{$\Gamma$ entails $\varphi$ in
$\mathcal{T}$}, written $\Gamma \models_\mathcal{T} \varphi$, if
every $\Sigma$-structure that satisfies all formulas in $\Gamma$ also
satisfies $\varphi$. If $\emptyset \models_\mathcal{T} \varphi$ for a
ground $\Sigma$-formula $\varphi$, the formula $\varphi$ is called
\emph{$\mathcal{T}$-valid} or a \emph{theory lemma}. A set $\Gamma$ of
ground $\Sigma$-formulas is called \emph{$\mathcal{T}$-inconsistent},
if $\Gamma \models_{\mathcal{T}} \bot$.
reassignment. A ground $\Sigma$-formula is said to be
\emph{satisfiable in the $\Sigma$-theory $\mathcal{T}$}, or
\emph{$\mathcal{T}$-satisfiable}, if there exists a $\Sigma$-structure
$\mathcal{A} \in \mathcal{T}$ such that $\mathcal{A}$ satisfies
$\varphi$. The structure $\mathcal{A}$ is then called a
\emph{$\mathcal{T}$-model} of $\varphi$. If $\varphi$ is a ground
$\Sigma$-formula and $\Gamma$ is a set of ground $\Sigma$-formulas, we
say that \emph{$\Gamma$ entails $\varphi$ in $\mathcal{T}$}, written
$\Gamma \models_\mathcal{T} \varphi$, if every $\Sigma$-structure that
satisfies all formulas in $\Gamma$ also satisfies $\varphi$. If
$\emptyset \models_\mathcal{T} \varphi$ for a ground $\Sigma$-formula
$\varphi$, the formula $\varphi$ is called \emph{$\mathcal{T}$-valid}
or a \emph{theory lemma}. A set $\Gamma$ of ground $\Sigma$-formulas
is called \emph{$\mathcal{T}$-inconsistent}, if
$\Gamma \models_{\mathcal{T}} \bot$.
% If $\varphi$
% and $\psi$ are ground $\Sigma$-formulas such that
......@@ -119,15 +118,14 @@ if $\Gamma \models_{\mathcal{T}} \bot$.
% lemma}.
For two signatures $\Sigma$ and $\Omega$, we call $\Omega$ a
\emph{sub-signature} of $\Sigma$ if $\Omega \subseteq \Sigma$,
i.e. $\Omega^f \subseteq \Sigma^f$ and $\Omega^p \subseteq
\Sigma^p$. Given a $\Sigma$-structure $\mathcal{A}$ and a signature
$\Omega$ that is a sub-signature of $\Sigma$, the \emph{reduct} of
$\mathcal{A}$ to a sub-signature $\Omega$ is a $\Omega$-structure
$\mathcal{A}'$ that coincides with $\mathcal{A}$ on all symbols from
$\Omega$. For a $\Sigma_1$-theory $\mathcal{T}_1$ and a
$\Sigma_2$-theory $\mathcal{T}_2$, their \emph{combination}
$\mathcal{T}_1 + \mathcal{T}_2$ is the largest
\emph{sub-signature} of $\Sigma$ if $\Omega^f \subseteq \Sigma^f$ and
$\Omega^p \subseteq \Sigma^p$. Given a $\Sigma$-structure
$\mathcal{A}$ and a signature $\Omega$ that is a sub-signature of
$\Sigma$, the \emph{reduct} of $\mathcal{A}$ to a sub-signature
$\Omega$ is an $\Omega$-structure $\mathcal{A}'$ that coincides with
$\mathcal{A}$ on all symbols from $\Omega$. For a $\Sigma_1$-theory
$\mathcal{T}_1$ and a $\Sigma_2$-theory $\mathcal{T}_2$, their
\emph{combination} $\mathcal{T}_1 + \mathcal{T}_2$ is the largest
$(\Sigma_1 \cup \Sigma_2)$-theory that contains all
$(\Sigma_1 \cup \Sigma_2)$-structures $\mathcal{A}$ for which the
reduct of $\mathcal{A}$ to $\Sigma_1$ is in $\mathcal{T}_1$ and the
......@@ -194,16 +192,17 @@ $\mathcal{T}$-\emph{solver}.
For some theories, it can be convinient to distinguish several types
of objects instead of having only one universe. This can be achieved
by using a \emph{many-sorted logic}. In contrast with a single-sorted
signature, defined in the previous subsection, a many-sorted signature
$\Sigma$ further contains a set of \emph{sort symbols}
$\Sigma^S$. Arities in a many-sorted logic are also modified. Arity of
a symbol determines not only a number of its arguments, but also their
types -- each function symbol has assigned $(n+1)$-tuple of sort
symbols for a non-negative integer $n$ and each predicate symbols has
assigned a $n$-tuple of sort symbols for a non-negative integer
$n$. Simultaneous inductive definition of terms of a sort
$S \in \Sigma^S$ and definitions of atoms, literals, clauses and
formulas are straightforward and can be found for example in Enderton.
signature, defined in the previous subsection, a \emph{many-sorted
signature $\Sigma$} additionally contains a set of \emph{sort
symbols} $\Sigma^S$. Arities in a many-sorted logic are also
modified. Arity of a symbol determines not only a number of its
arguments, but also their types -- each function symbol has assigned
$(n+1)$-tuple of sort symbols for a non-negative integer $n$ and each
predicate symbols has assigned a $n$-tuple of sort symbols for a
non-negative integer $n$. Simultaneous inductive definition of terms
of a sort $S \in \Sigma^S$ and definitions of atoms, literals, clauses
and formulas are straightforward and can be found for example in
Enderton~\cite{End01}.
For a many-sorted signature $\Sigma$, a \emph{$\Sigma$-structure}
$\mathcal{A}$ consists of an assignment $(\_)^\mathcal{A}$, which to
......@@ -211,16 +210,16 @@ each sort symbol $S \in \Sigma^S$ assigns a non-empty set
$S^\mathcal{A}$, caled the \emph{domain of S in $\mathcal{A}$}, to
each variable $x$ of sort $S$ assigns an element
$x^\mathcal{A} \in S^\mathcal{A}$, to each function symbol
$f \in \Sigma^f$ of arity $(S_1, \ldots, S_n, S_{n+1})$ assigns a
$f \in \Sigma^f$ of an arity $(S_1, \ldots, S_n, S_{n+1})$ assigns a
function
$f^\mathcal{A} \colon S_1^\mathcal{A} \times \ldots \times
S_n^\mathcal{A} \rightarrow S_{n+1}^\mathcal{A}$, and to each
predicate symbol $P \in \Sigma^p$ of arity $(S_1, \ldots, S_n)$
predicate symbol $P \in \Sigma^p$ of an arity $(S_1, \ldots, S_n)$
assigns a relation
$P^\mathcal{A} \subseteq S_1^\mathcal{A} \times \ldots \times
S_n^\mathcal{A}$. Definitions of many-sorted satisfiability, models,
entailment, and so on are also straightforward and can be found in
Enderton.
entailment, and so on are also straightforward and can also be found
in Enderton~\cite{End01}.
\section{Propositional satisfiability}
......@@ -403,13 +402,13 @@ Notable examples of decidable first-order theories include
to be undecidable by Gödel.} over the signature
$\{ +, \times, \leq \}$, which consists of all structures isomorphic
to real numbers with functions $+$ and $\times$ and the relation
$\leq$,
\item the theory of \emph{arrays} over the signature $\{ read, write \}$,
which consists of all structures isomorphic to the set of arrays
with a binary function $read(a, i)$ interpreted as a value in the
index $i$ of the array $a$, and a ternary function $write(a, i, v)$
interpreted as an array $a$ modified to contain the value $v$ on the
index $i$;
$\leq$;
\item the theory of \emph{arrays} over the signature
$\{ \arread, \arwrite \}$, which consists of all structures isomorphic
to the set of arrays with a binary function $\arread(a, i)$
interpreted as a value on the index $i$ of the array $a$, and a
ternary function $\arwrite(a, i, v)$ interpreted as an array $a$
modified to contain the value $v$ on the index $i$;
\item the theory of \emph{fixed-size bit-vectors}. \marginpar{TODO: describe}
\end{itemize}
For a detailed description of these theories and implementation of the
......@@ -417,7 +416,7 @@ respective $\mathcal{T}$-solvers, we refer the reader for example to the book of
Bradley and Manna~\cite{BM07}.
In pracitce, a satisfiability of formulas using a combination of
theories is often needed. For example, one formula may be using
theories is often needed. For example, a single formula may be using
integers, arrays, and uninterpreted functions. In their seminal work,
Nelson and Oppen have shown that satisfiability of combination of
stably infinite theories with disjoint signatures can be solved by
......@@ -425,9 +424,9 @@ using separate satisfiability solvers for the respective theories,
which interchange implied equalities and disequalities between shared
variables~\cite{NO79}. A theory $\mathcal{T}$ is \emph{stably
infinite} if every $\mathcal{T}$-satisfiable formula has a
$\mathcal{T}$ model whose universe is infinite. For a theory over in a
$\mathcal{T}$-model whose universe is infinite. For a theory over a
many-sorted logic, the theory is \emph{stably infinite} if every
$\mathcal{T}$-satisfiable formula has a model model, whose every sort
$\mathcal{T}$-satisfiable formula has a model, whose every sort
has an infinite domain. Although almost all practically used theories
are stably infinite, this is not true for inherently finite theories
like the theory of bit-vectors.
......@@ -931,11 +930,13 @@ exponential with respect to the size of the formula. Therefore,
bit-blasting shows that QF\_BV2 is in \NEXPTIME. On the other hand,
Kovásznai et al. have presented a polynomial time reduction of
satisfiability of \emph{dependent quantified Boolean formulas} (\dqbf)
to QF\_BV2. Since \dqbf is well known to be \NEXPTIME-complete, this
reduction shows \NEXPTIME-hardness of QF\_BV2~\cite{KFB12}. In
contrast, the precise complexity after adding quantifiers is not
known. BV2 is known to be in \EXPSPACE and because it contains all
formulas from QF\_BV2, it is also \NEXPTIME-hard.
to QF\_BV2. In contrast to \qbf, \dqbf formulas allow explicitly
stating on which variables can a quantified variable depend. Since
\dqbf is well known to be \NEXPTIME-complete, this reduction shows
\NEXPTIME-hardness of QF\_BV2~\cite{KFB12}. In contrast, the precise
complexity after adding quantifiers is not known. BV2 is known to be
in \EXPSPACE and because it contains all formulas from QF\_BV2, it is
also \NEXPTIME-hard.
Similarly to the case with the unary encoding, the complexity of the
quantifier-free fragment stays the same when the uninterpreted
......
......@@ -20,6 +20,9 @@
\newcommand{\nnf}{\textsc{nnf}\xspace}
\newcommand{\qsbf}{\textsc{qsbf}\xspace}
\newcommand{\arread}{\texttt{read}\xspace}
\newcommand{\arwrite}{\texttt{write}\xspace}
\newcommand{\true}{\ensuremath{\texttt{true}}}
\newcommand{\false}{\ensuremath{\texttt{false}}}
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment