Z3 Forall com array

Question

Z3 fornece desconhecido para o problema simples:

(assert
(forall ((y (Array Int Int)))
   (= (select y 1) 0))
 )
(check-sat)

Descobri que se torna sat se negar o forall, mas isso parece uma coisa particularmente simples de não ser possível resolver.

Isso está causando problemas porque a classe de problemas que desejo resolver é mais como,

(declare-fun u () Int)
(assert
 (forall ((y (Array Int Int)) )
     (=> 
        (= u 0) (<= (select y 1) 0))
 )
)
(check-sat)

Onde negar o forall sozinho não é o mesmo problema, então isso não pode ser feito aqui. Existe alguma maneira de apresentar esse tipo de problema ao Z3 para obter um resultado não satisfatório?

Answer 1

Problemas com quantificadores são sempre problemáticos com solucionadores SMT, especialmente se envolverem matrizes e quantificadores alternados como em seu exemplo. Você essencialmente tem exits u. forall y. P(u, y). Z3, ou qualquer outro solucionador SMT, terá dificuldade em lidar com esses tipos de problemas.

Quando você tem uma asserção quantificada como você faz quando está forallno nível superior ou aninhada com exists, a lógica se torna semidecidível. Z3 usa MBQI (instanciação de quantificador baseada em modelo) para resolver heuristicamente tais problemas, mas na maioria das vezes falha em fazê-lo. O problema não é apenas o z3 não ser capaz: não há procedimento de decisão para esses problemas e o z3 faz o melhor.

Você pode tentar fornecer padrões quantificadores para tais problemas para ajudar o z3, mas não vejo uma maneira fácil de aplicar isso ao seu problema. (Padrões quantificadores se aplicam quando você tem funções não interpretadas e axiomas quantificados.https://rise4fun.com/z3/tutorialcontent/guide#h28) Então, eu não acho que vai funcionar para você. Mesmo que existisse, os padrões são muito exigentes para programar e não robustos com relação a mudanças em sua especificação que, de outra forma, poderiam parecer inócuas.

Se você está lidando com tais quantificadores, os solucionadores SMT provavelmente não são uma boa opção. Procure provadores de teoremas semiautomáticos, como Lean, Isabelle, Coq, etc., que são projetados para lidar com quantificadores de uma maneira muito mais disciplinada. Claro, você perde a automação total, mas a maioria dessas ferramentas pode usar um solucionador SMT para descarregar submetas que são "fáceis" o suficiente. Dessa forma, você ainda faz o "trabalho pesado" manualmente, mas a maioria das submetas é tratada automaticamente pelo z3. (Especialmente no caso do Lean, veja aqui:https://leanprover.github.io/)

Answer 2

Há um parêntese de fechamento extra (à direita), que precisa ser removido. Além disso, adicione assert antes da instrução forall.

(assert ( forall ( (y (Array Int Int) ) ) 
   (= (select y 1) 0) 
))
(check-sat)

Execute o código acima e você deverá obter unsat como a resposta.

Para o segundo programa, a resposta do alias pode ser útil para você.