实数存在论理的概率可检查证明

我们为实数存在论证明 (ETR) 的概率可检查证明 (PCP) 定理进行了证明，表明 MAX-ETR-INV 的近似困难度为 $\exists\mathbb{R}$-硬。实数存在论 (ETR) 是一个决策问题，询问是否存在一组满足多项式约束和不等式的实值变量的赋值，而 $\exists\mathbb{R}$ 是可多项式时间归约到 ETR 的问题的复杂度类。许多重要的几何问题已知为 $\exists\mathbb{R}$-完整。$\exists\mathbb{R}$-硬度结果通常通过从 $\exists\mathbb{R}$-完整问题 ETR-INV 进行归约来实现，ETR-INV 询问是否存在一组每个变量在区间 $[\frac12, 2]$ 内的实变量，满足形式为 $x=1$、$xy=1$ 和 $x+y=z$ 的约束。MAX-ETR-INV 是一个相关的优化问题，给定一组形式为 $x=1$、$xy=1$ 和 $x+y=z$ 的约束，求最大可能大小的可行（即满足变量在 $[\frac12, 2]$ 内的可满足）约束子集。我们表明存在某个常数 $\epsilon>0$，使得逾越 $1-\epsilon$ 因子的 MAX-ETR-INV 近似问题是 $\exists\mathbb{R}$-硬。这意味着即使是非确定性多项式时间算法也不能在此因子范围内逾越 MAX-ETR-INV 除非 $\exists\mathbb{R}=\text{NP}$。我们还给出了一个多项式时间的 $8$ 因子近似算法和一个非确定性多项式时间的 $2$ 因子近似算法。