Regular resolution for CNFs with almost bounded one-sided treewidth

Autor:	Cali, Andrea, Razgon, Igor
Rok vydání:	2019
Předmět:	Computer Science - Computational Complexity Computer Science - Data Structures and Algorithms
Druh dokumentu:	Working Paper
Popis:	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. Comment: This is a significant generalization of the results of the first version
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/1905.10867 Zobrazit plný text záznamu View this record from Arxiv