simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-10 13:14:09 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

poste rupdate

Browse source
This commit is contained in:
Guillaume Bury 2017-08-31 13:32:16 +02:00
parent a0d0125eed
commit e847c73cf9
2 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

BIN
poster/poster.pdf
View file

Binary file not shown.

8
poster/poster.tex
View file

@ -127,6 +127,8 @@
\item Minimal impact on proof search (already done to compute
unsat-core)
\item Sufficient to rebuild the whole resolution tree
\item A proof is a clause and proof nodes are lazily expanded \\
$\rightarrow$ no memory issue
\item Enables various proof output:
\begin{itemize}[label=$\bullet$]
\item Dot/Graphviz (see example above)
@ -137,7 +139,6 @@
\tblock{Performances}
{
\begin{tabular}{c|@{\,}c@{\,}|@{\,}c@{\,}|c|c}
solvers & aez & mSAT & \begin{tabular}{c}minisat\\(minisat/sattools)\end{tabular} & \begin{tabular}{c}cryptominisat\\(sattools)\end{tabular} \\ \hline
uuf100 (1000 pbs) & 0.125 & 0.012 & 0.004 & 0.006 \\ \hline
@ -148,7 +149,10 @@
pigeon/hole9 & \begin{tabular}{c}timeout\\(600)\end{tabular} & 8.886 & 0.634 & 4.075 \\ \hline
pigeon/hole10 & \begin{tabular}{c}timeout\\(600)\end{tabular} & 161.478 & \begin{tabular}{c}9.579 (minisat)\\160.376 (sattools)\end{tabular} & 72.050 \\ \hline
\end{tabular}
\\
\begin{center}
Done using https://github.com/Gbury/sat-bench.
\end{center}
}
\end{multicols}