eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-08-22
59:1
59:15
10.4230/LIPIcs.MFCS.2022.59
article
Automating OBDD proofs is NP-hard
Itsykson, Dmitry
1
https://orcid.org/0000-0003-2680-4800
Riazanov, Artur
1
Steklov Institute of Mathematics at St. Petersburg, Russia
We prove that the proof system OBDD(∧, weakening) is not automatable unless P = NP. The proof is based upon the celebrated result of [Albert Atserias and Moritz Müller, 2019] about the hardness of automatability for resolution. The heart of the proof is lifting with multi-output indexing gadget from resolution block-width to dag-like multiparty number-in-hand communication protocol size with o(n) parties, where n is the number of variables in the non-lifted formula. A similar lifting theorem for protocols with n+1 participants was proved by [Göös et al., 2020] to establish the hardness of automatability result for Cutting Planes.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol241-mfcs2022/LIPIcs.MFCS.2022.59/LIPIcs.MFCS.2022.59.pdf
proof complexity
OBDD
automatability
lifting
dag-like communication