arXiv cs/02110312002-11-22cs.AIcs.CC

Redundancy in Logic I: CNF Propositional Formulae

Paolo Liberatore

备注：: Extended and revised version of a paper that has been presented at ECAI 2002
DOI：: 10.1016/j.artint.2004.11.002

英文摘要：

A knowledge base is redundant if it contains parts that can be inferred from the rest of it. We study the problem of checking whether a CNF formula (a set of clauses) is redundant, that is, it contains clauses that can be derived from the other ones. Any CNF formula can be made irredundant by deleting some of its clauses: what results is an irredundant equivalent subset (I.E.S.) We study the complexity of some related problems: verification, checking existence of a I.E.S. with a given size, checking necessary and possible presence of clauses in I.E.S.'s, and uniqueness. We also consider the problem of redundancy with different definitions of equivalence.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

Mining to Compact CNF Propositional Formulae

CRIL - CNRS, University of Artois（CRIL - 法国国家科学研究中心，阿图瓦大学）

In this paper, we propose a first application of data mining techniques to propositional satisfiability. Our proposed Mining4SAT approach aims to discover and to exploit hidden structural knowledge for reducing the size of propositional formulae in conjunctive normal form (CNF). Mining4SAT combines both frequent itemset mining techniques and Tseitin's encoding for a compact representation of CNF formulae. The experiments of our Mining4SAT approach show interesting reductions of the sizes of many application instances taken from the last SAT competitions.

2013-04-16cs.AI

On Forgetting in Tractable Propositional Fragments

Guizhou University（贵州大学）

Distilling from a knowledge base only the part that is relevant to a subset of alphabet, which is recognized as forgetting, has attracted extensive interests in AI community. In standard propositional logic, a general algorithm of forgetting and its computation-oriented investigation in various fragments whose satisfiability are tractable are still lacking. The paper aims at filling the gap. After exploring some basic properties of forgetting in propositional logic, we present a resolution-based algorithm of forgetting for CNF fragment, and some complexity results about forgetting in Horn, ren…

2015-02-10cs.AI

Redundancy in Logic II: 2CNF and Horn Propositional Formulae

We report complexity results about redundancy of formulae in 2CNF form. We first consider the problem of checking redundancy and show some algorithms that are slightly better than the trivial one. We then analyze problems related to finding irredundant equivalent subsets (I.E.S.) of a given set. The concept of cyclicity proved to be relevant to the complexity of these problems. Some results about Horn formulae are also shown.

2005-06-21cs.AIcs.LO

Generalizing Redundancy in Propositional Logic: Foundations and Hitting Sets Duality

University College Dublin（都柏林大学学院）；IST/INESC-ID（里斯本高等理工学院/葡萄牙国家系统与计算机工程研究所）

Detection and elimination of redundant clauses from propositional formulas in Conjunctive Normal Form (CNF) is a fundamental problem with numerous application domains, including AI, and has been the subject of extensive research. Moreover, a number of recent applications motivated various extensions of this problem. For example, unsatisfiable formulas partitioned into disjoint subsets of clauses (so-called groups) often need to be simplified by removing redundant groups, or may contain redundant variables, rather than clauses. In this report we present a generalized theoretical framework of la…

2012-07-10cs.AIcs.LO

The Good Old Davis-Putnam Procedure Helps Counting Models

