使用SMT-LIB与Z3建模重量平衡谜题遇阻，求技术支持

你的建模思路是对的：用-1、0、1表示砝码放置在对侧、不使用、放置在同侧，以此组合出1到40的所有整数。但原代码的核心问题在于量词交替（forall 嵌套 exists）——SMT求解器对整数域的这类约束处理能力有限，通常会返回unknown或无法有效找到解。

修正方案：移除量词，展开有限约束 #

由于目标整数范围是明确的1到40（有限集合），我们可以直接为每个整数单独添加可达性断言，避免使用量词。具体步骤如下：

• 定义一个辅助函数is_reachable，用于判断某个整数是否能通过砝码组合得到；
• 为1到40的每个整数单独断言其可达性；
• 保留原有的砝码范围、递增约束。

修正后的代码 #

(declare-const w1 Int)
(declare-const w2 Int)
(declare-const w3 Int)
(declare-const w4 Int)

; 辅助函数：判断整数i是否可通过砝码组合表示
(define-fun is_reachable ((i Int)) Bool
  (exists ((j Int) (k Int) (l Int) (m Int))
    (and
      ; 限制每个砝码的使用状态：-1（对侧）、0（不用）、1（同侧）
      (or (= j -1) (= j 0) (= j 1))
      (or (= k -1) (= k 0) (= k 1))
      (or (= l -1) (= l 0) (= l 1))
      (or (= m -1) (= m 0) (= m 1))
      ; 组合后的重量等于目标整数i
      (= i (+ (* w1 j) (* w2 k) (* w3 l) (* w4 m)))
    )
  )
)

(assert (and
    ; 砝码重量范围
    (<= 1 w1 40)
    (<= 1 w2 40)
    (<= 1 w3 40)
    (<= 1 w4 40)
    
    ; 砝码重量递增排序
    (<= w1 w2)
    (<= w2 w3)
    (<= w3 w4)
    
    ; 断言1到40的所有整数都可被组合出来
    (is_reachable 1)
    (is_reachable 2)
    (is_reachable 3)
    (is_reachable 4)
    (is_reachable 5)
    (is_reachable 6)
    (is_reachable 7)
    (is_reachable 8)
    (is_reachable 9)
    (is_reachable 10)
    (is_reachable 11)
    (is_reachable 12)
    (is_reachable 13)
    (is_reachable 14)
    (is_reachable 15)
    (is_reachable 16)
    (is_reachable 17)
    (is_reachable 18)
    (is_reachable 19)
    (is_reachable 20)
    (is_reachable 21)
    (is_reachable 22)
    (is_reachable 23)
    (is_reachable 24)
    (is_reachable 25)
    (is_reachable 26)
    (is_reachable 27)
    (is_reachable 28)
    (is_reachable 29)
    (is_reachable 30)
    (is_reachable 31)
    (is_reachable 32)
    (is_reachable 33)
    (is_reachable 34)
    (is_reachable 35)
    (is_reachable 36)
    (is_reachable 37)
    (is_reachable 38)
    (is_reachable 39)
    (is_reachable 40)
))

(check-sat)
(get-model)

关键说明 #

• 移除量词后，问题转为有限约束的可满足性问题，Z3等SMT求解器可以快速处理并返回解；
• 最终求解得到的砝码应为w1=1, w2=3, w3=9, w4=27——这是经典的三进制砝码组合，每个数可通过三进制表示转换为±1的系数组合，刚好覆盖1到40的所有整数。

内容的提问来源于stack exchange，提问作者Kaloyan Stoykov