intro_RU.tex

\section{Отказ от ответственности}

Автор этих строк ни в какой мере не является экспертом в SAT/SMT.
Это не сколько книга, сколько студенческий конспект.
Воспринимайте её с разумной долей сомнения...

\section{Последняя версия}

Последняя версия всегда доступна на \url{http://yurichev.com/writings/SAT_SMT_draft-RU.pdf}.
Англоязычная версия: \url{http://yurichev.com/writings/SAT_SMT_draft-EN.pdf}.

Время от времени здесь появляется что-то новое, см: \url{https://github.com/DennisYurichev/SAT_SMT_article/blob/master/ChangeLog}.

\section{Благодарности}

Armin Biere\footnote{\url{http://fmv.jku.at/biere/}} долго и терпеливо отвечал на мои скучные вопросы.

Также помогали:
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/}},
Mate Soos\footnote{\url{https://www.msoos.org/}}.

Masahiro Sakai\footnote{\url{https://twitter.com/masahiro_sakai}} помог с головоломкой numberlink.
% TODO \ref

Алекс ``clayrat'' Грызлов и @mztropics в твиттере нашли пару ошибок.

Ксения Галинская -- за тщательно выверенные периоды вынужденного отвлечения от работы.

\section{Отзывы}

``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, один из авторов Z3).

``Impressive collection of fun examples!''
(Pascal Fontaine\footnote{\url{https://members.loria.fr/PFontaine/}}, один из авторов veriT solver.)

\section{Введение}

\ac{SAT}/\ac{SMT} солверы можно рассматривать как солверы огромных систем уравнений.
Разница в том, что \ac{SMT}-солверы берут системы в произвольном формате,
в то время как \ac{SAT}-солверы ограничены булевыми уравнениями вида \ac{CNF}.

Огромное количество проблем их практики можно представить как проблемы решения систем уравнений.

\section{Это хайп? Очередная мода?}

Некоторые люди говорят, что это очередной хайп.
Нет, \ac{SAT} достаточно стар, чтобы быть фундаментальным в \ac{CS}.
Причина повышенного интереса в том, что компьютеры стали работать быстрее,
так что теперь больше попыток решать старые проблемы используя 
\ac{SAT}/\ac{SMT}, которые раннее были недоступны.