La cantidad máxima de recurso tipo memoria requerida durante una prueba o refutación, a menudo formalizada como el número máximo de fórmulas, cláusulas o líneas de prueba que deben mantenerse simultáneamente en memoria según un modelo de prueba especificado.

Principio

Captura los requisitos de almacenamiento concurrente: el espacio de prueba mide cuántos elementos intermedios deben retenerse en el pico, reflejando cuellos de botella de memoria independientes del número total de pasos.

Demostración

En los modelos de espacio de cláusulas para resolución, el espacio de prueba cuenta el mayor número de cláusulas que un algoritmo de refutación debe mantener almacenadas en cualquier momento; los argumentos tipo pebbling frecuentemente ilustran cotas inferiores sobre el espacio de prueba.

Aplicación incorrecta

Confundir el espacio de prueba con la huella total de memoria de una implementación (que incluye estructuras de datos, índices, caché) o con el tamaño del árbol de búsqueda conduce a una planificación errónea de recursos; el espacio es una métrica abstracta dependiente del modelo.

Consecuencia

Cotas inferiores altas sobre el espacio de prueba muestran la dificultad inherente de memoria para la refutación en el modelo y motivan estrategias de ahorro de espacio (por ejemplo, políticas de eliminación de cláusulas, pruebas reanudables) o el uso de sistemas de prueba alternativos.

Inversión

En vez de centrarse en los elementos concurrentes máximos, puede medirse el producto memoria-tiempo acumulado (integral de la memoria en el tiempo) para capturar el uso total de memoria durante toda la prueba, lo que desplaza el foco del pico al coste agregado.

Límite

Depende del modelo de espacio elegido (espacio de cláusulas, espacio de variables, espacio de fórmulas) y de las suposiciones sobre qué constituye almacenamiento y si se permite la reutilización o compresión; excluye recursos no relacionados con memoria como el tiempo CPU salvo que se combine.

Tensión semántica

Está en tensión con longitud y anchura: pruebas cortas pueden requerir gran espacio, y minimizar espacio puede obligar a pruebas más largas; el espacio formaliza un eje distinto de complejidad.

Síntesis

El espacio de prueba es la métrica del pico de necesidad de memoria que, junto con longitud y anchura, completa una tríada de medidas ortogonales de complejidad; comprender los compromisos de espacio informa algoritmos, estructuras de datos y la elección del cálculo de prueba para manejar la presión de memoria.