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

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

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

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

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

Помимо этого веду цифровой Zettelkasten в Obsidian и экспериментирую с интеграцией LLM, исследуя новые подходы к работе с информацией и идеями.

Разработал opensource плагин для Pycharm — GlossaryGuru.
  • Никита Борсов
    Разработчик, Райффайзен банк
    Инженер-исследователь и Python-энтузиаст. Использую Python во всём его разнообразии: от backend-сервисов и инструментов автоматизации до анализа данных и машинного обучения. В центре моих интересов формальные методы и логическое моделирование: изучаю, как выражать сложные условия и проверять их корректность на уровне кода и архитектуры.

    Помимо этого веду цифровой Zettelkasten в Obsidian и экспериментирую с интеграцией LLM, исследуя новые подходы к работе с информацией и идеями.

    Разработал opensource плагин для Pycharm — GlossaryGuru.
Все доклады трека