P vs NP:
a research notebook.

What would solving P vs NP require?

P contains decision problems solvable by a deterministic algorithm in time bounded by a polynomial in the input length. NP contains decision problems whose yes answers have polynomial-length certificates that a deterministic algorithm can verify in polynomial time. Every problem in P is in NP; whether the reverse inclusion holds is open.

One concrete target is SAT: given a Boolean formula, does some assignment of true and false make it true? SAT is NP-complete. A correct, deterministic algorithm for every SAT instance with a proven polynomial worst-case time bound would establish P = NP. Proving that no such algorithm exists would establish P ≠ NP. Input length means the length of the entire encoded formula, and the polynomial's exponent must be fixed. Stephen Cook's official problem description gives the formal setup.

We begin with a narrower strategy we can actually analyze: remove temporary variables from a short formula and express the remaining condition as a list of clauses. Can that list always stay small?

Three ideas for this investigation

Parity

Whether the number of 1s is even or odd. XOR, written ⊕, tracks this: 0 ⊕ 1 = 1 and 1 ⊕ 1 = 0.

CNF

A conjunction (AND) of clauses. Each clause is a disjunction (OR) of literals such as x or ¬x. Every clause must be true. For example: (x ∨ y) ∧ (¬x ∨ z).

Auxiliary variable

A temporary Boolean variable that records an intermediate result. Removing it means asking whether some setting of that variable makes the formula true—not simply deleting every clause that mentions it.

Consider n bits, x₁ through xₙ. We require their parity to equal a target bit b: x₁ ⊕ ⋯ ⊕ xₙ = b. Half of all assignments satisfy either target. Given an assignment, checking this condition takes a single pass through the bits.

Try it: change the bits, then the size

The result, with a complete proof

The bound is standard; it is stated in Emdin, Kulikov, Mihajlin and Slezkin, CNF Encodings of Parity (MFCS 2022). Their paper studies stronger tradeoffs when auxiliary variables are permitted. Here is an elementary argument for the case with no auxiliary variables.

1. Every useful clause must mention every variable. Remove duplicate literals and ignore tautological clauses containing both a variable and its negation. Suppose a remaining clause omits xⱼ. Set its mentioned variables so that every literal in the clause is false. Set any other omitted variables arbitrarily, then choose xⱼ to make the total parity b. This assignment satisfies the parity condition but falsifies the clause—a contradiction. So every non-tautological clause has all n variables.
2. Each such clause rules out exactly one assignment. A clause containing each variable once is false only when all its literals are false. There is exactly one choice of the n bits that does that.
3. There are 2ⁿ⁻¹ assignments to rule out. Flipping the first bit pairs every even-parity assignment with an odd-parity assignment. Exactly half of the 2ⁿ assignments have the wrong parity. Since a useful clause excludes only one, at least 2ⁿ⁻¹ clauses are necessary.
4. That many clauses suffice. For every wrong-parity assignment, include the clause false exactly on that assignment: use xᵢ when its bit is 0 and ¬xᵢ when its bit is 1. Their conjunction rejects all and only the wrong assignments. This gives precisely 2ⁿ⁻¹ clauses. ∎

This is a proof for arbitrary n. The experiments below check the implementation on finitely many instances; they are not the reason the theorem holds for every n.

A short description with temporary variables

For n ≥ 2, introduce z₂, …, zₙ and require:

Each relation z = a ⊕ c can be expressed using four clauses:

These exclude exactly the four incorrect rows of the three-variable truth table. The final condition zₙ = b is one unit clause. There are n − 1 XOR gates, so our encoding has n − 1 helper variables, 4n − 3 clauses, and 12n − 11 literal occurrences. Each clause has at most three literals. This is a standard application of Tseitin-style encoding.

For every assignment to the original bits, the gate relations force a unique sequence of helper values. That sequence satisfies the final unit clause exactly when the original parity is b. Thus:

Removing all helpers while insisting on an equivalent explicit CNF over the original bits therefore forces 2ⁿ⁻¹ clauses, each with n literals. This is an unavoidable output-size cost for that particular transformation.

What the experiment verified

We implement existential elimination using the Davis–Putnam resolution rule. For a variable z, combine every clause containing z with every clause containing ¬z, remove z from their resolvents, and discard tautologies and duplicates. Clauses that never mention z remain.

For n = 2 through 10 and both parity targets, we remove the helpers in forward, reverse, and reproducibly shuffled order. All 54 runs produce the exact direct parity CNF. Independent truth-table checks verify the output; smaller exhaustive checks enumerate helper assignments and every possible non-tautological clause.

The sizes above are clause counts, not execution times. With binary variable identifiers, the helper formula's bit encoding has size O(n log n). The direct CNF has n·2ⁿ⁻¹ literal occurrences. The blowup is exponential in the number n of original variables and superpolynomial in the input encoding length; those measures should not be silently exchanged.

Why this does not settle P vs NP

We have bounded a representation, not every possible computation. A SAT decision algorithm is allowed to return just yes or no. It need not produce the projected CNF, delete the helper variables, or use clauses internally.

Indeed, our own test family is easy. Checking an assignment uses n − 1 XOR operations. With no fixed input bits, finding a satisfying assignment for either parity is immediate: set all bits to 0 for even parity, or set one bit to 1 for odd parity. Systems of XOR equations can also be solved with elimination over the two-element field. An argument that concludes “parity needs a huge CNF, therefore parity requires huge computation” fails on this example.

What a future proof must confront

There are also rigorous limitations on broad proof techniques. They constrain approaches; they do not prove the problem is impossible to solve.

• Relativization. There are oracle settings with P = NP and others with P ≠ NP. An argument that works unchanged relative to every oracle cannot settle the original problem. Baker, Gill and Solovay (1975).
• Natural proofs. Assuming sufficiently strong pseudorandom functions exist, a broad class of efficiently recognizable, sufficiently common properties cannot prove the desired general circuit lower bounds. This barrier is conditional and has a specific definition of “natural.” Razborov and Rudich (1997).
• Algebrization. Even some techniques that use algebra to go beyond ordinary oracle arguments remain insufficient. A resolution of P vs NP needs a method outside this formal barrier. Aaronson and Wigderson (2009).

Clearing a barrier is not itself a proof. A proposed solution still needs every lemma justified and its conclusion checked against the actual computational model.

Reproduce the checks

The experiment uses Python 3.10 or newer and only the standard library. Download the script, then run:

python experiment.py --output results.json

Expected outcome: status: passed, 18 parity instances and 54 elimination runs. The results include the script's SHA-256 hash, fixed random seeds, exact size counts, and separate ranges for each exhaustive check. The script accesses no network and writes only the requested results file.

The test suite also checks the elimination routine against brute-force existential quantification on 300 seeded small formulas, including empty formulas, empty clauses and variables absent from clauses. This helps detect an implementation error that a check of clause counts alone would miss.

Where the investigation goes next

Our long-term objective is a rigorous resolution of P vs NP. This first checkpoint rules out one unrestricted claim about CNF projection and establishes a reproducible way to inspect similar claims.

1. Specify a proposed method exactly. State its input representation, output, correctness invariant, and resource measure before making a complexity claim.
2. Challenge its claimed generality. Test parity, easy SAT subclasses, contradictory inputs, and adversarial constructions. Record the smallest counterexample when a claim fails.
3. Audit any surviving argument. Identify its restricted models and assumptions, examine the relevant proof barriers, and seek independent expert review before calling it a solution.

We do not assume either answer in advance. Finite experiments can reject an algorithm or an invariant; a solution requires a proof covering the full problem.