Una medida del tamaño sintáctico máximo (por ejemplo, el número de literales en una cláusula) de fórmulas o cláusulas intermedias que aparecen en una prueba; en pruebas por resolución suele ser la anchura máxima de cláusulas encontrada.

Principio

Captura la complejidad combinatoria máxima de los objetos intermedios: cláusulas o fórmulas más anchas indican combinaciones mayores de literales que deben manejarse simultáneamente.

Demostración

En pruebas SAT basadas en resolución, la anchura de la prueba es el mayor número de literales presente en cualquier cláusula generada durante la refutación; las pruebas que necesariamente generan cláusulas de gran anchura suelen ser más difíciles de encontrar.

Aplicación incorrecta

Igualar anchura pequeña con facilidad en todos los sistemas pasa por alto efectos de codificación; una prueba de baja anchura en una codificación puede corresponder a una prueba de alta anchura o larga en otra codificación o sistema de prueba.

Consecuencia

Las cotas inferiores de anchura se usan para demostrar cotas exponenciales en la longitud de prueba en resolución; controlar la anchura es una técnica clave al diseñar algoritmos parametrizados o FPT.

Inversión

Puede considerarse en su lugar la anchura media o el recuento total de símbolos para enfatizar la masa global de las fórmulas en lugar de la anchura pico, desplazando la atención de la explosión intermedia peor-caso al coste agregado.

Límite

La anchura está ligada a la representación elegida (cláusulas, secuencias, fórmulas) y a la unidad sintáctica contada (literales vs átomos vs símbolos); no mide directamente pasos secuenciales o memoria a menos que se combine con otras métricas.

Tensión semántica

Compite con longitud y espacio: pruebas estrechas pueden seguir siendo largas o consumidoras de espacio, y pruebas de corta longitud pueden requerir fórmulas intermedias amplias; la anchura aísla la demanda combinatoria simultánea.

Síntesis

La anchura de la prueba cuantifica la carga combinatoria máxima simultánea que genera una prueba; junto con longitud y espacio ayuda a predecir cuellos de botella en la búsqueda y orienta transformaciones o codificaciones que mantengan pequeñas las representaciones intermedias.