SMT-LIB语言中的“at-most”关键字是什么意思（Z3 FixedPoint的扩展版）答案

【问题标题】：what's the meaning of "at-most" keyword in SMT-LIB language (extended version of Z3 FixedPoint)SMT-LIB语言中的“at-most”关键字是什么意思（Z3 FixedPoint的扩展版）
【发布时间】：2020-11-15 05:57:04
【问题描述】：

喜欢这个文件中规则中的“最多”关键字：

horn1.smt2（来自 Z3 github 存储库示例/python/data）

(declare-rel Goal (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool))
(declare-rel Invariant (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool))
(declare-var A Bool)
(declare-var B Bool)
(declare-var C Bool)
(declare-var D Bool)
(declare-var E Bool)
(declare-var F Bool)
(declare-var G Bool)
(declare-var H Bool)
(declare-var I Bool)
(declare-var J Bool)
(declare-var K Bool)
(declare-var L Bool)
(declare-var M Bool)
(declare-var N Bool)
(declare-var O Bool)
(declare-var P Bool)
(declare-var Q Bool)
(declare-var R Bool)
(declare-var S Bool)
(declare-var T Bool)
(declare-var U Bool)
(declare-var V Bool)
(declare-var W Bool)
(declare-var X Bool)
(rule (=> (not (or L K J I H G F E D C B A)) (Invariant L K J I H G F E D C B A)))
(rule (let ((a!1 (and (Invariant X W V U T S R Q P O N M)
                (=> (not (and true)) (not F))
                (=> (not (and true)) (not E))
                (=> (not (and W)) (not D))
                (=> (not (and W)) (not C))
                (=> (not (and U)) (not B))
                (=> (not (and U)) (not A))
                (= L (xor F X))
                (= K (xor E W))
                (= J (xor D V))
                (= I (xor C U))
                (= H (xor B T))
                (= G (xor A S))
                (=> D (not E))
                (=> C (not E))
                (=> B (not C))
                (=> A (not C))
                ((_ at-most 5) L K J I H G))))
  (=> a!1 (Invariant L K J I H G F E D C B A))))
(rule (=> (and (Invariant L K J I H G F E D C B A) L (not K) J (not I) H G)
    (Goal L K J I H G F E D C B A)))
(query Goal)

似乎关键字“最多”的含义是六个字面量（L K J I H G）中只有五个字面量可以同时为真，或者它意味着什么，我想不通。如果有任何好人可以帮助我，我真的很感激。

【问题讨论】：

标签： smt horn

【解决方案1】：

这些是伪布尔函数，有关详细信息，请参阅此答案：K-out-of-N constraint in Z3Py

基本上：

at-most: 最多就这么多吧
at-least：至少有这么多是真的
pble: 最多就是这么多，加权
pbge: 至少有这么多，加权
pbeq: 就是这么多，加权

加权版本本质上是布尔值的乘数，并采用整数的常量列表。

请注意，这些是 z3 特定的，实际上并未在 SMTLib 中定义。当然，也可能有其他求解器支持它。

【讨论】：