Un tiempo agotado no es un aprobado: resultados «No determinado»
Cuando el motor se queda sin presupuesto o alcanza un límite de tamaño, informa «No determinado», nunca un aprobado. Abajo, la conversión a forma normal de una cadena XOR de 14 entradas se detiene en el límite de términos y lo dice; una comprobación que supera su presupuesto de tiempo informa de la misma manera.
Todo análisis del motor tiene un límite enunciado: las tablas de verdad se detienen en 12 entradas, los mapas de Karnaugh en 4 variables, las formas normales en 4.096 términos y 20.000 apariciones de literales, el simplificador en 500 pasos, y cada comprobación y conversión se ejecuta bajo un presupuesto de tiempo. Cuando se alcanza un límite, el resultado lleva un estado que dice qué límite, y ningún veredicto. El artefacto de esta página es uno de esos resultados: la forma normal disyuntiva de x1 XOR … XOR x14 tendría 8.192 términos de 14 literales cada uno, muy por encima de los límites, y el conversor informa de que un desarrollo intermedio superó las 20.000 apariciones de literales, en lugar de imprimir una forma truncada.
Una comprobación se comporta igual. Su veredicto es uno de tres, se cumple, no se cumple o desconocido, y el desconocido viene con una razón. La interfaz muestra el desconocido como «No determinado», y un resultado obsoleto, calculado para una revisión anterior del modelo, se etiqueta como obsoleto. Ninguno de ellos es un aprobado, y ninguno es un suspenso; la regla de resultados honestos mantiene separados el estado del transporte (¿terminó el cálculo?) y el veredicto (¿qué encontró?).
La consecuencia práctica para las pruebas es que un conjunto de pruebas que trate cualquier cosa distinta de «no se cumple» como éxito contará los tiempos agotados como aprobados. Lee el estado antes que el veredicto, y cuando una comprobación no esté determinada, reduce el modelo, añade supuestos que estrechen el alcance, o divide la regla en partes con nombre que el motor pueda comprobar una a una.
Un resultado que superó el límite
x1 XOR x2 XOR x3 XOR x4 XOR x5 XOR x6 XOR x7 XOR x8 XOR x9 XOR x10 XOR x11 XOR x12 XOR x13 XOR x14
14 entradas · límites: 4096 términos, 20000 literales
Forma normal conjuntiva (FNC)
Forma normal disyuntiva (FND)
El error habitual
Escribir un paso de integración continua que falla solo ante un contraejemplo. Una comprobación que agotó su presupuesto no produjo contraejemplo ni demostración; la CLI la informa como no determinada, y el paso debe tratarlo como un fallo al decidir, no como luz verde.
Preguntas
¿Por qué no subir simplemente los límites?
Porque la respuesta honesta a cualquier tamaño es la misma: o el cálculo terminó y el veredicto es exacto, o no terminó y no existe veredicto. Los límites mantienen rápido el primer caso y visible el segundo; subirlos mueve la línea, no la elimina.
¿Qué dice la exportación a SMT-LIB sobre el desconocido?
Lo mismo: su cabecera indica que unknown no resuelve nada, y que unsat lo comprueba el solucionador, no es una demostración verificada de forma independiente.
Relacionado
Herramientas
- Comprobador de equivalencia lógica: dos expresiones, veredicto exacto, contraejemplo
- Generador de tablas de verdad: cualquier expresión booleana, hasta 12 variables, con columnas intermedias
Véase también
- La cobertura no es corrección: las pruebas siguen necesitando resultados esperados
- Comprobación exhaustiva: definición, ejemplo y equivalente en inglés
- Solucionador SAT: definición, ejemplo y equivalente en inglés
- Lógica booleana en SMT-LIB: declare-const, assert y check-sat con Z3
- Conversor a FNC y FND: formas normales conjuntiva y disyuntiva, mintérminos y maxtérminos
- Lista de revisión de reglas de decisión (para analistas y revisores)
- Ley distributiva: A·(B+C) = A·B + A·C, ambas formas
Errores comunes
Generado a partir del motor de Tangibool, semántica tangibool-semantics/1, motor 1.0.0, compilación . Cada tabla, mapa, simplificación y veredicto de estas páginas lo calculó el motor de Tangibool al compilar el sitio, y cada afirmación la volvió a comprobar el mismo verificador exacto que usa la app. Los límites se indican donde aplican. © 2026 Foreranger LTD.