<p>First, let me mention that this setup for proving NP-hardness of automatability did not originate in the paper you quote, but in the seminal paper of <a href="https://arxiv.org/abs/1904.02991" rel="nofollow noreferrer">Atserias and Müller</a> who proved such a result for Resolution.</p>
<p>Let me fix the implied constants for ease of reference: assume that <span class="math-container">$A$</span> is a poly-time algorithm such than given a 3-CNF <span class="math-container">$\phi$</span> in <span class="math-container">$n$</span> variables:</p>
<ul>
<li><p>if <span class="math-container">$\phi$</span> is satisfiable, then <span class="math-container">$A(\phi)$</span> has an <span class="math-container">$S$</span>-refutation of size <span class="math-container">$\le n^c$</span>;</p>
</li>
<li><p>if <span class="math-container">$\phi$</span> is unsatisfiable, than <span class="math-container">$A(\phi)$</span> has no <span class="math-container">$S$</span>-refutation of size <span class="math-container">$\le2^{n^\epsilon}$</span>.</p>
</li>
</ul>
<p>Now, assume that <span class="math-container">$M$</span> is a polynomial automating algorithm for <span class="math-container">$S$</span>, i.e., there is a constant <span class="math-container">$d$</span> such that if <span class="math-container">$\phi$</span> is unsatisfiable, then <span class="math-container">$M(\phi)$</span> finds an <span class="math-container">$S$</span>-refutation of <span class="math-container">$\phi$</span> in time <span class="math-container">$k^d$</span>, where <span class="math-container">$k$</span> is the minimal size of an <span class="math-container">$S$</span>-refutation of <span class="math-container">$\phi$</span>. (Let me assume for simplicity that any refutation includes the whole formula, so that we can require <span class="math-container">$k\ge n$</span>.)</p>
<p>Then the following algorithm decides 3-SAT in polynomial time. Given a 3-CNF <span class="math-container">$\phi$</span> in <span class="math-container">$n$</span> variables, where <span class="math-container">$n$</span> is sufficiently large:</p>
<ul>
<li>Compute <span class="math-container">$A(\phi)$</span>, and run <span class="math-container">$M$</span> on <span class="math-container">$A(\phi)$</span> for <span class="math-container">$n^{cd}$</span> steps. If it finds an <span class="math-container">$S$</span>-refutation of <span class="math-container">$A(\phi)$</span>, output YES; otherwise (including the case where it does not halt within the allotted time), output NO.</li>
</ul>
<p>Indeed, if <span class="math-container">$\phi$</span> is satisfiable, then <span class="math-container">$A(\phi)$</span> has a refutation of size at most <span class="math-container">$n^c$</span>, thus <span class="math-container">$M(A(\phi))$</span> finds a refutation of <span class="math-container">$A(\phi)$</span> in time <span class="math-container">$n^{cd}$</span>, and the algorithm accepts. On the other hand, if the algorithm accepts, then <span class="math-container">$M$</span> finds a refutation of <span class="math-container">$A(\phi)$</span> in time at most <span class="math-container">$n^{cd}$</span>, which means the refutation itself has size at most <span class="math-container">$n^{cd}$</span>. This is only possible if <span class="math-container">$\phi$</span> is satisfiable, because otherwise all refutations of <span class="math-container">$A(\phi)$</span> (if any) have size <span class="math-container">$&gt;2^{n^\epsilon}$</span>, which is more than <span class="math-container">$n^{cd}$</span> for <span class="math-container">$n$</span> sufficiently large.</p>
<p>Note that in usual complexity theory, such as in the definition of things like P, NP, or polynomial reductions, complexity is measured in terms of the length of the input. This does not mesh well with the definition of automatability given in terms of the size of the shortest <span class="math-container">$S$</span>-refutation of <span class="math-container">$\phi$</span>. If you want a version of automatability that is literally NP-hard, consider the following promise problem:</p>
<ul>
<li>Given an input <span class="math-container">$(\psi,1^k)$</span>, accept if <span class="math-container">$\psi$</span> has an <span class="math-container">$S$</span>-refutation of size <span class="math-container">$\le k$</span>, and reject if it has no <span class="math-container">$S$</span>-refutation of size <span class="math-container">$\le2^{k^{\epsilon/c}}$</span>.</li>
</ul>
<p>Then assuming the existence of <span class="math-container">$A$</span> as above, <span class="math-container">$\phi\mapsto(A(\phi),n^c)$</span> (where <span class="math-container">$n$</span> is the number of variables of <span class="math-container">$\phi$</span>, and <span class="math-container">$n$</span> is sufficiently large) is a poly-time reduction of 3-SAT to this problem.</p>

