forked from small-evil-beast/SAT_SMT_article
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathintro.tex
123 lines (79 loc) · 5.02 KB
/
intro.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
\chapter{Introduction}
\epigraph{The SAT problem is evidently a killer app, because it is key to the solution of so many other problems.}
{Donald Knuth, The Art of Computer Programming, section 7.2.2.2}
\section{What this is 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.
\section{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 developers).
``Impressive collection of fun examples!''
(Pascal Fontaine\footnote{\url{https://members.loria.fr/PFontaine/}}, one of veriT solver's developers.)
``This is a great book. I've been recommending it to the students in my SMT class, as it's (by far) the largest compendium of constraint satisfaction problems/solutions that I'm aware of, including tons of unique and obscure ones. Good work, Dennis!''
(Rolf Rolles\footnote{\url{https://twitter.com/rolfrolles/status/1005259729919193088}}.)
\section{Thanks}
Armin Biere\footnote{\url{http://fmv.jku.at/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/}}
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}.
Chad Brewbaker has fixed my job shop version: \ref{JobShop}.
Alex ``clayrat'' Gryzlov, @mztropics on twitter and Jason Bucata found couple of bugs.
Xenia Galinskaya: for carefully planned periods of forced distraction from the work.
English grammar fixes: Priyanshu Jain.
Evan Wallace fixed Minesweeper section.
\section{Disclaimer}
This collection is a non-academic reading for ``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 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...
\section{Python}
Majority of code in the book is written in Python.
\section{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{\GitHubBlobMasterURL/ChangeLog}.
\section{Proofreaders wanted!}
You see how horrible my English is?
Please do not hesitate to drop me an email about my mistakes:
dennis@yurichev.com.
Or even better, submit patch: \url{\GitHubURL}.
\iffalse
\section{Illustrator wanted}
... who can draw in the following manner:
\href{https://github.com/DennisYurichev/RE-for-beginners/blob/master/cover.jpg}{1},
\href{https://github.com/DennisYurichev/RE-for-beginners/blob/master/cover2.jpg}{2},
\href{https://github.com/DennisYurichev/RE-for-beginners/blob/master/cover3.jpg}{3},
\href{https://github.com/DennisYurichev/RE-for-beginners/blob/master/cover4.jpg}{4}.
... for this book, which is open-source and free, and unlikely to be published.
However, someone maybe interested, in a self-advertisement sense...
Please contact me: dennis@yurichev.com.
\fi
\section{The source code}
Some people find it inconvenient to copy\&paste source code from this PDF.
Everything is available on GitHub: \url{\GitHubURL}.
\section{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 for increased interest to 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},
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.