Proceedings

Backdoor DNFs

Sebastian Ordyniak, Andre Schidler, Stefan Szeider

Download BibTeX Cite

Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence. Main Track. Pages 1403-1409.

https://doi.org/10.24963/ijcai.2021/194

Keywords

  • Constraints and SAT: SAT: Algorithms and Techniques

Abstract

We introduce backdoor DNFs, as a tool to measure the theoretical hardness of CNF formulas. Like backdoor sets and backdoor trees, backdoor DNFs are defined relative to a tractable class of CNF formulas. Each conjunctive term of a backdoor DNF defines a partial assignment that moves the input CNF formula into the base class. Backdoor DNFs are more expressive and potentially smaller than their predecessors backdoor sets and backdoor trees. We establish the fixed-parameter tractability of the backdoor DNF detection problem. Our results hold for the fundamental base classes Horn and 2CNF, and their combination. We complement our theoretical findings by an empirical study. Our experiments show that backdoor DNFs provide a significant improvement over their predecessors.

Sebastian Ordyniak, Andre Schidler, and Stefan Szeider. 2021. Backdoor DNFs. In Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI-21. IJCAI, 1403–1409. https://doi.org/10.24963/ijcai.2021/194
Welcome Future Conferences AI Journal Division IJCAI Proceedings About IJCAI IJCAI Awards