New algorithms for testing the satisfiability of propositional formulae