A reduction of proof complexity to computational complexity for $AC^0[p]$ Frege systems
我们给出了一个一般性的减少证明长度的下界的恒定深度Frege系统在DeMorgan语言增加了连接计数模一个素数$p$（所谓的$AC^0[p]$ Frege系统）的计算复杂性下界的搜索任务，涉及搜索树分支上的值的映射的向量空间上的低次多项式在有限域与$p$元素。
2014-08-22 cs.CC math.LO
Pebble Games, Proof Complexity, and Time-Space Trade-offs
卵石游戏在20世纪70年代和80年代在许多不同的背景下被广泛研究。在过去的十年里，人们对卵石游戏的兴趣从证明复杂性的领域中复苏。Pebbling已被证明是一个有用的工具，用于研究基于分辨率的证明系统，比较不同子系统的强度，显示证明空间的界限，并建立大小空间的权衡。这是一个关于证明复杂性的研究的调查，利用了pebbling的结果和工具，重点是证明空间的下限以及证明大小和证明空间之间的权衡。
2013-09-20 cs.CC cs.DM cs.LO
Proof complexity of systems of (non-deterministic) decision trees and branching programs
本文研究命题证明系统中的行序列的决策树或分支程序-确定性和非确定性。系统LDT和LNDT是命题证明系统，其中线表示确定性或非确定性决策树。分支程序被建模为决策dags。将扩展添加到LDT和LNDT给出系统eLDT和eLNDT，其中行分别表示确定性和非确定性分支程序。确定性和非确定性分支程序分别对应于对数空间（L）和非确定性对数空间（NL）。因此系统eLDT和eLNDT是用（非一致）L和NL属性推理的命题证明系统。本文的主要结果是仿真和非仿真结果的树型和dag样的证明系统LDT，LNDT，eLDT，和eLNDT。并与Frege系统、常深度Frege系统和扩展Frege系统作了比较
2019-10-18 cs.CC cs.LO math.LO
Proof Complexity and the Kneser-Lovász Theorem
我们研究了一类命题公式的证明复杂性，这些公式表达了一个被称为Kneser-Lovász定理的组合原理。这是一个命题重言式族，由一个非负整数参数$k$索引，它推广了鸽子洞原理（为$k=1$获得）。我们表明，对于所有固定的$k$，$2^{Ω(n)}$下界分辨率的复杂性和指数下界有界深度弗雷格证明。这些结果甚至适用于更严格的一类公式编码Schrijver的加强Kneser-Lovász定理。另一方面，对于$k=2,3$（Kneser-Lovász定理的组合证明是已知的）的情况下，我们给出多项式大小的弗雷格（$k=2$），分别扩展弗雷格（$k=3$）的证明。本文最后简要宣布了Kneser-Lovász定理一般情况下证明复杂性的结果（在随后的工作中提出）。
2018-05-15 cs.CC cs.LO
A proof complexity perspective on effectively zero-knowledge proofs
Charles University（查理大学）
研究从证明复杂性视角探讨有效零知识证明，通过逻辑语言重新阐述并给出相关性质证明，利用证明复杂性生成器理论，在一定假设下将其转化为真正的零知识证明。
2026-07-16 cs.CC math.LO
Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae
Jeanábek表明，在深度推理中，经典命题逻辑证明中的切割可以在准多项式时间内消除。证明是间接的，它依赖于Atserias，Galesi和Pudlák关于单调微积分的结果以及该系统与无割深度推理证明之间的对应关系。本文给出了Jeábek结果的一个直接证明：给出了经典命题逻辑在深度推理中的一个拟多项式时间截消过程。主要的新成分是使用了一种称为原子流的深层推理证明的计算跟踪，它既非常简单（它们只跟踪结构规则，而忘记了逻辑规则），又足够强大，可以忠实地表示切消过程。
2016-05-02 cs.CC cs.LO
On P vs. NP, Geometric Complexity Theory, Explicit Proofs and the Complexity Barrier
几何复杂性理论（GCT）是研究P vs. NP及相关问题的一种方法。这篇文章给出了它的复杂性理论概述，而不假设任何背景代数几何或表示论。
2009-08-19 cs.CC
Expansions of pseudofinite structures and circuit and proof complexity
我将描述一个一般的模型理论的任务，以构造伪有限结构的展开式，并讨论几个与计算复杂性特别相关的例子。然后，我将提出一个特定的情况下，找到一个合适的扩展将意味着，假设一个单向置换存在，计算类NP是不封闭的补充。
2015-05-01 cs.CC math.LO
Automating Sized Type Inference for Complexity Analysis (Technical Report)
本文介绍了一种高阶函数程序复杂性分析的新方法，它基于三个组成部分：一个强大的类型系统的规模分析和一个健全的类型推断过程，一个滴答单子变换和约束求解。值得注意的是，所提出的方法可以完全自动化，并且能够分析一系列大多数竞争对手方法无法处理的例子。这是可能的，因为选择采用抽象索引语言和索引多态性在更高的排名。原型实现可用。
2017-06-28 cs.CC cs.LO
Proof Complexity of Symbolic QBF Reasoning
CNRS（法国国家科学研究中心）；Univ. Artois（阿尔图瓦大学）；TU Wien（维也纳工业大学）
我们介绍和调查量化布尔公式（QBF）的符号证明系统的有序二元决策图（OBDDs）。这些系统捕获执行符号量词消去的QBF求解器，并因此承认有界路径宽度和量词复杂性的公式的简短证明。因此，我们从标准子句证明系统中获得指数分离，特别是（长距离）QU-Resolution和IR-Calc。我们进一步开发了一个下界技术的符号QBF证明系统的基础上，从通信复杂性的战略提取，升降机已知的下界。这使我们能够推导出强大的下界对符号QBF证明系统是独立的变量排序的基础OBDDs，并举行，即使证明系统被允许访问一个NP-预言。
2021-04-06 cs.AI cs.CC cs.LO
On optimal heuristic randomized semidecision procedures, with application to proof complexity
（p-）最优命题证明系统的存在性是（证明）复杂性中的一个主要公开问题;许多人猜测这样的系统不存在。Krajicek和Pudlak（1989）证明了这个问题等价于存在一个算法，这个算法在所有的命题重言式上都是最优的。Monroe（2009）最近给出了一个猜想，暗示这样的算法不存在。我们表明，在错误的存在下，这样的最佳算法确实存在。这个概念的动机是启发式算法的概念。也就是说，我们允许算法声称少量的假“定理”（根据任何采样分布的非重言式）和错误的有界概率在其他输入。我们的结果也可以被看作是存在的最佳证明系统在一类证明系统通过推广自动化证明系统。
2010-02-03 cs.CC cs.LO
Proof Complexity of Linear Logics
Bernoulli Institute, University of Groningen（格罗宁根大学伯努利研究所）；Department of Computer Science, University of Bath（巴斯大学计算机科学系）
研究经典命题逻辑相继式演算$\mathbf{LK}$证明规模下界问题，以$\mathbf{FL_e}$为基础系统，通过构造公式族得出收缩规则影响下的指数证明规模下界，展示特定相继式得出切割规则有指数级加速，实现多个线性演算及其无切割对应物的指数分离。
2026-07-10 cs.CC cs.LO math.LO
A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP
MMSNP逻辑是存在二阶逻辑的一个限制性片段，它允许表达图论和有限模型理论中许多有趣的查询。该逻辑由Feder和Vardi引入，他们表明每个MMSNP语句在计算上等价于有限域约束满足问题（CSP）;所涉及的概率约简由Kun使用扩展结构的显式构造去随机化。我们提出了一个新的证明减少到有限域CSP不依赖于昆的结果。这个新的证明使我们能够得到一个更强的声明，并验证更一般的Bodirsky-Pinsker二分法猜想的CSP在MMSNP。我们的方法利用了这样一个事实，即每个MMSNP语句描述了可数无限$ω$ -范畴结构的CSP的有限并集;此外，根据Hubička和Nešetzil最近的结果，这些结构可以扩展到具有有限关系签名和Ramsey性质的同构结构。这使得我们能够使用泛代数方法来研究MMSNP的计算复杂性。
2020-11-25 cs.CC cs.LO math.LO
Proof complexity of positive branching programs
本文研究正分支程序系统的证明复杂性，提出系统eLNDT+，证明其可在正矢列上多项式模拟eLNDT，并形式化计数函数性质及给出鸽巢原理的多项式大小证明。
2025-03-08 cs.CC cs.LO math.LO
Proof Complexity Meets Algebra
我们分析了约束满足问题之间的标准约简如何影响它们的证明复杂性。我们发现，对于大多数研究的命题，代数和半代数证明系统，经典的PP-可解释性，同态等价和常数添加到一个核心的建设保持CSP的证明复杂性。因此，对于这些证明系统，存在小的不可满足性证书的约束语言类可以用代数来表征。我们说明了我们的结果的间隙定理说，约束语言要么有分辨率反驳的恒定宽度，或没有有界深度弗雷格反驳的次指数大小。前者适用于广泛研究的一类有界宽度的约束语言。这个类也被称为符合类的语言与反驳的次线性度平方和多项式微积分在实域上，我们提供替代证明。然后，我们要求存在一个自然的证明系统，具有良好的行为方面的减少，同时小尺寸反驳超过有界宽度。我们给出了这样一个证明系统的一个例子，表明有界度的Lovász-Schrijver满足这两个要求。最后，建立在已知的下界，我们证明了方法的适用性，简化和构造新的明确的硬实例的图3-着色问题的所有研究证明系统。
2018-09-25 cs.CC cs.LO
Kernelization, Proof Complexity and Social Choice
我们展示了核化和数据简化的概念从参数化复杂性到证明复杂性的应用：具体来说，我们证明了参数化问题的数据简化规则的存在性（a）。小长度减速链，和（b）.小尺寸（扩展）弗雷格证明证明的合理性减少步骤意味着存在的次指数大小（扩展）弗雷格证明的命题形式化的给定问题。我们应用我们的结果来推断存在的次指数弗雷格和扩展弗雷格证明各种问题。改进了Aisenberg等人（ICALP 2015）的早期结果，我们证明了表达Kneser-Lovász定理（更强形式）的命题公式对于参数k的每个常数值都有多项式大小的Frege证明。以前只知道拟多项式的界（并且只知道普通的Kneser-Lovász定理）。我们的框架的另一个值得注意的应用是不可能的结果在计算社会选择：我们表明，对于任何固定数量的代理，命题翻译的箭头和Gibbard Satterthwaite不可能定理有次指数大小的弗雷格证明。
2021-04-28 cs.CC cs.DS cs.GT
Proof Complexity and Feasible Interpolation
本文综述命题证明复杂性基础，重点介绍可行插值方法及其在构造经典与非经典逻辑证明系统中超多项式长度困难定理方面的应用。
2025-05-05 cs.CC math.LO
Proof Complexity Modulo the Polynomial Hierarchy: Understanding Alternation as a Source of Hardness
我们提出并研究了一个框架，在这个框架中，人们可以提出基于替代的证明长度的下界在证明系统中的量化布尔公式。这个框架中的一个关键概念是证明系统集成，它（本质上）是一个证明系统的序列，对于每个证明系统，可以在多项式层次结构中执行证明检查。我们介绍了一个证明系统合奏称为放松QU-RES的基础上建立的证明系统QU-resolution。我们的主要结果包括一个指数分离的树形和一般版本的放松QU-RES，和一个指数下限放松QU-RES，这些都是类似的经典结果命题证明的复杂性。
2016-02-18 cs.CC
On the proof complexity of MCSAT
可满足性模理论（SMT）和SAT求解器是许多正式软件工具中的关键组件，主要是因为它们能够轻松地解决具有数百万个变量和子句的逻辑问题实例。传统的复杂性理论认为，这些求解器解决的问题在最坏的情况下被认为是困难的。为了解决理论与实践之间的这种明显差异，理论家们提出了将这些求解器作为证明系统进行研究，以便能够建立适当的复杂性下限和上限。例如，近年来已经表明，SAT求解器（的理想化模型）多项式等价于命题逻辑的一般归结证明系统，并且使用CDCL（T）架构的SMT求解器多项式等价于Res*（T）证明系统。在本文中，我们扩展此程序的MCSAT方法SMT解决表明，MCSAT架构是多项式等价的Res*（T）证明系统。因此，我们从证明复杂性理论的角度建立了CDCL（T）和MCSAT之间的等价性。这是迈向更丰富的理论的第一步，也是必不可少的一步，可以帮助（参数化）描述基于MCSAT的SMT求解器可以很好地执行的公式类型。
2021-09-03 cs.CC cs.LO
A Proof Checking View of Parameterized Complexity
PCP定理是计算复杂性理论中最令人震惊的结果之一，是一系列关于证明检验的结果的顶点，它揭示了计算问题的一些深层结构。作为一个令人惊讶的副作用，它也给出了强大的非近似性结果。在本文中，我们发起的证明检查的参数化复杂性范围内的研究。特别是，我们适应和扩展PCP[n log log n，n log log n] Feige等人的结果。几个参数化类，并讨论了一些推论。
2012-07-27 cs.CC
On the Complexity of Finding Narrow Proofs
我们研究的复杂性，以下“分辨率宽度问题”：是否一个给定的3-CNF有一个决议反驳的宽度k？证明了该问题的时间复杂度为O（n^（（k-3）/12））.这个下限是无条件的，不依赖于任何未经证明的复杂性理论假设。这个下界与n^O（k）的平凡上界相匹配。我们还证明了分辨率宽度问题是EXPTIME完全的（如果k是输入的一部分）。这证实了Vardi的一个猜想，他首先提出了分辨率宽度问题的复杂性问题。此外，我们证明了正则归结的归结宽度问题的变体是PSPACE-完全的，证实了Urquhart的一个猜想。
2012-09-11 cs.CC cs.LO
Information in propositional proofs and algorithmic proof search
我们从证明复杂性的角度研究（非正式）证明搜索问题：是否有一个最佳的方法来搜索命题证明？我们注意到，对于任何固定的证明系统，存在一个时间最优的证明搜索算法。利用经典的证明复杂性的反射原理的结果，我们证明了一个时间最优的证明搜索算法存在不限制证明系统当且仅当一个p-最优证明系统存在。为了精确地描述单个公式所需的时间证明搜索算法，我们引入了一种新的基于算法信息概念的证明复杂性度量。特别地，对于证明系统$P$，我们附加{ \bf信息效率函数} $i_P(τ)$，将重言式分配给自然数，并且我们表明：- $i_P(τ)$表征任何$P$证明搜索算法必须在$τ$上使用的时间，并且对于固定的$P$，存在这样的信息最优算法，-证明系统是信息效率最优的当且仅当它是p最优的，- 对于不可自动化的系统$P$，存在具有短证明但具有大信息测度$i_P(τ)$的公式$τ$。我们隔离和激励的问题，建立无条件的超对数下限$i_P(τ)$没有超多项式大小的下限是已知的。我们还指出了新的措施与其他证明搜索的证明复杂性的一些主题的连接。
2021-09-05 cs.CC math.LO
On $NP \cap coNP$ proof complexity generators
Faculty of Mathematics and Physics, Charles University（查理大学数学与物理学院）
本文研究了基于证明复杂性生成器的Σ²P搜索问题DD_P，提出假设(ST)表明在某些强证明系统中，DD_P在学生-教师模型下无法在多项式时间内解决，从而推导出NP≠coNP。
2026-05-05 cs.CC math.LO
Proof Theory at Work: Complexity Analysis of Term Rewrite Systems
本论文主要研究“项重写系统的复杂性”。此外，大部分的工作涉及的“自动化”这样的复杂性分析。本导言的目的是以一种易于理解的方式介绍主要思想，使公众能够了解所介绍的结果。有些技术性的问题，必然会被过于简单化。
2009-12-30 cs.CC cs.LO cs.SC
Complexity of Propositional Proofs under a Promise
我们研究-命题证明复杂性的框架内-CNF公式的承诺下，任何可满足的公式有许多令人满意的任务，其中“许多”代表一个明确指定的函数$\Lam$的变量$n$的证明不可满足的问题。为此，我们开发命题证明系统下不同的措施的承诺（即不同的$\Lam$）作为扩展的决议。这是通过增加公理的分辨率来实现的，这些公理大致可以消除布尔电路定义的真值分配集。然后，我们研究了这样的系统的复杂性，在平均情况下，在不同大小的承诺下，分辨率之间的指数分离：1。对于任何常数$0<\eps<1$，当承诺为$\eps\cd2^n$时，对于所有不可满足的3CNF公式，归结具有多项式大小的反驳。2.对于任意常数$0<δ<1$，当promise为$2^{δn}$（子句数为$o(n^{3/2})$）时，随机3CNF公式没有次指数大小分辨率反驳。
2007-07-28 cs.CC cs.LO
Truth Predicate of Inductive Definitions and Logical Complexity of Infinite-Descent Proofs
Nagasaki University（长崎大学）；National Institute of Informatics / Sokendai（信息学国立研究所/综合研究大学院大学）
本文研究了无限下降证明系统LKID-omega中可证性的逻辑复杂性，证明其为(Pi-1-1)-完全。
2026-03-04 cs.CC cs.LO
On Computation Complexity of True Proof Number Search
University of Alberta（阿尔伯塔大学）
指出了任意有向无环图中证明数搜索的真\emph{proof}数和真\emph{disproof}数的计算是NP困难的，这是证明数搜索的一个重要理论结果.该证明需要对SAT进行约简，这表明为任意DAG找到真证明/反证数至少与决定任意SAT实例是否可满足一样困难，因此是NP困难的。
2021-02-08 cs.AI cs.CC
A direct proof for Lovett's bound on the communication complexity of low rank matrices
通信复杂性中的对数秩猜想表明，任何布尔秩r函数的确定性通信复杂性都有polylog（r）的界。最近，Lovett取得了重大进展，他证明了通信复杂性是O（r^1/2 * log r）的。洛维特的证明是基于已知的估计的差异低秩矩阵。我们给出了一个简单的，直接的证明的基础上，超平面舍入参数，在我们看来，揭示了更多的原因，为什么一个根因子就足够了，什么是必要的，以改善这个因素。
2014-09-22 cs.CC cs.DM
On proof theory in computational complexity: overview
在[GH1]和[GH2]（也见[GH3]）中，我们给出了等式NP = coNP = PSPACE的充分证明。这些结果已经得到了新的证明理论树到dag压缩技术，适合Prawitz的自然演绎（ND）的命题最小逻辑加上相应的Hudelmaier的无割演算。在本文中，我们提出了一个概述我们的证明。
2022-01-09 cs.CC
Proofs, Circuits, and Communication
我们调查下界的复杂性理论，已通过新发现的命题证明复杂性，布尔电路复杂性，查询/通信复杂性之间的相互联系。我们主张总搜索问题（TFNP）的理论作为这些连接的统一语言，并讨论如何从这个角度提出了一个整体方案，进一步研究。
2022-02-17 cs.CC
Many Proof Complexity Generators Inside One Demi-Bits Generator
Johns Hopkins University（约翰斯·霍普金斯大学）；Institute for Advanced Study（高等研究院）
本文证明每个半比特生成器包含指数多个证明复杂度生成器，利用Pajor引理，并引入零误差分散器族，从几乎非平凡的半比特生成器构造证明复杂度生成器，展示范围回避问题的困难性。
2026-09-22 cs.CC cs.LO
Relativization and Interactive Proof Systems in Parameterized Complexity Theory
我们介绍了一些经典的复杂性理论的技术参数化复杂性。首先，我们研究了Chen，Flum和Grohe（2005）用来描述一些参数化复杂性类的机器模型的相对化。在这里，我们得到了一个新的和非平凡的表征的A-层次的甲骨文机，并参数化一个著名的结果，贝克，吉尔和Solovay（1975），通过证明，相对于特定的甲骨文，FPT和A[1]可以重合或不同（一个类似的声明适用于FPT和W[P]）。其次，我们开始研究交互式证明系统的参数化设置，并表明，类AW[SAT]中的每个问题都有一个证明系统与“短”的相互作用，在这个意义上说，轮数是上限的参数值。
2018-03-02 cs.CC
$P \ne NP$, propositional proof complexity, and resolution lower bounds for the weak pigeonhole principle
最近的结果建立了弱鸽子洞原理的任何分辨率证明的长度的指数下界。更正式地，证明了弱鸽子洞原理的任何归结证明，具有$n$洞和任何数量的鸽子，长度为$Ω(2^{n^ε})$（对于常数$ε= 1/3$）。一个推论是陈述$P \ne NP$的某些命题公式没有简短的归结证明。在简短介绍了$P \ne NP$问题和命题证明复杂性的研究领域之后，我将讨论上述弱鸽子洞原理的下界以及与证明$P \ne NP$的难度的关系。
2003-04-28 cs.CC
Revisiting Algebra and Complexity of Inference in Graphical Models
University of Alberta（阿尔伯塔大学）
本文利用代数结构提供的抽象，研究了图模型中推理的形式和复杂性。特别是，我们广泛的形式化推理问题的图形模型，将它们视为一系列的操作的基础上交换半群。然后，我们研究的计算复杂性的推理组织成一个“推理层次”的各种问题。当推理问题的底层结构是一个交换半环（即两个交换半群与分配律的组合）时，一个称为信念传播的消息传递过程可以利用这个分配律来对某些问题进行多项式时间推理。在建立NP-困难的推断在任何交换半环，我们调查之间的关系，在此设置的代数性质，并进一步表明，多项式时间的推理使用分配律不（平凡）扩展到推理问题，表示使用两个以上的交换半群。然后，我们扩展的代数处理的消息传递过程调查传播，提供了一个新的角度使用两个交换半环的组合。这一提法概括了调查传播的应用，以新的设置。
2015-05-03 cs.AI cs.CC math.RA
On the Bit Complexity of Sum-of-Squares Proofs
在最近的论文中经常有人声称，如果通过椭球算法存在，则可以找到d度平方和证明。在[O 17]中，Ryan O 'Donnell指出这个被广泛引用的主张不一定是正确的。他提出了一个有界系数的多项式系统的例子，允许非负性的低次证明，但这些证明必然涉及具有指数位数的数字，导致椭圆算法需要指数时间。在本文中，我们得到了积极和消极的结果位复杂性的SoS证明。首先，我们提出了一个充分条件的多项式系统，意味着一个约束的系数在一个SoS证明。我们证明了这个充分条件适用于SoS算法的常见用例，例如Max-CSP，平衡分离器，Max-Clique，Max-Bisection和Unit-Vector约束。在消极的一面，O 'Donnell问是否每个包含布尔约束的多项式系统都允许多项式位复杂性的证明。我们以否定的方式回答这个问题，给出了一个反例系统和一个非负多项式，它具有二阶SoS证明，但在Omega（sqrt（n））阶之前没有小系数的SoS证明。
2017-02-16 cs.CC
Parameterized Complexity Results for Bayesian Inference
我们提出了完整的结果，在贝叶斯网络的推理与两个不同的参数化，即变量的数量和拓扑顶点分离数。为此，我们引入参数化复杂性类$\mathsf{W[1]PP}$和$\mathsf{XLPP}$，它们分别与$\mathsf{W[1]}$和$\mathsf{XNLP}$相关，就像$\mathsf{PP}$与$\mathsf{NP}$相关一样。第二个参数的目的是作为路径宽度的概念的自然翻译到有向无环图的情况下，因此它是一个比更常见的树宽更强的参数。根据最近的猜想，这个参数的完整性结果表明，确定性算法的推理需要指数空间的路径宽度和扩展树宽。这些结果的目的是有助于更精确地理解贝叶斯推理的参数化复杂性，从而在时间和空间方面所需的计算资源。
2022-06-14 cs.CC
Generating Matrix Identities and Proof Complexity
受证明复杂性的基本下界问题的启发，我们开始研究矩阵恒等式作为强证明系统的硬实例。域$\mathbb{F}$上的$d \times d$矩阵的矩阵恒等式是$\mathbb{F}$上的非交换多项式$f(x_1,\ldots,x_n)$，使得$f$在每个$d \times d$矩阵对其变量的赋值上为零。我们专注于算术证明，这是证明的多项式恒等式运算算术电路和其公理是多项式环公理（这些证明作为一个代数模拟的扩展弗雷格命题证明系统，并在$GF(2)$，他们正式构成一个子系统的扩展弗雷格[HT12]）。我们引入了一个强度递减的证明系统的算术证明，其中$d$第th级是一个健全的和完整的证明系统，证明$d \times d$矩阵恒等式（在一个给定的字段）。对于每一级$d>2$的层次结构中，我们建立了一个证明大小的下界在矩阵单位证明的变量的数量：我们显示了一个家庭的矩阵单位$f_n$与$n$变量的存在，这样的任何证明$f_n=0$需要$Ω(n^{2d})$行的数量。下界参数使用了多项式恒等式代数理论的基本结果以及[Hru 11]中参数的推广。然后，我们开始研究矩阵恒等式作为（完整）算术证明的硬实例。我们提出了两个apturtures，一个关于非交换算术电路的复杂性和其他有关证明的复杂性，根据指数大小的下界算术证明（在算术电路的大小证明的身份）举行。最后，我们讨论了我们的方法，如扩展弗雷格强命题证明系…
2014-09-03 cs.CC
Average-Case Hardness of Binary-Encoded Clique in Proof and Communication Complexity
Lund University（隆德大学）；University of Copenhagen（哥本哈根大学）；EPFL（洛桑联邦理工学院）
研究在证明和通信复杂性中确定图中无大 clique 的平均情况难度，证明了切割平面和有限深度解析 over parities 的 refutations 长度的指数下界，并显示在这些公式中寻找被否决子句的随机通信复杂度为多项式。
2026-05-11 cs.CC
Finite Model Theory and Proof Complexity revisited: Distinguishing graphs in Choiceless Polynomial Time and the Extended Polynomial Calculus
本文扩展了以前的工作，从有限模型理论和命题/代数证明系统的逻辑之间的连接。我们表明，如果所有的非同构图在一个给定的图类中可以区分在逻辑无选择多项式时间计数（CPT），那么他们也可以区分在有界度扩展多项式演算（EPC），和反驳有大致相同的大小的CPT-语句的资源消耗。这使得转移EPC的CPT的下限，从而构成了一个新的潜在的方法，更好地了解CPT的限制。图同构问题的PTIME实例的超多项式EPC下界将CPT与PTIME分离，从而解决有限模型理论中的一个主要公开问题。进一步，利用我们的结果，我们提供了一个模型理论证明有界次数多项式演算和有界次数扩展多项式演算的分离。
2022-11-04 cs.CC cs.LO
Structural Complexity of Rational Interactive Proofs
本文研究理性交互证明的结构复杂性，证明DRMA[k]的预言机等价性，并揭示对数通信单轮理性证明类等于PP，且黑盒采样Parity-P需线性通信。
2023-05-08 cs.CC
Tradeoffs for small-depth Frege proofs
我们研究了小深度弗雷格证明的复杂性，并给出了每行的大小和行数之间的第一个权衡。现有的下限适用于整个证明大小-所有行的大小之和-并且不区分这些复杂性概念。对于深度$d$弗雷格证明的Tseitin原则的$n \times n$网格中的每一行是一个大小$s$公式，我们证明了$\exp(n/2^{Ω(d\sqrt{\log s})})$许多行是必要的。这就产生了新的行复杂度下限，而Håstad最近的$\exp(n^{Ω(1/d)})$对整个证明大小的下限并没有暗示这一点。例如，对于$s = \mathrm{poly}(n)$，我们的下限仍然是所有$d = o(\sqrt{\log n})$的$\exp(n^{1-o(1)})$，而Håstad的下限是$\exp(n^{o(1)})$一次$d = ω_n(1)$。我们的主要概念性贡献是简单的观察，建立电路复杂性的相关界限的技术可以利用建立这样的权衡证明复杂性。
2022-04-07 cs.CC
Towards an algebraic natural proofs barrier via polynomial identity testing
我们观察到，某种代数证明-它基本上涵盖了所有已知的代数电路下界的日期-不能用来证明下界对VP当且仅当我们所谓的简洁击中集存在VP。这类似于布尔电路复杂性中的Razborov-Rudich自然证明障碍，因为我们在去随机化假设下排除了一大类下界技术。我们还讨论了这个代数自然证明障碍，几何复杂性理论和（代数）证明复杂性之间的联系。
2017-01-06 cs.CC math.AG
A Casual Tour Around a Circuit Complexity Bound
我将讨论最近的证明，复杂性类NEXP（非确定性指数时间）缺乏多项式大小的非均匀ACC电路。这个证明将从试图发现它的人的角度来描述。
2011-11-04 cs.CC
Barriers to Complexity-Theoretic Proofs that "AGI" Using Machine Learning is Impossible
University of Toronto（多伦多大学）
本文指出van Rooij等人证明人类智能不可行的复杂性理论证明依赖于不合理的数据分布假设，并讨论了修复证明的两个根本障碍：定义“人类智能”的必要性和考虑特定机器学习系统的归纳偏置。
2026-04-04 cs.AI cs.CC
Approximability and proof complexity
这项工作是有关证明的证明复杂性，证明优化问题\emph{not}有很好的解决方案。具体来说，我们考虑有界度的“平方和”（SOS）证明，一个强大的代数证明系统在1999年推出的格里戈里耶夫和Vorobjov。Shor、Lasserre和Parrilo的工作表明，这个证明系统可以使用半定规划（SDP）自动化，这意味着任何$n$ -可变度- $d$证明都可以在时间$n^{O(d)}$中找到。此外，SDP是著名的Lasserre SDP层次的对偶，这意味着优化问题的“$d/2$轮Lasserre值”等于使用度- $d$ SOS证明可证明的最佳界。Barak等人在最近的一篇论文中利用了这些想法。(STOC 2012年），这表明，已知的“硬实例”的唯一游戏问题实际上是解决接近最佳的一个恒定水平的拉萨尔SDP层次结构。我们将继续研究SOS证明在困难的优化问题的背景下的力量。特别地，我们证明了Devanur等人提出的平衡分离器完整性缺口实例。可以通过4级SOS证明其最佳值。关键成分是KKL定理的SOS证明。我们还调查了在何种程度上的Khot-Vishnoi最大切割完整性差距的实例可以有其最佳值认证的SOS证明。我们可以证明，他们可以在一个因素.952（$> .878$）使用一个恒定的程度证明。这些调查也提出了一个有趣的数学问题：是否有一个常数度SOS证明的中心极限定理？
2012-11-08 cs.CC
From Proof Complexity to Circuit Complexity via Interactive Protocols
本文证明：若隐式扩展弗雷格系统iEF能高效证明标准去随机化假设，则iEF证明长度的超多项式下界可推出#P不在FP/poly中，从而在证明复杂性与电路复杂性之间建立条件性联系。
2024-05-03 cs.CC
Nonogram: Complexity of Inference and Phase Transition Behavior
本文分析了Nonogram谜题推理问题的计算复杂性，并通过实验发现其难度随填充单元格密度呈现相变行为，同时提出了基于正则表达式的CNF编码方法。
2025-09-10 cs.CC
Two Simple Proofs of Müller's Theorem
针对Müller定理原始证明冗长的问题，本文给出两个更简单的证明，并建立带误差量子Kolmogorov复杂度的新界。
2024-07-02 cs.CC quant-ph
Understanding Space in Proof Complexity: Separations and Trade-offs via Substitutions
对于当前最先进的DPLL SAT解算器，两个主要瓶颈是所使用的时间和存储器量。在证明复杂性中，这些资源对应于归结证明的长度和空间。已经有一个长期的研究调查这些证明复杂性的措施，但虽然强有力的结果已经建立了长度，我们的理解空间，以及它如何与长度仍然相当差。特别是，分辨率证明是否可以同时针对长度和空间进行优化，或者这两种措施之间是否存在权衡，这个问题基本上仍然是开放的。在本文中，我们纠正这种情况，证明了主机的长度空间权衡结果的决议。我们的权衡集合几乎涵盖了公式的空间复杂度的整个值范围，并且大多数权衡都是超多项式的，甚至是指数的，并且本质上是紧的。使用类似的技术，我们表明，这些权衡，实际上扩展到指数更强的k-DNF分辨率证明系统，其中操作的析取范式公式与有界arity k项。我们还回答了开放的问题是否k-DNF决议系统形成一个严格的层次结构，相对于空间的肯定。我们的关键技术贡献是下面这个有点令人惊讶的定理：任何CNF公式F都可以通过简单的变量替换转换成新的公式F '，使得如果F具有正确的性质，则F'可以以与F基本相同的长度被证明，而另一方面，在F '的任何证明中，需要同时在存储器中保持的最小行数较低-在F的任何证明中同时需要的变量的最小数量的限制。应用这个定理，所谓的卵石公式定义的卵石游戏的有向无环图，我们得到我们的结果。
2010-08-10 cs.CC
Relating and contrasting plain and prefix Kolmogorov complexity
在[3]中给出了一个简短的证明，证明了某些字符串具有最大的简单Kolmogorov复杂度，但不具有最大的无前缀复杂度。证明使用了Levin的信息对称性，Levin的公式与简单和前缀复杂度有关，以及Gacs的定理，即给定字符串的复杂度可以很高。我们认为，证明技术和上述结果是有用的，以简化现有的证明和解决开放的问题。我们给出了Solovay的结果[21]的一个简短证明，该结果与普通复杂度和前缀复杂度有关：$K (x) = C (x) + CC (x) + O(CCC (x))$和$C (x) = K (x) - KK (x) + O(KKK (x))$（这里$CC(x)$表示$C(C(x))$等）。我们证明了存在$ω$使得$\liminf C(ω_1\dots ω_n) - C(n)$是无限的，而$\liminf K(ω_1\dots ω_n) - K(n)$是有限的，即无穷常C-平凡实数与无穷常K-平凡实数不相同（即[1，问题1]）. Solovay表明，对于无穷多个$x$，我们有$|x| - C (x) \le O(1)$和$|x| + K (|x|) - K (x) \ge \log^{(2)} |x| - O(\log^{(3)} |x|)$，（这里$|x|$表示$x$和$\log^{(2)} = \log\log$的长度，等等）。我们证明了这一结果适用于某些2-随机序列的前缀…
2014-05-07 cs.CC cs.IT math.IT
Complexity of Planar Graph Orientation Consistency, Promise-Inference, and Uniqueness, with Applications to Minesweeper Variants
本文研究了扫雷游戏的三个计算复杂性问题：一致性、推断和可解性，修正了已有推断证明的缺陷，并首次证明了可解性问题的coNP完全性。
2024-04-22 cs.CC
Quantum interactive proofs and the complexity of separability testing
我们确定了一个正式的物理问题之间的联系有关的检测可分离（非纠缠）的量子态和复杂性类的理论计算机科学。特别地，我们证明了几乎每个量子交互证明复杂性类（包括BQP，QMA，QMA（2）和QSZK），都对应着一个自然可分性测试问题，该问题对于该类是完全的。特别令人感兴趣的是，确定等距是否可以产生可分离态的问题是QMA完全的或QMA（2）完全的，这取决于量子态之间的距离是由单向LOCC范数还是迹范数测量的。我们通过证明对于每个n比特最大纠缠态，存在一个固定的单向LOCC测量，该测量将其与任何具有在n中指数衰减的错误概率的可分离态区分开来，从而获得强硬度结果。
2014-09-30 cs.CC quant-ph
Note on "The Complexity of Counting Surjective Homomorphisms and Compactions"
Focke，Goldberg和Rumivnnovel（arXiv 2017）证明了从一个没有循环的大型输入图G到一个可能有循环的固定图H的满射同态计数问题的复杂性二分法。本文给出了一个较弱结果的简短证明：即我们只证明了更一般的G有环问题的P-硬度。我们的证明是Lovász（2012）的一个强大框架的应用，它类似于Curticapean，Dell和Marx（STOC 2017）的证明，他们研究了“对偶”问题，其中模式图G很小，主图H是输入。独立地，Chen（arXiv 2017）使用Lovász的框架证明了一个复杂性二分法，用于计算固定有限结构的满射同态。
2017-10-04 cs.CC
Arthur-Merlin Streaming Complexity
我们研究了亚瑟-梅林概率证明系统在数据流模型中的能力。我们展示了一个典型的$\mathcal{AM}$流算法的数据流问题的广泛的一类。该算法在证明长度和空间复杂度之间进行了折衷，并给出了一个求解\emph{Distinct Elements}问题的$\mathcal{AM}$流算法。给定长度为$m$的数据流在大小为$n$的字母表上，该算法使用$\tilde O(s)$空间和大小为$\tilde O(w)$的证明，对于每个$s,w$，使得$s \cdot w \ge n$（其中$\tilde O$隐藏$\polylog(m,n)$因子）。我们还证明了一个下界，表明每个$\mathcal{MA}$流算法的\emph{Distinct Elements}问题，使用$s$位的空间和大小$w$的证明，满足$s \cdot w = Ω(n)$。作为\emph{Distinct Elements}问题下界证明的一部分，我们给出了关于\emph{Gap Hamming Distance}问题的$\mathcal{MA}$通信复杂度的$Ω(\sqrt n)$的一个新下界，并证明了它的紧性.
2013-02-02 cs.CC cs.DS
