On Boolean Models for Quantified Boolean Horn Formulas
On Boolean Models for Quantified Boolean Horn Formulas
复制标题
量化布尔霍恩公式的布尔模型
DOI：
--
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
Xishun Zhao
中科院分区：
文献类型：
--
作者：
H. K. Büning;K. Subramani;Xishun Zhao
对于量化布尔公式（（{it QBF }））Φ=Qφ，赋值是将Φ的每个存在量化变量映射到布尔函数的函数（cal M），其中φ是命题公式，Q是Φ的变量上的量词的线性排序。一个赋值（cal M）被称为是适当的，如果对于每个存在量化变量y i，相关联的布尔函数fi不依赖于其量词在Q中接替y i的量词的泛量化变量。一个赋值（cal M）被称为Φ的一个模型，如果它是适当的，并且公式（phi^{cal M}）是重言式，其中（phi^{cal M}）是通过用f i替换每个存在量化变量y i而从φ得到的公式。我们发现，任何真正的量化霍恩公式有一个布尔模型组成的单调单项式和常数函数，相反，如果一个QBF有这样一个模型，那么它包含一个子句子公式（{it QHORN }帽{it SAT }）。
For a Quantified Boolean Formula (({it QBF })) Φ=Qφ, an assignment is a function (cal M) that maps each existentially quantified variable of Φ to a Boolean function, where φ is a propositional formula and Q is a linear ordering of quantifiers on the variables of Φ. An assignment (cal M) is said to be proper, if for each existentially quantified variable y i , the associated Boolean function f i does not depend upon the universally quantified variables whose quantifiers in Q succeed the quantifier of y i . An assignment (cal M) is said to be a model for Φ, if it is proper and the formula (phi^{cal M}) is a tautology, where (phi^{cal M}) is the formula obtained from φ by substituting f i for each existentially quantified variable y i . We show that any true quantified Horn formula has a Boolean model consisting of monotone monomials and constant functions only; conversely, if a QBF has such a model then it contains a clause–subformula in ({it QHORN }cap {it SAT }).