Z3中Record、数组（集合）及未解释字段常量的使用问题

一、建模逻辑问题：Unsat原因与修正 #

你的初始代码返回Unsat，核心问题是forall量词作用于所有可能的Student实例，而非仅你声明的S001、S002。

原断言：

(assert (forall ((l Student) (r Student)) (xor (= l r) (distinct (seat l) (seat r)))))

这个断言要求：任意两个Student，要么是同一个对象，要么座位必须不同。但Z3的类型是开放的，除了你声明的S001、S002，还存在无数其他Student实例（比如姓名为"Charlie"的，或者姓名和S001相同但座位不同的）。由于座位只有A-G共7种，必然存在不同学生座位相同的情况，直接触发断言矛盾，导致返回Unsat。

修正方案 #

针对少量学生的直接约束

如果只需要约束已声明的S001、S002座位不同，去掉量词，用简单断言即可：

(declare-datatypes () ((Seat A B C D E F G)))
(declare-datatypes () ((Student (mkstudent (name String) (seat Seat)))))
(declare-const S001 Student)
(declare-const S002 Student)
(assert (= (name S001) "Alice"))
(assert (= (name S002) "Bob"))
(assert (distinct (seat S001) (seat S002))) ; 直接约束两个学生座位不同
(check-sat)
(get-model)

针对多学生的量化约束

如果后续要扩展到多个学生，可先通过数组/序列定义学生集合，再用量词遍历集合内元素约束唯一性：

(declare-datatypes () ((Seat A B C D E F G)))
(declare-datatypes () ((Student (mkstudent (name String) (seat Seat)))))
(declare-const students (Array Int Student))
(assert (= (name (select students 0)) "Alice"))
(assert (= (name (select students 1)) "Bob"))
(assert (= (name (select students 2)) "Charlie"))
; 约束数组中0-2索引的学生，任意两个不同学生座位不同
(assert (forall ((i Int) (j Int))
    (implies (and (>= i 0) (<= i 2) (>= j 0) (<= j 2) (distinct i j))
             (distinct (seat (select students i)) (seat (select students j))))))
(check-sat)
(get-model)

二、优雅建模方案：批量定义学生 #

Z3的SMT语法不支持直接匿名留空未解释字段（比如你期望的(mkstudent "Alice" _)写法），但可以通过以下方式简化建模：

方案1：数组+批量断言姓名 #

用数组存储学生，对每个数组索引的学生断言姓名，座位自动成为未解释变量（Z3会为其分配合法值）：

(declare-datatypes () ((Seat A B C D E F G)))
(declare-datatypes () ((Student (mkstudent (name String) (seat Seat)))))
; 声明存储学生的数组，索引用0、1、2...对应不同学生
(declare-const students (Array Int Student))

; 批量断言每个学生的姓名
(assert (= (name (select students 0)) "Alice"))
(assert (= (name (select students 1)) "Bob"))
(assert (= (name (select students 2)) "Charlie"))

; 可选：约束所有学生座位唯一
(assert (forall ((i Int) (j Int))
    (implies (and (>= i 0) (<= i 2) (>= j 0) (<= j 2) (distinct i j))
             (distinct (seat (select students i)) (seat (select students j))))))

(check-sat)
(get-model)

方案2：序列+量化断言姓名 #

用序列类型存储学生，结合断言和量词约束姓名与座位唯一性：

(declare-datatypes () ((Seat A B C D E F G)))
(declare-datatypes () ((Student (mkstudent (name String) (seat Seat)))))
(declare-const students (Seq Student))

; 断言序列包含3个学生
(assert (= (seq.len students) 3))
; 断言每个位置的学生姓名
(assert (= (name (seq.at students 0)) "Alice"))
(assert (= (name (seq.at students 1)) "Bob"))
(assert (= (name (seq.at students 2)) "Charlie"))

; 约束序列中任意两个不同位置的学生座位不同
(assert (forall ((i Int) (j Int))
    (implies (and (>= i 0) (< i (seq.len students))
                  (>= j 0) (< j (seq.len students))
                  (distinct i j))
             (distinct (seat (seq.at students i)) (seat (seq.at students j))))))

(check-sat)
(get-model)

方案3：宏定义简化构造 #

Z3的define-fun不能在内部声明局部常量，但可以通过宏定义简化学生构造的写法，配合全局座位变量实现批量建模：

(declare-datatypes () ((Seat A B C D E F G)))
(declare-datatypes () ((Student (mkstudent (name String) (seat Seat)))))

; 声明学生的座位变量
(declare-const seat_alice Seat)
(declare-const seat_bob Seat)
(declare-const seat_charlie Seat)

; 宏定义快速创建学生（简化重复写法）
(define-fun mk-student-with-name ((n String) (s Seat)) Student
    (mkstudent n s))

; 声明学生数组
(declare-const students (Array Int Student))
(assert (= (select students 0) (mk-student-with-name "Alice" seat_alice)))
(assert (= (select students 1) (mk-student-with-name "Bob" seat_bob)))
(assert (= (select students 2) (mk-student-with-name "Charlie" seat_charlie)))

; 约束座位唯一
(assert (distinct seat_alice seat_bob seat_charlie))

(check-sat)
(get-model)

关键注意点 #

• Z3中没有“局部未解释常量”的概念，所有未解释变量都需要全局声明，或通过量化式引入（但量化式会增加求解复杂度）。
• 批量建模的核心是用数组/序列组织学生，通过断言或量化式约束字段值，避免逐个声明独立的Student常量。

内容的提问来源于stack exchange，提问作者Jason Kleban