University of Limerick
Browse
Belov_2012_computing.pdf (870.2 kB)

On computing minimal equivalent subformulas

Download (870.2 kB)
conference contribution
posted on 2013-01-02, 10:19 authored by Anton Belov, Mikolas Janota, Inês Lynce, Joao Marques-Silva
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.

History

Publication

18th International Conference on Principles and Practice of Constraint Programming (CP 2012). Lecture Notes in Computer Science;pp. 158-174

Publisher

Springer

Note

peer-reviewed

Other Funding information

SFI

Rights

The original publication is available at www.springerlink.com

Language

English

Usage metrics

    University of Limerick

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC