Z3 parte 2 - Resolvendo Sudoku

Este é um artigo de continuação Para o primeiro artigo

Neste artigo vou ensiná-lo como resolver Sudoku usando Z3, a fim de resolver Sudoku ou qualquer outro desafio matemático você deve primeiro entender quais são as regras do desafio.

Depois de ter entendido as regras, você deve defini-las ao Z3 e ele próprio encontrará os números que se encaixam nessas regras.

Para baixar o código do artigo
Para baixar o exercício que apresentei no vídeo

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

Então, se olharmos para o quadro sudoku do seguinte site:

Podemos dividi-lo nas seguintes 4 regras:

• Em cada célula, devemos inserir um número de 1 a 9
• Cada linha deve conter números únicos
• Cada coluna deve conter números únicos
• Cada pequeno quadrado de 3 por 3 deve conter números únicos

Agora vamos pegar essas regras e transformá-las em código, passo a passo.

Vamos começar definindo as variáveis:

As variáveis:

• game – Irá conter o jogo inteiro na lista sendo que cada célula do jogo é equivalente a uma linha no tabuleiro
• board_rules – Irá conter a regra de que cada célula deve ter um número entre 1 e 9
• row_rules – Irá conter a regra de que cada linha deve ser única
• column_rules – Irá conter a regra de que cada coluna deve ser única
• cube_3x3_rules – Irá conter a regra de que cada pequeno quadrado deve ser único

Uma vez definidas nossas variáveis, passaremos para a definição das regras, definiremos o jogo para conter as variáveis do tipo Int e definiremos que cada célula deve estar entre 1 e 9 usando and da seguinte maneira:

Para garantir que cada linha tenha números exclusivos, usaremos Distinct assim:

Para definir que cada coluna tenha números únicos iremos manter todos os números da coluna na variável auxiliar e a seguir iremos realizar Distinct de novo como fizemos anteriormente:

Passaremos à definição das regras do cubo pequeno de 3 por 3, para isso definiremos uma variável auxiliar que conterá todos os cubos:

Vamos agora definir uma série de condições que irão dividir todos os valores em-[game[x][y De acordo com os quadrados:

Depois de terminar de dividir todos os valores por suas posições em cubos, faremos Distinct em cada cubo individualmente e salvaremos o resultado em cube_3x3_rules.

Assim que terminarmos de definir todas as regras do jogo precisamos adicionar uma última regra que definirá nosso estado inicial no tabuleiro, para isso definiremos a variável auxiliar start_position_rules:

E vamos definir o estado inicial assim:

] Assim, vamos definir uma condição em Z3 usando If, a condição irá verificar se o valor no local -[game[x][y é 0, então não criaremos nenhuma outra regra se tivermos qualquer outro número, o valor no local-[game[x][y Deve ser igual a este número.

Agora precisamos adicionar todas essas regras ao Z3 Solver, que resolverá o sudoku para nós:

Verificaremos se as regras que definimos fazem sentido e se nosso sudoku pode ser resolvido e, em seguida, resolveremos o sudoku usando o model assim:

O resultado ficará assim: