APPLICATION OF INCREMENTAL SATISFIABILITY PROBLEM SOLVERS FOR NON-DETERMINISTIC POLYNOMIAL-TIME HARD PROBLEMS AS ILLUSTRATED BY MINIMAL BOOLEAN FORMULA SYNTHESIS PROBLEM

Chukharev K.I. Application of incremental satisfiability problem solvers for non-deterministic polynomial-time hard problems as illustrated by minimal Boolean formula synthesis problem. Scientific and Technical Journal of Information Technologies, Mechanics and Optics, 2020, vol. 20, no. 6, pp. 841-847 (in Russian). doi: 10.17586/2226-1494-2020-20-6-841-847

Subject of Research. The paper considers a method for solution of the nondeterministic polynomial hard problem (NP-hard problem) of a minimal Boolean formula synthesis from a given truth table. The solution of this problem is proposed based on its reduction to the Boolean satisfiability problem (SAT). The issues of efficient and convenient software implementation are discussed for reducing nondeterministic polynomial hard problems to the satisfiability problem. Method. For a minimal Boolean formula synthesis, the constraint programming approach was used: a SATformula was created for a given truth table, satisfiable if and only if, there exists a Boolean formula of a given size that satisfies the given truth table. The developed method accent is the application of incremental satisfiability problem solvers. Main Results. A method is proposed for synthesis of a Boolean formula, minimal with respect to the number of operators and terminals, for a given truth table. The method is based on reducing to satisfiability problem and provides the usage of incremental satisfiability problem solvers. The kotlin-satlib framework is developed with the possibility to use the Kotlin and Java languages effectively and conveniently for the software implementation of reducing various nondeterministic polynomial-time hard problems to satisfiability problem. Native interaction with satisfiability problem solvers by Java Native Interface (JNI) technology is used. The proposed method for the minimal Boolean formula synthesis is implemented in the Kotlin programming language using the developed kotlin-satlib framework. Practical Relevance. An experimental study on the example of minimal Boolean formula synthesis has shown that the usage of incremental satisfiability problem solvers for nondeterministic polynomial hard problems is reasonable, since it reduces the total solving time in comparison with the non-incremental approach application.

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, vol. 10981, pp. 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, pp. 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, pp. 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, pp. 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, vol. 8977, pp. 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, pp. 466–483. doi: 10.1007/978-3-642-81955-1_28

9. Biere A. PicoSAT Essentials. Journal on Satisfiability, Boolean Modeling and Computation, 2008, vol. 4, no. 2-4, pp. 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, vol. 2919, pp. 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, pp. 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, vol. 5584, pp. 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, vol. 1894, pp. 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, pp. 46–53. doi: 10.1145/2833258.2833293

15. Björk M. Successful SAT encoding techniques. Journal on Satisfiability, Boolean Modeling and Computation, 2011, vol. 7, no. 4, pp. 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, vol. 6695, pp. 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