SAT-задача, или задача выполнимости булевых формул, является фундаментальной в информатике - она является первой задачей, для которой удалось доказать ее принадлежность к классу NP-полных задач (при формулировке задачи в форме КНФ = 1), имеет широкое применение в ряде областей, включая искусственный интеллект, верификацию программного обеспечения, криптографию, проектирование интегральных схем [1].
На текущий момент лидирующим подходом решения SAT-задачи является CDCL (Conflict Driven Clause Learning), в основе которого лежит классический алгоритм DPLL, и основная идея которого состоит в анализе встречаемых «конфликтов» в ходе решения и добавления новых искусственно сконструированных дизъюнктов в исходную КНФ, отражающих в себе информацию о соответствующих конфликтах, позволяющую в дальнейшем поиске их избегать [1].
В ряде практических задач возникает необходимость в решении смежной задачи - задачи нахождения корня как можно меньшего ранга логического уравнения вида КНФ = 1 (минимизации корня уравнения КНФ = 1).
Так, например, построение тестовых наборов для неисправности схемы в [2] сводится к поиску допустимых интервалов некоторой КНФ, где проверяющий тест задается набором таких интервалов (конъюнкций). При этом чем меньше их ранг, тем больше возможностей для сокращения длины проверяющего теста, что является предпочтительным.
В сравнении с задачей выполнимости булевых формул количество научных работ, рассматривающих эту расширенную задачу, существенно меньше. Из них можно обратить внимание на [3], где предложена модификация алгоритма Закревского с детерминированной эвристикой ветвления, направленной на сокращение ранга искомого корня.
В данной дипломной работе разработан метод поиска корня как можно меньшего ранга логического уравнения вида КНФ = 1, в основу которого взят модифицированный алгоритм CDCL со стохастической эвристикой ветвления основанной на предложенной в [3].
В целях исследования работы предлагаемого алгоритма и сравнения его с существующим методом [3] был реализован «решатель» (программная реализация), поддерживающий оба метода, и обладающий относительно простым программным интерфейсом, позволяющим заменять эвристику ветвления, условие останова, механизм поиска (DPLL, CDCL) и другие параметры поиска.
В данной работе была рассмотрена задача минимизации корня логического уравнения КНФ = 1, а также смежная с ней задача выполнимости булевых формул в формулировке КНФ.
Был изучен один из существующих методов поиска допустимого интервала КНФ как можно меньшего ранга, основанный на алгоритме Закревского. Были выявлены несколько недостатков этого метода.
На основе этого анализа был разработан метод поиска корня как можно меньшего ранга логического уравнения КНФ = 1, представляющий собой модифицированный алгоритм CDCL с рестартами и стохастической эвристикой ветвления.
Разработанный метод был реализован на языке С++, его эффективность в сравнении с предыдущим методом показана экспериментально (на рассмотренных бенчмарках).
Реализованный «решатель» (программная реализация) поддерживает оба из рассмотренных методов и имеет относительно простой программный интерфейс, позволяющий заменять эвристику ветвления, условие останова, механизм поиска (DPLL, CDCL) и другие параметры поиска, что делает его применимым для дальнейших исследований в данном направлении.
