A new algorithm for the propositional satisfiability problem