From d943be5fc1de20083315ee4b82f53c5eec45789f Mon Sep 17 00:00:00 2001 From: Tobias Eidelpes Date: Wed, 20 May 2020 12:30:27 +0200 Subject: [PATCH] Finish evaluation for QBFs --- review_1/review_1.tex | 80 ++++++++++++++++++++++++++++++------------- 1 file changed, 57 insertions(+), 23 deletions(-) diff --git a/review_1/review_1.tex b/review_1/review_1.tex index e3be484..a3b1848 100644 --- a/review_1/review_1.tex +++ b/review_1/review_1.tex @@ -4,6 +4,8 @@ \usepackage[utf8]{inputenc} \usepackage[english]{babel} \usepackage{csquotes} +\usepackage[margin=1in]{geometry} +\usepackage{hyperref} \begin{document} @@ -22,32 +24,64 @@ is summarized in the conclusion. \section{Evaluation} \label{sec:Evaluation} - - -\section{Overall impression} -\label{sec:Overall impression} - -Overall I think your paper provides a good overview of quantified boolean -formulae. - -\section{Language} -\label{sec:Language} - 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. Most notably indefinite articles that are missing or wrong -(e.g., page 5 in the section \emph{Planning}: \enquote{A existence...}). Some -sentences are grammatically incorrect or are hard to read due to their -structure. The sentence on the bottom of page 3 and the beginning of page 4 is -an example of this. Scientific writing normally does not use abbreviations such -as \emph{doesn't} or \emph{we're}. There is also one sentence at the end of -section 4.3.1 which is started with \enquote{Another} but never finished. +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. -\section{Layout} -\label{sec:Layout} +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. -It seems that the course template has been used, although the title page has -been changed to be on a single page and a table of contents is included. The -introductory slides of this course states that +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}