|
Рубрика:
Наука и технологии /
Раздел для научных публикаций
|
Facebook
Мой мир
Вконтакте
Одноклассники
Google+
|
Гданский Н.И.,
профессор кафедры прикладной математики и искусственного интеллекта института Информационных и вычислительных технологий, ФГБОУ ВО «Национальный исследовательский университет «МЭИ», Москва, РФ, al-kpp@mail.ru
Денисов А.А.,
аспирант, ФГБОУ ВО «Национальный исследовательский университет «МЭИ», Москва, РФ, aadenisov88@gmail.com
Декомпозиция конъюнктивных нормальных форм
в задаче выполнимости
Рассмотрены существующие методы декомпозиции конъюнктивных нормальных форм булевых функций. На основе их анализа предложен метод дистрибутивной декомпозиции формул КНФ
Введение
В задаче выполнимости булевых функций, которая заключается в поиске решений уравнения F = true, данные функции обычно представлены в виде конъюнктивной нормальной формы (КНФ) вида F = С1&С2&…&Сk. В ней дизъюнкты С1 - Сk являются логическими суммами литер – переменных или их отрицаний. Обозначим длины дизъюнктов С1 - Сk через l1 - lk.
Задача выполнимости КНФ является первой, для которой доказана NP-полнота [1]. Переход к задаче выполнимости является одним из наиболее эффективных подходов при автоматизации решения многих практических задач, таких как построения шаблонов [2, 3], автоматизация доказательства теорем [4], model checking [5], искусственный интеллект [6] и многих других.
<...>
Полную версию статьи читайте в журнале
Подпишитесь на журнал
Купите в Интернет-магазине
Facebook
Мой мир
Вконтакте
Одноклассники
Google+
|
Декомпозиция конъюнктивных нормальных форм в задаче выполнимости
