<p>I have published the source code on GitHub.
<a href="https://github.com/nagata442000/PrimeAndCompositeTautology" rel="nofollow noreferrer">https://github.com/nagata442000/PrimeAndCompositeTautology</a></p>

CC BY-SA 4.0
2024-10-21T11:47:43.657Z
2024-10-21T11:47:43.657Z
Jogenara
<p>I'm exploring the possibility of encoding a proposition in CNF that might have an exponential lower bound for the number of steps needed to prove it unsatisfiable using propagation redundancy. While there are well-known propositions with exponential lower bounds for resolution (such as the pigeonhole principle) and for cutting planes (such as clique coloring tautologies), I haven't found any for propagation redundancy.</p>
<h3>Proposition:</h3>
<p>I considered the following contradictory proposition as a potential candidate:</p>
<p>&quot;There exists a natural number <span class="math-container">$N$</span> that is both prime and composite.&quot;</p>
<h3>My Approach:</h3>
<ol>
<li><p><strong>Decompose the proposition</strong>:</p>
<ul>
<li><span class="math-container">$N$</span> is prime <span class="math-container">$P(N)$</span></li>
<li><span class="math-container">$N$</span> is composite <span class="math-container">$C(N)$</span></li>
</ul>
</li>
<li><p><strong>Challenges in Encoding</strong>:</p>
<ul>
<li>I realize that a straightforward encoding of this proposition might lead to a CNF with exponential size relative to <span class="math-container">$N$</span>.</li>
<li>I am seeking a more efficient or alternative approach to encode this in CNF.</li>
</ul>
</li>
</ol>
<h3>Clarifications based on feedback:</h3>
<ol>
<li><p><strong>What is &quot;propagation redundancy&quot;?</strong></p>
<ul>
<li>Propagation redundancy is a method in propositional logic proof systems that preserves satisfiability by repeatedly transforming formulas. It is known for handling symmetries in formulas exceptionally well. Propagation redundancy can prove many difficult CNFs, such as the pigeonhole principle, bit pigeonhole principle, parity principle, clique-coloring principle, mutilated chcessboards and tseitin tautologies. in polynomial size relative to the input. For more details, please refer to <a href="https://arxiv.org/abs/1909.00520" rel="nofollow noreferrer">this paper</a>.</li>
</ul>
</li>
<li><p><strong>Representation of <span class="math-container">$N$</span>:</strong></p>
<ul>
<li><span class="math-container">$N$</span> is expressed in binary form.</li>
</ul>
</li>
<li><p><strong>Requirements for encoding:</strong></p>
<ul>
<li>The encoding should be equisatisfiable, meaning that it can introduce new variables as long as the original logical structure is preserved.</li>
</ul>
</li>
<li><p><strong>Acceptable encoding criteria:</strong></p>
<ul>
<li><p>I have an n-bit natural number <span class="math-container">$X$</span>, and I denote the i-th bit of <span class="math-container">$X$</span> in its binary representation as <span class="math-container">$x_i$</span></p>
</li>
<li><p>CNF <span class="math-container">$F_n(x_1,x_2,...,x_n,y_1,y_2,...,y_m)$</span> is satisfiable if and only if <span class="math-container">$X$</span> is a prime number. Futhermore, the size of <span class="math-container">$F_n$</span> is polynomial in n.</p>
</li>
<li><p>CNF <span class="math-container">$G_n(x_1,x_2,...,x_n,z_1,z_2,...,z_k)$</span> is satisfiable if and only if <span class="math-container">$X$</span> is a composite number. Futhermore, the size of <span class="math-container">$G_n$</span> is polynomial in n.</p>
</li>
<li><p>I am envisioning <span class="math-container">$F_n$</span> <span class="math-container">$\wedge$</span> <span class="math-container">$G_n$</span>.</p>
</li>
</ul>
</li>
<li><p><strong>Why not use &quot;False&quot; as the encoding?</strong></p>
<ul>
<li>Using &quot;False&quot; trivially represents the contradiction but does not explore the structure of the problem or provide insights into propagation redundancy.</li>
</ul>
</li>
</ol>
<h3>Questions:</h3>
<ol>
<li>Is there a known method to efficiently encode such a proposition in CNF?</li>
<li>Are there more suitable propositions with exponential lower bounds in propagation redundancy that might serve as better examples?</li>
<li>Any insights or references on propagation redundancy and its limits would be greatly appreciated.</li>
</ol>
<p>Thank you for your assistance!</p>

