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

创建: 2023-04-03 14:25
更新: 2023-04-04 12:22
链接: 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 :
    m   = s.model()
    print( 'x = %s, y = %s' % ( m[x], m[y] ) )
else :
    print( 'No solution' )
--------------------------------------------------------------------------

x = -22, y = 92

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

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

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

下面是盘古2.0给的实现

--------------------------------------------------------------------------
import z3

#
# Define the variables
#
a, b, c, d  = z3.Ints( 'a b c d' )
#
# Define the equation and constraint
#
eq          = 199*a + 299*b + 399*c + 499*d == 7174
con         = z3.And( a > 0, b > 0, c > 0, d > 0, a + b + c + d == 26 )
#
# Create a solver object and add the equation and constraint
#
solver      = z3.Solver()
solver.add( eq, con )
#
# Check if the solver is satisfiable and print the values of the variables
#
if solver.check() == z3.sat :
    m   = solver.model()
    print( "a = %s, b = %s, c = %s, d = %s" % ( m[a], m[b], m[c], m[d] ) )
else :
    print( 'No solution' )
--------------------------------------------------------------------------

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