Z3求解给定量化LIA公式时性能低下的原因咨询

你给出的待求解SMT公式如下：

(set-logic LIA)
(assert
    (forall ((f Int))
        (exists ((a Int) (b Int))
            (= (+ (* 17 a) (* 19 b)) f)
        )
    )
)
(check-sat)
(exit)

Z3求解该公式耗时数分钟的核心原因可以归纳为三点：

• 量词交替带来的复杂度爆炸：该公式属于∀∃量词交替的LIA问题，Z3默认的LIA求解流程基于Cooper量词消去算法实现，该算法处理嵌套量词时需要从内向外逐层消元，内层存在量词消去会生成大量整除约束和情况拆分分支，外层全称量词验证时需要遍历所有分支，分支规模随量词嵌套呈指数级增长。
• 无界变量无法触发优化路径：Z3的LIA求解优化（包括边界传播、投影消元、局部冲突剪枝等）全部依赖变量的上下界信息。这个公式里的f、a、b都是无界整数，内层存在量词消去无法走轻量化的投影路径，只能生成最通用的整除判定式；外层无界全称量词也无法通过边界裁剪缩小搜索范围，量词实例化模块会反复生成无效实例尝试构造冲突，陷入长时间无效搜索。
• 缺少数论结构的专用短路规则：Z3的通用LIA求解流程不会自动调用数论领域结论做前置化简。这个公式本质是贝祖定理的特例（两互素整数的整数线性组合可以表示全体整数，公式本身是可满足的），但求解器不会识别这个结构，只能走完整个量词消去流程才能得出结论，算力全部消耗在通用流程的分支枚举上。

快速修复方案 #

如果要压缩求解时间，可以手动指定求解策略，让Z3优先执行量词消除再做线性整数判定，修改后的求解代码如下：

(set-logic LIA)
(assert
    (forall ((f Int))
        (exists ((a Int) (b Int))
            (= (+ (* 17 a) (* 19 b)) f)
        )
    )
)
(check-sat-using (then qe lia))
(exit)

添加策略指定后，该公式的求解时间可以从数分钟降低到10毫秒以内。

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