SAT, paritat reordenada i una frontera concreta al voltant de P contra NP

Aquesta entrada és la versió senzilla del preprint publicat a Zenodo. El punt de partida era una intuïció ambiciosa: si un problema de cerca té exponencialment moltes possibilitats i cap direcció local útil, potser resoldre’l de manera òptima exigeix explorar un espai exponencial. Aquesta intuïció apunta cap a P != NP, però no és una demostració.

El que sí hem tancat és més modest i més precís: una família explícita de fórmules SAT insatisfactibles que es reconstrueix exactament com a contradiccions de Tseitin de grau acotat, conté una graella certificada en la seva estructura i hereta lower bounds coneguts per a resolució regular i amplada de resolució general.

La idea en una frase

Prenem dues restriccions de paritat incompatibles sobre les mateixes variables, les codifiquem en dos ordres diferents i fem servir la diferència entre els ordres per forçar una estructura de graella que certs sistemes de prova no poden refutar amb proves petites.

Glossari mínim

SAT: el problema de decidir si una fórmula booleana pot fer-se vertadera triant valors per a les variables.

CNF: una forma estàndard d’escriure fórmules SAT com un conjunt de clàusules.

Resolució: un sistema clàssic per certificar que una fórmula CNF no té cap solució.

Resolució regular: una variant restringida on, a cada branca de la prova, no es pot resoldre dues vegades sobre la mateixa variable.

Tseitin: una família clàssica de contradiccions de paritat associades a grafs. Les fórmules de Tseitin són exemples durs estàndard en complexitat de proves.

Amplada: el nombre de literals en una clàusula. De vegades, provar que tota refutació necessita clàusules amples permet deduir lower bounds de mida.

Flux conceptual

dues paritats incompatibles
        |
        v
codificacions XOR en dos ordres
        |
        v
CNF de paritat reordenada
        |
        v
graf amb una graella explícita
        |
        v
contradicció de Tseitin de grau acotat
        |
        v
lower bounds coneguts per a resolució

La construcció comença amb dues equacions que no poden ser certes alhora:

la suma XOR de totes les variables val 0
la suma XOR de totes les variables val 1

Vistes com a àlgebra lineal sobre GF(2), la contradicció és immediata. Per això no afirmem que la família sigui difícil per a qualsevol mètode imaginable. La dificultat apareix quan les paritats s’expressen com una CNF i s’estudien dins de sistemes concrets de prova.

Per què importa la reordenació

Una paritat es codifica en l’ordre natural de les variables. L’altra es codifica amb un salt modular. Per a n = m^2 - 1, el salt m visita totes les variables una vegada perquè m i m^2 - 1 són coprimers.

Quan unim els dos ordres, el graf que apareix no és una línia simple. Conté una graella explícita de mida (m - 1) x (m - 1). Les graelles tenen amplada d’arbre gran, i aquesta amplada és el pont cap a resultats coneguts de complexitat de proves.

La part útil del preprint és que no deixa aquesta imatge com una metàfora. Reconstrueix la fórmula com una contradicció de Tseitin sobre un graf de grau màxim 3. Així la família queda connectada amb maquinària estàndard en lloc de dependre d’una intuïció vaga sobre “moltes possibilitats”.

Què queda demostrat

Si N és el nombre de variables de la CNF, el preprint obté:

resolució regular: mida 2^Omega(sqrt(N))
resolució general: amplada Omega(sqrt(N))

La primera afirmació diu que tota refutació regular ha de créixer exponencialment en sqrt(N). La segona diu que fins i tot una refutació de resolució general necessita clàusules d’amplada proporcional a sqrt(N).

No són lower bounds per a tot algorisme SAT. Són lower bounds dins de models de prova concrets. Aquesta precisió és important: converteix una intuïció ampla en una afirmació matemàtica revisable.

El límit central

Hi ha una via clàssica per convertir lower bounds d’amplada en lower bounds de mida: el tradeoff de Ben-Sasson i Wigderson. En aquesta família, però, l’amplada creix com sqrt(N), i la conversió depèn d’una quantitat del tipus:

(W - W0)^2 / N

Amb W = Theta(sqrt(N)) i W0 = O(1), aquesta expressió queda en Theta(1). No dona un lower bound superpolinòmic de mida per a resolució general.

La lectura conservadora és que la construcció és “grid-like”, no “expander-like”. La graella dona amplada i duresa per a resolució regular, però no l’expansió que normalment cal per obtenir mida forta en resolució general.

Què no mostra el paper

No prova P != NP.

No prova que SAT sigui difícil en general.

No prova un lower bound de mida per a resolució general sense restriccions.

No prova que els solvers SAT moderns hagin de fallar sempre amb aquesta família. Un solver pràctic pot fer servir preprocessament, aprenentatge, heurístiques i raonament algebraic.

Per què val la pena registrar-ho

El resultat és una peça acotada i publicable: dona una família explícita, certifica l’estructura de graella, la identifica com a Tseitin de grau acotat i documenta exactament on es bloqueja el salt cap a un resultat més fort.

Per al programa més ambiciós al voltant de P != NP, això no és una prova. És una eina d’orientació. Si volem avançar, el següent objectiu raonable no és repetir cerques a l’atzar, sinó buscar una versió expander-like que conservi la presentació compacta i permeti atacar mida en resolució general.

La conclusió curta és aquesta: hem convertit una intuïció sobre absència d’orientació local en un objecte matemàtic reproduïble. L’objecte no resol el gran problema, però marca una frontera concreta on la propera idea hauria de millorar l’anterior.