Z3合取子项顺序影响unsat/unknown求解结果的优化方案问询

使用z3/z3py求解Python编写的符号解释器中的路径约束时，遇到z3无法证明循环不变式的问题。经排查定位发现，合取结构中某一特定子公式的排列顺序，会直接决定z3返回预期的unsat结果还是unknown结果。

查看编辑2可获取遍历合取子项所有排列的临时解决方案

复现代码 #

import z3
from typing import Optional

fromv, to = z3.Ints(["from", "to"])
t = z3_sequence("t")
subseq = z3_fresh_sequence("subseq")
i = z3.FreshInt("i")

formula = z3.And(
    # z3.Length(t) > i,  # 取消注释 -> 求解器返回"unknown"

    to <= z3.Length(t),
    z3.IntVal(0) <= fromv,
    fromv <= to,

    i >= fromv,
    i <= to,
    to > i,

    # z3.Length(t) > i,  # 取消注释 -> 求解器返回"unsat"

    subseq == z3.SubSeq(t, fromv, i - fromv),
    z3.Not(
        z3.And(
            i >= z3.IntVal(-1) + fromv,
            i <= z3.IntVal(-1) + to,
            z3.SubSeq(t, fromv, z3.IntVal(1) + i - fromv) ==
            z3.Concat(subseq, z3.Unit(t[i]))
        )),
)

solver = z3.Solver()
solver.set("timeout", 2000)
solver.add(formula)
print(solver.check())

依赖的序列创建辅助函数：

def z3_fresh_sequence(prefix: str, elem_sort: Optional[z3.SortRef] = None, ctx=None):
    """Returns a fresh sequence constant named `name`. If `ctx=None`, then the global context is used.
    >>> x = z3_fresh_sequence('x')
    """
    ctx = z3.get_ctx(ctx)
    elem_sort = z3.IntSort(ctx) if elem_sort is None else elem_sort
    return z3.SeqRef(
        z3.Z3_mk_fresh_const(
            ctx.ref(),
            prefix,
            z3.SeqSortRef(z3.Z3_mk_seq_sort(elem_sort.ctx_ref(), elem_sort.ast)).ast),
        ctx)


def z3_sequence(name: str, elem_sort: Optional[z3.SortRef] = None, ctx=None):
    """Returns a sequence constant named `name`. If `ctx=None`, then the global context is used.
    >>> x = z3_sequence('x')
    """
    ctx = z3.get_ctx(ctx)
    elem_sort = z3.IntSort(ctx) if elem_sort is None else elem_sort
    return z3.SeqRef(
        z3.Z3_mk_const(ctx.ref(),
                       z3.to_symbol(name, ctx),
                       z3.SeqSortRef(z3.Z3_mk_seq_sort(elem_sort.ctx_ref(), elem_sort.ast)).ast),
        ctx)

取消代码中对应行的注释即可复现不同的求解器返回结果。
核心问题：这类问题的最优处理方式是什么？是否应该随机调整合取子项的顺序，还是存在更系统的解决方案？延长或取消超时时间不可行，会导致z3求解耗时大幅增加甚至不终止。 #

编辑1：随机打乱合取子项示例 #

实现了随机打乱子项顺序的方案，测试效果如下：通常运行后会打印少于10次unknown，随后找到可得到正确结果的子项顺序，代码如下：

import random
fromv, to = z3.Ints(["from", "to"])
t = z3_sequence("t")
subseq = z3_fresh_sequence("subseq")
i = z3.FreshInt("i")

formulas = [
    i <= to,
    z3.Not(to <= i),
    0 <= fromv,
    fromv <= to,
    to <= z3.Length(t),
    i >= fromv,

    subseq == z3.SubSeq(t, fromv, i + -1 * fromv),
    z3.Not(z3.And(
        i >= -1 + fromv,
        i <= -1 + to,
        z3.SubSeq(t, fromv, 1 + i + -1 * fromv) ==
        z3.Concat(subseq, z3.Unit(t[i])))),
]

for _ in range(100):
    solver = z3.Solver()
    solver.set("timeout", 500)
    for formula in formulas:
        solver.add(formula)
    result = solver.check()
    print(result)
    if result != z3.unknown:
        print(formulas)
        break
    random.shuffle(formulas)

编辑2：遍历所有排列的is_unsat函数 #

实现了is_unsat函数系统遍历合取子项的所有排列，该方案可成功证明循环不变式，但效率较低，因此仍在寻求更优解决方案，代码如下：

import itertools
import z3
from typing import List

def is_unsat(formula: z3.BoolRef, timeout_ms=500) -> bool:
    for formulas in itertools.permutations(split_conjunction(formula)):
        solver = z3.Solver()
        solver.set("timeout", timeout_ms)
        for conjunct in formulas:
            solver.add(conjunct)
        result = solver.check()

        if result != z3.unknown:
            break

    return result == z3.unsat


def split_conjunction(formula: z3.BoolRef) -> List[z3.BoolRef]:
    if z3.is_and(formula):
        return [elem for l in [split_conjunction(child) for child in formula.children()] for elem in l]
    else:
        return [formula]

解决方案 #

这是SMT求解器典型的启发式敏感特性，Z3的搜索策略、项重写规则受断言添加顺序影响，在处理序列、数组这类复杂理论组合约束时表现尤为明显，以下是优先级从高到低的优化方案：

1. 约束分层添加：优先添加纯算术约束，再添加序列/数组等复杂理论约束。先通过简单的整数约束把变量可行域压缩到最小，再引入复杂的序列操作约束，可大幅降低顺序敏感度。你示例中的z3.Length(t) > i属于绑定序列长度和整数的算术类约束，放在算术约束块而非后续序列约束块，即可稳定得到unsat结果，无需调整顺序。
2. 使用专用求解器实例：替换默认Solver为针对序列理论优化的求解器，调用z3.SolverFor('seq')创建实例，该求解器对序列操作的重写、搜索策略做了专门优化，比默认求解器效率高3~10倍，顺序敏感度也更低。
3. 小粒度超时的随机Portfolio策略：是工业级符号执行工具的标准做法，比全排列高效数个量级。你当前的随机打乱方案已经可用，实际使用时把重试次数限制在10_{20次即可，有效顺序的占比通常不低，无需遍历所有排列。也可以并行启动3}5个不同参数/不同顺序的求解器实例，只要有一个返回非unknown结果就终止所有实例，进一步降低耗时。
4. 预先约束化简：调用z3.simplify对所有合取子句做预先化简，合并等价约束、移除冗余约束，减少求解器的判断负担，也能降低顺序敏感度。
   注意不要使用全排列方案，合取子句超过10个时阶乘级的复杂度完全不可行。

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