7 Weak Equivalence in Propositional Calculus

Abstract. The main purpose of this paper is to present a new algorithm (NEW-SAT) for deciding the (un)satisfiability of propositional formulae. It is based on a somehow dual (versus resolution) idea: we succesively add complementary literals to already obtained clauses instead of solving them. Hence, the unsatisfiability of a formula is detected by reaching “a complete set of maximal clauses ” instead of reaching the empty clause. Only weak (semantical) equivalence is preserved. In fact, although the strong equivalence is not preserved, we have something more than a simple weak equivalence. To be more precise, in case of satisfiability, the number of truth assignments is also preserved. Let LP be the propositional logic over the denumerable set of atomic formulae (propositional variables) V = {A1, A2,...}. A literal is an atomic formula (positive literal) or its negation (negative literal). For any litera