Regular resolution for CNF of bounded incidence treewidth with few long clauses
arXiv: Computational Complexity, 2019.
We demonstrate that Regular Resolution is FPT for two restricted families of CNFs of bounded incidence treewidth. The first includes CNFs having at most $p$ clauses whose removal results in a CNF of primal treewidth at most $k$. The parameters we use in this case are $p$ and $k$. The second class includes CNFs of bounded one-sided (inci...More
PPT (Upload PPT)