Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style

Reports tagged with automatability:
TR20-105 | 14th July 2020
Zoë Bell

Automating Regular or Ordered Resolution is NP-Hard

We show that is hard to find regular or even ordered (also known as Davis-Putnam) Resolution proofs, extending the breakthrough result for general Resolution from Atserias and Müller to these restricted forms. Namely, regular and ordered Resolution are automatable if and only if P = NP. Specifically, for a CNF ... more >>>

TR21-033 | 7th March 2021
Susanna de Rezende

Automating Tree-Like Resolution in Time $n^{o(\log n)}$ Is ETH-Hard

We show that tree-like resolution is not automatable in time $n^{o(\log n)}$ unless ETH is false. This implies that, under ETH, the algorithm given by Beame and Pitassi (FOCS 1996) that automates tree-like resolution in time $n^{O(\log n)}$ is optimal. We also provide a simpler proof of the result of ... more >>>

TR24-029 | 16th February 2024
Noel Arteche, Gaia Carenini, Matthew Gray

Quantum Automating $\mathbf{TC}^0$-Frege Is LWE-Hard

We prove the first hardness results against efficient proof search by quantum algorithms. We show that under Learning with Errors (LWE), the standard lattice-based cryptographic assumption, no quantum algorithm can weakly automate $\mathbf{TC}^0$-Frege. This extends the line of results of Kraí?ek and Pudlák (Information and Computation, 1998), Bonet, Pitassi, and ... more >>>

TR24-033 | 24th February 2024
Sam Buss, Emre Yolcu

Regular resolution effectively simulates resolution

Regular resolution is a refinement of the resolution proof system requiring that no variable be resolved on more than once along any path in the proof. It is known that there exist sequences of formulas that require exponential-size proofs in regular resolution while admitting polynomial-size proofs in resolution. Thus, with ... more >>>

ISSN 1433-8092 | Imprint