# Regular resolution for CNFs with almost bounded one-sided treewidth

## TL;DR

This paper introduces a new tree decomposition for CNFs and shows that regular resolution complexity is fixed-parameter tractable for CNFs close to bounded one-sided incidence treewidth, advancing understanding in proof complexity.

## Contribution

It defines a one-sided incidence tree decomposition for CNFs and proves FPT bounds on resolution size for CNFs near bounded one-sided treewidth, generalizing previous classes.

## Key findings

- Resolution size is FPT for CNFs with small p and k
- Introduces a new one-sided incidence tree decomposition
- Generalizes known classes of bounded incidence treewidth CNFs

## Abstract

We introduce a one-sided incidence tree decomposition of a CNF $\varphi$. This is a tree decomposition of the incidence graph of $\varphi$ where the underlying tree is rooted and the set of bags containing each clause induces a directed path in the tree. The one-sided treewidth is the smallest width of a one-sided incidence tree decomposition. We consider a class of unsatisfiable CNF $\varphi$ that can be turned into one of one sided treewidth at most $k$ by removal of at most $p$ clauses. We show that the size of regular resolution for this class of CNFs is FPT parameterized by $k$ and $p$. The results contributes to understanding the complexity of resolution for CNFs of bounded incidence treewidth, an open problem well known in the areas of proof complexity and knowledge compilation. In particular, the result significantly generalizes all the restricted classes of CNFs of bounded incidence treewidth that are known to admit an FPT sized resolution. The proof includes an auxiliary result and several new notions that may be of an independent interest.