On computing minimal equivalent subformulas

A propositional formula in Conjunctive Normal Form (CNF) may contain redundant clauses | clauses whose removal from the for- mula does not a ect the set of its models. Identi cation of redundant clauses is important because redundancy often leads to unnecessary com- putation, wasted storage, and may obscure the structure of the problem. A formula obtained by the removal of all redundant clauses from a given CNF formula F is called a Minimal Equivalent Subformula (MES) of F. This paper proposes a number of e cient algorithms and optimization techniques for the computation of MESes. Previous work on MES com- putation proposes a simple algorithm based on iterative application of the de nition of a redundant clause, similar to the well-known deletion- based approach for the computation of Minimal Unsatis able Subfor- mulas (MUSes). This paper observes that, in fact, most of the existing algorithms for the computation of MUSes can be adapted to the compu- tation of MESes. However, some of the optimization techniques that are crucial for the performance of the state-of-the-art MUS extractors cannot be applied in the context of MES computation, and thus the resulting algorithms are often not e cient in practice. To address the problem of e cient computation of MESes, the paper develops a new class of al- gorithms that are based on the iterative analysis of subsets of clauses. The experimental results, obtained on representative problem instances, con rm the e ectiveness of the proposed algorithms. The experimental results also reveal that many CNF instances obtained from the practical applications of SAT exhibit a large degree of redundancy.