标题: 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库求解四元一次不定方程的一组正整数特解

199a+299b+399c+499d=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( 199a + 299b + 399c + 499d == 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

19916+2991+3998+4991=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( 326x+78y == 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)+7892=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 = 199a + 299b + 399c + 499d == 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