Algorithm of Sub Exponential Complexity for the SAT Problem Solution

Abstract

The SAT problem is a task of satisfiability of a Boolean formula. The formula is considered satisfiable if it has a set of variables to satisfy it, i.e. a set of values for all variables which makes it true. In Russian it is known as the problems „выполнимость‟ (ВЫП). The problem finds practical application: in hard-and software verification of modern computers, in designing FPGA [2-6], in solving automated proving problems, linked with checking inconsistency of sets of disjunctions in propositional calculus. For example, complex rail infrastructure control processes including passenger traffic control, power supply of various objects, logic control of objects at stations and railway spans, and complex information transfer telecommunications subsystems between infrastructure objects require efficient solution to diagnose such objects, which is possible due to improvements in the mathematical apparatus used in fault detection systems part of which are methods to solve SAT problems.