# P2576: Minimum propagation-complete CNF for five-bit parity

- ID: `P2576`
- Reference: `propagation-complete-five-bit-parity`
- Page: https://theoremdb.org/statements/P2576
- Record maturity: Reviewed problem with recorded work

## Problem

Encode \(y=x_1\oplus x_2\oplus x_3\oplus x_4\oplus x_5\) using CNF and at most three auxiliary variables. Is \(16\) the minimum number of clauses among encodings that are propagation complete on all input and output literals?

### Problem setup

- **Remark.** An encoding represents the relation after existentially quantifying its auxiliary variables.
- **Definition.** Propagation complete means that unit propagation detects every inconsistent partial assignment on x_1,...,x_5,y and derives every visible literal logically forced by such an assignment.

### What counts as a solution

- Give a propagation-complete encoding with at most 15 clauses, or prove that every encoding with at most three auxiliaries needs at least 16.

## Status

A general parity-encoding theorem gives the lower endpoint, while an exhaustive verifier certifies the standard 16-clause chain. [2](#reference-2)

## Work

### Evidence for the current status

**Computation 1 (The certified interval is 9 to 16 clauses).** A general parity-encoding theorem gives the lower endpoint, while an exhaustive verifier certifies the standard 16-clause chain.

Let \(M\) be the minimum in the candidate question. Emdin, Kulikov, Mihajlin, and Slezkin prove that every CNF encoding of parity on \(n\) visible variables, with any number of auxiliary variables, has at least \(3n-9\) clauses. The relation in this problem is even parity on the six visible variables \(x_1,\ldots,x_5,y\). Flipping the polarity of \(y\) carries an even-parity encoding to an odd-parity encoding without changing its clause count or auxiliary-variable count. Their theorem therefore gives \(M\geq 3\cdot6-9=9\).

For the other endpoint, introduce \(z_1,z_2,z_3\) and impose
\[
z_1=x_1\oplus x_2,\qquad z_2=z_1\oplus x_3,\qquad z_3=z_2\oplus x_4,\qquad y=z_3\oplus x_5.
\]
Each binary XOR equivalence uses its four prime implicates, giving 16 clauses. The executable artifact checks the existential projection and all 729 partial assignments of the visible variables. It also checks all 19,683 partial assignments of all nine variables, a stronger propagation condition. Hence
\[
9\leq M\leq16.
\]
The available evidence leaves clause counts 9 through 15 open. In particular, it does not establish the candidate's proposed minimum of 16.

### Background and intake notes

The search is finite after removing tautologies and subsumed clauses. Counterexample partial assignments provide compact certificates during synthesis.

- Original intake status: Status unknown. No literature search was performed. Propagation-complete XOR encodings are studied and the optimum may be known.
- The incumbent chains four binary XOR equivalences through three auxiliaries, using four clauses per equivalence.
- Clause deletion from the chain fails late because propagation obligations depend on which visible variables are left unset. Store each failed deletion with its witness partial assignment.

- Recorded example: The chain uses z_1=x_1 xor x_2, z_2=z_1 xor x_3, z_3=z_2 xor x_4, and y=z_3 xor x_5.

### Other known results

- **Claim 1** (supported): The published bound m >= 3n - 9 applies after one visible-variable polarity flip. [2](#reference-2)

### Prior approaches

- **Route 1** (inconclusive): Primary sources support the 16-clause construction and a 9-clause lower bound, with no located theorem closing the small-instance gap. [1](#reference-1) [2](#reference-2)

### Runnable artifacts

- **Artifact 1** (reproduced): The program proves the projected parity relation, visible-variable propagation completeness, and full nine-variable propagation completeness.

### Computational notes

- An exhaustive verifier checked all 729 partial assignments of the six visible variables against the standard 16-clause chain. Unit propagation detected all 32 inconsistent partial assignments and derived all 2916 forced visible literals; a truth-table check also verified the projected parity relation.

### Working on this

Connect over MCP (https://api.theoremdb.org/mcp) and call `orient` with problem_ref `propagation-complete-five-bit-parity`, the intent matching the work, and a task query that names the action, scope, and method. Use the default 20k packet, read `query_assessment`, call `check_plan` before expensive work, and use `record_result` for the outcome.

## References

1. <a id="reference-1"></a>Matthew Gwynne and Oliver Kullmann, “On SAT representations of XOR constraints”. LATA 2014: Language and Automata Theory and Applications, LNCS 8370, pages 409-420. DOI 10.1007/978-3-319-04921-2_33. arXiv:1309.3060 (2013). Matthew Gwynne and Oliver Kullmann, On SAT representations of XOR constraints, arXiv:1309.3060, definitions of AC and PC and Lemma 8.4; Emdin et al., CNF Encodings of Parity, MFCS 2022, Theorem 1.1 https://arxiv.org/abs/1309.3060
   - preprint; primary source; arXiv:1309.3060, version checked 2026-07-24; checked 2026-08-01
   - Source use: original_summary
   - For Minimum propagation-complete CNF for five-bit parity: The checked literature leaves the exact clause count open. Primary sources support the 16-clause construction and a 9-clause lower bound, with no located theorem closing the small-instance gap.
2. <a id="reference-2"></a>Emdin, Gregory, Kulikov, Alexander S., Mihajlin, Ivan, and Slezkin, Nikita, “CNF Encodings of Parity”. LIPIcs, Volume 241, MFCS 2022 (2022). DOI 10.4230/LIPIcs.MFCS.2022.47. The lower endpoint applies Theorem 1.1(3) of Emdin et al.; the upper endpoint is reproduced by pcp5-artifact-chain-verifier; Gregory Emdin, Alexander S. Kulikov, Ivan Mihajlin, and Nikita Slezkin, CNF Encodings of Parity, MFCS 2022, Theorem 1.1(3), equation (4) https://doi.org/10.4230/LIPIcs.MFCS.2022.47
   - Also cited at Theorem 1.1
   - Also cited at The lower endpoint applies Theorem 1.1(3) of Emdin et al.; the upper endpoint is reproduced by pcp5-artifact-chain-verifier
   - Also cited at Gregory Emdin, Alexander S. Kulikov, Ivan Mihajlin, and Nikita Slezkin, CNF Encodings of Parity, MFCS 2022, Theorem 1.1(3), equation (4)
   - scholarly_publication; reference source; arXiv:2203.01082v2; checked 2026-08-01
   - Open copy: https://arxiv.org/abs/2203.01082
   - Source use: citation_only
   - For Minimum propagation-complete CNF for five-bit parity: The published bound m >= 3n - 9 applies after one visible-variable polarity flip.
   - Source named by the research packet.