CC BY-SA 4.0
2024-05-25T10:14:09.787Z
I realized that this question might be more appropriate for Theoretical Computer Science Stack Exchange. Could a moderator help with moving it there? Thank you!
Jogenara
CC BY-SA 4.0
2024-05-27T22:57:44.853Z
When an inference rule requires exponential steps to prove the unsatisfiability of a certain CNF, we say that the inference rule has an exponential lower bound.For example, resolution requires exponential steps to prove the pigeonhole principle, and cutting planes requires exponential steps to prove the clique-coloring tautology.Propagation redundancy is a very powerful inference rule, and an exponential lower bound has not been found for it. I am looking for one.
Jogenara
CC BY-SA 4.0
2024-05-28T04:06:17.723Z
Thank you for all the clarifications!  I am migrating this to CSTheory.SE as requested.
D.W.
CC BY-SA 4.0
2024-05-28T08:28:12.247Z
The definition of compositeness is NP, hence you can express it as satisfiability of a suitable CNF. This might take some work to construct (you basically need to simulate a multiplication circuit). For primality, you can try to translate Pratt’s NP definition, of the AKS algorithm, or (nonconstructively) nonuniform circuits simulating the Miller–Rabin coRP algorithm. But in any case, proving that the resulting tautologies are hard will be a tall order. We do not have any lower bound techniques applicable to number-theoretic statements like this, and a good deal of elementary number theory ...
Emil Jeřábek
CC BY-SA 4.0
2024-05-28T08:29:09.120Z
... *is*, in fact, formalizable in fragments of bounded arithmetic, and as such translate to short proofs in various propositional proof systems.
Emil Jeřábek
CC BY-SA 4.0
2024-05-28T09:15:29.220Z
D.W.,

Thank you very much for your assistance and for migrating my question to CSTheory.SE. I appreciate your help!

Emil Jeřábek,

Thank you for your detailed comments and insights on my question. I appreciate your help!
Jogenara
CC BY-SA 4.0
2024-10-21T14:30:13.113Z
If I understand correctly, the first question is about how to encode Pratt's certificate in CNF? If so, is there a particular part at which you're blocked? The reason I ask is because, as someone who works on SAT encodings, it seems like the kind of thing that is conceptually straightforward but the details are pretty annoying. So if you specify a part that's blocking you maybe we can help!
Bernardo Subercaseaux
CC BY-SA 4.0
2024-10-22T09:53:04.767Z
Thank you for the comment. First of all, I asked this question about four months ago, and at that time I had no idea how to implement this proposition in CNF. Since then, I’ve gradually done some research and realized that generating CNF directly would be too difficult, so I considered using yosys + abc to generate CNF. That approach worked out in some form. The result is the code on my GitHub, which I posted about a month ago. However, this code has a problem. Yosys applies optimizations, so it's not clear if the original structure of the expression is preserved.
Jogenara
CC BY-SA 4.0
2024-10-22T09:54:32.367Z
The ultimate goal of this project is to demonstrate exponential lower bounds for PR or SPR, so using expressions that yosys has optimized makes it difficult to conduct proper discussions. I believe I will ultimately need to generate CNF manually. However, I have no idea how to manually generate CNF. I think parts like add, sub, mul, div, mod, pow, if, and, or, greater than, etc., will be necessary as components of the CNF. How should I generate these components?
Jogenara
<untagged>
Seeking CNF Encoding with Exponential Lower Bound in Propagation Redundancy
Jogenara
# Seeking CNF Encoding with Exponential Lower Bound in Propagation Redundancy

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

I'm exploring the possibility of encoding a proposition in CNF that might have an exponential lower bound for the number of steps needed to prove it unsatisfiable using propagation redundancy. While there are well-known propositions with exponential lower bounds for resolution (such as the pigeonhole principle) and for cutting planes (such as clique coloring tautologies), I haven't found any for propagation redundancy.

### Proposition:

I considered the following contradictory proposition as a potential candidate:

"There exists a natural number $N$ that is both prime and composite."

### My Approach:

1. **Decompose the proposition**:

   * $N$ is prime $P(N)$
   * $N$ is composite $C(N)$
2. **Challenges in Encoding**:

   * I realize that a straightforward encoding of this proposition might lead to a CNF with exponential size relative to $N$.
   * I am seeking a more efficient or alternative approach to encode this in CNF.

### Clarifications based on feedback:

