On Propositional QBF Expansions and Q-Resolution
On Propositional QBF Expansions and Q-Resolution
复制标题
关于命题 QBF 展开式和 Q 分辨率
DOI：
10.1007/978-3-642-39071-5_7
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Joao Marques
中科院分区：
文献类型：
--
作者：
Mikoláš Janota;Joao Marques
多年来，命题可满足性证明系统（SAT）得到了广泛的研究。最近，量化布尔公式（QBF）的证明系统也受到了关注。Q-resolution是一种演算，能够从基于DPLL的QBF求解器中生成证明。虽然DPLL已成为SAT的主导技术，但QBF已被其他互补和竞争性方法所解决。这些方法之一是基于扩展变量，直到公式只包含一种类型的量词;在此基础上调用SAT求解器。这种方法激发了本文进行的理论分析。我们专注于一个两阶段的证明系统，在第一阶段扩展公式，并在第二阶段应用命题解决方案。这个证明系统的片段的定义和比较Q-分辨率。
Over the years, proof systems for propositional satisfiability (SAT) have been extensively studied. Recently, proof systems for quantified Boolean formulas (QBFs) have also been gaining attention. Q-resolution is a calculus enabling producing proofs from DPLL-based QBF solvers. While DPLL has become a dominating technique for SAT, QBF has been tackled by other complementary and competitive approaches. One of these approaches is based on expanding variables until the formula contains only one type of quantifier; upon which a SAT solver is invoked. This approach motivates the theoretical analysis carried out in this paper. We focus on a two phase proof system, which expands the formula in the first phase and applies propositional resolution in the second. Fragments of this proof system are defined and compared to Q-resolution.