Программа для решения трудных экземпляров проблемы булевой выполнимости с применением метода опорных векторов

Программа предназначена для решения трудных экземпляров проблемы булевой выполнимости (SAT). По данной на вход исходной булевой формуле в формате КНФ на первом этапе с помощью CDCL-решателя решается семейство простых SAT-задач, полученных с помощью подстановки в исходную КНФ случайных значений некоторого числа случайно выбранных переменных (от 10 до 100). На втором этапе осуществляется обучение линейной SVM-машины на конфликтных дизъюнктах, которые сгенерировал CDCL-решатель на первом этапе. При этом конфликтный дизъюнкт считается полезным, если он не был удален к моменту нахождения решения хотя бы одной задачи из семейства. На третьем этапе на короткий промежуток времени запускается CDCL-решатель, после чего с помощью обученной SVM-машины оценивается полезность всех сгенерированных конфликтных дизъюнктов. На четвертом этапе к исходной КНФ добавляются дизъюнкты, полезность которых была определена на третьем этапе, после чего на полученной КНФ запускается CDCL-решатель.