1. **What is "propagation redundancy"?**

   * Propagation redundancy is a method in propositional logic proof systems that preserves satisfiability by repeatedly transforming formulas. It is known for handling symmetries in formulas exceptionally well. Propagation redundancy can prove many difficult CNFs, such as the pigeonhole principle, bit pigeonhole principle, parity principle, clique-coloring principle, mutilated chcessboards and tseitin tautologies. in polynomial size relative to the input. For more details, please refer to [this paper](https://arxiv.org/abs/1909.00520).
2. **Representation of $N$:**

   * $N$ is expressed in binary form.
3. **Requirements for encoding:**

   * The encoding should be equisatisfiable, meaning that it can introduce new variables as long as the original logical structure is preserved.
4. **Acceptable encoding criteria:**

   * I have an n-bit natural number $X$, and I denote the i-th bit of $X$ in its binary representation as $x\_i$
   * CNF $F\_n(x\_1,x\_2,...,x\_n,y\_1,y\_2,...,y\_m)$ is satisfiable if and only if $X$ is a prime number. Futhermore, the size of $F\_n$ is polynomial in n.
   * CNF $G\_n(x\_1,x\_2,...,x\_n,z\_1,z\_2,...,z\_k)$ is satisfiable if and only if $X$ is a composite number. Futhermore, the size of $G\_n$ is polynomial in n.
   * I am envisioning $F\_n$ $\wedge$ $G\_n$.
5. **Why not use "False" as the encoding?**

   * Using "False" trivially represents the contradiction but does not explore the structure of the problem or provide insights into propagation redundancy.

### Questions:

1. Is there a known method to efficiently encode such a proposition in CNF?
2. Are there more suitable propositions with exponential lower bounds in propagation redundancy that might serve as better examples?
3. Any insights or references on propagation redundancy and its limits would be greatly appreciated.

Thank you for your assistance!

**Tags:** untagged
> **Comments:**
> **username_0**: I realized that this question might be more appropriate for Theoretical Computer Science Stack Exchange. Could a moderator help with moving it there? Thank you!  
> **username_0**: When an inference rule requires exponential steps to prove the unsatisfiability of a certain CNF, we say that the inference rule has an exponential lower bound.For example, resolution requires exponential steps to prove the pigeonhole principle, and cutting planes requires exponential steps to prove the clique-coloring tautology.Propagation redundancy is a very powerful inference rule, and an exponential lower bound has not been found for it. I am looking for one.  
> **username_1**: Thank you for all the clarifications!  I am migrating this to CSTheory.SE as requested.  
> **username_2**: The definition of compositeness is NP, hence you can express it as satisfiability of a suitable CNF. This might take some work to construct (you basically need to simulate a multiplication circuit). For primality, you can try to translate Pratt’s NP definition, of the AKS algorithm, or (nonconstructively) nonuniform circuits simulating the Miller–Rabin coRP algorithm. But in any case, proving that the resulting tautologies are hard will be a tall order. We do not have any lower bound techniques applicable to number-theoretic statements like this, and a good deal of elementary number theory ...  
> **username_2**: ... *is*, in fact, formalizable in fragments of bounded arithmetic, and as such translate to short proofs in various propositional proof systems.  
> **username_0**: D.W.,  Thank you very much for your assistance and for migrating my question to CSTheory.SE. I appreciate your help!  Emil Jeřábek,  Thank you for your detailed comments and insights on my question. I appreciate your help!  
> **username_3**: If I understand correctly, the first question is about how to encode Pratt's certificate in CNF? If so, is there a particular part at which you're blocked? The reason I ask is because, as someone who works on SAT encodings, it seems like the kind of thing that is conceptually straightforward but the details are pretty annoying. So if you specify a part that's blocking you maybe we can help!  
> **username_0**: Thank you for the comment. First of all, I asked this question about four months ago, and at that time I had no idea how to implement this proposition in CNF. Since then, I’ve gradually done some research and realized that generating CNF directly would be too difficult, so I considered using yosys + abc to generate CNF. That approach worked out in some form. The result is the code on my GitHub, which I posted about a month ago. However, this code has a problem. Yosys applies optimizations, so it's not clear if the original structure of the expression is preserved.  
> **username_0**: The ultimate goal of this project is to demonstrate exponential lower bounds for PR or SPR, so using expressions that yosys has optimized makes it difficult to conduct proper discussions. I believe I will ultimately need to generate CNF manually. However, I have no idea how to manually generate CNF. I think parts like add, sub, mul, div, mod, pow, if, and, or, greater than, etc., will be necessary as components of the CNF. How should I generate these components?  

---

## 1 answers

### Answer by username_0 on 2024-10-21. Score: 0

I have published the source code on GitHub.
<https://github.com/nagata442000/PrimeAndCompositeTautology>


---

