Решение магических квадратов в Z3

Question

Я новичок в Z3, и в качестве попытки попытался использовать магический квадрат, адаптировав существующий решатель судоку (http://lauri.võsandi.com/tub/qaoes/z3.html). Я не даю никаких фактов (т. Е. Никаких конкретных чисел в конкретных блоках), кроме суммы всех строк, столбцов и основных диагоналей, равно и записи различны и в диапазоне [1, N * N]. Он отлично подходит для квадратов размером до 4. Все выше, и я отказываюсь ждать решения.

Это нормально? Или опытные программисты z3 предполагают, что у моей реализации есть проблемы, поскольку проблемы такого размера должны быть разрешимы?

Спасибо.

Answer 1

Вы можете получить лучшие результаты, выразив запись в каждой ячейке как переменную BitVec(), а не переменную Int().

См. https://github.com/0vercl0k/z3-playground/blob/master/magic_square_z3.py для примера реализации. Эта реализация способна найти решение для магического квадрата 5x5 за 1 секунду, 6x6 магического квадрата за 13 секунд и магического квадрата 7x7 за 24 секунды (на моем компьютере), поэтому он, кажется, делает значительно лучше, чем ваша формулировка ,