Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR22-046 | 4th April 2022 09:50

Automating OBDD proofs is NP-hard

RSS-Feed




TR22-046
Authors: Dmitry Itsykson, Artur Riazanov
Publication: 4th April 2022 18:01
Downloads: 462
Keywords: 


Abstract:

We prove that the proof system OBDD(and, weakening) is not automatable unless P = NP. The proof is based upon the celebrated result of Atserias and Muller [FOCS 2019] about the hardness of automatability for resolution. The heart of the proof is lifting with a 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. el. [STOC 2020] to establish the hardness of automatability result for Cutting Planes.



ISSN 1433-8092 | Imprint