Investigation of the application of the algorithm of subexponential complexity for solving the SAT problem in the case of an unsolvable problem

Abstract

Nowadays, the transition to a new element base of control systems is underway in railway transport. Their design includes the solution of the Boolean formulas feasibility problem (SAT problem). The peculiarity of solving this problem in control systems is finding a solution in realtime. In this paper, the possibility of improving the process of designing control systems based on Boolean functions using the algorithm of subexponential complexity of solving the SAT problem [1] for the case of an infeasibility function.