我想知道是否可以使用命名表达式来实现软约束，而无需明确使用手动“跟踪”变量 .
-
在消息Soft/Hard constraints in Z3中，Leonardo解释了如何使用辅助布尔值以手动方式实现软约束 .
-
在以下消息：z3 behaviour changing on request for unsat core中，莱昂纳多说命名表达式基本上被视为模型查找的含义 .
使用上面第一条消息中描述的手动跟踪相当麻烦，因为它需要多次调用求解器（事实上，在最坏的情况下可能需要调用 2^n 来获得满足最大可能的软约束集合 n 软约束） . 是否有可能将这两个想法结合起来让Z3以更简单的方式实现软约束？基于这两个消息的想法，我天真地尝试了以下内容：
(set-option :produce-models true)
(set-option :produce-unsat-cores true)
(assert (! false :named absurd))
(check-sat)
我希望z3会告诉我 sat 因为在模型中将 absurd 作为 false 会满足这个人为的例子;但它产生了 unsat ;这是合理的，但不是很有用..
我很感激您提供的任何见解;或者给我一些关于z3如何更详细地使用命名表达式的文档 . （我浏览了手册，但没有在任何地方看到它们的详细解释 . ）
1 回答
命名表达式是SMT-LIB 2.0标准的一部分 . 在Z3中，它们只是使用辅助布尔常量的方法的“语法糖” .
在SMT-LIB 2.0标准中，命名表达式用于"tracking"命令的"tracking"断言（参见SMT-LIB 2.0 reference manual的第5.1.5节） . 在您的示例中，如果我们在
(check-sat)之后执行(get-unsat-core)，则会得到(absurd). Here是在线示例的链接 .关于软/硬约束，似乎你想要MaxSAT . Z3附带了一个使用2种不同算法的示例，使用C API和辅助布尔常量来实现MaxSAT . 最简单的就是使用以下基本思想 .
对于每个软约束
C_i，它断言b_i implies C_i，其中b_i是一个新的布尔变量 .b_i为false的赋值实际上忽略了约束C_i.使用
AtMostK形式的约束来强制最多Kb_i为false . 然后，我们可以使用线性搜索来找到可以满足的最大软约束数 . 我们也可以使用二进制搜索（在这种情况下，只需要log N调用，其中N是软约束的数量） . 在许多伪布尔解算器中使用这种方法的变体 .examples\maxsat的示例还包含Fu和Malik建议的更智能的算法 . 该示例还说明了如何编码约束AtMostK.