Объявить матрицу с неизвестным размером в Z3
Я знаю, что я могу объявить матрицу z3.Real в Z3 объявив его элементы индивидуально (может быть, через понимание списка). Есть ли способ представить матрицу с неизвестным размером?
Например, рассмотрим следующий пример: при фильтрации изображений, для изображения I size [X,Y] и ядро фильтра K из size [M,N], свертка между изображением I и ядро фильтра K является I*K, мне бы хотелось Z3 доказать (или опровергнуть) существование фильтра F1 а также F2 любого размера, такого, что I*K == I*F1*F2,
Сама проблема полностью решена и, вероятно, не имеет смысла. Идея в том, могу ли я спросить Z3 найти матрицу неизвестного размера, такую, чтобы матрица удовлетворяла определенному свойству, которое может быть выражено линейной функцией. Спасибо!
2 ответа
Z3 поддерживает просто типизированные логические спецификации первого порядка. В некотором смысле, первый вопрос заключается в том, как бы вы выразили интересующие вас свойства в логике. Для моделей ограниченного размера вы можете создавать экземпляры размеров X,Y, M, N и выражать запросы контрпримеров для подходящего конечного домена. Если вам нужны параметрические размеры, вы бы выразили поведение * как троичное отношение. Например, вы можете использовать функции I, K, I_K, которые принимают два аргумента и выражают, как I_K(x,y) относится к записям в I, K. Затем вы столкнетесь с такими проблемами, как доказательства действительно требуют индукции. Среды с хорошей поддержкой взаимодействия, такие как Lean, PVS, Coq, Isabelle или среды, такие как Dafny, больше подходят для создания доказательств.
Ответ Николая, кажется, ударил гвоздь по голове. Я думаю, что Z3 (или любой SMT-решатель) не будет лучшим инструментом для решения таких проблем, когда вы ожидаете рассуждать о матрицах "неизвестных" размеров, как вы выразились. Когда у вас есть конкретные примеры проблемы, я думаю, что Z3 может быть достаточно эффективным; но не в общем случае. Такие заявления обычно требуют индуктивных доказательств и лучше подходят для других инструментов.
Тем не менее, вы можете сойти с неинтерпретированных функций. Если вы представляете свою матрицу и фильтры как неинтерпретированные функции и кодируете свою свертку в терминах этого. Вам, вероятно, придется принять верхнюю границу для NxM (то есть, N < 100, M < 100 или аналогичное) и соответствующим образом кодировать, чтобы все, что выходит за пределы, приводило к подходящим результатам. (Что это означает, конечно, будет зависеть от рассматриваемой проблемы.)
Вы можете быть удивлены тем, насколько крутой Z3 может быть при таких настройках, так как я подозреваю, что это даст вам довольно хорошие результаты. Я хотел бы услышать, что вы узнаете, если вы попробуете этот подход.