在6×5棋盘上放置所有棋子
本文延续了作者关于使用大语言模型生成代码解决国际象棋问题的系列探索。这次作者使用Claude生成Z3/Python代码，解决一个经典谜题：如何在6×5的棋盘上放置所有棋子——包括王、后、两只车、两只象和两只马——使得它们互不攻击。文章展示了LLM在生成约束求解代码方面的能力。
背景速读
- 这是一个经典的棋盘放置谜题：在一个6×5的棋盘上放置所有国际象棋棋子（王、后、双车、双象、双马、八兵），使得它们互不攻击。这是"最大密度"排列问题的一个变体，常用于测试约束求解和逻辑编程。
- John D. Cook 是知名的数学家兼程序员博主，长期探讨数学、统计学与编程的交叉话题，尤其关注形式化方法和约束求解工具。
- Z3 是微软开发的高性能约束求解器（SMT求解器），常用于自动化推理、程序验证、符号执行和求解组合谜题。Z3的Python API允许用Python描述约束条件，自动搜索解。
- 这是作者系列实验的第三篇：前两篇分别用Claude生成Prolog代码、用ChatGPT生成Prolog代码来解决同一个谜题。本篇改用Claude生成Z3/Python代码，旨在比较不同大语言模型和不同求解范式（逻辑编程vs约束求解）在处理这类组合搜索问题时的表现。