论文标题
超级：布尔公式最小化复杂性分析的工具
Superredundancy: A tool for Boolean formula minimization complexity analysis
论文作者
论文摘要
超级子句是一个子句，在公式的分辨率闭合中是多余的。相反的超少数概念可确保所有最小CNF公式的子句的成员资格，等效于给定的公式。这允许构建公式，在最小化尺寸时固定某些子句。一个例子是最小公式大小问题的复杂性硬度的证明。忘记变量或修改公式时，其他人是大小的证明。大多数子句可以通过将其分配到新变量中来使其成为超级条款。
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.
