doi: 10.17586/2226-1494-2020-20-6-


УДК 004.832.25

ПРИМЕНЕНИЕ ИНКРЕМЕНТАЛЬНЫХ SAT-РЕШАТЕЛЕЙ ДЛЯ РЕШЕНИЯ NP-ТРУДНЫХ ЗАДАЧ НА ПРИМЕРЕ ЗАДАЧИ СИНТЕЗА МИНИМАЛЬНЫХ БУЛЕВЫХ ФОРМУЛ

Чухарев К.И.


Читать статью полностью 
Язык статьи - русский

Ссылка для цитирования:
Чухарев К.И. Применение инкрементальных SAT-решателей для решения NP-трудных задач на примере задачи синтеза минимальных булевых формул // Научно-технический вестник информационных технологий, механики и оптики. 2020. Т. 20. № 6. С. doi: 10.17586/2226-1494-2020-20-6-


Аннотация
Предмет исследования. Рассмотрен метод решения NP-трудной задачи синтеза минимальной булевой формулы по заданной таблице истинности. Предложено решение указанной задачи, основанное на ее сведении к задаче выполнимости булевой формулы (SAT). Рассмотрены вопросы эффективной и удобной программной реализации сведений NP-трудных задач к SAT. Метод. Для решения задачи синтеза минимальной булевой формулы используется подход программирования в ограничениях: для заданной таблицы истинности строится SAT-формула, выполнимая тогда и только тогда, когда существует искомая булева формула заданного размера, удовлетворяющая заданной таблице. Отличительной особенностью разработанного метода является возможность использования инкрементальных программных средств для решения SAT (SAT-решателей). Основные результаты. Предложен метод синтеза минимальной по числу операторов и терминалов булевой формулы по заданной таблице истинности. Метод основан на сведении к SAT и позволяет использовать инкрементальные SAT-решатели. Разработан фреймворк kotlin-satlib, позволяющий эффективно и удобно использовать языки Kotlin и Java для программной реализации сведения различных NP-трудных задач к SAT, пользуясь нативным взаимодействием с SAT-решателями посредством технологии JNI. Предложенный метод синтеза минимальной булевой формулы реализован на языке программирования Kotlin с использованием разработанного фреймворка kotlin-satlib. Практическая значимость. Экспериментальное исследование на примере синтеза минимальной булевой формулы показало, что использование инкрементальных SAT-решателей для решения NP-трудных задач является целесообразным, поскольку позволяет уменьшить суммарное время решения задач по сравнению с использованием неинкрементального подхода.

Ключевые слова: задача выполнимости SAT, инкрементальные SAT-решатели, NP-трудные задачи, программирование в ограничениях, синтез булевых формул, преобразования Цейтина, нарушение симметрии, Kotlin, фреймворк, Java Native Interface

Благодарности. Исследование выполнено при финансовой поддержке JetBrains Research.

Creative Commons License

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License
Информация 2001-2020 ©
Научно-технический вестник информационных технологий, механики и оптики.
Все права защищены.

Яндекс.Метрика