ChatGPT用Python3的z3库求解不定方程

创建: 2023-04-03 14:25
https://scz.617.cn/python/202304031425.txt

z3库真香，以前看初等数论时，没用这类工具，亏了。感谢「0x指纹」提供信息。

pip3 install z3-solver

我是这样问ChatGPT的

请用Python3的z3库求解四元一次不定方程的一组正整数特解

199*a+299*b+399*c+499*d=7174
a+b+c+d=26

ChatGPT给了一段可用代码

import z3

#
# Create four integer variables a, b, c, and d
#
a, b, c, d  = z3.Ints( 'a b c d' )
#
# Create a solver
#
s           = z3.Solver()
#
# Add constraints
#
s.add( 199*a + 299*b + 399*c + 499*d == 7174 )
s.add( a + b + c + d == 26 )
s.add( a >  0 )
s.add( b > 0 )
s.add( c > 0 )
s.add( d > 0 )
#
# Solve the equations
#
if s.check() == z3.sat :
    #
    # Print a non-zero solution
    #
    print( 'a =', s.model()[a] )
    print( 'b =', s.model()[b] )
    print( 'c =', s.model()[c] )
    print( 'd =', s.model()[d] )
else :
    print( 'No solution' )

a = 16
b = 1
c = 8
d = 1

199*16+299*1+399*8+499*1=7174

一个有趣之处是，「0x指纹」让GPT-4和Claude+直接求解前述不定方程，未果。但我加了约束条件，问GPT-3.5如何用z3库求解，它就解出来了。经验教训是，尽可能增强向GPT提问时的约束条件。

行文至此，重新问GPT-3.5一个之前GPT-4求解失败的问题，不让GPT直接求解，而是指明用z3库求解。

请用Python3的z3库求解二元一次不定方程的一组非零整数特解

326x+78y=4

果然，GPT-3.5求解成功。

import z3

x, y    = z3.Ints( 'x y' )
s       = z3.Solver()
s.add( 326*x+78*y == 4 )
s.add( x != 0 )
s.add( y != 0 )
if s.check() == z3.sat :
    print( 'x =', s.model()[x] )
    print( 'y =', s.model()[y] )
else :
    print( 'No solution' )

x = -22
y = 92

326*(-22)+78*92=4

该组特解与手工辗转相除法求得的特解完全相同。

逆向工程中可能遭遇求解多元不定方程的需求，写keygen的更有同感，z3库是很好的生产力工具，GPT更是生产力工具。诸君宜沉下心来拥抱变化，勿流于形式。再就是，多多交流为上，一个人的精力有限，有靠谱的同行者时，可省去不少试错成本。