APPLICATION OF INCREMENTAL SATISFIABILITY PROBLEM SOLVERS FOR NON-DETERMINISTIC POLYNOMIAL-TIME HARD PROBLEMS AS ILLUSTRATED BY MINIMAL BOOLEAN FORMULA SYNTHESIS PROBLEM
Journal: Scientific and Technical Journal of Information Technologies, Mechanics and Optics (Vol.20, No. 6)Publication Date: 2020-12-03
Authors : Chukharev K.I.;
Page : 841-847
Keywords : satisfiability problem (SAT); incremental satisfiability problem (SAT) solvers; non-deterministic polynomial-time (NP) hard problems; Tseytin transformations; symmetry breaking; Kotlin; framework; Java Native Interface;
Abstract
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.
Other Latest Articles
- INFERRING OF REGULATORY NETWORKS FROM EXPRESSION DATA USING BAYESIAN NETWORKS
- HYPERPARAMETER OPTIMIZATION BASED ON A PRIORI AND A POSTERIORI KNOWLEDGE ABOUT CLASSIFICATION PROBLEM
- CONCEPT OF DIGITAL TWINS AT LIFE CYCLE STAGES OF PRODUCTION SYSTEMS
- METHOD OF JOINT CLUSTERING IN NETWORK AND CORRELATION SPACES
- FAST MOTION ESTIMATION ALGORITHM FOR HEVC VIDEO CODEC
Last modified: 2020-12-05 01:20:20