es.davy.ai

Preguntas y respuestas de programación confiables

¿Tienes una pregunta?

Si tienes alguna pregunta, puedes hacerla a continuación o ingresar lo que estás buscando.

Encontrar contraejemplos para un objeto solucionador “Horn”.

05 Aug, 2023 Programación

Estoy tratando de aprender cómo escribir código para proporcionar un contraejemplo a una cláusula de Horn y su interpretación adivinada. En el código siguiente, sea I la función no interpretada (es una invarianza de bucle trivial). Las primeras 3 s.add() agregan los requisitos de condición para I(x), y la cuarta es una suposición candidata para I. Intento usar la instrucción s.prove para obtener un contraejemplo a mi suposición adivinada para I. Parece que estoy obteniendo un gran registro de errores al ejecutar este código, ¿alguien podría decirme qué está mal?

s = SolverFor("HORN")
I = Function('I', IntSort(), BoolSort())
x, x2 = Ints('x x2')
s.set("produce-proofs", True)
s.add(ForAll([x], Implies(x == 0, I(x))))
s.add(ForAll([x, x2], Implies(And(I(x), x2 == x + 1, x < 5), I(x2))))
s.add(ForAll([x], Implies(And(I(x), Not(x < 5)), x == 5)))
s.add(ForAll([x], And(Implies(I(x), x == 2), Implies(x == 2, I(x)))))
# ¡Añadiendo invariante adivinado aquí!
assert unsat == s.check()
print(s.proof())
Tags:  ,

Answer

  1. Avatar for davy.ai
    davy.ai

    Hay un par de problemas con el código proporcionado:

    • La variable unsat no está definida. Esto causaría un NameError al ejecutar el código.
    • La afirmación assert unsat == s.check() asume que el solucionador debe producir un resultado de insatisfacibilidad, lo cual puede no ser el caso. Dependiendo de la entrada, el solucionador puede producir satisfacibilidad o desconocido como resultado. Es mejor verificar el resultado devuelto por s.check() y manejarlo en consecuencia.
    • Parece haber un error tipográfico en la cuarta cláusula de ForAll. La condición Implies( I(x) , (x == 2) ) debería ser Implies( I(x) , (x2 == 2) ).

    Aquí hay una versión corregida del código:

    s = SolverFor("HORN")
I = Function('I', IntSort(), BoolSort())
x, x2 = Ints('x x2')
s.set("produce-proofs", True)
s.add(ForAll([x], Implies(x == 0, I(x))))
s.add(ForAll([x, x2], Implies(And(I(x), x2 == x + 1, x < 5), I(x2))))
s.add(ForAll([x], Implies(And(I(x), Not(x < 5)), x == 5)))
s.add(ForAll([x], And(Implies(I(x), x2 == 2), Implies(x2 == 2, I(x)))))
result = s.check()
if result == unsat:
    print(s.proof())
else:
    print("Resultado del solucionador:", result)

    Esta versión verifica el resultado devuelto por s.check() e imprime la prueba solo si devuelve unsat. Si el resultado es sat o unknown, imprime el resultado del solucionador.

Comments are closed.