distribued Z3

Mar 9, 2015 at 6:41 PM
As a newbie I apologize in advance if this question has already be answered.

Is there any kind of distribued implementation of Z3?

Thank you in advance
Coordinator
Mar 20, 2015 at 8:48 PM
Edited Mar 20, 2015 at 8:50 PM
No there isn't. Z3 has parallel_and/_or tactics built in, but there are no distribution mechanisms. Is there a specific need for which this would be required, e.g., huge files?
Mar 20, 2015 at 10:45 PM
Edited Mar 20, 2015 at 10:46 PM
Thank you for the information.

In fact I am trying to use SMT's as an approach to the Learning Parity with Noise (LPN) problem. It is quite straightforward to reduce LPN to a Heavy Fourier Coefficients problem which can be directly represented by a SMT constraint. The constraint is just an expantion of the Walsh-Hadamard transform: we get a huge sum with a term for each sample of the LPN oracle. I have used QF-BV and with a single bit vector variable.


In a single i3 processor I can solve a 16 bit LPN in about 200sec; a 32 bit LPN did not produce an answer after 48 hours. However, in my research group, we have a private cloud with quite a bunch of these processors; I was wondering if I could use this setup to speed up the search.

Obviously, since LPN is probably NP-hard, we may not expect much; however there is allways hope !!