如何用SymPy求解器判断变量是否为固定值？

核心思路 #

对于每个变量，只需判断是否存在解使得变量取1以及是否存在解使得变量取-1：

• 如果仅存在取1的解，变量固定为1；
• 如果仅存在取-1的解，变量固定为-1；
• 两种情况都存在则变量不固定。

这种方法避免了遍历所有解（指数级耗时），也不需要单独求解单个变量（会忽略变量间的约束），而是通过可满足性检查直接验证变量取值的可能性。

实现方案 #

方法1：直接使用原变量与satisfiable #

利用SymPy的satisfiable函数检查约束+变量取值的组合是否有解：

from sympy import symbols, Eq, And, satisfiable

# 定义变量
ep0c1, ep0c2, ep1c2 = symbols('ep0c1 ep0c2 ep1c2')

# 约束方程组（建议用Eq形式更清晰）
constraints = [
    Eq(ep0c1**2, 1),
    Eq(ep0c2**2, 1),
    Eq(ep1c2**2, 1),
    Eq(25*ep1c2 + 25, 0)
]

fixed_vars = {}
for var in [ep0c1, ep0c2, ep1c2]:
    # 检查变量取1时是否存在有效解
    has_one = satisfiable(And(*constraints, Eq(var, 1)))
    # 检查变量取-1时是否存在有效解
    has_neg_one = satisfiable(And(*constraints, Eq(var, -1)))
    
    if has_one and not has_neg_one:
        fixed_vars[var] = 1
    elif not has_one and has_neg_one:
        fixed_vars[var] = -1

print(fixed_vars)  # 输出: {ep1c2: -1}

方法2：布尔变量转化（更高效处理多变量场景） #

将±1变量转化为布尔变量（b=True对应原变量=1，b=False对应原变量=-1），利用布尔SAT求解器的优势提升效率：

from sympy import symbols, Eq, And, satisfiable

# 定义布尔变量
b0c1, b0c2, b1c2 = symbols('b0c1 b0c2 b1c2', boolean=True)
# 布尔变量与原变量的映射：x = 2b - 1
var_map = {
    b0c1: 2*b0c1 - 1,
    b0c2: 2*b0c2 - 1,
    b1c2: 2*b1c2 - 1
}

# 原约束转化为布尔表达式
constraints = [
    Eq(var_map[b1c2]**2, 1),
    Eq(25*var_map[b1c2] + 25, 0)
]
# 过滤恒成立的约束（比如x²=1对±1变量自动成立）
bool_constraints = [c for c in constraints if not c.is_true]

fixed_vars = {}
for b_var, orig_var_expr in var_map.items():
    has_true = satisfiable(And(*bool_constraints, b_var))
    has_false = satisfiable(And(*bool_constraints, ~b_var))
    
    if has_true and not has_false:
        fixed_vars[orig_var_expr.subs(b_var, True)] = 1
    elif not has_true and has_false:
        fixed_vars[orig_var_expr.subs(b_var, False)] = -1

print(fixed_vars)  # 输出: {ep1c2: -1}

关键说明 #

• satisfiable函数专门用于判断逻辑命题是否存在解，内部采用优化的SAT求解算法，远快于遍历所有可能的变量组合；
• 避免单独求解单个变量：单独求解时会将其他变量视为自由变量，无法捕捉变量间的约束关系，导致判断错误；
• 多变量场景下，布尔变量转化的方法效率更高，因为SAT求解器对布尔约束的处理更成熟。

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