Skip to content

Commit

Permalink
Address NII colleagues' feedback
Browse files Browse the repository at this point in the history 
Improve the presentation of experimental results

Report time measurement using scientific notations

- For a fixed number of significant digits as suggested by BenchExec paper
- E.g., if the measurement precision is 0.1%, we have three significant digits (a.bc * 10^x)

Reorganize the presentation of evaluation results

- Put the implications before results (because they are more important)
- Highlight rows in the tables (to attract the focus of the audience)

Correct the order of appendix slides
  • Loading branch information
nianze committed Jun 1, 2021
1 parent 524dc42 commit 1d2e20b
Show file tree
Hide file tree
Showing 5 changed files with 70 additions and 95 deletions.
40 changes: 20 additions & 20 deletions Talks/oral_defense/appendix.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -259,6 +259,26 @@
}
\end{frame}

\begin{frame}
\frametitle{Approximate E-MAJSAT Solving: \erssatb on \textit{MPEC}}
\begin{table}[ht]
\centering
\scriptsize
\pgfplotstabletypeset[
every head row/.style={before row={\toprule
& \multicolumn{4}{c}{\dcssat} & \multicolumn{8}{c}{\erssatb}\\},after row=\midrule},
every last row/.style={after row=\bottomrule},
empty cells with={--},
formula column/.list={0},
time column/.list={1,3},
prob column/.list={2,4},
lbound column/.list={5},
lbtime column/.list={6}
]
{exist-random-ssat/parsed-MPEC-erssatb.csv}
\end{table}
\end{frame}

\begin{frame}
\frametitle{Computational Complexity of DSSAT}
\begin{block}{Theorem: NEXPTIME-Completeness of DSSAT}
Expand Down Expand Up @@ -286,26 +306,6 @@
\end{block}
\end{frame}

\begin{frame}
\frametitle{Approximate E-MAJSAT Solving: \erssatb on \textit{MPEC}}
\begin{table}[ht]
\centering
\scriptsize
\pgfplotstabletypeset[
every head row/.style={before row={\toprule
& \multicolumn{4}{c}{\dcssat} & \multicolumn{8}{c}{\erssatb}\\},after row=\midrule},
every last row/.style={after row=\bottomrule},
empty cells with={--},
formula column/.list={0},
time column/.list={1,3},
prob column/.list={2,4},
lbound column/.list={5},
lbtime column/.list={6}
]
{exist-random-ssat/parsed-MPEC-erssatb.csv}
\end{table}
\end{frame}

\begin{frame}
\frametitle{Modeling Decentralized POMDP}
\begin{center}
Expand Down
68 changes: 18 additions & 50 deletions Talks/oral_defense/exist-random-ssat/evaluation.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,21 @@
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Implications from the Results}
\begin{itemize}
\item \erssat performs similarly as \dcssat on random formulas
\pause
\item \erssat is not suitable for certain application formulas
\begin{itemize}
\item Clause-containment learning might degenerate to brute-force search
\item Overhead incurred by the heuristics to strengthen learnt clauses
\end{itemize}
\pause
\item \erssat is good at deriving tight lower bounds for large formulas
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Quantile Plot for Random Formulas}
\begin{figure}
Expand Down Expand Up @@ -147,6 +162,8 @@
every head row/.style={before row={\toprule
& \multicolumn{4}{c}{\dcssat} & \multicolumn{8}{c}{\erssat}\\},after row=\midrule},
every last row/.style={after row=\bottomrule},
every row no 0/.style={before row={\rowcolor{yellow}}},
every row no 8/.style={before row={\rowcolor{yellow}}},
empty cells with={--},
formula column/.list={0},
time column/.list={1,3},
Expand All @@ -156,53 +173,4 @@
]
{exist-random-ssat/parsed-MPEC-erssat.csv}
\end{table}
\end{frame}

\begin{frame}
\frametitle{Implications from the Results}
\begin{itemize}
\item \erssat performs similarly as \dcssat on random formulas
\pause
\item \erssat is not suitable for certain application formulas
\begin{itemize}
\item Clause-containment learning might degenerate to brute-force search
\item Overhead incurred by the heuristics to strengthen learnt clauses
\end{itemize}
\pause
\item \erssat is good at deriving tight lower bounds for large formulas
\end{itemize}
\end{frame}

\iffalse
\begin{frame}
\frametitle{Memory Quantile Plot for Random Formulas}
\begin{figure}
\centering
\includegraphics{fig/exist-random-ssat/quantile-memory-Random.pdf}
\end{figure}
\end{frame}

\begin{frame}
\frametitle{Memory Quantile Plot for Application Formulas}
\begin{figure}
\centering
\includegraphics{fig/exist-random-ssat/quantile-memory-Application.pdf}
\end{figure}
\end{frame}

\begin{frame}
\frametitle{CPU-Time Scatter Plot: \erssat vs. \erssatb}
\begin{figure}
\centering
\includegraphics{fig/exist-random-ssat/scatter-erssat.pdf}
\end{figure}
\end{frame}

