QBF solvers implementing the QCDCL paradigm are powerful algorithms that successfully tackle many computationally complex applications. However, our theoretical understanding of the strength and limitations of these QCDCL solvers is very limited. In this paper we suggest to formally model QCDCL solvers as proof systems. We define different policies that can be used for decision heuristics and unit propagation and give rise to a number of sound and complete QBF proof systems (and hence new QCDCL algorithms). With respect to the standard policies used in practical QCDCL solving, we show that the corresponding QCDCL proof system is incomparable (via exponential separations) to Q-resolution, the classical QBF resolution system used in the literature. This is in stark contrast to the propositional setting where CDCL and resolution are known to be p-equivalent. This raises the question what formulas are hard for standard QCDCL, since Q-resolution lower bounds do not necessarily apply to QCDCL as we show here. In answer to this question we prove several lower bounds for QCDCL, including exponential lower bounds for a large class of random QBFs. We also introduce a strengthening of the decision heuristic used in classical QCDCL, which does not necessarily decide variables in order of the prefix, but still allows to learn asserting clauses. We show that with this decision policy, QCDCL can be exponentially faster on some formulas. We further exhibit a QCDCL proof system that is p-equivalent to Q-resolution. In comparison to classical QCDCL, this new QCDCL version adapts both decision and unit propagation policies.


翻译:QCDCL 模式的QCDCL 执行 QCDCL 模式的 QBF 解决方案是强大的算法。 但是,我们对这些QCDCL 解决方案的力度和局限性的理论理解非常有限。 在本文中,我们建议正式模拟 QCDCL 解决方案作为验证系统。 我们定义了可用于决策超常和单位传播的不同政策, 并产生了一些健全和完整的 QCDCL 验证系统( 因而产生了新的 QCDCL 算法 ) 。 关于在实际 QCDCL 解决方案中所使用的标准政策, 我们发现相应的 QCDCDCL 验证系统无法与Q- 分辨率兼容( 指数分解法) 。 在文献中使用的经典 QBFCL 解算系统, 这与人们知道 CD CLL 和 分辨率是等等量的假设环境环境相悖。 这引起了一个问题, QCDCL 解算法的分解法不一定适用于QCDCLLL 。 在本文中我们所展示的快速校准的QQQ QL, QLCLDLDL 的校正 的校验系统也必然地显示了这个CLE 的校验法。

0
下载
关闭预览

相关内容

【干货书】开放数据结构,Open Data Structures,337页pdf
专知会员服务
16+阅读 · 2021年9月17日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
最新BERT相关论文清单,BERT-related Papers
专知会员服务
52+阅读 · 2019年9月29日
深度卷积神经网络中的降采样
极市平台
12+阅读 · 2019年5月24日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
Disentangled的假设的探讨
CreateAMind
9+阅读 · 2018年12月10日
【推荐】决策树/随机森林深入解析
机器学习研究会
5+阅读 · 2017年9月21日
【学习】Hierarchical Softmax
机器学习研究会
4+阅读 · 2017年8月6日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
Arxiv
0+阅读 · 2021年10月29日
VIP会员
相关资讯
深度卷积神经网络中的降采样
极市平台
12+阅读 · 2019年5月24日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
Disentangled的假设的探讨
CreateAMind
9+阅读 · 2018年12月10日
【推荐】决策树/随机森林深入解析
机器学习研究会
5+阅读 · 2017年9月21日
【学习】Hierarchical Softmax
机器学习研究会
4+阅读 · 2017年8月6日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
Top
微信扫码咨询专知VIP会员