辅助变元之于命题与量化布尔公式的作用

The Power of Auxiliary Variables for Propositional and Quantified Boolean Formulas

使用辅助变元来引入定义,在知识表达中是一个流行和有力的技巧,能够得到更短、更自然的编码而无需冗长的重复。这篇论文中,我们形式地定义了辅助变元的概念,检验了其表达力并讨论了有趣的相关应用。我们把以下两者联系起来:一是,反复使用中间结果而不通过定义重复;二是,布尔函数其他表达中的相似概念。特别的,我们表明带定义的命题逻辑与具有任意输出端的布尔线路以及约束变元满足Horn性质的存在量化布尔公式(记作(?)HORN^b)具有相同的表达力。本文还考虑了定义结构的限制,以及命题定义的扩充。特别的,我们检验了正命题定义与带存在量化的正定义之间的关系(或等价地,检验了(?)HORN^b公式和约束变元未被Horn限定的存在量化的CNF公式(记作(?)CNF~*)之间的关系)。对命题定义的进一步扩充,是允许在定义中使用任意的量词,或等价地,允许布尔公式的嵌入。我们还证明了,量化CNF公式中的约束变元的表达力,是由子句中被约束部分的极小不可满足子公式或极小假子公式的结构所决定的。

Using auxiliary variables to introduce definitions is a popular and powerful technique in knowledge representation which can lead to shorter and more natural encodings without long repetitions. In this paper, we formally define the notion of auxiliary variables and then examine their expressive power and discuss interesting applications. We relate the idea of reusing intermediate results without copying by definitions to similar concepts in other representations of Boolean functions. In particular, we show that propositional logic with definitions has essentially the same expressive power as Boolean circuits with arbi- trary fan-out and existentially quantified Boolean formulas in which the bound variables satisfy the Horn property （called HORN^b）. The paper also considers restrictions on the structure of definitions and extensions of propositional definitions. In particular, we examine the relationship between positive propositional definitions and positive definitions with existential quantification or, equivalently, the relationship between HORN^b formulas and existentially quantified CNF formulas without the Horn restriction on the bound variables （CNF^＊）. A further extension is to allow arbitrary quantifiers or, equivalently, nesting of Boolean formulas. The expressive power of the bound variables in a quantified CNF formula is shown to be determined by the structure of minimal unsatisfiable or minimal false subformulas of the bound parts of the clauses.