Regular resolution for CNFs with almost bounded one-sided treewidth

Andrea Cali, Igor Razgon

We introduce a one-sided incidence tree decomposition of a CNF $\phi$. This is a tree decomposition of the incidence graph of $\phi$ where the underlying tree is rooted and the set of ba…