Superredundancy: A tool for Boolean formula minimization complexity analysis
This work addresses a theoretical problem in computational complexity and logic for researchers in AI and computer science, but it appears incremental as it builds on existing concepts in Boolean formula analysis.
The paper tackles the problem of analyzing the complexity of Boolean formula minimization by introducing the concepts of superredundancy and superirredundancy, which allow certain clauses to be fixed during minimization, leading to proofs of hardness for minimal formula size and other applications like variable forgetting and formula revision.
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.