For quantified Boolean formulas (QBF), a resolution system with a symmetry rule was recently introduced by Kauers and Seidl (Inf. Process. Lett. 2018). In this system, many formulas hard for QBF resolution admit short proofs.

Kauers and Seidl apply the symmetry rule on symmetries of the original formula. Here we ... more >>>

A locally decodable code (LDC) C:{0,1}^k -> {0,1}^n is an error correcting code wherein individual bits of the message can be recovered by only querying a few bits of a noisy codeword. LDCs found a myriad of applications both in theory and in practice, ranging from probabilistically checkable proofs to ... more >>>

We prove an $\Omega(d \lg n/ (\lg\lg n)^2)$ lower bound on the dynamic cell-probe complexity of statistically $\mathit{oblivious}$ approximate-near-neighbor search (ANN) over the $d$-dimensional Hamming cube. For the natural setting of $d = \Theta(\log n)$, our result implies an $\tilde{\Omega}(\lg^2 n)$ lower bound, which is a quadratic improvement over the ... more >>>