主要观点：

• 作者将“Linkedin Queens”问题表示为 SAT 问题并使用 CVC5 求解，后用 Z3 展示在 SMT 级别求解该问题更易，且效率低于原始 SAT 求解器但仍比 SAT 求解更易，以此解释为何人们更倾向于 SMT 而非 SAT。
• 强调在编码过程中要进行 sanity check，通过添加测试和检查来尽早发现错误，如检查区域编码是否正确等。

关键信息：

• 2025 年 6 月 12 日，下周无 newsletter，作者将在Systems Distributed演讲，其演讲尚未完成导致本期 newsletter 较晚且简短。
• “Linkedin Queens”问题是在 NxN 网格中放置 N 个皇后，每行、列和区域各一个且对角线上不能相邻，这是“Star Battle”游戏的变体。
• 用 SAT 表示皇后位置需 N²个布尔变量，而在 SMT 中可编码为 N 个整数，如“queens[n] = col of queen on row n”。
• 在 Z3 中通过一系列约束条件来求解“Linkedin Queens”问题，包括约束整数在[0, N)范围内、不同列、非对角相邻等，最后通过solver.check()和solver.model()获取解。
• 进行 sanity check 的代码，包括检查是否遗漏或重复方块的测试，以及打印区域的代码以确认编码正确。

重要细节：

• 区域需手动编码，如“purple”区域的坐标等。
• 作者在编码中使用 0 基索引是个错误，导致后续编码区域很困难。
• 未对代码进行大量清理，时间紧迫。
• 未对 SMT 求解的时间进行基准测试，但想象其比原始 SAT 求解器慢。
• 可以通过这里订阅 newsletter，作者主要网站为这里，新书《Logic for Programmers》已进入早期访问，可这里获取。
• 对“Boolean SATisfiability Solver”（SAT 求解器）和“Satisfiability Modulo Theories”（SMT）进行了简单解释和引用。