Я написал два решателя судоку в Z3, один раз с использованием 81 переменной, а другой с помощью функции, которая отображает координаты x и y в число в квадрате[x][y]. Я предполагаю, что вместо этого можно также использовать массив.
В чем разница между наличием массива Python переменных Z3, наличием массива Z3 или наличием функции в Z3? Когда я должен использовать какой?
Общеприменимого ответа на этот вопрос нет. Обычно существует более одного способа моделирования проблемы, и никогда не ясно, какой из них будет лучшим на практике. Как правило, имеет смысл держать его в рамках одной теории, поскольку это позволяет избежать дорогостоящих рассуждений о перекрестных теориях; т. е. придерживайтесь бит-векторов или (ограниченных) целых чисел, но не пытайтесь переводить целые числа в бит-векторы (например, термин int2bv по существу рассматривается Z3 как не интерпретируемый). Также известно, что есть лучшие решения для решения проблем с массивами, чем то, что реализовано в Z3, поэтому, если они не очень нужны, помогает их устранить.
