108 lines
5.3 KiB
TeX
108 lines
5.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 using spellcheck software.
|
|
Abbreviations such as \emph{don't} or \emph{we're} should generally be avoided
|
|
when writing scientific papers. 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 QBF 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 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 QBFs 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. The length
|
|
of the paper is within the 7-10 pages if the table of contents is left out and
|
|
the space on the title page is removed. 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}
|
|
|
|
\begin{itemize}\setlength{\itemsep}{0pt}
|
|
\item Abstract, Introduction and Conclusion are too short (see
|
|
section~\ref{sec:Evaluation} for suggestions)
|
|
\item Although the general structure is intuitive, the individual points and
|
|
sections are missing a red line that takes the reader from one point to
|
|
the next
|
|
\item It is very hard to grasp the concepts without reading additional
|
|
material
|
|
\end{itemize}
|
|
|
|
\section{Minor issues}
|
|
\label{sec:Minor issues}
|
|
|
|
\begin{itemize}\setlength{\itemsep}{0pt}
|
|
\item The table of contents should be left out for short papers
|
|
\item The title page is on a separate page
|
|
\item Some figures and equations are not referenced correctly (sometimes the
|
|
word equation or figure is missing before the reference)
|
|
\item Some spelling and grammatical errors
|
|
\item Some references are missing information (e.g., [2] should mention the
|
|
workshop at IJCAI 2016; [5] was published in the lecture notes on
|
|
computer science and submitted to the SAT 2011 conference)
|
|
\end{itemize}
|
|
|
|
\end{document}
|