Quantified Boolean Formula (QBF) is a notoriously hard generalization of \textsc{SAT}, especially from the point of view of parameterized complexity, where the problem remains intractable for most standard parameters. A recent work by Eriksson et al.~[IJCAI 24] addressed this by considering the case where the propositional part of the formula is in CNF and we parameterize by the number $k$ of existentially quantified variables. One of their main results was that this natural (but so far overlooked) parameter does lead to fixed-parameter tractability, if we also bound the maximum arity $d$ of the clauses of the given CNF. Unfortunately, their algorithm has a \emph{double-exponential} dependence on $k$ ($2^{2^k}$), even when $d$ is an absolute constant. Since the work of Eriksson et al.\ only complemented this with a SETH-based lower bound implying that a $2^{O(k)}$ dependence is impossible, this left a large gap as an open question. Our main result in this paper is to close this gap by showing that the double-exponential dependence is optimal, assuming the ETH: even for CNFs of arity $4$, QBF with $k$ existential variables cannot be solved in time $2^{2^{o(k)}}|φ|^{O(1)}$. Complementing this, we also consider the further restricted case of QBF with only two quantifier blocks ($\forall\exists$-QBF). We show that in this case the situation improves dramatically: for each $d\ge 3$ we show an algorithm with running time $k^{O_d(k ^{d-1})}|φ|^{O(1)}$ and a lower bound under the ETH showing our algorithm is almost optimal.


翻译:量化布尔公式(QBF)是\textsc{SAT}问题一个著名的困难推广,尤其从参数化复杂度的视角来看,该问题对于大多数标准参数仍然是难解的。Eriksson等人近期的工作[IJCAI 24]通过考虑公式的命题部分为CNF且以存在量化变量的数量$k$作为参数的情形来应对这一挑战。他们的主要结果之一是,如果我们同时限定给定CNF子句的最大元数$d$,那么这个自然(但此前被忽视)的参数确实能导出固定参数可解性。遗憾的是,他们的算法对$k$(即使$d$为绝对常数时)存在\emph{双指数}依赖关系($2^{2^k}$)。由于Eriksson等人的工作仅辅以一个基于SETH的下界,表明$2^{O(k)}$的依赖关系不可能实现,这为开放问题留下了巨大的间隙。本文的主要结果是通过证明在假设ETH成立的情况下,双指数依赖关系是最优的,从而填补这一间隙:即使对于元数为$4$的CNF,具有$k$个存在变量的QBF问题也无法在时间$2^{2^{o(k)}}|φ|^{O(1)}$内求解。作为补充,我们还考虑了仅有两个量词块的QBF进一步受限情况($\forall\exists$-QBF)。我们证明在此情形下情况显著改善:对于每个$d\ge 3$,我们给出了一个运行时间为$k^{O_d(k ^{d-1})}|φ|^{O(1)}$的算法,并基于ETH给出了下界,表明我们的算法几乎是最优的。

0
下载
关闭预览

相关内容

在数学和计算机科学之中,算法(Algorithm)为一个计算的具体步骤,常用于计算、数据处理和自动推理。精确而言,算法是一个表示为有限长列表的有效方法。算法应包含清晰定义的指令用于计算函数。 来自维基百科: 算法
《四元数神经网络进展》最新138页
专知会员服务
40+阅读 · 2024年11月8日
强化学习扫盲贴:从Q-learning到DQN
夕小瑶的卖萌屋
52+阅读 · 2019年10月13日
深入理解BERT Transformer ,不仅仅是注意力机制
大数据文摘
22+阅读 · 2019年3月19日
换个角度看GAN:另一种损失函数
机器之心
16+阅读 · 2019年1月1日
再谈变分自编码器VAE:从贝叶斯观点出发
PaperWeekly
13+阅读 · 2018年4月2日
入门 | 从Q学习到DDPG,一文简述多种强化学习算法
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2014年12月31日
国家自然科学基金
2+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
Arxiv
0+阅读 · 4月29日
VIP会员
最新内容
BES:让语言模型通过双向进化搜索自我改进
专知会员服务
2+阅读 · 5月30日
以色列-美国-伊朗战争中的无人机:关键要点
专知会员服务
4+阅读 · 5月30日
《Palantir任务保障性软件安全标准(MA-S2)》
专知会员服务
9+阅读 · 5月30日
基于声学的无人机检测技术综述
专知会员服务
6+阅读 · 5月30日
《当代混合战争分析框架:俄乌战争经验教训》
战略前沿人工智能的再思考(中文)
专知会员服务
8+阅读 · 5月29日
《量化地基防空系统间接效应的博弈论方法》
专知会员服务
6+阅读 · 5月29日
相关VIP内容
《四元数神经网络进展》最新138页
专知会员服务
40+阅读 · 2024年11月8日
相关基金
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2014年12月31日
国家自然科学基金
2+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
Top
微信扫码咨询专知VIP会员