Если вы никогда не работали с SMT-солверами, вы не одиноки. Несмотря на то, что эти инструменты не часто встречаются в практике Python-специалистов, они способны формулировать и решать задачи там, где обычный код буквально бессилен.
В рамках этого доклада я познакомлю вас с основами SMT и покажу, каким мощным и незаменимым может быть этот инструмент. Также разберёмся с масштабируемостью: сколько переменных, логических связей и условий способен выдержать солвер, прежде чем перестанет справляться.
Доклад будет полезен всем, кому интересны поиск решений в пространствах высокого уровня сложности, а также инструменты на стыке логики и кода.