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

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

Тип публикации: Статья в журнале

Тип материала: Текст

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

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

Язык публикации: russian

Том: 7

Номера страниц: 5-10

Количество страниц: 6

Номер: 12

Год публикации: 2019

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

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

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

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

Индексируется УБС: Нет

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

Индексируется ВАК: Нет

Индексируется CORE: Нет