On efficient algorithms for SAT

Abstract

There are several papers in which SAT is solved in linear time by various new computing paradigms, and specially by various membrane computing systems. In these approaches the used alphabet depends on the number of variables. That gives different classes of the problem by the number of the variables.In this paper we show that the set of valid SAT-formulae and n-SAT-formulae over finite sets of variables are regular languages. We show a construction of deterministic finite automata which accept the SAT and n-SAT languages in conjunctive normal form checking both their syntax and satisfiable evaluations. Thus, theoretically the words of the SAT languages can be accepted in linear time with respect to their lengths by a traditional computer. © 2013 Springer-Verlag.