\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{} is a SAT solving library written in OCaml. It allows to solve the satisfiability
  of propositional problems in clausal normal form, and produce either a propositional model,
  or a resolution proof of the problem's unsatisfiability.
}

\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$ which 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 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}minisat\\sattools\\ocaml-sat-solvers\end{tabular} & SAT & C bindings & only pure SAT \\ \hline
    Alt-ergo & SMT & binary only & Fixed theory \\ \hline
    Alt-ergo-zero & SMT & OCaml lib & Fixed theory \\ \hline
    \begin{tabular}{c}ocamlyices\\yices2\end{tabular} & SMT & C bindings & Fixed theory \\ \hline
  \end{tabular}
  \end{center}
}


\columnbreak

\tblock{Problem example}
{
  \vspace{.5cm}
  \[
  \begin{matrix}
    H1: & a = b   & \quad & H2: & b = c \lor b = d \\
    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 it "history", that 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 output:
      \begin{itemize}[label=$\bullet$]
        \item Dot/Graphviz (see example above)
        \item Coq formal proof
      \end{itemize}
  \end{itemize}
}

\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
    uuf125 (100 pbs) & 2.217 & 0.030 & 0.006 & 0.013 \\ \hline
    uuf150 (100 pbs) & TODO & TODO & TODO & TODO \\ \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 & \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}
}

\end{multicols}

\end{center}

\end{document}