ПРИМЕНЕНИЕ ИНКРЕМЕНТАЛЬНЫХ 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-трудных задач является целесообразным, поскольку позволяет уменьшить суммарное время решения задач по сравнению с использованием неинкрементального подхода.

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. 9^th 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. 3^rd 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. 21^st 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

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License