As was shown recently, many important AI problems require counting the number of models of propositional formulas. The problem of counting models of such formulas is, according to present knowledge, computationally intractable in a worst case. Based on the Davis-Putnam procedure, we present an algorithm, CDP, that computes the exact number of models of a propositional CNF or DNF formula F. Let m and n be the number of clauses and variables of F, respectively, and let p denote the probability that a literal l of F occurs in a clause C of F, then the average running time of CDP is shown to be O(…

2011-06-01cs.AI

Local Backbones

Vienna University of Technology（维也纳工业大学）；DePaul University（德保罗大学）

A backbone of a propositional CNF formula is a variable whose truth value is the same in every truth assignment that satisfies the formula. The notion of backbones for CNF formulas has been studied in various contexts. In this paper, we introduce local variants of backbones, and study the computational complexity of detecting them. In particular, we consider k-backbones, which are backbones for sub-formulas consisting of at most k clauses, and iterative k-backbones, which are backbones that result after repeated instantiations of k-backbones. We determine the parameterized complexity of decidi…

2014-07-18cs.AIcs.CC

更多相关论文收起更多论文

PBCounter：伪布尔公式上的加权模型计数

PBCounter: Weighted Model Counting on Pseudo-Boolean Formulas

Jilin University（吉林大学）；Northeast Normal University（东北师范大学）

针对CNF表示不自然的问题，提出在表达能力更强的伪布尔公式上执行加权模型计数，基于ADDMC框架实现工具PBCounter，实验表明其优于现有CNF计数器。

2023-12-26cs.AIcs.LO

Efficient Encodings of Conditional Cardinality Constraints

CRIL-CNRS UMR 8188, Université d’Artois（法国国家科学研究中心联合研究单位8188-里尔信息学研究中心，阿尔图瓦大学）；SAMOVAR, Télécom SudParis, CNRS, Univ. Paris-Saclay（萨莫瓦尔实验室，南巴黎电信学院，法国国家科学研究中心，巴黎萨克雷大学）

In the encoding of many real-world problems to propositional satisfiability, the cardinality constraint is a recurrent constraint that needs to be managed effectively. Several efficient encodings have been proposed while missing that such a constraint can be involved in a more general propositional formulation. To avoid combinatorial explosion, Tseitin principle usually used to translate such general propositional formula to Conjunctive Normal Form (CNF), introduces fresh propositional variables to represent sub-formulas and/or complex contraints. Thanks to Plaisted and Greenbaum improvement, …

2018-03-31cs.AI

通过预处理提高d-DNNF表示的查询效率

Enhancing Query Efficiency for d-DNNF Representations Through Preprocessing

CRIL, U. Artois & CNRS（里尔计算机科学实验室，法国北部加来海峡大区大学与法国国家科学研究中心）

研究如何通过预处理提高d-DNNF表示的查询效率，聚焦三项基本任务，指出多数现有预处理器不适用于此，而保持模型计数的预处理器可有效利用，经实验验证其预处理方法高效且能显著提升模型访问查询性能。

2026-07-14cs.AI

Clause/Term Resolution and Learning in the Evaluation of Quantified Boolean Formulas

Resolution is the rule of inference at the basis of most procedures for automated reasoning. In these procedures, the input formula is first translated into an equisatisfiable formula in conjunctive normal form (CNF) and then represented as a set of clauses. Deduction starts by inferring new clauses by resolution, and goes on until the empty clause is generated or satisfiability of the set of clauses is proven, e.g., because no new clauses can be generated. In this paper, we restrict our attention to the problem of evaluating Quantified Boolean Formulas (QBFs). In this setting, the above outli…

2011-09-26cs.AI

构建精确的伪布尔模型计数器

Engineering an Exact Pseudo-Boolean Model Counter

GrabTaxi Holdings（GrabTaxi控股）；Grab-NUS AI Lab（Grab-新加坡国立大学人工智能实验室）；National University of Singapore（新加坡国立大学）；University of Toronto（多伦多大学）

本文提出首个基于知识编译和代数决策图的精确伪布尔模型计数器PBCount，实验证明其能处理1513个实例，远超现有方法的1013个，为该领域未来研究开辟了新途径。

2024-02-18cs.AI

为什么是这个而不是那个？一个基于逻辑的反事实解释框架

Why this and not that? A Logic-based Framework for Contrastive Explanations

TU Wien（维也纳技术大学）；Tampere University（塔尔库大学）

本文提出一个基于命题逻辑的反事实解释框架，通过计算并比较P和Q的原因来回答“为什么是P而不是Q”，分析了计算复杂性，并使用回答集编程实现了CNF公式的问题。

2025-07-11cs.AIcs.LGcs.LO

General Boolean Formula Minimization with QBF Solvers

Utrecht University（乌得勒支大学）；IIIA, CSIC（西班牙国家研究委员会人工智能研究所）

The minimization of propositional formulae is a classical problem in logic, whose first algorithms date back at least to the 1950s with the works of Quine and Karnaugh. Most previous work in the area has focused on obtaining minimal, or quasi-minimal, formulae in conjunctive normal form (CNF) or disjunctive normal form (DNF), with applications in hardware design. In this paper, we are interested in the problem of obtaining an equivalent formula in any format, also allowing connectives that are not present in the original formula. We are primarily motivated in applying minimization algorithms t…

2023-03-12cs.AIcs.CCcs.LO