Quantifier elimination (QE) is an important problem that has numerous applications. Unfortunately, QE is computationally very hard. Earlier we introduced a generalization of QE called $\mathit{partial}$ QE (or PQE for short). PQE allows to unquantify a $\mathit{part}$ of the formula. The appeal of PQE is twofold. First, many important problems can be solved in terms of PQE. Second, PQE can be drastically faster than QE if only a small part of the formula gets unquantified. To make PQE practical, one needs an algorithm for verifying the solution produced by a PQE solver. In this paper, we describe a very simple SAT-based verifier called $\mathit{VerPQE}$ and provide some experimental results.


翻译:量词消除(QE)是具有许多应用的重要问题。不幸的是,QE在计算上非常困难。我们早期介绍了一种称为$\mathit{部分}$QE(或简称PQE)的QE泛化。PQE允许解除公式的$\mathit{部分}$量词。PQE的吸引力有两点。首先,许多重要问题可以通过PQE来解决。其次,如果只解除公式的一小部分,则PQE比QE要快得多。为了使PQE实用,需要一种验证由PQE求解器产生的解的算法。在本文中,我们描述了一种非常简单的基于SAT的验证器$\mathit{VerPQE}$并提供了一些实验结果。

0
下载
关闭预览

相关内容

SAT是研究者关注命题可满足性问题的理论与应用的第一次年度会议。除了简单命题可满足性外,它还包括布尔优化(如MaxSAT和伪布尔(PB)约束)、量化布尔公式(QBF)、可满足性模理论(SMT)和约束规划(CP),用于与布尔级推理有明确联系的问题。官网链接:http://sat2019.tecnico.ulisboa.pt/
【2022新书】基于概率知识系统的知识集成方法,203页pdf
专知会员服务
50+阅读 · 2022年12月28日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
征稿 | International Joint Conference on Knowledge Graphs (IJCKG)
开放知识图谱
2+阅读 · 2022年5月20日
灾难性遗忘问题新视角:迁移-干扰平衡
CreateAMind
17+阅读 · 2019年7月6日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
Capsule Networks解析
机器学习研究会
11+阅读 · 2017年11月12日
可解释的CNN
CreateAMind
17+阅读 · 2017年10月5日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
Arxiv
0+阅读 · 2023年5月17日
Arxiv
0+阅读 · 2023年5月11日
VIP会员
相关主题
相关资讯
征稿 | International Joint Conference on Knowledge Graphs (IJCKG)
开放知识图谱
2+阅读 · 2022年5月20日
灾难性遗忘问题新视角:迁移-干扰平衡
CreateAMind
17+阅读 · 2019年7月6日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
Capsule Networks解析
机器学习研究会
11+阅读 · 2017年11月12日
可解释的CNN
CreateAMind
17+阅读 · 2017年10月5日
相关基金
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
Top
微信扫码咨询专知VIP会员