Propositional Satisfiability (SAT) as a language problem

We present an approach to propositional satisfiability as a Finite State Automata automata construction problem. From a theoretical point of view it has consequences for languages beyond context free power. There are no consequences on complexity issues due to Automata construction (using intersection) is PSPACE-complete. From a practical point of view it was shown that this approach is competitive with ALL-SAT approaches and even with state of the art SAT solvers on traditional hard problems. Here, we show that techniques used in DPLL can be used in an automata approach. This kind of approach opens a new path of research on propositional satisfiability. Presentado en el II Workshop Aspectos Teóricos de Ciencia de la Computación (WATCC) Red de Universidades con Carreras en Informática (RedUNCI)