A decomposition based algorithm for maximal contractions

This paper proposes a decomposition based algorithm for revision problems in classical propositional logic. A set of decomposing rules are presented to analyze the satisfiability of formulas. The satisfiability of a formula is equivalent to the satisfiability of a set of literal sets. A decomposing function is constructed to calculate all satisfiable literal sets of a given formula. When expressing the satisfiability of a formula, these literal sets are equivalent to all satisfied models of such formula. A revision algorithm based on this decomposing function is proposed, which can calculate maximal contractions of a given problem. In order to reduce the memory requirement, a filter function is introduced. The improved algorithm has a good performance in both time and space perspectives.