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


УДК 004.832.25

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

Чухарев К.И.


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

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


Аннотация
Предмет исследования. Рассмотрен метод решения 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.

Список литературы
1. Akshay S., Chakraborty S., Goel S., Kulal S., Shah S. What's hard about boolean functional synthesis? // Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2018. V. 10981. P. 251–269. doi: 10.1007/978-3-319-96145-3_14
2. Brayton R.K., Hachtel G.D., McMullen C.T., Sangiovanni-Vincentelli A.L. Logic Minimization Algorithms for VLSI Synthesis. Kluwer Academic Publishers, 1984. 206 p. doi: 10.1007/978-1-4613-2821-6
3. Fišer P., Kubátová H. Flexible two-level boolean minimizer BOOM-II and its applications // Proc. 9th EUROMICRO Conference on Digital System Design: : Architectures, Methods and Tools (DSD 2006). Dubrovnik, Croatia. 2006. P. 369–376. doi: 10.1109/DSD.2006.53
4. Biere A., Heule M., van Maaren H., Walsh T. Handbook of Satisfiability. IOS Press, 2009. 980 p.
5. Cook S.A. The complexity of theorem-proving procedures // Proc. 3rd Annual ACM Symposium on Theory of Computing. 1971. P. 151–158. doi: 10.1145/800157.805047
6. Marques Silva J.P., Sakallah K.A. GRASP - A new search algorithm for satisfiability // Proc. IEEE/ACM International Conference on Computer-Aided Design. 1996. P. 220–227. doi: 10.1109/ICCAD.1996.569607
7. Ulyantsev V., Zakirzyanov I., Shalyto A. BFS-based symmetry breaking predicates for DFA identification // Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2015. V. 8977. P. 611–622. doi: 10.1007/978-3-319-15579-1_48
8. Tseitin G.S. On the complexity of derivation in propositional calculus // Automation of Reasoning: 2: Classical Papers on Computational Logic. Berlin: Springer Berlin Heidelberg, 1983. P. 466–483. doi: 10.1007/978-3-642-81955-1_28
9. Biere A. PicoSAT Essentials // Journal on Satisfiability, Boolean Modeling and Computation. 2008. V. 4. N 2-4. P. 75–97. doi: 10.3233/sat190039
10. Eén N., Sörensson N. An extensible SAT-solver // Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2004. V. 2919. P. 502–518. doi: 10.1007/978-3-540-24605-3_37
11. Audemard G., Simon L. Predicting learnt clauses quality in modern SAT solvers // Proc. 21st International Joint Conference on Artifical Intelligence (IJCAI 2009). 2009. P. 399–404.
12. Soos M., Nohl K., Castelluccia C. Extending SAT solvers to cryptographic problems // Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2009. V. 5584. P. 244–257. doi: 10.1007/978-3-642-02777-2_24
13. Walsh T. SAT v CSP // Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2000. V. 1894. P. 441–456. doi: 10.1007/3-540-45349-0_32
14. Nguyen V.-H., Mai S.T. A new method to encode the at-most-one constraint into SAT // ACM International Conference Proceeding Series. 2015. P. 46–53. doi: 10.1145/2833258.2833293
15. Björk M. Successful SAT encoding techniques // Journal on Satisfiability, Boolean Modeling and Computation. 2011. V. 7. N 4. P. 189–201. doi: 10.3233/SAT190085
16. Petke J., Jeavons P. The order encoding: From tractable CSP to tractable SAT // Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2011. V. 6695. P. 371–372. doi: 10.1007/978-3-642-21581-0_34


Creative Commons License

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

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