Commit e5708327 authored by Martin Jonáš's avatar Martin Jonáš
Browse files

Reference complexity

parent dc84792d

Chapters/Chapter02.tex

+1 −0
Original line number Diff line number Diff line
@@ -855,6 +855,7 @@ reduces to finding values $a$ and $b$. 




\section{Computational complexity of bit-vector logics}

\label{sec:complexity}

The propositional satisfiability problem is well known from the

computational complexity perspective, as it is the first problem that

was shown to be \NP-complete. The complexity of the satisfiability

Chapters/Chapter04.tex

+5 −5
Original line number Diff line number Diff line
@@ -66,11 +66,11 @@ hybrid approach and its evaluation on the representative set of 
benchmark is expected.



\subsection{Complexity of BV2}

As was explained in section ???, the precise complexity of quantified

bit-vector formulas with binary-encoded bit-widths and without

uninterpreted functions is not known. It is known to be in \EXPSPACE

and to be \NEXPTIME-hard. However, a class for which the problem is

complete is not known.

As was explained in section \ref{sec:complexity}, the precise

complexity of quantified bit-vector formulas with binary-encoded

bit-widths and without uninterpreted functions is not known. It is

known to be in \EXPSPACE and to be \NEXPTIME-hard. However, a class

for which the problem is complete is not known.



Acording to our investigation, it is probably complete for neither of

those complexity classes. We are working on a proof which shows that