updated Nitpick SAT Solver doc
authorblanchet
Sun, 25 Sep 2011 18:43:25 +0200
changeset 45949dbf6612461dc
parent 45948 3cb902212af5
child 45950 bdb00fad5687
updated Nitpick SAT Solver doc
doc-src/Nitpick/nitpick.tex
     1.1 --- a/doc-src/Nitpick/nitpick.tex	Sun Sep 25 18:43:25 2011 +0200
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Sun Sep 25 18:43:25 2011 +0200
     1.3 @@ -2337,42 +2337,43 @@
     1.4  
     1.5  \begin{enum}
     1.6  
     1.7 +\item[$\bullet$] \textbf{\textit{Lingeling\_JNI}:}
     1.8 +Lingeling is an efficient solver written in C. The JNI (Java Native Interface)
     1.9 +version of Lingeling is bundled with Kodkodi and is precompiled for the major
    1.10 +platforms. It is also available from the Kodkod web site \cite{kodkod-2009}. 
    1.11 +
    1.12 +\item[$\bullet$] \textbf{\textit{CryptoMiniSat}:} CryptoMiniSat is the winner of
    1.13 +the 2010 SAT Race. To use CryptoMiniSat, set the environment variable
    1.14 +\texttt{CRYPTO\-MINISAT\_}\discretionary{}{}{}\texttt{HOME} to the directory that contains the \texttt{crypto\-minisat}
    1.15 +executable.%
    1.16 +\footnote{Important note for Cygwin users: The path must be specified using
    1.17 +native Windows syntax. Make sure to escape backslashes properly.%
    1.18 +\label{cygwin-paths}}
    1.19 +The \cpp{} sources and executables for Crypto\-Mini\-Sat are available at
    1.20 +\url{http://planete.inrialpes.fr/~soos/}\allowbreak\url{CryptoMiniSat2/index.php}.
    1.21 +Nitpick has been tested with version 2.51.
    1.22 +
    1.23 +\item[$\bullet$] \textbf{\textit{CryptoMiniSat\_JNI}:} The JNI (Java Native
    1.24 +Interface) version of CryptoMiniSat is bundled with Kodkodi and is precompiled
    1.25 +for the major platforms. It is also available from the Kodkod web site
    1.26 +\cite{kodkod-2009}.
    1.27 +
    1.28  \item[$\bullet$] \textbf{\textit{MiniSat}:} MiniSat is an efficient solver
    1.29  written in \cpp{}. To use MiniSat, set the environment variable
    1.30  \texttt{MINISAT\_HOME} to the directory that contains the \texttt{minisat}
    1.31  executable.%
    1.32 -\footnote{Important note for Cygwin users: The path must be specified using
    1.33 -native Windows syntax. Make sure to escape backslashes properly.%
    1.34 -\label{cygwin-paths}}
    1.35 +\footref{cygwin-paths}
    1.36  The \cpp{} sources and executables for MiniSat are available at
    1.37  \url{http://minisat.se/MiniSat.html}. Nitpick has been tested with versions 1.14
    1.38 -and 2.0 beta (2007-07-21).
    1.39 -
    1.40 -\item[$\bullet$] \textbf{\textit{MiniSat\_JNI}:} The JNI (Java Native Interface)
    1.41 +and 2.2.
    1.42 +
    1.43 +\item[$\bullet$] \textbf{\textit{MiniSat\_JNI}:} The JNI
    1.44  version of MiniSat is bundled with Kodkodi and is precompiled for the major
    1.45 -platforms. It is also available from \texttt{native\-solver.\allowbreak tgz},
    1.46 -which you will find on Kodkod's web site \cite{kodkod-2009}. Unlike the standard
    1.47 -version of MiniSat, the JNI version can be used incrementally.
    1.48 -
    1.49 -\item[$\bullet$] \textbf{\textit{CryptoMiniSat}:} CryptoMiniSat is the winner of
    1.50 -the 2010 SAT Race. To use CryptoMiniSat, set the environment variable
    1.51 -\texttt{CRYPTO\-MINISAT\_}\discretionary{}{}{}\texttt{HOME} to the directory that contains the \texttt{crypto\-minisat}
    1.52 -executable.%
    1.53 -\footref{cygwin-paths}
    1.54 -The \cpp{} sources and executables for Crypto\-Mini\-Sat are available at
    1.55 -\url{http://planete.inrialpes.fr/~soos/}\allowbreak\url{CryptoMiniSat2/index.php}.
    1.56 -Nitpick has been tested with version 2.51.
    1.57 -
    1.58 -\item[$\bullet$] \textbf{\textit{PicoSAT}:} PicoSAT is an efficient solver
    1.59 -written in C. You can install a standard version of
    1.60 -PicoSAT and set the environment variable \texttt{PICOSAT\_HOME} to the directory
    1.61 -that contains the \texttt{picosat} executable.%
    1.62 -\footref{cygwin-paths}
    1.63 -The C sources for PicoSAT are
    1.64 -available at \url{http://fmv.jku.at/picosat/} and are also bundled with Kodkodi.
    1.65 -Nitpick has been tested with version 913.
    1.66 -
    1.67 -\item[$\bullet$] \textbf{\textit{zChaff}:} zChaff is an efficient solver written
    1.68 +platforms. It is also available from the Kodkod web site \cite{kodkod-2009}.
    1.69 +Unlike the standard version of MiniSat, the JNI version can be used
    1.70 +incrementally.
    1.71 +
    1.72 +\item[$\bullet$] \textbf{\textit{zChaff}:} zChaff is an older solver written
    1.73  in \cpp{}. To use zChaff, set the environment variable \texttt{ZCHAFF\_HOME} to
    1.74  the directory that contains the \texttt{zchaff} executable.%
    1.75  \footref{cygwin-paths}
    1.76 @@ -2407,14 +2408,6 @@
    1.77  executable.%
    1.78  \footref{cygwin-paths}
    1.79  
    1.80 -\item[$\bullet$] \textbf{\textit{Jerusat}:} Jerusat 1.3 is an efficient solver
    1.81 -written in C. To use Jerusat, set the environment variable
    1.82 -\texttt{JERUSAT\_HOME} to the directory that contains the \texttt{Jerusat1.3}
    1.83 -executable.%
    1.84 -\footref{cygwin-paths}
    1.85 -The C sources for Jerusat are available at
    1.86 -\url{http://www.cs.tau.ac.il/~ale1/Jerusat1.3.tgz}.
    1.87 -
    1.88  \item[$\bullet$] \textbf{\textit{SAT4J}:} SAT4J is a reasonably efficient solver
    1.89  written in Java that can be used incrementally. It is bundled with Kodkodi and
    1.90  requires no further installation or configuration steps. Do not attempt to