0

How can one find multiple answers using the package Z3 in Python? Also is there a way to integrate the SymPy.gcd in the Z3.Solve function?

Komheim
  • 1
  • 2
  • If you give a specific problem having multiple solutions, needing gcd, it would help direct an answer. Z3 is accessible to Python per https://ericpony.github.io/z3py-tutorial/guide-examples.htm. – smichr Feb 19 '22 at 17:12

1 Answers1

0

Multiple solutions: There are several different ways, but the best known method is to do a divide-and-conquer based method. See https://stackoverflow.com/a/70656700/936310 for details.

Mixing/matching z3 with SymPy: In general, no. You cannot use SymPy functions directly in your z3 code; as z3 has no means of neither accessing nor symbolically running SymPy code. You'd have to code these up yourself. And, for a function like gcd which is essentially recursive, it's not going to be an easy task. (That is, you can code it, but the solver is unlikely to deal with it in any efficient way.) But to get a better answer, you'll need to provide more details as to exactly what you are trying to do.

alias
  • 28,120
  • 2
  • 23
  • 40
  • I am currently working on https://projecteuler.net/problem=785, and need to set the gcd to the limit given from that problem. – Komheim Feb 20 '22 at 09:30