ECCC-Report TR22-046https://eccc.weizmann.ac.il/report/2022/046Comments and Revisions published for TR22-046en-usMon, 04 Apr 2022 18:01:16 +0300
Paper TR22-046
| Automating OBDD proofs is NP-hard |
Artur Riazanov,
Dmitry Itsykson
https://eccc.weizmann.ac.il/report/2022/046We 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.Mon, 04 Apr 2022 18:01:16 +0300https://eccc.weizmann.ac.il/report/2022/046