An algorithm for the SAT problem via inclusion-exclusion: SATINEX

This paper proposes an algorithm that decides the Satisfiability of any conjunctive formula #PHI# with k clauses on n variables. The method checks whether the number of models of the negation of #PHI# is strictly lower than 2"n. This counting is computed by using the inclusion-exclusion principle. We propose an elementary counting algorithm in time O(2"kn) that is improved after using combinatorial arguments. (orig.)SIGLEAvailable from TIB Hannover: RN 7886(98) / FIZ - Fachinformationszzentrum Karlsruhe / TIB - Technische InformationsbibliothekDEGerman