如何用sorted、key和lambda对Z3模型变量列表按序号排序？

你当前的排序逻辑是基于变量名的字符串比较，这会导致字典序排序而非数字序排序：比如字符串"x_10"会排在"x_2"前面，因为字符'1'的ASCII值小于'2'，这就是排序混乱的核心原因。

正确的排序实现 #

需要从变量名中提取出数字部分并转为整数，以此作为排序依据：

solved = solver.model()
# 提取变量名中的序号数字，转为整数后排序
sorted_vars = sorted(
    [(var, solved[var]) for var in solved],
    key=lambda item: int(str(item[0]).split('_')[1])
)

代码说明 #

1. str(item[0])：将Z3变量对象转为字符串形式（如"x_2"）
2. split('_')[1]：通过下划线分割字符串，提取出序号部分（如"2"）
3. int(...)：将序号字符串转为整数，确保按数字大小排序

预期排序结果 #

执行后变量会按x_0 → x_1 → x_2 → ... → x_10 → x_11 ...的顺序排列，示例开头部分为：

[(x_0, 0), (x_1, 1), (x_2, 0), (x_3, 27), (x_4, 23), (x_5, 1), (x_6, 1), (x_7, 2), (x_8, 27), (x_9, 20), (x_10, 2), ...]

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