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

• Main Author: Konstantin I. Chukharev
• Format: Article
• Language: English
• Published: Saint Petersburg National Research University of Information Technologies, Mechanics and Optics (ITMO University) 2020-12-01
• Series: Naučno-tehničeskij Vestnik Informacionnyh Tehnologij, Mehaniki i Optiki
• Subjects: satisfiability problem (sat); incremental satisfiability problem (sat) solvers; non-deterministic polynomial-time (np) hard problems; constraint programming; boolean formula synthesis; tseytin transformations; symmetry breaking; kotlin; framework; java native interface
• Online Access: https://ntv.ifmo.ru/file/article/20008.pdf

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 SAT-formula 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.