Tradeoffs in the complexity of backdoor detection

摘要: There has been considerable interest in the identification of structural properties combinatorial problems that lead to efficient algorithms for solving them. Some these are "easily" identifiable, while others because they capture key aspects state-of-the-art constraint solvers. In particular, it was recently shown problem identifying a strong Horn- or 2CNF-backdoor can be solved by exploiting equivalence with deletion backdoors, and is NP-complete. We prove backdoor becomes harder than NP (unless NP=coNP) as soon inconsequential sounding feature empty clause detection (present all modern SAT solvers) added. More interestingly, practice such well polynomial time propagation mechanisms often much smaller sets. fact, despite worst-case complexity results detection, we show Satz-Rand remarkably good at finding small backdoors on range experimental domains. Our suggest notions explored designing should both statically dynamically identifiable properties.