# Parity and the cost of eliminating auxiliary variables

Kestrel Exams · Research notebook 01 · September 9, 2026

Status: reproduction of established mathematics, with an elementary proof and a reproducible experiment. P vs NP remains unresolved. No novelty, external peer review, or formal proof-assistant verification is claimed.

## The theorem

Let P(n,b) be the Boolean condition that the XOR of n input bits equals b, where n >= 1 and b is 0 or 1. Any CNF representing P(n,b) using only the n original variables requires at least 2^(n-1) clauses. This number suffices.

### Proof

Remove repeated literals from each clause and discard tautological clauses. Every remaining clause is an implicate of P(n,b): every satisfying assignment to P(n,b) must satisfy it.

Suppose a non-tautological clause omits a variable x_j. Assign every variable mentioned in the clause to falsify its literal. Assign any other omitted variables arbitrarily, except x_j. We can choose x_j to make the total parity equal b. This gives an assignment satisfying P(n,b) but falsifying the clause, a contradiction. Hence every non-tautological clause contains every original variable, exactly once after duplicate removal.

Each full-width clause is false on exactly one assignment. There are 2^(n-1) assignments of the wrong parity: flipping the first bit is a bijection between the two parity classes. Every wrong assignment must falsify at least one clause. Therefore at least 2^(n-1) clauses are necessary.

For sufficiency, for each wrong-parity assignment a, create a clause C_a containing x_i if a_i=0, and not x_i if a_i=1. C_a is false exactly on a. The conjunction of these clauses therefore rejects all and only the wrong-parity assignments and uses exactly 2^(n-1) clauses. QED.

## A compact encoding with auxiliary variables

For n >= 2 introduce n-1 auxiliaries z_2,...,z_n. Require z_2=x_1 XOR x_2, z_i=z_(i-1) XOR x_i for 3<=i<=n, and z_n=b.

Encode z=a XOR c as the four clauses

    (a OR c OR NOT z)
    (a OR NOT c OR z)
    (NOT a OR c OR z)
    (NOT a OR NOT c OR NOT z).

Add the unit clause z_n for b=1, or NOT z_n for b=0. There are 4n-3 clauses and 12n-11 literal occurrences, with clause width at most three. This construction is not claimed optimal.

For any assignment of the original bits, the gate constraints force a unique extension to the auxiliaries. The extension satisfies the final unit clause exactly when its parity equals b. Thus existentially quantifying the auxiliaries gives P(n,b).

### Corollary

Any transformation required to eliminate all auxiliaries from this encoding and output an equivalent explicit CNF over only the original variables must produce at least 2^(n-1) clauses and n*2^(n-1) literal occurrences. This is a lower bound on a specified output representation. The compact input has O(n log n) bits with binary variable identifiers, so the output is superpolynomial in that input length and exponential in n.

## Scope of the conclusion

The corollary refutes the universal claim that all such projections have small explicit CNFs. It does not constrain every SAT algorithm. A decision algorithm need not materialize the projected function as a CNF; it may use other representations or simply return a decision.

Parity itself is easy: an assignment is checked with n-1 XOR operations. A satisfying assignment for one unrestricted parity constraint is immediate. In particular, this example does not prove P != NP or furnish a polynomial algorithm for general SAT.

## Computational verification

`experiment.py` uses only the Python standard library. Run:

    python experiment.py --output results.json

It constructs both parity targets for n=2..10 and checks forward, reverse and seeded shuffled Davis-Putnam elimination orders. All final CNFs are compared with a separately constructed truth-table CNF. Exhaustive extension checks cover n=2..6; enumeration of every possible non-tautological clause covers n=2..7. The elimination routine is separately checked against existential truth-table semantics on 300 seeded random small formulas. Tests check implementation behavior; the argument above proves the result for arbitrary n.

## Sources

- Gregory Emdin, Alexander S. Kulikov, Ivan Mihajlin, Nikita Slezkin, *CNF Encodings of Parity*, MFCS 2022. The zero-auxiliary bound above is stated as established background; the paper proves stronger auxiliary-variable tradeoffs. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.47
- Tommi Junttila, Aalto University, *CNF Translations*. Gate encodings and the Tseitin transformation. https://users.aalto.fi/~tjunttil/2023-DP-AUT/notes-sat/cnf2.html
- Stephen Cook, *The P versus NP Problem*, official Clay problem description. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

Canonical notebook: https://kestrelexams.com/research/p-vs-np/