Аннотация:
Рассматривается задача выполнимости (SAT-problem) булевых формул, заданных в конъюнктивной нормальной форме с ограничением, что каждый дизъюнкт содержит по три литерала переменных (3-КНФ). В эмпирических исследованиях широко используется генерация случайных формул с фиксированной длиной дизъюнкта. Феноменом этого метода является многократно подтвержденная линейная зависимость числа дизъюнктов формулы от числа булевых переменных в точке «фазового перехода» — от статуса выполнимых к статусу невыполнимых (когда доля невыполнимых формул становится превалирующей). Предложен и исследован метод генерации случайных формул, имеющий меньший коэффициент (3,49) пропорциональности между числом дизъюнктов и числом переменных в точке «фазового перехода» (для известного метода генерации этот коэффициент равен 4,23).
Ключевые слова:
задача выполнимости (SAT-problem), конъюнктивная нормальная форма (КНФ), дизъюнкт, литерал, булевы переменные.
Статья представлена к публикации членом редколлегии:А. А. Лазарев
Поступила в редакцию: 06.10.2017 После доработки: 15.04.2019 Принята к публикации: 18.07.2019