Оптимізація алгоритму субекспоненціальної складності для розв’язання SAT задачі

Abstract

UA: При модернізації і створенні сучасних систем управління на залізничному транспорті створюються оптоелектронні аналоги електромагнітних реле. При їх побудові виникає необхідність розв’язання в реальному часі задачі здійсненності бу́ левих фо́рмул (SAT задача). В даній роботі для SAT задачі запропоновано алгоритм субекспоненціальної складності, який визначає, чи здійсненна функція, а також процедура, що дозволяє перерахувати всі набори змінних, на яких булева функція здійсненна за субекспоненціальний час.

EN: During the modernization and creation of modern control systems on railway transport, new modern optoelectronic analogues of electromagnetic relays are being created. When constructing them, it becomes necessary to model the interaction of nodes. To this end, Boolean functions of algebra-logic are constructed, which can be of a high degree of complexity and contain a large number of clauses. Further, there arises the need to solve the Boolean satisfiability problem in real time (SAT task), and in the case of the feasibility of the task it is additionally necessary to specify all the sets of variables for which it is true. The algorithms described in the literature at the present time have an exponential dependence of complexity on the number of changes and complexity of the function, and accordingly the execution time increases exponentially with the complexity of the function. In this paper, a subexponential complexity algorithm for the SAT task, which determines whether a function is feasible is proposed, and also a procedure that allows you to enumerate all sets of variables under which the Boolean function being analyzed can be realized for subexponential time. This makes it possible to achieve a significant gain in time with Boolean functions with a large number of changes and clauses.