APPLICATION OF INCREMENTAL SATISFIABILITY PROBLEM SOLVERS FOR NON-DETERMINISTIC POLYNOMIAL-TIME HARD PROBLEMS AS ILLUSTRATED BY MINIMAL BOOLEAN FORMULA SYNTHESIS PROBLEM
Annotation
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.
Keywords
Постоянный URL
Articles in current issue
- APPLICATION OF INDUCED MECHANICAL STRESSES IN FORMATION OF SPHERICAL SURFACES OF INTERFERENCE MIRROR SUBSTRATES
SENSITIVITY VARIATION RESEARCH OF TILTED FIBER BRAGG GRATING DURING CHEMICAL ETCHING
- APLICATION FEATURES OF OPTICAL POLYMERS IN OPTICAL SYSTEMS DESIGN
- EFFECT OF PLANT EXTRACTS ON ACTIVITY OF STAPHYLOCOCCUS AUREUS BY ELECTROCHEMICAL BIOTESTING
- FAST MOTION ESTIMATION ALGORITHM FOR HEVC VIDEO CODEC
- METHOD OF JOINT CLUSTERING IN NETWORK AND CORRELATION SPACES
- CONCEPT OF DIGITAL TWINS AT LIFE CYCLE STAGES OF PRODUCTION SYSTEMS
- HYPERPARAMETER OPTIMIZATION BASED ON APRIORI AND A POSTERIORI KNOWLEDGE ABOUT CLASSIFICATION PROBLEM
- INFERRING OF REGULATORY NETWORKS FROM EXPRESSION DATA USING BAYESIAN NETWORKS
- DISTRIBUTION EVALUATION OF REFLECTIVE CHARACTERISTICS WITH QUASI-CONTINUOUS ULTRA-WIDEBAND PROBING SIGNAL
- ADAPTIVE PROBLEM OF EXTENDED REPRODUCTION WITH MINIMIZATION OF GENERALIZED COSTS
- PREDICTION OF REACTION CONDITIONS BY DEEP LEARNING TECHNIQUES
- MODELING OF VERTICAL LIGHT PIPES FOR DAYLIGHT ILLUMINATION OF INDOOR INDUSTRIAL BUILDINGS(in English)
- CONDITION EQUATION OF POLYMER FILAMENTS
- PREDICTION OF MECHANICAL PROPERTIES FOR ONE-DIMENSIONAL POLYMER STRUCTURES
- INDEPENDENT COMPONENT ANALYSIS FOR INITIAL APPROXIMATION DETERMINATION IN IDENTIFICATION OF ACTIVE MODULES IN BIOLOGICAL GRAPHS
- CLINICAL DECISIONSUPPORT SYSTEM WITH PROCESSING OF MULTIMODAL MEDICAL DATA FOR RADIOLOGIST EFFICIENCY IMPROVEMENT PRACTICE