重み付き木幅を使ってCNFの短い反駁証明を保証する

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.