CC BY-SA 4.0
2024-11-07T11:32:23.903Z
2024-11-07T11:32:23.903Z
Emil Jeřábek
<p>I'm reading a seminal paper <a href="https://eccc.weizmann.ac.il/report/2020/064/" rel="nofollow noreferrer">[Automating Algebraic Proof Systems is NP-Hard]</a>, which states:</p>
<blockquote>
<p>There exists a polynomial-time algorithm <span class="math-container">$A$</span> that, given an <span class="math-container">$n$</span>-variable 3-CNF formula <span class="math-container">$F$</span>, outputs a CNF formula <span class="math-container">$A(F)$</span> such that for any proof system <span class="math-container">$S$</span> (e.g., Res, NS, PC, SA):</p>
<ul>
<li>If <span class="math-container">$F$</span> is satisfiable, then <span class="math-container">$A(F)$</span> admits an <span class="math-container">$S$</span>-refutation of size at most <span class="math-container">$n^{O(1)}$</span>.</li>
<li>If <span class="math-container">$F$</span> is unsatisfiable, then any <span class="math-container">$S$</span>-refutation of <span class="math-container">$A(F)$</span> has size at least <span class="math-container">$2^{n^{\Omega(1)}}$</span>.</li>
</ul>
</blockquote>
<p>This theorem is used to show that it's NP-hard to approximate the minimum refutation size within a factor of <span class="math-container">$2^{n^\varepsilon}$</span> for some constant <span class="math-container">$\varepsilon &gt; 0$</span>. Consequently, these proof systems are not automatable unless <span class="math-container">$\text{P} = \text{NP}$</span>.</p>
<p>Before delving into my question, here's a quick overview of the definition of <strong>automatability</strong>:</p>
<p>A proof system <span class="math-container">$S$</span> is automatable (<a href="https://example.com/reference" rel="nofollow noreferrer">BPR97</a>) if there exists an algorithm that takes as input an unsatisfiable CNF formula <span class="math-container">$F$</span> and outputs an <span class="math-container">$S$</span>-refutation of <span class="math-container">$F$</span> <strong>in time polynomial in the size of the shortest <span class="math-container">$S$</span>-refutation of <span class="math-container">$F$</span></strong> (plus the size of <span class="math-container">$F$</span>). Intuitively, automatability addresses the proof search problem: how hard is it to find a proof? Automatability (or lack thereof) for well-studied proof systems is a central question for automated theorem proving and SAT solving.</p>
<p><strong>My Try:</strong></p>
<p>If these proof systems were automatable, then we would have an algorithm that could find an <span class="math-container">$S$</span>-refutation of <span class="math-container">$A(F)$</span> in time polynomial in the size of the shortest <span class="math-container">$S$</span>-refutation. Since Theorem 1.1 states that <span class="math-container">$A(F)$</span> has a short refutation (polynomial size) if <span class="math-container">$F$</span> is satisfiable and a long refutation (exponential size) if <span class="math-container">$F$</span> is unsatisfiable, this algorithm could distinguish satisfiable formulas from unsatisfiable ones by finding a refutation in polynomial time (relative to the shortest refutation size). Thus, automatability would allow us to solve 3-SAT in polynomial time, implying that <span class="math-container">$\text{P} = \text{NP}$</span>, which contradicts the assumption that <span class="math-container">$\text{P} \neq \text{NP}$</span>.</p>
<p><strong>My Question:</strong></p>
<p>If the shortest refutation for <span class="math-container">$A(F)$</span> (when <span class="math-container">$F$</span> is unsatisfiable) already has exponential size, then even a polynomial-factor approximation of this size remains exponential. In other words, multiplying an exponential function by a polynomial still yields an exponential function. So, how does this theorem demonstrate NP-hardness in approximating the minimum refutation size?</p>
<p>Could someone clarify how Theorem 1.1 implies NP-hardness in this context, especially when the minimal proof sizes are exponential? How does the difference in the exponential sizes (e.g., different exponents) allow us to distinguish between satisfiable and unsatisfiable cases, thereby showing NP-hardness?</p>

<np-hardness><sat><proof-complexity><automated-theorem-proving>
Why Does Theorem 1.1 Imply That Algebraic Proof Systems Are Not Automatable?
Jxb
# Why Does Theorem 1.1 Imply That Algebraic Proof Systems Are Not Automatable?

(Asked by: username_0 on 2024-11-07)

I'm reading a seminal paper [[Automating Algebraic Proof Systems is NP-Hard]](https://eccc.weizmann.ac.il/report/2020/064/), which states:

> There exists a polynomial-time algorithm $A$ that, given an $n$-variable 3-CNF formula $F$, outputs a CNF formula $A(F)$ such that for any proof system $S$ (e.g., Res, NS, PC, SA):
>
> * If $F$ is satisfiable, then $A(F)$ admits an $S$-refutation of size at most $n^{O(1)}$.
> * If $F$ is unsatisfiable, then any $S$-refutation of $A(F)$ has size at least $2^{n^{\Omega(1)}}$.

