在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。这个实现能够在1秒内找到5x5魔方的解决方案，在13秒内找到6x6魔方的解决方案，在24秒内找到7x7魔方的解决方案(在我的计算机上)，因此它似乎比您的公式做得更好。