Medida cuantitativa de los recursos necesarios para producir refutaciones en el sistema de pruebas proposicional por resolución, típicamente cuantificada por parámetros como longitud de la prueba (número de cláusulas derivadas), anchura (tamaño máximo de cláusula) y espacio (memoria medida por cláusulas almacenadas simultáneamente).

Principio

La complejidad de resolución organiza la dureza al registrar cómo las restricciones sobre los recursos de prueba fuerzan refutaciones más largas o más anchas; los intercambios entre longitud, anchura y espacio determinan la dificultad de refutar fórmulas insatisfacibles en resolución.

Demostración

Ejemplo concreto: las codificaciones proposicionales del principio de las casillas solo admiten refutaciones por resolución cuya longitud crece exponencialmente con el número de elementos; las cotas inferiores de anchura pueden usarse para probar cotas inferiores de longitud para esa familia de fórmulas.

Aplicación incorrecta

Confundir la complejidad de resolución con la complejidad temporal algorítmica general o asumir que las cotas inferiores en resolución se trasladan directamente a sistemas de prueba arbitrarios o a solvers SAT sin considerar relaciones de simulación y heurísticas.

Consecuencia

Su aplicación correcta proporciona cotas inferiores rigurosas sobre la búsqueda de pruebas, explica por qué los solvers SAT tienen dificultades en ciertas familias de fórmulas y guía el diseño de sistemas de prueba y heurísticas al revelar cuál recurso es el cuello de botella.

Inversión

Invertir la perspectiva preguntando qué fórmulas admiten refutaciones en resolución cortas, estrechas y con poco espacio; la inversión destaca subclases tratables y estrategias constructivas de prueba en lugar de la dureza.

Límite

Se aplica específicamente al sistema de pruebas proposicional por resolución (y a procedimientos relacionados como el aprendizaje de cláusulas); no mide directamente pruebas en cálculos de secuencias, sistemas de Frege o refutaciones semánticas salvo que existan simulaciones explícitas.

Tensión semántica

Compite con la noción más amplia de complejidad de pruebas (que abarca muchos sistemas de prueba) y con medidas sintácticas como el tamaño de circuito; la complejidad de resolución es más estrecha pero con frecuencia más accesible a técnicas combinatorias para cotas inferiores.

Síntesis

La complejidad de resolución reúne los parámetros cuantitativos (longitud, anchura, espacio) que caracterizan el coste de derivar contradicciones en resolución; estudiar los intercambios entre esos parámetros proporciona explicaciones precisas de la dureza proposicional y orientaciones para el diseño de solvers.