\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}