有限域下含多余未知量的非线性代数方程组求解优化方案咨询

Hey there! I totally get why you're stuck here—SymPy's nonlinsolve is fantastic for symbolic solving over continuous domains, but it's just not built to handle discrete, constrained problems like yours where each variable only has 5 fixed values. Let's walk through practical fixes and alternatives to get this working.

First, Trim Redundant Equations #

Looking at your system, some equations are duplicates thanks to basic algebra. For example, eqn2 and eqn4 are identical (multiplication is commutative, so x1*x2 = x2*x1, x10*x11 = x11*x10, etc.). The same goes for eqn3/eqn7 and eqn6/eqn8. Removing these duplicates will immediately lighten the computational load.

Switch to a Discrete Constraint Solver #

SymPy isn't optimized for brute-forcing or pruning discrete variable spaces efficiently. Instead, use an SMT (Satisfiability Modulo Theories) solver like Z3—it's designed exactly for problems with fixed discrete variables and logical constraints.

Here's a quick adaptation of your problem using Z3:

from z3 import Ints, Solver, And, Or

# Map x_i to integers: y_i = 2*x_i, so y_i ∈ {-2, -1, 0, 1, 2} (eliminates fractions)
y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16,y17,y18 = Ints('y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 y17 y18')
s = Solver()

# Set domain constraints for each y variable
for var in [y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16,y17,y18]:
    s.add(Or(var == -2, var == -1, var == 0, var == 1, var == 2))

# Convert equations to integer form (multiply through by 4 to remove fractions)
s.add(y1**2 - y10**2 + y4**2 - y13**2 + y7**2 - y16**2 == 4)
s.add(y1*y2 - y10*y11 + y4*y5 - y13*y14 + y7*y8 - y16*y17 == 0)
s.add(y1*y3 - y10*y12 + y4*y6 - y13*y15 + y7*y9 - y16*y18 == 0)
s.add(y2**2 - y11**2 + y5**2 - y14**2 + y8**2 - y17**2 == 2)
s.add(y2*y3 - y11*y12 + y5*y6 - y14*y15 + y8*y9 - y17*y18 == 0)
s.add(y3**2 - y12**2 + y6**2 - y15**2 + y9**2 - y18**2 == 0)

# Add remaining non-redundant equations
s.add(y1*y11 - y10*y2 + y4*y14 - y13*y5 + y7*y17 - y16*y8 == 0)
s.add(y1*y12 - y10*y3 + y4*y15 - y13*y6 + y7*y18 - y16*y9 == 0)
s.add(y2*y10 - y11*y1 + y5*y13 - y14*y4 + y8*y16 - y17*y7 == 0)
s.add(y2*y12 - y11*y3 + y5*y15 - y14*y6 + y8*y18 - y17*y9 == 0)
s.add(y3*y10 - y12*y1 + y6*y13 - y15*y4 + y9*y16 - y18*y7 == 0)
s.add(y3*y11 - y12*y2 + y6*y14 - y15*y5 + y9*y17 - y18*y8 == 0)

# Add non-triviality constraints (square sums can't be zero)
s.add(y1**2 + y2**2 + y3**2 >= 1)
s.add(y4**2 + y5**2 + y6**2 >= 1)
s.add(y7**2 + y8**2 + y9**2 >= 1)
s.add(y10**2 + y11**2 + y12**2 >= 1)
s.add(y13**2 + y14**2 + y15**2 >= 1)
s.add(y16**2 + y17**2 + y18**2 >= 1)

# Check for solutions
if s.check() == sat:
    model = s.model()
    # Convert back to original x values (x = y/2)
    solution = {f"x{i+1}": model[var].as_long()/2 for i, var in enumerate([y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16,y17,y18])}
    print(solution)
else:
    print("No solution found")

If You Want to Stick with SymPy #

If you prefer using SymPy, you need to manually prune the search space instead of letting nonlinsolve handle it:

• Start with equations that only involve squared terms (eqn1, eqn5, eqn9) since they have fewer possible combinations.
• Generate all valid tuples for the variables in these equations, then iterate through them to check other equations incrementally.
• Use itertools.product for small variable subsets, filter valid combinations, then build up to the full set.

Here's a partial example to get you started:

from sympy import symbols
import itertools

x1,x10,x4,x13,x7,x16 = symbols('x1 x10 x4 x13 x7 x16')
domain = [-1, -1/2, 0, 1/2, 1]

# Generate all valid combinations for variables in eqn1
valid_eqn1 = []
for vals in itertools.product(domain, repeat=6):
    x1_val, x10_val, x4_val, x13_val, x7_val, x16_val = vals
    if x1_val**2 - x10_val**2 + x4_val**2 - x13_val**2 + x7_val**2 - x16_val**2 == 1:
        valid_eqn1.append(vals)

# Next, take each valid tuple and check against eqn5, then eqn9, adding more variables each time

Why Your Original Code Hangs #

SymPy's nonlinsolve first tries to find symbolic solutions over the real numbers, then applies domain constraints as an afterthought. With 18 variables and non-linear terms, this creates an enormous search space that SymPy can't navigate efficiently. Discrete solvers like Z3 use smart pruning techniques (backtracking, constraint propagation) to eliminate impossible combinations early.

备注：内容来源于stack exchange，提问作者rooted-and-grounded