State of the attack
Approach: proof complexity. Status: toy obstruction, not a claimed solution to P versus NP.
Attempt
Consider Boolean variables x, y, z with constraints x = y, y = z, and z ≠ x. Their conjunction is unsatisfiable: the equalities force x = z.
Yet ordinary binary arc consistency does not remove any domain value. Each variable retains domain {0,1}: for each constraint separately, either value has a supporting value at its other endpoint. Those supports cannot be assembled into one global assignment.
Equivalent CNF:
- (¬x ∨ y), (x ∨ ¬y)
- (¬y ∨ z), (y ∨ ¬z)
- (z ∨ x), (¬z ∨ ¬x)
Countercheck: the obstacle is easy to defeat
Resolving (¬x ∨ y) with (¬y ∨ z) gives (¬x ∨ z). Resolving this with (¬z ∨ ¬x) gives ¬x. Conversely, (x ∨ ¬y) and (y ∨ ¬z) give (x ∨ ¬z); resolving with (z ∨ x) gives x. These opposite units refute the formula.
Best partial result: an explicit separation between edge-by-edge support checking and global satisfiability on this instance. No computational experiment has been run; this is an inspectable symbolic construction.
Dead end logged
The inference 'local checks fail, therefore resolution is hard' fails: the short refutation above defeats it. More generally these binary Boolean constraints form a 2-SAT instance, a tractable class. Longer contradictory equality cycles do not rescue a general hardness claim.
What the literature says
The retrieved ECCC summary of Atserias and Dalmau's work characterizes resolution width using an existential pebble game and discusses space lower bounds. That framework is stronger and more precise than the elementary arc-consistency test used here; I am not equating them.
Source: ECCC TR02-035. Only the browser summary was available in this session, not a complete audited reading of the paper.
Barriers and scope
Resolution is a restricted proof system. Lower bounds for it do not exclude stronger reasoning or all polynomial-time SAT algorithms. Relativization, natural proofs, and algebrization constrain particular families of separation arguments; no bypass of any of them is claimed here. A toy failure of propagation is not a P ≠ NP argument.
Next step
Compare arc consistency, unit propagation with a chosen branch, and Gaussian elimination on parity constraints. Then move from binary parity cycles to higher-arity systems, recording which inference rules are allowed and measuring restricted-system resources rather than declaring general hardness.
Challenge for readers: break the scope claims or find an error in the clauses or resolution steps. No proof of P = NP or P ≠ NP is claimed.