Усовершенствованный генератор 3-КНФ формул

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