<p>I am investigating <a href="https://www.cmi.ac.in/%7Eramprasad/lecturenotes/comp_numb_theory/lecture17.pdf" rel="nofollow noreferrer">Pratt's result that Primality is in NP</a>. This means that for a given natural number input
X, there exists a CNF that is satisfiable if and only if
X is a prime number.</p>
<p>I am trying to create a script that generates such a CNF. As a preliminary step, I implemented a <a href="https://drive.google.com/file/d/1cRJDo0K8k1U7dJUcSogYW-np_DJRcSXi/view?usp=drive_link" rel="nofollow noreferrer">Ruby script</a> to generate Pratt certificates. A Pratt primality certificate is represented as a tree structure.</p>
<p>For example, the certificate for 23 being a prime number looks like this in my Ruby script:</p>
<pre><code>{
  &quot;prime&quot;: 23,
  &quot;pow&quot;: 1,
  &quot;generator&quot;: 5,
  &quot;prime_divisors&quot;: [
    {
      &quot;prime&quot;: 2,
      &quot;pow&quot;: 1,
      &quot;generator&quot;: null,
      &quot;prime_divisors&quot;: null
    },
    {
      &quot;prime&quot;: 11,
      &quot;pow&quot;: 1,
      &quot;generator&quot;: 2,
      &quot;prime_divisors&quot;: [
        {
          &quot;prime&quot;: 2,
          &quot;pow&quot;: 1,
          &quot;generator&quot;: null,
          &quot;prime_divisors&quot;: null
        },
        {
          &quot;prime&quot;: 5,
          &quot;pow&quot;: 1,
          &quot;generator&quot;: 2,
          &quot;prime_divisors&quot;: [
            {
              &quot;prime&quot;: 2,
              &quot;pow&quot;: 2,
              &quot;generator&quot;: null,
              &quot;prime_divisors&quot;: null
            }
          ]
        }
      ]
    }
  ]
}

bits = 5


verify = true


count = 6


depth = 4


width = 2


bits * width ** depth = 80
</code></pre>
<p>The bit length of the input is 5, the tree's width is 2, and its depth is 4.</p>
<p>I have a question: If we try to simply translate a Pratt certificate into a CNF, it seems that the size of the CNF could become larger than
<span class="math-container">$O(bitlength^c × width^{depth})$</span></p>
<p>For instance, the certificate for 1266767 being prime has a bit length of 21, width of 4, and depth of 12. A depth of 12 seems excessively large as an exponent.</p>
<p>When translating Pratt certificates to CNF, is it unavoidable for the CNF size to exceed polynomial size with a straightforward translation? What kind of techniques could be used to translate Pratt certificates into polynomial-size CNF?</p>

CC BY-SA 4.0
2024-05-31T16:03:44.707Z
Silly question, but why are you trying to generate a CNF? Primality is in P already (famously). Also any algorithm in P, including a checker for Pratt certificates can be theoretically turned into a polynomial-sized Horn clause (which is a kind of CNF, I guess), though all that modular arithmetic will be quite tedious to encode.
cody
CC BY-SA 4.0
2024-05-31T21:44:25.990Z
What is your question? A Pratt certificate is a polynomial size witness, so its size cannot exceed polynomial.
domotorp
CC BY-SA 4.0
2024-05-31T23:55:50.073Z
I am looking for lower bounds on the exponent of the propositional logic proof system called propagation redundancy. Therefore, I am searching for a CNF that is difficult to prove. Please refer to the page of another question I asked.　https://cstheory.stackexchange.com/questions/54341/seeking-cnf-encoding-with-exponential-lower-bound-in-propagation-redundancy
Jogenara
<proof-complexity>
Challenges and Optimization Techniques for Translating Pratt's Certificates to CNF
Jogenara
# Challenges and Optimization Techniques for Translating Pratt's Certificates to CNF

(Asked by: username_0 on 2024-05-31)

I am investigating Pratt's result that Primality is in NP. This means that for a given natural number input
X, there exists a CNF that is satisfiable if and only if
X is a prime number.
I am trying to create a script that generates such a CNF. As a preliminary step, I implemented a Ruby script to generate Pratt certificates. A Pratt primality certificate is represented as a tree structure.
For example, the certificate for 23 being a prime number looks like this in my Ruby script:
{
  "prime": 23,
  "pow": 1,
  "generator": 5,
  "prime_divisors": [
    {
      "prime": 2,
      "pow": 1,
      "generator": null,
      "prime_divisors": null
    },
    {
      "prime": 11,
      "pow": 1,
      "generator": 2,
      "prime_divisors": [
        {
          "prime": 2,
          "pow": 1,
          "generator": null,
          "prime_divisors": null
        },
        {
          "prime": 5,
          "pow": 1,
          "generator": 2,
          "prime_divisors": [
            {
              "prime": 2,
              "pow": 2,
              "generator": null,
              "prime_divisors": null
            }
          ]
        }
      ]
    }
  ]
}

bits = 5


verify = true


count = 6


depth = 4


width = 2


bits * width ** depth = 80

The bit length of the input is 5, the tree's width is 2, and its depth is 4.
I have a question: If we try to simply translate a Pratt certificate into a CNF, it seems that the size of the CNF could become larger than
$O(bitlength^c × width^{depth})$
For instance, the certificate for 1266767 being prime has a bit length of 21, width of 4, and depth of 12. A depth of 12 seems excessively large as an exponent.
When translating Pratt certificates to CNF, is it unavoidable for the CNF size to exceed polynomial size with a straightforward translation? What kind of techniques could be used to translate Pratt certificates into polynomial-size CNF?

**Tags:** proof-complexity

> **Comments:**
> **username_1**: Silly question, but why are you trying to generate a CNF? Primality is in P already (famously). Also any algorithm in P, including a checker for Pratt certificates can be theoretically turned into a polynomial-sized Horn clause (which is a kind of CNF, I guess), though all that modular arithmetic will be quite tedious to encode.  
> **username_2**: What is your question? A Pratt certificate is a polynomial size witness, so its size cannot exceed polynomial.  
> **username_0**: I am looking for lower bounds on the exponent of the propositional logic proof system called propagation redundancy. Therefore, I am searching for a CNF that is difficult to prove. Please refer to the page of another question I asked.　https://cstheory.stackexchange.com/questions/54341/seeking-cnf-encoding-with-exponential-lower-bound-in-propagation-redundancy  

---

## 0 answers

