88 lines
4.3 KiB
TeX
88 lines
4.3 KiB
TeX
\documentclass[11pt,a4paper]{article}
|
|
|
|
\usepackage[T1]{fontenc}
|
|
\usepackage[utf8]{inputenc}
|
|
\usepackage[english]{babel}
|
|
\usepackage{csquotes}
|
|
\usepackage[margin=1in]{geometry}
|
|
\usepackage{hyperref}
|
|
|
|
\begin{document}
|
|
|
|
\section{Summary}
|
|
\label{sec:Summary}
|
|
|
|
The paper first gives a short introduction to the history of QBF solvers and
|
|
their relation to SAT solvers. The general structure of the paper is introduced.
|
|
A section about defining the terms used throughout the paper follows and the
|
|
complexity of these types of problems is mentioned. The Couterexample-Guided
|
|
Abstraction Refinement (CEGAR) technique for solving QBFs is defined and the
|
|
principle is demonstrated by using pseudocode. The fourth, and main, section of
|
|
the paper discusses different applications for QBFs and the content of the paper
|
|
is summarized in the conclusion.
|
|
|
|
\section{Evaluation}
|
|
\label{sec:Evaluation}
|
|
|
|
The language used throughout the paper is in general suitable for scientific
|
|
writing with respect to the used vocabulary. There are some grammatical and
|
|
spelling errors that should be resolvable by either using spellcheck software or
|
|
by rereading the paper (for the grammatical errors). Abbreviations such as
|
|
\emph{don't} or \emph{we're} should not be used in scientific writing. At the
|
|
end of section 4.3.1 a sentence is started with \enquote{Another} but never
|
|
finished.
|
|
|
|
The abstract is very short and does not describe the relevance of your topic or
|
|
the content of your paper. I would start with a sentence like
|
|
\enquote{Quantified Boolean Formulae allow encoding complex problems such as
|
|
planning, two-player games and verification in a compact and natural way...}.
|
|
Hinting at the speed or general performance of QFB solvers is also an option.
|
|
|
|
The introduction touches upon the relevant information needed to put solving
|
|
QBFs into relation with other problems, e.g., the SAT problem. The motivation
|
|
for solving QBFs and why QBFs are important is not clear. I would suggest
|
|
including a sentence or two about what makes QBFs interesting, what kind of
|
|
problems are solvable by using QBFs and why the research community could not do
|
|
that before by using SAT solvers for example.
|
|
|
|
The individual parts of the paper are a bit disjointed because the transition
|
|
from one section to the next is not always clear. See for example from section 2
|
|
to section 3 where suddenly 2QBFs are introduced. Additionally, it is not said
|
|
why we need CEGAR and what it is good for. I like the idea to compare QBFs to
|
|
normal SAT in terms of complexity. For someone who is mostly familiar with the
|
|
complexity classes up to \textsf{NP}, further explanations for \textsf{PSPACE}
|
|
would be beneficial. For example discussing why \textsf{PSPACE} mirrors games
|
|
would aid in understanding the complexity landscape for these types of problems.
|
|
I would also suggest rewriting the sentence at the bottom of page 3 to page 4
|
|
because it is worded in such a way that it is difficult to understand without
|
|
rereading the sentence multiple times.
|
|
|
|
For section number 4 going into more detail about each of the different problems
|
|
would give the reader a more complete picture. It is not clear for example why
|
|
section 4.1 is named \emph{Compression}. The text following the headline defines
|
|
the reachability problem which the reader cannot put into relation with the term
|
|
\emph{Compression}. The same problem applies to section 4.4 where the relation
|
|
of the headline to the text is only vaguely perceptible. The first paragraph for
|
|
\emph{Model Checking}, however, gives a short and concise description of the
|
|
problem and what the goal is. Likewise, section 4.3.1 contains a clear
|
|
description of the problem, how it is modeled using QBFs and what the solution
|
|
looks like. Applying a similar approach to the other sections would make it
|
|
easier for readers to know what to expect from each section and help them find
|
|
the information they need.
|
|
|
|
The conclusion is missing an outlook on further research directions in the field
|
|
of QFBs which would wrap up the paper in a straightforward fashion.
|
|
|
|
In summary, the structure of the paper is good although the individual sections
|
|
could contain more explanations of the problems and their solutions. See
|
|
section~\ref{sec:Major issues} and \ref{sec:Minor issues} for a listing of the
|
|
identified problems.
|
|
|
|
\section{Major issues}
|
|
\label{sec:Major issues}
|
|
|
|
\section{Minor issues}
|
|
\label{sec:Minor issues}
|
|
|
|
\end{document}
|