Redundancy in Logic I: CNF Propositional Formulae

TL;DR

This paper investigates the complexity of identifying redundancy in CNF propositional formulas, focusing on the existence, verification, and uniqueness of irredundant equivalent subsets under various conditions.

Contribution

It provides a detailed complexity analysis of redundancy-related problems in CNF formulas, including verification, existence, and uniqueness of irredundant subsets.

Findings

Complexity results for verification of redundancy.

Algorithms for checking existence of irredundant subsets.

Analysis of conditions for uniqueness of irredundant subsets.

Abstract

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.