加载中…
For every , we show the existence of a CNF tautology over variables of width such that it has a Polynomial Calculus Resolution refutation over variables of size but any Polynomial Calculus refutation over variables requires size . This shows that Polynomial Calculus sizes over the and bases are incomparable (since Tseitin tautologies show a separation in the other direction) and answers an open problem posed by Sokolov [Sok20] and Razborov.

生成讲解博客的中文版本

生成AI智能校验的中文版本