En este artículo, proponemos un método novedoso que permite a las GNN resolver problemas SAT mediante la aplicación de una técnica a la programación lineal entera mixta (MILP). Tras asignar la fórmula k-CNF al problema MILP, la codificamos en un grafo bipartito ponderado y la introducimos como entrada en la GNN para entrenamiento y pruebas. Teóricamente, (i) establecemos los resultados de invariancia de permutación y equivalencia, que producen salidas estables bajo reordenamientos de cláusulas y variables; (ii) verificamos el límite teórico de que las GNN estándar no siempre pueden distinguir entre instancias satisfacibles e insatisfacibles para una clase de fórmulas denominadas fórmulas plegables; y (iii) demostramos un teorema de aproximación universal que establece que la inicialización aleatoria de nodos (RNI) permite a las GNN aproximar soluciones SAT con precisión arbitraria en un conjunto de datos finito (es decir, las GNN son aproximadamente sólidas y completas en el conjunto de datos). También demostramos que se pueden lograr las mismas garantías de aproximación sin RNI para fórmulas no plegables. Finalmente, presentamos evaluaciones experimentales que demuestran resultados prometedores a pesar de la simplicidad de la arquitectura de la red neuronal.
