otimizações de sudoku

[arademaker]

O artigo que usamos em #10 apresenta a codificação do problema em CNF. Podemos ter uma representação mais intuitiva das regras "at most" usando a mesma idéia do que usamos no problema dos vestidos para dizer que cada pessoa só vestia uma cor. Podemos experimentar o desempenho do Tableaux com esta nova representação.

[bernardorusso]

Fiz um pull request com novo arquivo "sudoku-1" com as modificações nas cláusulas "at most"

[arademaker]

conforme falamos hoje, podemos explorar mais as equivalências:

'(and
        (implies A (and (not B) (not C)))
        (implies B (and (not A) (not C)))
        (implies C (and (not A) (not B))))  

'(and
        (implies A (and (not B) (not C)))
        (implies B (not C)))

'(and (or (not A) (not B)) (or (not A) (not C)) (or (not B) (not C)))

Intuitivamente, sabendo que (and X (or A B)) é equivalente a (or (and X A) (and X B) e que (implies A B) é equivalente a (or (not A) B), podemos pensar em realmente provar esta equivalência.

tableaux> (prove '(and (or (not A) (not B)) (or (not A) (not C)) (or (not B) (not C))))
((<[true] A> <[true] B>) (<[true] B> <[true] C>)
 (<[true] A> <[true] C>))

tableaux> (prove '(and
           (implies A (and (not B) (not C)))
           (implies B (not C))))
((<[true] B> <[true] A>) (<[true] C> <[true] B>)
 (<[true] C> <[true] A>))

A intuição de que a segunda fórmula acima é suficiente é que estamos querendo garantir um AT MOST entre as 3. Se A e B ou A e C forem verdade, a primeira implicação é falsa. Resta então apenas dizer que B e C também não podem ser verdade, o que negaria a segunda implicação.

[arademaker]

Resta sabermos se a codificação alternativa proposta pelo @bernardorusso é equivalente a proposta no artigo.

[bernardorusso]

Todas as implicações devem ser Verdadeiras Como a cláusula é da forma "at most one", queremos que, se um átomo é T, todos os outros são F.

A1 => ~(A2 ou A3 ou ... ou An ) A2 => ~(A3 ou A4 ou ... ou An ) . . . An-1 => ~An

Supomos que Ak é T (1<=k<=n) Ak => ~(Ak+1 ou ... ou An) Ak => ~Ak+1 e ~Ak+2 e ... e ~An

Como A=>(B e C) <=> (A=>B) e (A=>C), (Ak => ~Ak+1) e ... e (Ak => ~An) Como Ak é T, Ak+1,...,An são todos F (a sentença acima é verdadeira)

Para um j<k, (Aj => ~Aj+1) e ... e (Aj => ~Ak) e ... e (Aj => ~An) onde Aj => ~Ak é T se e somente se Aj é F

Portanto, dado um k qualquer, provamos que se Ak é T, todos os outros são F, garantindo a propriedade "at most one" da cláusula.

(Vale para todas as cláusulas b)

[arademaker]

obrigado por colocar aqui sua argumentação.

[arademaker]

ainda pensando em como contornar a complexidade deste problema, poderíamos ter alguns testes que recebam tabuleiros que transformados em valorações para as letras proposicionais, nos permitiriam "testar"se as clausulas estão corretas.

[arademaker]

Duas leituras relevantes sobre o problema:

http://maude.sip.ucm.es/~miguelpt/papers/sudoku.pdf https://sites.google.com/site/modante/sudokusolver

[arademaker]

podemos ver também se prove do tableaux está efetivamente fazendo busca em largura ou profundidade.