Papers for

sat solver engineers

Papers whose findings have a practical use for this group, as judged from the abstract. Open a paper to read what it means in practice.

New bounds on resolution proof sizes for CNF formulas with weighted treewidth

Short Resolution Refutations for CNFs with Bounded Weighted Incidence Treewidth

Abstract: 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.

Thu 1 OctComputational Complexity
The gist
Resolving why some logical formulas cannot be true is a key challenge in computer science. The authors look at a way to measure complexity called 'incidence treewidth' and introduce new versions that weight parts of the formula differently. They show that for formulas with these weighted measures, we can create shorter and more efficient proofs that they are unsatisfiable. This improves understanding of how the structure of logical formulas affects the difficulty of proving their unsatisfiability.
Open → 2610.02047v1