Z3 parte 1 - o Básico

Z3 É um Solver SMT escrito pela Microsoft: https://github.com/Z3Prover/z3

Pessoalmente, tive que usar o Z3 em vários desafios diferentes. Quando você precisa encontrar uma senha para um nome de usuário e a lógica é matemática, Z3 o ajudará a encontrar a senha

Abaixo está um vídeo que demonstra como realizar o processo:

Solver É uma espécie de extensão para-SAT Solver (satisfiability), SAT Solver Obtém um conjunto de condições e verifica se elas retornam True ou False. Se todas as condições retornarem True, um sinal de que temos uma solução para as condições obtidas.

SAT Funciona apenas com condições booleanas, o SMT faz o mesmo para todos os tipos de condições para que possamos escrever um exercício matemático padrão ou inserir nele algum problema que desejamos resolver para nós.

por exemplo:

(x > 1 OR y < 5) AND (x = 2 OR x = 3 and x = y) AND (y > 0 OR x>y)

Nosso software verificará todas as condições e chegará a uma solução, pegara na primeira linha a x > 1 Então, na segunda linha o

x = 3 and x = y E na terceira linha o y > 0 Tudo funciona, então a resposta é True.

Mas no caso de recebermos algo assim:

( x > 2*x, x > 0 )

Ficamos com unsat porque o exercício não pode ser resolvido, então quando trabalharmos com z3, primeiro verificaremos se o exercício pode ser resolvido usando o comando check() E só então vamos resolver-lo usando ()model O que parece assim.:

If solv.check() == sat:    solv.model()

Para instalar o z3, usaremos o seguinte comando:

pip install z3-solver

No Z3 primeiro temos que definir nossas variáveis usando INT, BitVec, Bool ou qualquer outra coisa dependendo do exercício, por exemplo, se quisermos resolver o próximo exercício facilmente sem realizar um teste:

x = Int('x') y = Int('y') solve(x > 2, y < 10, x + 2*y == 7)

É assim que realmente definimos x e y, que são números que correspondem ao exercício matemático que é colocado no solve e o resultado é:

[y = 0, x = 7]

Também é possível simplificar um exercício matemático atravez do comando simplify assim:

x = Int('x') y = Int('y') print simplify(x + y + 2*x + 4)

O resultado será uma simplificação do exercício matemático:

4 + 3*x + y

Ao definir um exercício matemático ele pode ser mantido em uma variável e então será possível trabalhar com ele da seguinte maneira:

x = Int('x') y = Int('y') n = x + y >= 3 print n print "num args: ", n.num_args() print "children: ", n.children() print "1st child:", n.arg(0) print "2nd child:", n.arg(1) print "operator: ", n.decl() print "op name: ", n.decl().name()

O resultado ficará assim:

Se quisermos que o resultado seja em números reais (números quebrados), Usaremos-Real:

x = Real('x') y = Real('y') solve(x**2 + y**2 == 3, x**3 == 2) set_option(precision=30) print "Solving, and displaying result with 30 decimal places" solve(x**2 + y**2 == 3, x**3 == 2)

O resultado:

Usamos aqui o comando.:

set_option(precision=30)

Então, basicamente definimos quantos dígitos queremos após o ponto, a ideia por trás de set_option é basicamente uma definição do ambiente do z3.
Se houver uma variável True ou False iremos defini-la dessa forma:

p = Bool('p') q = Bool('q') r = Bool('r') solve(r == Not(q), Or(Not(p), r))

E o resultado será assim.:

[q = True, p = False, r = False]

Se fizermos algum exercício matemático como você viu no vídeo e tentarmos resolvê-lo:

No total teremos que definir todas as nossas variáveis e as condições do exercício da seguinte maneira, primeiro vamos definir todas as nossas variáveis:

`from z3 import *

x1 = Int("x1")
x2 = Int("x2")
x3 = Int("x3")
x4 = Int("x4")
x5 = Int("x5")
x6 = Int("x6")
x7 = Int("x7")
x8 = Int("x8")
x9 = Int("x9")
`

Em seguida, definiremos um solver para que possamos colocar nossas regras nele e examiná-lo:

solv = Solver() solv.add(x1+13*x2/x3+x4+12*x5-x6-11+x7*x8/x9-10 == 66) solv.add(x1 > 0, x2 >0 ,x3 >0 ,x4 > 0,x5 >0 ,x6>0,x7>0,x8>8,x9>0)

Finalmente, verificaremos se o exercício pode ser resolvido usando o SAT Solver e pediremos ao z3 para resolver o exercício usandomodel-:

`if solv.check() == sat:
     print solv.model()
else:
     print "failed to solve"

`

O resultado ficará assim:

No próximo artigo, vou mostrar como você pode resolver o sudoku usando o z3 e até mesmo resolver um exercício de engenharia reversa que exige que deciframos qual é a senha usando z3, vale a pena esperar!