This theorem is used to show that it's NP-hard to approximate the minimum refutation size within a factor of $2^{n^\varepsilon}$ for some constant $\varepsilon > 0$. Consequently, these proof systems are not automatable unless $\text{P} = \text{NP}$.

Before delving into my question, here's a quick overview of the definition of **automatability**:

A proof system $S$ is automatable ([BPR97](https://example.com/reference)) if there exists an algorithm that takes as input an unsatisfiable CNF formula $F$ and outputs an $S$-refutation of $F$ **in time polynomial in the size of the shortest $S$-refutation of $F$** (plus the size of $F$). Intuitively, automatability addresses the proof search problem: how hard is it to find a proof? Automatability (or lack thereof) for well-studied proof systems is a central question for automated theorem proving and SAT solving.

**My Try:**

If these proof systems were automatable, then we would have an algorithm that could find an $S$-refutation of $A(F)$ in time polynomial in the size of the shortest $S$-refutation. Since Theorem 1.1 states that $A(F)$ has a short refutation (polynomial size) if $F$ is satisfiable and a long refutation (exponential size) if $F$ is unsatisfiable, this algorithm could distinguish satisfiable formulas from unsatisfiable ones by finding a refutation in polynomial time (relative to the shortest refutation size). Thus, automatability would allow us to solve 3-SAT in polynomial time, implying that $\text{P} = \text{NP}$, which contradicts the assumption that $\text{P} \neq \text{NP}$.

**My Question:**

If the shortest refutation for $A(F)$ (when $F$ is unsatisfiable) already has exponential size, then even a polynomial-factor approximation of this size remains exponential. In other words, multiplying an exponential function by a polynomial still yields an exponential function. So, how does this theorem demonstrate NP-hardness in approximating the minimum refutation size?

Could someone clarify how Theorem 1.1 implies NP-hardness in this context, especially when the minimal proof sizes are exponential? How does the difference in the exponential sizes (e.g., different exponents) allow us to distinguish between satisfiable and unsatisfiable cases, thereby showing NP-hardness?

**Tags:** np-hardness, sat, proof-complexity, automated-theorem-proving


---

## 1 answers

### Answer by username_1 on 2024-11-07. Score: 4 | Accepted answer

First, let me mention that this setup for proving NP-hardness of automatability did not originate in the paper you quote, but in the seminal paper of [Atserias and Müller](https://arxiv.org/abs/1904.02991) who proved such a result for Resolution.

Let me fix the implied constants for ease of reference: assume that $A$ is a poly-time algorithm such than given a 3-CNF $\phi$ in $n$ variables:

* if $\phi$ is satisfiable, then $A(\phi)$ has an $S$-refutation of size $\le n^c$;
* if $\phi$ is unsatisfiable, than $A(\phi)$ has no $S$-refutation of size $\le2^{n^\epsilon}$.

Now, assume that $M$ is a polynomial automating algorithm for $S$, i.e., there is a constant $d$ such that if $\phi$ is unsatisfiable, then $M(\phi)$ finds an $S$-refutation of $\phi$ in time $k^d$, where $k$ is the minimal size of an $S$-refutation of $\phi$. (Let me assume for simplicity that any refutation includes the whole formula, so that we can require $k\ge n$.)

Then the following algorithm decides 3-SAT in polynomial time. Given a 3-CNF $\phi$ in $n$ variables, where $n$ is sufficiently large:

* Compute $A(\phi)$, and run $M$ on $A(\phi)$ for $n^{cd}$ steps. If it finds an $S$-refutation of $A(\phi)$, output YES; otherwise (including the case where it does not halt within the allotted time), output NO.

Indeed, if $\phi$ is satisfiable, then $A(\phi)$ has a refutation of size at most $n^c$, thus $M(A(\phi))$ finds a refutation of $A(\phi)$ in time $n^{cd}$, and the algorithm accepts. On the other hand, if the algorithm accepts, then $M$ finds a refutation of $A(\phi)$ in time at most $n^{cd}$, which means the refutation itself has size at most $n^{cd}$. This is only possible if $\phi$ is satisfiable, because otherwise all refutations of $A(\phi)$ (if any) have size $>2^{n^\epsilon}$, which is more than $n^{cd}$ for $n$ sufficiently large.

Note that in usual complexity theory, such as in the definition of things like P, NP, or polynomial reductions, complexity is measured in terms of the length of the input. This does not mesh well with the definition of automatability given in terms of the size of the shortest $S$-refutation of $\phi$. If you want a version of automatability that is literally NP-hard, consider the following promise problem:

* Given an input $(\psi,1^k)$, accept if $\psi$ has an $S$-refutation of size $\le k$, and reject if it has no $S$-refutation of size $\le2^{k^{\epsilon/c}}$.

Then assuming the existence of $A$ as above, $\phi\mapsto(A(\phi),n^c)$ (where $n$ is the number of variables of $\phi$, and $n$ is sufficiently large) is a poly-time reduction of 3-SAT to this problem.


---

