Superredundancy: A tool for Boolean formula minimization complexity analysis

TL;DR

This paper introduces superredundancy and superirredundancy concepts for Boolean formulas, enabling analysis of formula minimization complexity and fixed clauses in minimal equivalent CNF representations.

Contribution

It defines superredundancy and superirredundancy, providing tools to analyze and construct minimal CNF formulas with fixed clauses, advancing understanding of formula minimization complexity.

Findings

Superredundant clauses are redundant in the resolution closure.

Superirredundant clauses are in all minimal equivalent CNF formulas.

Splitting clauses over new variables can make them superirredundant.

Abstract

A superredundant clause is a clause that is redundant in the resolution closure of a formula. The converse concept of superirredundancy ensures membership of the clause in all minimal CNF formulae that are equivalent to the given one. This allows for building formulae where some clauses are fixed when minimizing size. An example are proofs of complexity hardness of the problems of minimal formula size. Others are proofs of size when forgetting variables or revising a formula. Most clauses can be made superirredundant by splitting them over a new variable.