Un algoritmo numérico para problemas de satisfacción booleana sin álgebra

Abstract

Con un método novedoso de resolución para el clásico problema de decisión de Satisfacción Booleana (SAT) formulado con cláusulas CNF se describen algoritmos que permiten determinar cuando una formula pertenece al lenguaje SAT, o no pertenece, sin recurrir al álgebra. El método se basa en la clase especial de problemas SAT, que denominamos Simple SAT (SSAT). El resultado es un algoritmo numérico computable en la base binaria cuya complejidad es lineal con respecto al numero de cláusulas mas un proceso de datos sobre las soluciones parciales y que esta acotado por a lo mas 2n−1 iteraciones. Se presentan resultados teóricos de la conmutabilidad y de la complejidad de los algoritmos similares o mejores a los del estado del arte para resolver SAT.