我想在整数空间中找到满足某些属性的n维点(x1...xn)，同时还最大化x与m（预定义/常数）n维点(z11...z1n, z21...z2n... zm1...zmn)的集合中的任何元素之间的最小距离。有没有办法用Z3做到这一点？
当然。见：https://rise4fun.com/Z3/tutorial/optimization
上面的链接讨论了SMTLib接口，但同样也可以从Python接口获得。 （以及与Z3的大多数其他绑定。）
请注意，优化主要用于线性属性。如果您有非线性项，则可能需要对它们进行表达，以便可以优化线性计数器部分。即使使用非线性术语，您也可能获得良好的结果，如果不尝试就无法知道。