Пороги для задачи выполнимости случайной k-КНФ: различия между версиями

SAT-решатели (программы для решения задачи выполнимости булевых формул) применяются, в частности, в таких областях, как верификация последовательных цепей, искусственный интеллект, автоматическое вычисление и планирование, СБИС, САПР, проверка моделей и другие виды формальной верификации. Недавно автоматические методы проверки моделей на основе SAT начали использоваться для эффективного поиска атак на протоколы безопасности.