SAT, reordered parity, and a concrete boundary around P versus NP

This is the plain-language version of the preprint deposited on Zenodo. The starting intuition was ambitious: if a search problem has exponentially many possibilities and no useful local direction, perhaps solving it optimally requires exploring an exponential space. That intuition points toward P != NP, but it is not a proof.

What we did close is narrower and more precise: an explicit family of unsatisfiable SAT formulas that is reconstructed exactly as bounded-degree Tseitin contradictions, contains a certified grid in its structure, and inherits known lower bounds for regular resolution and general-resolution width.

The idea in one sentence

Take two incompatible parity constraints over the same variables, encode them in two different orders, and use the mismatch between those orders to force a grid-like structure that certain proof systems cannot refute with small proofs.

Mini-glossary

SAT: the problem of deciding whether a Boolean formula can be made true by assigning values to its variables.

CNF: a standard format for SAT formulas, written as a set of clauses.

Resolution: a classical proof system for certifying that a CNF formula has no satisfying assignment.

Regular resolution: a restricted form of resolution where each branch of the proof resolves on any given variable at most once.

Tseitin: a classical family of parity contradictions associated with graphs. Tseitin formulas are standard hard examples in proof complexity.

Width: the number of literals in a clause. Sometimes proving that every refutation needs wide clauses can be converted into proof-size lower bounds.

Conceptual flow

two incompatible parities
        |
        v
XOR encodings in two orders
        |
        v
reordered-parity CNF
        |
        v
graph with an explicit grid
        |
        v
bounded-degree Tseitin contradiction
        |
        v
known resolution lower bounds

The construction starts with two equations that cannot both hold:

the XOR sum of all variables is 0
the XOR sum of all variables is 1

Seen as linear algebra over GF(2), the contradiction is immediate. So the claim is not that the family is hard for every conceivable method. The difficulty appears when the parities are expressed as CNF and studied inside concrete proof systems.

Why the reordering matters

One parity is encoded in the natural variable order. The other is encoded by a modular stride. For n = m^2 - 1, the stride m visits every variable once because m and m^2 - 1 are coprime.

When the two orders are combined, the resulting graph is not just a line. It contains an explicit (m - 1) x (m - 1) grid. Grids have large treewidth, and that width is the bridge to known proof-complexity results.

The useful part of the preprint is that this is not left as a metaphor. The formula is reconstructed as a Tseitin contradiction over a graph of maximum degree 3. That connects the family to standard machinery instead of relying on a loose intuition about “many possibilities”.

What the paper establishes

If N is the number of CNF variables, the preprint gives:

regular resolution: size 2^Omega(sqrt(N))
general resolution: width Omega(sqrt(N))

The first statement says that every regular-resolution refutation must grow exponentially in sqrt(N). The second says that even unrestricted general resolution needs clauses of width proportional to sqrt(N).

These are not lower bounds for every SAT algorithm. They are lower bounds inside specific proof models. That precision matters: it turns a broad intuition into a checkable mathematical claim.

The central limitation

There is a standard route from width lower bounds to size lower bounds: the Ben-Sasson and Wigderson size-width tradeoff. For this family, however, the width grows as sqrt(N), and the conversion depends on a quantity of the form:

(W - W0)^2 / N

With W = Theta(sqrt(N)) and W0 = O(1), this stays at Theta(1). It does not yield a superpolynomial size lower bound for unrestricted general resolution.

The conservative reading is that the construction is grid-like, not expander-like. The grid gives width and regular-resolution hardness, but not the kind of expansion usually needed for strong general-resolution size lower bounds.

What the paper does not show

It does not prove P != NP.

It does not prove that SAT is hard in general.

It does not prove an unrestricted general-resolution size lower bound.

It does not prove that modern SAT solvers will always fail on this family. Practical solvers can use preprocessing, learning, heuristics, and algebraic reasoning.

Why the result is worth recording

The result is a bounded, publishable piece: it gives an explicit family, certifies the grid structure, identifies the family as bounded-degree Tseitin, and documents exactly where the route to a stronger result breaks.

For the larger program around P != NP, this is not a proof. It is an orientation tool. If we want to move forward, the reasonable next target is not another random search, but an expander-like version that keeps the compact presentation and gives a credible attack on general-resolution size.

The short takeaway is this: a vague intuition about missing local direction has been converted into a reproducible mathematical object. The object does not solve the big problem, but it marks a concrete boundary where the next idea would have to improve on it.