Страница публикации

Использование метода опорных векторов для оценки полезности конфликтных дизъюнктов в CDCL-выводе

Авторы: Заикин О.С., Кочемазов С.Е.

Журнал: International Journal of Open Information Technologies

Том: 7

Номер: 12

Год: 2019

Отчётный год: 2020

Издательство:

Местоположение издательства:

URL:

Аннотация: Многие современные алгоритмы для решения проблемы булевой выполнимости (SAT) основаны на алгоритме CDCL. В процессе своей работы они генерируют большое количество т. н. конфликтных дизъюнктов, соответствующих пройденным ветвям дерева возможных решений. Часть конфликтных дизъюнктов необходимо время от времени удалять, чтобы поддерживать высокую скорость работы алгоритма. Таким образом, возникает задача оценки полезности конфликтных дизъюнктов, чтобы выявить какие из них оставлять, а какие нет. В настоящем исследовании для решения этой задачи предложена эвристика, основанная на использовании метода опорных векторов. На первом этапе формируется семейство упрощенных версий исходной SAT-задачи, затем они решаются с помощью SAT-решателя. На втором этапе осуществляется обучение машины опорных векторов, при этом конфликтный дизъюнкт считается полезным, если он не был удален к моменту нахождения решения хотя бы одной задачи из семейства. На третьем этапе при решении исходной SAT-задачи полезность некоторых дизъюнктов оценивается с помощью обученной машины опорных векторов. Базируясь на предложенной эвристике, был реализован модифицированный вариант одного из современных SAT-решателей, основанного на CDCL. Согласно проведенным вычислительным экспериментам, модифицированная версия решателя работает эффективнее оригинала на нескольких семействах сложных экземпляров SAT.

Индексируется WOS: 0

Индексируется Scopus: 0

Индексируется РИНЦ: 1

Публикация в печати: 0

Добавил в систему: