sidekick/propal.tex

\documentclass{llncs}

\usepackage[T1]{fontenc}
\usepackage[margin=1.5in]{geometry}
\usepackage[usenames,dvipsnames,svgnames,table]{xcolor}
\usepackage{hyperref}

\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}}

\begin{document}

\title{\msat{}: An OCaml SAT Solver}
\author{Guillaume~Bury}
\institute{\inria{}/ \lsv{}/\ens{}, Cachan, France\\\email{guillaume.bury@inria.fr}}

\maketitle

\begin{abstract}
  We present \msat{}, a modular SAT solving library written entirely in OCaml.
  While there already exist OCaml bindings for SAT solvers written in C,
  \msat{} provides more features, such as proof output, and the ability to
  instantiate an SMT solver using a first-order theory given by the user,
  while being reasonably efficient compared to the existing bindings.
\end{abstract}

\section*{Introduction}

Deciding the satisfiability of propositional logical formulae is an interesting
and recurring problem for which SAT solvers are now the standard solution.
However, there exist very few SAT solvers available in OCaml. There are
currently 4 opam\cite{opam} packages that provide an OCaml library for SAT
solving\footnote{There are a few additional packages for SMT solving, which we
do not include because of the added complexity providing a full SMT solver
compared to providing an interface for SAT solving.}, 3 of which are bindings to
one or more SAT solvers written in C (such as minisat\cite{minisat}). We will
present the fourth one, \msat{}, which is entirely written in OCaml.

\section*{Sat and SMT Solving}

Sat solvers work on propositional clauses, which are disjunctions of atomic
propositions. A set of propositional clauses is satisfiable iff there exist a
model for it, that is an assignment from the atomic propositions to booleans, such
that for every clause there exist an atomic proposition in the clause which is
assigned to $\top$. A SAT solver solves the satisfiability problems, meaning that for an
input problem given as a set of clauses, it returns either `sat' if the problem
is satisfiable, or `unsat' if it is not.

SMT\footnote{Acronym for Satisfiability Modulo Theories.} solvers are extensions
of SAT solvers to quantifier-free clauses built using first-order theories (like
linear arithmetic); clauses such as
$\neg (x + 1 > y) \lor \neg (y > z - 5) \lor (x > z - 10)$. In order to verify
the satisfiability of a set of first-order clauses, a SAT solver is combined
with a first-order theory: the basic idea is for the SAT solver to enumerate
all propositional models, and for each of them, ask the theory if it is
satisfiable\footnote{In practice, incomplete models are incrementally given to
the theory, and efficient backtracking is used in order to reach good
performances.}. If the theory returns `sat' for at least one propositional model,
the SMT solver returns `sat', in the other case, it returns `unsat'. That way,
the theory only has to deal with the satisfiability of a set of first-order
atomic propositions, while the SAT solver deals with the propositional structure
of the input problem.

\section*{\msat{}}

\msat{}\cite{msat} is a library entirely written in OCaml, which derives from
\aez{}\cite{aez}, itself derived from the SMT solver
\altergo{}\cite{altergo}\footnote{Apart from the initial fork of \aez{}, it is of
interest to note that the development of \msat{} is completely separate and independant
from that of \aez{} and \altergo{}}. While there exist full SMT solvers as well SAT solvers
available in OCaml, \msat{} is somewhere between the two: it doesn't provides builtin theories
like SMT solvers, but instead allows the user to provide her own implementation of
theories, something which is impossible to do using the bindings to SAT solvers written in C.
\msat{} is therefore the first OCaml library to allow to create custom SMT solvers.

Specifically, \msat{} provides functors to instantiate SMT solvers,
and by extension SAT solvers, since an SMT solver with an empty theory (that is, a
theory which always returns `sat') is a SAT solver. This closely follows the
theoretical foundation of SMT solvers, where any theory respecting adequate
invariants can be plugged into a SAT solver to make a SMT solver.

\msat{} supports most usual
features of SAT solvers, such as local assumptions, but more
importantly provides unique and original features like:
\begin{itemize}
  \item the ability to instantiate one's own SMT solver
  \item a detailed proof output for unsatisfiable problems, including printing
    of coq proof scripts
\end{itemize}


\section*{Presentation}

The presentation will introduce the basics of SAT and SMT solving, and then
explain the interfaces exported by the library, focusing on three different
points:

\begin{itemize}
  \item How to use the SAT solver exported by \msat{}
  \item How to instantiate a custom SMT solver using \msat{}, explaining in
    detail the various documented invariant expected to create a fully
    operational SMT solver, and the design choices behind them.
    This will be accompanied by an example of such instantiation.
  \item The design of the proof output of \msat{}
\end{itemize}

Lastly, there will be a comparison between \msat{} and the other SAT solvers
in the OCaml ecosystem. This comparison will be about available features
as well as performance.

\bibliographystyle{unsrt}
\begin{thebibliography}{1}

  \bibitem{msat}
    \msat{}: a modular sat/smt solver with proof output.
    \url{https://github.com/Gbury/mSAT}

  \bibitem{opam}
    Opam: a Package manager for ocaml.
    \url{https://opam.ocaml.org}

  \bibitem{minisat}
    MiniSat is a minimalistic, open-source SAT solver.
    \url{http://minisat.se/Main.html}

  \bibitem{aez}
    Alt-Ergo Zero is an OCaml library for an SMT solver.
    \url{http://cubicle.lri.fr/alt-ergo-zero/}

  \bibitem{altergo}
    Alt-Ergo.
    \url{http://alt-ergo.lri.fr/}

\end{thebibliography}

\end{document}