Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR22-062 | 2nd May 2022 12:24

Superredundancy: A tool for Boolean formula minimization complexity analysis

RSS-Feed




TR22-062
Authors: Paolo Liberatore
Publication: 2nd May 2022 13:53
Downloads: 397
Keywords: 


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.



ISSN 1433-8092 | Imprint