发表机构
Key Laboratory of System Software (Chinese Academy of Sciences); Institute of Software, Chinese Academy of Sciences; University of Chinese Academy of Sciences（系统软件重点实验室（中国科学院）; 中国科学院软件研究所; 中国科学院大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文针对不可满足 CNF 公式，引入对数加权和部分对数加权关联树宽，证明存在 FPT 规模或多项式长度的消解反驳，并给出宽度上界。
AI 中文摘要
在证明复杂性中，一个悬而未决的问题是：是否每个不可满足的 CNF 公式都具有以关联树宽为参数的 FPT 规模的消解反驳。本文针对这一问题建立了若干关于消解反驳长度的上界。考虑一个不可满足的 CNF 公式 $F$，它有 $n$ 个变量、$m$ 个子句、最大子句宽度 $k$，以及关联树宽 $\mathrm{tw}^*(F)$。本文引入了关联树宽的两种变体。其定义可非正式地表述如下。第一种是对数加权关联树宽 $\mathrm{tw}_{\log}^*(F)$，它是加权关联图的树宽，其中变量权重为一，每个子句的权重等于其宽度的对数。第二种是部分对数加权关联树宽 $\mathrm{tw}^*_{\mathrm{plog}}(F)$，它是对数加权关联树宽的细化。在这种变体中，对于关联图的一个好的树分解，每个子句在其被选定的路径上权重为一，而在其他地方，其权重等于一加上其文字中变量不出现在该路径任何袋中的文字数量的对数，并且变量权重为一。对于每个不可满足的 CNF 公式 $F$，我们证明了以下存在性：(i) 以对数加权关联树宽为参数的 FPT 规模的消解反驳，其宽度至多为 $\mathrm{tw}_{\log}^*(F)+k$；(ii) 长度为 $(n+m)k^{O(\mathrm{tw}^*(F))}$ 且宽度至多为 $\mathrm{tw}^*(F)+k$ 的消解反驳；(iii) 以部分对数加权关联树宽为参数的 FPT 规模的消解反驳；(iv) 以对数加权关联树宽为参数的 FPT 规模的正则消解反驳。我们的主要思想是构造以关联树宽为参数的 FPT 规模的 $k$-DNF 消解反驳，然后将它们转换为消解反驳。
英文摘要
It is an open problem in proof complexity whether every unsatisfiable CNF formula has an FPT-sized resolution refutation parameterized by incidence treewidth. In this paper, we establish several upper bounds on resolution refutation length related to this problem. Consider an unsatisfiable CNF formula $F$ with $n$ variables, $m$ clauses, maximum clause width $k$, and incidence treewidth $\mathrm{tw}^*(F)$. In this paper, we introduce two variants of incidence treewidth. Their definitions can be stated informally as follows. The first is log-weighted incidence treewidth $\mathrm{tw}_{\log}^*(F)$, which is the treewidth of the weighted incidence graph, in which variables have weight one and each clause has weight equal to the logarithm of its width. The second is partially log-weighted incidence treewidth $\mathrm{tw}^*_{\mathrm{plog}}(F)$, which is a refinement of log-weighted incidence treewidth. In this variant, for a nice tree decomposition of the incidence graph, each clause has weight one along a path selected for that clause and elsewhere has weight equal to the logarithm of one plus the number of its literals whose variables do not appear in any bag on that path, and variables have weight one. For every unsatisfiable CNF formula $F$, we prove the existence of (i) an FPT-sized resolution refutation parameterized by log-weighted incidence treewidth, with width at most $\mathrm{tw}_{\log}^*(F)+k$; (ii) a resolution refutation of length $(n+m)k^{O(\mathrm{tw}^*(F))}$ and width at most $\mathrm{tw}^*(F)+k$; (iii) an FPT-sized resolution refutation parameterized by partially log-weighted incidence treewidth; and (iv) an FPT-sized regular resolution refutation parameterized by log-weighted incidence treewidth. Our main idea is to construct FPT-sized $k$-DNF resolution refutations parameterized by incidence treewidth, and then convert them into resolution refutations.
