Python z3 solver returns 'unknown' for satisfiable constraints

[arkapravag22]

The z3Py constraints along with the required declarations have been given below in the link
[https://docs.google.com/document/d/1wgT0sMl-AJMfiNR3F2HJVXtb_IkeLsNv-P6H5fnZOak/edit?usp=sharing]

A similar set of equations with a smaller set of variables seems to work fine.

Please let me know how this issue can be resolved.

[NikolajBjorner]

z3 isn't suitable for this kind of problems. It contains terms of the form 0.09118819981813431.
In order to be sound as a priority, z3 uses big-num arithmetic. It tends to be more reasonable to tolerate floating point imprecisions for data-sets like these and gain much more efficient LP operations. Mainstream MIP solvers are more suitable.

[arkapravag22]

We have reduced the floating-point precision in z3Py using set_option(precision=7).

All the real floating-point numbers in the constraints have a maximum of 5 significant digits after the decimal.

Trying to solve 180 variables with 210 constraints in Linear Real Arithmetic, z3 returns UNKNOWN after a timeout time of 1 hour.

Here is what some of the constraints look line: [https://docs.google.com/document/d/1YOPIWBMyoV2grv3a72XVmsgZdvAqUHYsbvrOLHCWy3Q/edit?usp=sharing]

Is there anything we can try to fix this, or should we move to a different solver?