\newchapter{Introduction}

\leveldown{}

\epigraph{The SAT problem is evidently a killer app, because it is key to the solution of so many other problems.}
{Donald Knuth, 1974 ACM Turing Award Recipient, from The Art of Computer Programming, section 7.2.2.2}

\epigraph{The practical solving of SAT is a key technology for computer science in the 21st century}
{Edmund Clarke, 2007 ACM Turing Award Recipient}

\epigraph{The SAT problem is at the core of arguably the most fundamental question in computer science: What makes a problem hard?}
{Stephen Cook, 1982 ACM Turing Award Recipient}

\epigraph{Major progresses in logic may come from SAT}
{Moshe Vardi}

\myheading{What is this all about?}

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

\myheading{Praise}

See here: \url{https://smt.st}.

\myheading{As recommended reading at several universities}

For a list, see: \url{https://smt.st}.

\myheading{Thanks}

Armin Biere has patiently answered to my endless and 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/}},
Johannes Altmanninger\footnote{\url{https://github.com/krobelus}}
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}.

Helped with KLEE:
Cristian Cadar\footnote{\url{https://github.com/ccadar}},
Frank Busse\footnote{\url{https://github.com/251}}.

Chad Brewbaker,
Evan Wallace, 
Ben Gardiner,
and Wojciech Niedbala 
have fixed some bugs and made improvements.

Xing Shi Cai,
Arseny Nerinovsky,
Raphael Wimmer, 
Andrea Jemmett,
Jason Bucata
and Tom Chase
have found many bugs.

English grammar fixes: Priyanshu Jain, John Winston Garth.

Denis Fokin found a typo.

Martin Nyx Brain has helped with CBMC, etc.

\myheading{Disclaimer}

This collection is a non-academic reading for \textit{end-users},
i.e., programmers, etc.

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 a grain of salt...

Despite the fact there are many examples for Z3 SMT-solver,
the author of these lines is not affiliated with the Z3 team in any way...
Nor with any other SAT/SMT teams.

\myheading{Python}

Majority of code in the book is written in Python 3.
Basic understanding is recommended.

\myheading{Latest versions}

Latest version is always available at \url{https://smt.st/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{\RepoURL/ChangeLog}.

\myheading{Proofreaders wanted!}

You see how horrible my English is?
Please do not hesitate to drop me an email about my mistakes: dennis(@)yurichev.com.

\myheading{The source code}

Some people find it inconvenient to copy\&paste source code from this PDF.
You can get the source code here: \url{https://smt.st/src}.

\myheading{Subscribe to my news}

For news and updates, subscribe to my \href{https://yurichev.com/news/}{blog}\\
(\href{https://yurichev.com/news/rss.xml}{RSS}).\\
Also, subscribe to my
\href{https://groups.google.com/forum/#!forum/yurichev}{mailing list} by sending\\
an empty email to \textbf{yurichev+subscribe@googlegroups.com}\\

\myheading{Is it hype? Yet another fad?}

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

One significant step is GRASP SAT solver (1996)
\footnote{\url{https://www.cs.cmu.edu/~emc/15-820A/reading/grasp_iccad96.pdf}}, known as \ac{CDCL},
the next is Chaff (2001)
\footnote{\url{http://www.princeton.edu/~chaff/publication/DAC2001v56.pdf}}.

In 1999, a new paper proposed using SAT instead of BDD for symbolic model checking:
Armin Biere, Alessandro Cimatti, Edmund Clarke, Yunshan Zhu -- Symbolic Model Checking without BDDs
\footnote{\url{http://fmv.jku.at/papers/BiereCimattiClarkeZhu-TACAS99.pdf}}.
See also: \url{http://fmv.jku.at/biere/talks/Biere-CAV18Award-talk.pdf}.

SMT-LIB mailing list was created in 2002
\footnote{\url{https://cs.nyu.edu/pipermail/smt-lib/2002/}}.

Also, SAT/SMT are not special or unique.
There are adjacent area like ASP: Answer Set Programming.
CSP: Constraint Satisfaction Problems.
Also, Prolog programming language.

\myheading{Backward computation}

A nice definition from
\href{https://www.goodreads.com/book/show/388007.The_Elements_of_Artificial_Intelligence_Using_Common_LISP}{The Elements of Artificial Intelligence Using Common LISP by Steven L. Tanimoto}.

Of course, this is also true for SAT/SMT, CSP, etc...

<<Unlike other programming languages, Prolog makes it easy to compute functions ``backward.''>>

\myheading{Is this another programming language?}

There are folks who come from Haskell, Coq, other theorem provers.
There are folks who come from type theory, etc.
And sometimes they have a misconception that this is a \ac{PL} too.

No, it's not.
It's just a library/framework/API.

\myheading{Hacking/tinkering plan}

Where can you start hacking?

From easiest to hardest:

\begin{itemize}
\item CBMC examples.
CBMC\footnote{\url{http://www.cprover.org/cbmc/}} is easy to install.
Examples are in pure C, so anybody can hack them without additional training.
CBMC exists for Windows.

\item KLEE examples. Also in pure C, but KLEE is trickier to install, 
via docker\footnote{\url{https://klee.github.io/docker/}}...
No Windows supports, AFAIR.

\item Z3Py examples. These are for Z3 Python API. Only Python knowledge is required. Grep for "from z3 import *" in *.py files, these are for Z3Py.

\item SMT-LIB 2.x examples.
Lispy language, way less handy than Python, C++, C\#, etc...
But this language is \textit{distilled},
and not \textit{contaminated} by Python's (or C++'s) specific features,
operator overloading, etc, so there you can see a clear border between 
SMT API and API's implementation in specific \ac{PL}.

\item SAT examples. Low-level. Like assembly language -- hard to understand,
hard to use, but the most efficient way of using SAT solvers.
\end{itemize}

So grab \href{https://smt.st/src/}{the source code} for my book and start
tinkering...

\levelup{}