Название: SAT/SMT by Example
Автор: Dennis Yurichev / Денис Юричев
Издательство: Интернет-издание
Год: версия от 27.11.2020
Страниц: 593
Язык: английский
Формат: pdf (true)
Размер: 12.7 MB

SAT/SMT solvers can be viewed as solvers of huge systems of equations. The difference is that SMT solvers takes systems in arbitrary format, while SAT solvers are limited to boolean equations in CNF form. A lot of real world problems can be represented as problems of solving system of equations. Majority of code in the book is written in Python. This collection is a non-academic reading for “end-users”, i.e., programmers, etc.

Some people say, this is just another hype. No, SAT is old enough and fundamental to Computer Science (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 SAT/SMT, which were inaccessible in past.

SMT vs. SAT is like high level Programming Language vs. assembly language. The latter can be much more efficient, but it’s hard to program in it. SAT is abbreviation of “Boolean satisfiability problem”. The problem is to find such a set of variables, which, if plugged into boolean expression, will result in “true”.

Python (and other high-level Programming Language's like C#) interface is highly popular, because it’s practical, but in fact, there is a standard language for SMT-solvers called SMT-LIB. So when you look back to my Python code, you may feel that these 3 expressions could be executed. This is not true: Z3Py API offers overloaded operators, so expressions are constructed and passed into the guts of Z3 without any execution. I would call it “embedded DSL”. Same thing for Z3 C++ API, you may find there “operator+” declarations and many more. Z3 API 7 s for Java, ML and .NET are also exist.

"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

"The practical solving of SAT is a key technology for computer science in the 21st century" -Edmund Clarke