阅读： 9

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更是生产力工具。诸君宜沉下心来拥抱变化，勿流于形式。再就是，多多交流为上，一个人的精力有限，有靠谱的同行者时，可省去不少试错成本。

版权声明
本站“技术博客”所有内容的版权持有者为绿盟科技集团股份有限公司（“绿盟科技”）。作为分享技术资讯的平台，绿盟科技期待与广大用户互动交流，并欢迎在标明出处（绿盟科技-技术博客）及网址的情形下，全文转发。
上述情形之外的任何使用形式，均需提前向绿盟科技（010-68438880-5462）申请版权授权。如擅自使用，绿盟科技保留追责权利。同时，如因擅自使用博客内容引发法律纠纷，由使用者自行承担全部法律责任，与绿盟科技无关。