intro.tex

\section{Introduction}

\subsection{Disclaimer}

The author of these lines is no expert in SAT/SMT, by any means.
This is not a book, rather a student's notes.
Take it with grain of salt...

\subsection{Latest versions}

Latest version is always available at \url{http://yurichev.com/writings/SAT_SMT_by_example.pdf}.

Russian version has been dropped -- it's too hard for me to maintain two versions. Sorry.

New parts are appearing here from time to time, see: \url{https://github.com/DennisYurichev/SAT_SMT_by_example/blob/master/ChangeLog}.

\subsection{The source code}

Some people find it inconvenient to copy\&paste source code from this PDF.
Everything is available on GitHub: \url{https://github.com/DennisYurichev/SAT_SMT_by_example}.

\subsection{Thanks}

Armin Biere\footnote{\url{http://fmv.jku.at/biere/}} has patiently answered to my endless boring questions.

Leonardo Mendonça de Moura\footnote{\url{https://www.microsoft.com/en-us/research/people/leonardo/}},
Nikolaj Bjørner\footnote{\url{https://www.microsoft.com/en-us/research/people/nbjorner/}}
and Mate Soos\footnote{\url{https://www.msoos.org/}} have also helped.

Masahiro Sakai\footnote{\url{https://twitter.com/masahiro_sakai}} has helped with numberlink puzzle: \ref{numberlink}.

Alex ``clayrat'' Gryzlov and @mztropics on twitter found couple of bugs.

Xenia Galinskaya -- for carefully measured periods of forced distraction from the work.

\subsection{Praise}

``This is quite instructive for students. I will point my students to this!'' (Armin Biere).

``An excellent source of well-worked through and motivating examples of using Z3's python interface.''
\footnote{\url{https://github.com/Z3Prover/z3/wiki}}
(Nikolaj Bjorner, one of Z3's authors).

``Impressive collection of fun examples!''
(Pascal Fontaine\footnote{\url{https://members.loria.fr/PFontaine/}}, one of veriT solver's authors.)

\subsection{Introduction}

\ac{SAT}/\ac{SMT} solvers can be viewed as solvers of huge systems of equations.
The difference is that \ac{SMT} solvers takes systems in arbitrary format,
while \ac{SAT} solvers are limited to boolean equations in \ac{CNF} form.

A lot of real world problems can be represented as problems of solving system of equations.

\subsection{Is it a hype? Yet another fad?}

Some people say, this is just another hype.
No, \ac{SAT} is old enough and fundamental to \ac{CS}.
The reason of increased interest to it is that computers gets faster over the last couple decades,
so there are attempts to solve old problems using \ac{SAT}/\ac{SMT}, which were inaccessible in past.