Andrew Krapivin, Benjamin Przybocki, Bernardo Subercaseaux
We study the minimum number of clauses required to encode a boolean function into a CNF formula with auxiliary variables. Our main result is that if a boolean function can be evaluated in nondeterministic time $t$ (in the RAM model) with $m$ bits of advice such that at most $b$ bits of advice are accessed for each input, then it admits a CNF encoding with $\widetilde{O}(t + \sqrt{mb})$ clauses. This constitutes a nonuniform generalization of Robson's (TCS'91) variant of the Cook--Levin theorem, for which a naïve generalization would yield $\widetilde{O}(t+m)$ clauses; our applications leverage $b = o(m)$ to obtain significantly better bounds. Since preprocessed data structures can be modeled as computation with advice, our result allows us to translate space- and time-efficient data structures to compact CNF encodings. As an application, we derandomize a data structure of Larsen and Williams (SODA'17) to show that every $k$-CNF function on $n$ inputs can be encoded with $n^k/2^{Ω_k(\sqrt{\lg n})}$ clauses. Notably, despite encoding a $k$-CNF function, the encoding itself necessarily contains clauses of unbounded width, since an information-theoretic argument shows that the minimum number of bounded-width clauses to encode such functions is $Ω_k(n^{k}/\lg n)$ in the worst case. In general terms, our results imply that for a wide variety of NP-complete problems, one can reduce to CNF-SAT in a way that results in asymptotically fewer clauses than previously known methods.
David P. Woodruff, Vincent Cohen-Addad, Lalit Jain, Jieming Mao, Song Zuo, MohammadHossein Bateni, Simina Branzei, Michael P. Brenner 等 36 位作者
Recent advances in large language models (LLMs) have opened new avenues for accelerating scientific research. While models are increasingly capable of assisting with routine tasks, their ability to contribute to novel, expert-level mathematical discovery is less understood. We present a collection of case studies demonstrating how researchers have successfully collaborated with advanced AI models, specifically Google's Gemini-based models (in particular Gemini Deep Think and its advanced variants), to solve open problems, refute conjectures, and generate new proofs across diverse areas in theoretical computer science, as well as other areas such as economics, optimization, and physics. Based on these experiences, we extract common techniques for effective human-AI collaboration in theoretical research, such as iterative refinement, problem decomposition, and cross-disciplinary knowledge transfer. While the majority of our results stem from this interactive, conversational methodology, we also highlight specific instances that push beyond standard chat interfaces. These include deploying the model as a rigorous adversarial reviewer to detect subtle flaws in existing proofs, and embedding it within a "neuro-symbolic" loop that autonomously writes and executes code to verify complex derivations. Together, these examples highlight the potential of AI not just as a tool for automation, but as a versatile, genuine partner in the creative process of scientific discovery.