\begin{frame}
\frametitle{CPU-Time Scatter Plot: \erssat vs. \dcssat}
\begin{figure}
\centering
\includegraphics{fig/exist-random-ssat/scatter-dcssat.pdf}
\end{figure}
\end{frame}
\fi
\end{frame}
7 changes: 4 additions & 3 deletions Talks/oral_defense/preamble.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@
\usecolortheme{default}

% packages
\usepackage{colortbl}
\usepackage{etoolbox}
\usepackage[square,numbers,sort&compress]{natbib}
\usepackage{algorithm}
Expand Down Expand Up @@ -174,7 +175,7 @@
},
time column/.style={
/pgfplots/table/display columns/#1/.style={
string replace={nan}{},fixed,fixed zerofill,dec sep align,precision=2,column name=T (s)
string replace={nan}{},sci,sci zerofill,sci sep align,precision=2,sci e,column name=T (s)
}
},
prob column/.style={
Expand All @@ -194,12 +195,12 @@
},
ubtime column/.style={
/pgfplots/table/display columns/#1/.style={
string replace={nan}{},fixed,fixed zerofill,dec sep align,precision=2,column name=T-UB (s)
string replace={nan}{},sci,sci zerofill,sci sep align,precision=2,sci e,column name=T-UB (s)
}
},
lbtime column/.style={
/pgfplots/table/display columns/#1/.style={
string replace={nan}{},fixed,fixed zerofill,dec sep align,precision=2,column name=T-LB (s)
string replace={nan}{},sci,sci zerofill,sci sep align,precision=2,sci e,column name=T-LB (s)
}
}
}
Expand Down
26 changes: 15 additions & 11 deletions Talks/oral_defense/prob-design-eval/evaluation.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,17 @@
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Implications from the Results}
\begin{itemize}
\item \bddsp performs the best for small- and medium-sized circuits
\pause
\item \approxmc uniquely solves large instances
\pause
\item \cachet and \dcssat do not scale well
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Results for PEC ($\dr=0.01$)}
\begin{table}
Expand All @@ -56,6 +67,8 @@
every head row/.style={before row={\toprule
& \multicolumn{4}{c}{\bddsp} & \multicolumn{4}{c}{\dcssat} & \multicolumn{4}{c}{\cachet} & \multicolumn{4}{c}{\approxmc}\\},after row=\midrule},
every last row/.style={after row=\bottomrule},
every row no 0/.style={before row={\rowcolor{yellow}}},
every row no 9/.style={before row={\rowcolor{yellow}}},
empty cells with={--},
circuit column/.list={0},
time column/.list={1,3,5,7},
Expand All @@ -74,22 +87,13 @@
every head row/.style={before row={\toprule
& \multicolumn{4}{c}{\bddsp} & \multicolumn{4}{c}{\bddspnr} & \multicolumn{4}{c}{\dcssat}\\},after row=\midrule},
every last row/.style={after row=\bottomrule},
every row no 0/.style={before row={\rowcolor{yellow}}},
every row no 11/.style={before row={\rowcolor{yellow}}},
empty cells with={--},
circuit column/.list={0},
time column/.list={1,3,5},
prob column/.list={2,4,6}
]
{prob-design-eval/parsed-MPEC-D-0.01.csv}
\end{table}
\end{frame}

\begin{frame}
\frametitle{Implications from the Results}
\begin{itemize}
\item \bddsp performs the best for small- and medium-sized circuits
\pause
\item \approxmc uniquely solves large instances
\pause
\item \cachet and \dcssat do not scale well
\end{itemize}
\end{frame}
24 changes: 13 additions & 11 deletions Talks/oral_defense/random-exist-ssat/evaluation.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,17 @@
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Implications from the Results}
\begin{itemize}
\item \ressat outperforms \dcssat on random and strategic formulas
\pause
\item \ressat is able to derive non-trivial bounds when \dcssat timeouts
\pause
\item Minterm generalization is crucial to the performance of \ressat
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Quantile Plot for Random Formulas}
\begin{figure}
Expand All @@ -72,6 +83,8 @@
every head row/.style={before row={\toprule
& \multicolumn{4}{c}{\dcssat} & \multicolumn{6}{c}{\ressat} & \multicolumn{6}{c}{\ressatb}\\},after row=\midrule},
every last row/.style={after row=\bottomrule},
every row no 0/.style={before row={\rowcolor{yellow}}},
every row no 10/.style={before row={\rowcolor{yellow}}},
empty cells with={--},
formula column/.list={0},
time column/.list={1,3,6},
Expand All @@ -80,15 +93,4 @@
]
{random-exist-ssat/parsed-PEC-0.01.csv}
\end{table}
\end{frame}

\begin{frame}
\frametitle{Implications from the Results}
\begin{itemize}
\item \ressat outperforms \dcssat on random and strategic formulas
\pause
\item \ressat is able to derive non-trivial bounds when \dcssat timeouts
\pause
\item Minterm generalization is crucial to the performance of \ressat
\end{itemize}
\end{frame}

0 comments on commit 1d2e20b

Please sign in to comment.