Regular resolution for CNF of bounded incidence treewidth with few long clauses

05/26/2019
by   Andrea Calì, et al.
0

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 (incidence) treewdth, a new parameter generalizing both primal treewidth and incidence pathwidth. The parameter we use in this case is the one-sided treewidth.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset