如何在Z3 C++ API中直接使用平方根求解方程组？

当然有更可靠的直接方案！你遇到的结果不准确问题，根源在于平方替换会引入伪解——比如x*x = 4的解是2和-2，但数学上sqrt(4)的结果只有非负的2，这就是替换法出错的核心原因。

Z3的实数理论原生支持平方根函数，在C++ API中可以直接通过z3::sqrt()调用，它完全符合数学中平方根的定义（仅返回非负实数解，且自动约束根号内的表达式非负），能避免替换法带来的额外解问题。

示例代码 #

下面是一个简单的使用示例，直接求解x = sqrt(4)：

#include <z3++.h>
using namespace z3;

int main() {
    context c;
    expr x = c.real_const("x");
    solver s(c);
    
    // 直接调用sqrt函数，无需手动平方替换
    s.add(x == sqrt(c.real_val(4)));
    
    if (s.check() == sat) {
        model m = s.get_model();
        std::cout << "x = " << m.eval(x) << std::endl;
        // 输出结果只会是x = 2，不会出现-2
    } else {
        std::cout << "unsat" << std::endl;
    }
    return 0;
}

处理复杂平方根表达式 #

对于更复杂的场景，比如sqrt(x + 5) = 3，直接使用sqrt函数的优势更明显：

// 替换法需要手动添加约束，否则会得到无效解
// s.add((x + 5) == 9);
// s.add(x + 5 >= 0); // 必须手动加，否则会得到x=-14（无意义）

// 直接用sqrt函数的话，Z3会自动处理定义域约束
s.add(sqrt(x + c.real_val(5)) == c.real_val(3));

这种情况下，Z3会自动确保x +5 >=0，求解结果只会是x=4，不会出现无效的负数值解。

为什么替换法会失效？ #

替换法本质是将等式a = sqrt(b)转化为a*a = b，但丢失了两个关键约束：

1. a >= 0（平方根的结果非负）
2. b >= 0（根号内的表达式必须非负）
   如果你的场景没有手动补充这两个约束，就会出现不符合数学定义的伪解，导致结果不准确。

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