\documentclass[portrait,a0,final]{a0poster}

\usepackage[utf8]{inputenc}
\usepackage[OT1]{fontenc}
\usepackage[french]{babel}
\usepackage{enumitem}
\usepackage{verbatim}
\usepackage{amsfonts, amsmath, amssymb, amsthm, dsfont}

%\usepackage{listings}
%\lstset{language=[Objective]Caml}

\usepackage{minted}

\usepackage{bussproofs}
\newcommand\typ[2]{\Gamma\vdash#1:#2}

\input{template_deducteam.tex}

\def\aez{\textsf{Alt-Ergo~Zero}}
\def\altergo{\textsf{Alt-Ergo}}
\def\ens{\textsf{ENS Paris-Saclay}}
\def\inria{\textsf{Inria}}
\def\lsv{\textsf{LSV}}
\def\msat{\textsf{mSAT}}
\def\opam{\textsf{opam}}

\begin{document}

\sffamily % Font Family

\postertitle
{\msat{}:~An~OCaml~SAT~Solver}
{Guillaume \textsc{Bury}}
{DEDUC$\vdash$EAM (INRIA) - LSV / CNRS\\
\Large \textcolor{black}{\texttt{guillaume.bury@inria.fr}}}

\begin{center}

\begin{multicols}{2}

\tblock{Introduction} % TODO
{
  \vspace{0.5cm} % Pour pas se faire manger par le titre

  \msat{}: a SAT solving library in OCaml. It solves the \textbf{satisfibility}
  of propositional clauses. It is \textbf{Modular}: the user provides
  the theory. And it \textbf{produces formal proofs}.
}

\tblock{Conflict Driven Clause Learning}
{
  \begin{description}
    \item[Propagation] If there exists a clause $C = C' \lor a$, where
      $C'$ is false in the partial model, then add $a \mapsto \top$ to
      the partial model, and record $C$ as the reason for $a$.
    \item[Decision] Take an atom $a$ that is not yet in the partial model,
      and add $a \mapsto \top$ to the model.
    \item[Conflict] A conflict is a clause $C$ that is false in the current partial
      model.
    \item[Analyze] Perform resolution between the analyzed clause and the reason
      behind the propagation of its most recently assigned litteral, until
      the analyzed clause is suitable for backumping.
    \item[Backjump] A clause is suitable for backjumping if its most recently
      assigned litteral $a$ is a decision. We can then backtrack to before the
      decision, and add the analyzed clause to the solver, which will then enable
      to propagate $a \mapsto \bot$.
    \item[SMT] Formulas using first-order theories can be handled using a theory.
      Each formula propagated or decided is sent to the theory, which then
      has the duty to check whether the conjunction of all formulas seen so
      far is satisfiable, if not, it should return a theory tautology (as a clause),
      that is not satisfied in the current partial model.
  \end{description}
}

\tblock{Implementation}
{
  \begin{itemize}[label=$\blacktriangleright$]
    \item Imperative design
      \begin{itemize}[label=\checkmark]
        \item 2-watch litteral
        \item Backtrackable theories (less demanding than immutable theories)
      \end{itemize}
    \item Features
      \begin{itemize}[label=\checkmark]
        \item Functorized design, using generative functors
        \item Local assumptions
        \item Model output and proof output (Coq, dot)
      \end{itemize}
  \end{itemize}
}

\cblock{Solver Interface}
{
  \inputminted{ocaml}{solver_intf.ml}
}

\tblock{Other Solvers}
{
  \begin{center}
    \begin{tabular}{c@{\quad}|@{\quad}c@{\quad}|@{\quad}c@{\quad}|@{\quad}c}
    regstab & SAT & binary only & only pure SAT \\ \hline
    \begin{tabular}{c}\textbf{minisat}\\\textbf{sattools}\\ocaml-sat-solvers\end{tabular} & SAT & C bindings & only pure SAT \\ \hline
    Alt-ergo & SMT & binary only & Fixed theory \\ \hline
    \textbf{Alt-ergo-zero} & SMT & OCaml lib & Fixed theory \\ \hline
    \begin{tabular}{c}ocamlyices\\yices2\end{tabular} & SMT & C bindings & Fixed theory \\
  \end{tabular}
  \end{center}
}


\columnbreak

\tblock{Problem Example}
{
  \vspace{.2cm}
  \[
  \begin{matrix}
    \text{Are the following} & \quad & H1: & a = b   & \quad & H2: & b = c \lor b = d \\
    \text{hypotheses satisfible ?} & \quad & H3: & a <> d  & \quad & H4: & a <> c \\
  \end{matrix}
  \]
  \includegraphics[height=33cm]{proof}
}

\cblock{Theory Interface}
{
  \inputminted{ocaml}{theory_intf.ml}
}

\tblock{Proof generation}
{
  \begin{itemize}[label=\checkmark]
    \item Each clause records its "history" which is the clauses
      used during analyzing
    \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 expanded on demand\\
      $\rightarrow$ no memory issue
    \item Enables various proof outputs:
      \begin{itemize}[label=$\bullet$]
        \item Dot/Graphviz (see example above)
        \item Coq (and soon dedukti) formal proofs
      \end{itemize}
  \end{itemize}
}

\tblock{Performances}
{
  \\ \\
  \begin{tabular}{c|@{\,}c@{\,}|@{\,}c@{\,}|c|c}
    \begin{tabular}{c}solver\\{\small (package)}\end{tabular} & \begin{tabular}{c}Alt-ergo-zero\\{\small aez}\end{tabular} & \begin{tabular}{c}mSAT\\{\small msat}\end{tabular} & \begin{tabular}{c}minisat\\{\small (minisat/sattools)}\end{tabular} & \begin{tabular}{c}cryptominisat\\{\small (sattools)}\end{tabular} \\ \hline
    uuf100 (1000 pbs) & 0.125 & 0.012 & 0.004 & 0.006 \\ \hline
    uuf125 (100 pbs) & 2.217 & 0.030 & 0.006 & 0.013 \\ \hline
    uuf150 (100 pbs) & 67.563 & 0.087 & 0.017 & 0.045 \\ \hline
    pigeon/hole6 & 0.120 & 0.018 & 0.006 & 0.006 \\ \hline
    pigeon/hole7 & 4.257 & 0.213 & 0.015 & 0.073 \\ \hline
    pigeon/hole8 & 31.450 & 0.941 & 0.096 & 2.488 \\ \hline
    pigeon/hole9 & timeout (600) & 8.886 & 0.634 & 4.075 \\ \hline
      pigeon/hole10 & timeout (600) & 161.478 & \begin{tabular}{c}9.579 {\small (minisat)}\\160.376 {\small (sattools)}\end{tabular} & 72.050 \\
  \end{tabular}
}

\end{multicols}

\end{center}

\end{document}