.png){kind=icon}
返回
Algorithms for computing minimal equivalent subformulas
.png){kind=icon}
OA
AI
DOI：10.1016/j.artint.2014.07.011.png)
.png){kind=icon}
.png){kind=icon}
分享.png){kind=icon}
收藏
摘要
En 中文
Knowledge representation and reasoning using propositional logic is an important component of AI systems. A propositional formula in Conjunctive Normal Form (CNF) may contain redundant clauses - clauses whose removal from the formula does not affect the set of its models. Identification of redundant clauses is important because redundancy often leads to unnecessary computation, 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 called a Minimal Equivalent Subformula (MES) of F. This paper proposes a number of efficient algorithms and optimization techniques for the computation of MESes. Previous work on MES computation proposes a simple algorithm based on iterative application of the definition of a redundant clause, similar to the well-known deletion-based approach for the computation of Minimal Unsatisfiable Subformulas (MUSes). This paper observes that, in fact, most of the existing algorithms for the computation of MUSes can be adapted to the computation 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 efficient in practice. To address the problem of efficient computation of MESes, the paper develops a new class of algorithms that are based on the iterative analysis of subsets of clauses, and a lightweight pruning technique based on the computation of backbones. The experimental results, obtained on representative problem instances, confirm the effectiveness of the proposed methods. The experimental results also reveal that many CNF instances obtained from the practical applications of SAT exhibit a large degree of redundancy. (C) 2014 Elsevier B.V. All rights reserved.
Keyword:
Boolean satisfiability
Redundancy
Irredundant subformula
Minimal unsatisfiability
AI总结
对已上传原文的论文进行重点信息的提取，主要内容包括：简要概述、研究摘要、背景介绍、关键亮点、图文解析、展望与总结。
期刊
IF:
13.9
论文数:
6.1K
被引数:
1.9W
机构
引用论文
.png){kind=icon}
分享收藏分享收藏
查看更多内容