布尔公式的可满足性问题(SAT)是最早被证明为NP完全的问题之一，具有重要的理论意义和实际应用意义，因此一直受计算机及相关领域研究人员的广泛关注与深入研究，并产生了很多积极的成果。量化布尔公式作为布尔公式带E与A量词的扩展，其可满足性问题(CSAT)也是近年来人们研究的热点之一。上述两类公式采用的是传统的布尔变量，即每个变量的取值为0或者1。但是在很多实际应用中，变量的取值范围并不限于{0，1}，我们称这类变量为非布尔变量。人们发现使用非布尔变量对很多应用进行编码会更简洁方便，所以开始了对非布尔变量的带标公式(signed formulae)的深入研究。本文的工作主要是在三类带标公式，即广义子句集(generalized clause-sets)、单一带标公式(monosigned formulae)和正规带标公式(regular signed formulae)上进行量化扩展，并引入相关的消解演算，同时证明这些演算是可靠的和拒绝性完备的；本文还证明了这三类公式的一些子类的可满足性问题是多项式时间可解的。此外，本文还研究了量化带标的Horn公式和2-公式，给出了这些公式的可满足性问题的计算复杂度；特别的，本文指出量化带标q-Horn公式的可满足性问题是多项式时间可解的。