SAT, paridad reordenada y una frontera concreta alrededor de P frente a NP

Esta entrada es la versión sencilla del preprint publicado en Zenodo. El punto de partida fue una intuición ambiciosa: si ciertas búsquedas no tienen orientación local útil, quizá la única forma de resolverlas sea recorrer un espacio exponencial. Esa intuición apunta hacia P != NP, pero por sí sola no es una demostración.

Lo que sí conseguimos cerrar es más modesto y más preciso: una familia explícita de fórmulas SAT insatisfacibles que se traduce exactamente a contradicciones de Tseitin de grado acotado, contiene una rejilla certificada en su estructura y hereda lower bounds conocidos para resolución regular y anchura de resolución general.

La idea en una frase

Tomamos dos restricciones de paridad incompatibles sobre las mismas variables, las codificamos en dos órdenes distintos y usamos esa diferencia de orden para forzar una estructura de rejilla que ciertos sistemas de prueba no pueden refutar de forma pequeña.

Glosario mínimo

SAT: el problema de decidir si una fórmula booleana puede hacerse verdadera eligiendo valores para sus variables.

CNF: una forma estándar de escribir fórmulas SAT como un conjunto de cláusulas.

Resolución: un sistema clásico para certificar que una fórmula CNF no tiene solución.

Resolución regular: una variante restringida donde, en cada rama de la prueba, no se puede resolver dos veces sobre la misma variable.

Tseitin: una familia clásica de contradicciones de paridad asociadas a grafos. Es una fuente estándar de fórmulas difíciles en complejidad de pruebas.

Anchura: el número de literales en una cláusula. A veces probar que toda refutación necesita cláusulas anchas permite deducir lower bounds de tamaño.

El flujo conceptual

dos paridades incompatibles
        |
        v
codificación XOR en dos órdenes
        |
        v
CNF de paridad reordenada
        |
        v
grafo con una rejilla explícita
        |
        v
contradicción de Tseitin de grado acotado
        |
        v
lower bounds conocidos para resolución

La construcción empieza con dos ecuaciones que no pueden ser ciertas a la vez:

la suma XOR de todas las variables vale 0
la suma XOR de todas las variables vale 1

Si se miran como álgebra lineal sobre GF(2), la contradicción es inmediata. Por eso no estamos afirmando que la familia sea difícil para cualquier método imaginable. La dificultad aparece cuando esas paridades se expresan como una CNF y se estudian dentro de sistemas concretos de prueba.

Por qué el reordenamiento importa

Una paridad se codifica en el orden natural de las variables. La otra se codifica usando un salto modular. Para n = m^2 - 1, el salto m recorre todas las variables sin repetir porque m y m^2 - 1 son coprimos.

Al unir los dos órdenes, el grafo que aparece no es una línea simple. Contiene una rejilla explícita de tamaño (m - 1) x (m - 1). Las rejillas tienen anchura de árbol grande, y esa anchura es el puente hacia resultados conocidos de complejidad de pruebas.

La parte útil del preprint es que no deja esta imagen como una analogía. Reconstruye la fórmula como una contradicción de Tseitin sobre un grafo de grado máximo 3. Así la familia queda conectada con maquinaria estándar en lugar de depender de una intuición informal sobre “muchas posibilidades”.

Qué queda demostrado

Si N es el número de variables de la CNF, el preprint obtiene:

resolución regular: tamaño 2^Omega(sqrt(N))
resolución general: anchura Omega(sqrt(N))

La primera afirmación dice que toda refutación regular debe crecer exponencialmente en sqrt(N). La segunda dice que incluso una refutación de resolución general necesita cláusulas de anchura proporcional a sqrt(N).

No son lower bounds para todo algoritmo SAT. Son lower bounds dentro de modelos de prueba concretos. Esa precisión es importante: convierte una intuición amplia en una afirmación revisable.

El límite central

Hay una vía clásica para convertir lower bounds de anchura en lower bounds de tamaño: el tradeoff de Ben-Sasson y Wigderson. En esta familia, sin embargo, la anchura crece como sqrt(N), y la conversión depende de una cantidad del tipo:

(W - W0)^2 / N

Con W = Theta(sqrt(N)) y W0 = O(1), esa expresión queda en Theta(1). No da un lower bound superpolinómico de tamaño para resolución general.

La lectura conservadora es que la construcción es “grid-like”, no “expander-like”. La rejilla da anchura y regular-resolution hardness, pero no la expansión que normalmente se necesita para tamaño fuerte en resolución general.

Qué no muestra el paper

No prueba P != NP.

No prueba que SAT sea difícil en general.

No prueba un lower bound de tamaño para resolución general sin restricciones.

No prueba que los solvers SAT modernos vayan a fallar siempre con esta familia. Un solver práctico puede usar preprocesado, aprendizaje, heurísticas y razonamiento algebraico.

Por qué merece existir

El resultado es publicable como una pieza acotada: da una familia explícita, certifica la estructura de rejilla, la identifica como Tseitin de grado acotado y documenta exactamente dónde se bloquea el salto a un resultado más fuerte.

Para el programa más ambicioso alrededor de P != NP, esto no es una prueba. Es una herramienta de orientación. Si queremos avanzar, el siguiente objetivo razonable no es repetir búsquedas al azar, sino buscar una versión expander-like que conserve la presentación compacta y permita atacar tamaño en resolución general.

La conclusión corta es esta: hemos convertido una intuición sobre ausencia de orientación local en un objeto matemático reproducible. El objeto no resuelve el problema grande, pero sí delimita una frontera concreta donde la siguiente idea tendría que mejorar la anterior.