ВходНаше всё Теги codebook PARTS Поиск Опросы Закон Вторник
4 августа
/845431
Evgeny_CD, Архитектор (02.06.2018 02:26 - 02:29, просмотров: 877)
[Satisfiability modulo theories, SMT, задача выполнимости формул в теориях] Мощнейший математический аппарат для формальной верификации ПО (в том числе). ссылка ссылка Есть классическая Зада́ча выполни́мости бу́левых фо́рмул (SAT) -> Экземпляром задачи SAT является булева формула, состоящая только из имен переменных, скобок и операций. Задача заключается в следующем: можно ли назначить всем переменным, встречающимся в формуле, значения ложь и истина так, чтобы формула стала истинной. В SMP народ расширил теорию до небулевых формул, чем сильно повысил компактность описания реальных задач. Также создана целая куча решателей этих формул и способы формального описания формул.
Ответить
Ответы