Z3 integer expression expected while trying to solve an equation

Question

I'm completely new to Z3, so bear with me. I have the following values (see code below):

n, a, b, c

I need to find out:

m, n, q

These are 512 bit prime numbers:

p, q

n is just a multiplication result of p and q. a is a result of m by the power of p with a modulus of n. b is equal to the m poewr of q with a modulus of n again, c is equal to m to the power of n and a modulus of n. I tried the following code:

from z3 import *

s = Solver()
m = Int('m')
p = Int('p')
q = Int('q')
n = 101205131618457490641888226172378900782027938652382007193297646066245321085334424928920128567827889452079884571045344711457176257019858157287424646000972526730522884040459357134430948940886663606586037466289300864147185085616790054121654786459639161527509024925015109654917697542322418538800304501255357308131
a = 38686943509950033726712042913718602015746270494794620817845630744834821038141855935687477445507431250618882887343417719366326751444481151632966047740583539454488232216388308299503129892656814962238386222995387787074530151173515835774172341113153924268653274210010830431617266231895651198976989796620254642528
b = 83977895709438322981595417453453058400465353471362634652936475655371158094363869813512319678334779139681172477729044378942906546785697439730712057649619691929500952253818768414839548038664187232924265128952392200845425064991075296143440829148415481807496095010301335416711112897000382336725454278461965303477
c = 21459707600930866066419234194792759634183685313775248277484460333960658047171300820279668556014320938220170794027117386852057041210320434076253459389230704653466300429747719579911728990434338588576613885658479123772761552010662234507298817973164062457755456249314287213795660922615911433075228241429771610549

s.add(n == p * q,m ** p % n == a,m ** q % n == b,m ** n % n == c)
print(s.check())
print(s.model())

But apparently I get the following error:

Traceback (most recent call last):
  File "/home/user/Downloads/Test/Test1/Test1/solve.py", line 12, in <module>
    s.add(n == p * q,m ** p % n == a,m ** q % n == b,m ** n % n == c)
  File "/home/user/.local/lib/python3.10/site-packages/z3/z3.py", line 2568, in __mod__
    _z3_assert(a.is_int(), "Z3 integer expression expected")
  File "/home/user/.local/lib/python3.10/site-packages/z3/z3.py", line 107, in _z3_assert
    raise Z3Exception(msg)                                                                                                                                                                                                                 
z3.z3types.Z3Exception: Z3 integer expression expected

How do I correctly solve this equation?

According to this I've already tried setting the numbers to Real, but it didn't help: z3.z3types.Z3Exception: Z3 integer expression expected

Answer 1

Using ToInt will solve the "integer-expression expected" problem:

from z3 import *

s = Solver()
m = Int('m')
p = Int('p')
q = Int('q')
n = 101205131618457490641888226172378900782027938652382007193297646066245321085334424928920128567827889452079884571045344711457176257019858157287424646000972526730522884040459357134430948940886663606586037466289300864147185085616790054121654786459639161527509024925015109654917697542322418538800304501255357308131
a = 38686943509950033726712042913718602015746270494794620817845630744834821038141855935687477445507431250618882887343417719366326751444481151632966047740583539454488232216388308299503129892656814962238386222995387787074530151173515835774172341113153924268653274210010830431617266231895651198976989796620254642528
b = 83977895709438322981595417453453058400465353471362634652936475655371158094363869813512319678334779139681172477729044378942906546785697439730712057649619691929500952253818768414839548038664187232924265128952392200845425064991075296143440829148415481807496095010301335416711112897000382336725454278461965303477
c = 21459707600930866066419234194792759634183685313775248277484460333960658047171300820279668556014320938220170794027117386852057041210320434076253459389230704653466300429747719579911728990434338588576613885658479123772761552010662234507298817973164062457755456249314287213795660922615911433075228241429771610549

s.add(n == p * q, ToInt(m ** p) % n == a, ToInt(m ** q) % n == b, ToInt(m ** n) % n == c)
print(s.check())

This prints:

unknown

But you won't be able to use z3 to actually "solve" this system. Note that it said unknown, an admission that this is too difficult for an SMT solver to handle. (So, if you run print(s.model()) you'll get an error message after this, since there's no model.)

As to why this is too difficult to handle: Because of non-linear arithmetic. Multiplication of variables, raising to constant/variable powers etc. create very difficult problems; and an SMT solver won't be able to get you a solution. More technically, such equations over integers do not have a decision procedure, and solvers do their best but usually give up quickly as in this case. See https://stackoverflow.com/a/13898524/936310 for a more detailed answer for why.

As a side note: You're essentially trying to factor very large integers, and this is an inherently difficult problem. Expecting an automated SMT solver to do this for you is not realistic. SMT solvers are excellent tools for reasoning with booleans, linear-arithmetic, data-types, etc.; but not for solving equations from number theory.