1
$\begingroup$

Z3 has bindings for various programming languages, e.g., C, C++, Java, Python, and so on. Are there any for Mathematica? Or how to implement one?

$\endgroup$
2
  • 2
    $\begingroup$ Curious. What do Z3 solvers offer over Mathematica's solvers? There are options in the Mma solver functions that give you fine control of thier algorithms and parameters. $\endgroup$
    – Edmund
    Commented Jul 31, 2023 at 13:30
  • $\begingroup$ Related 180728. $\endgroup$
    – Edmund
    Commented Jul 31, 2023 at 13:36

1 Answer 1

1
$\begingroup$

As you mentioned Z3 has different interfaces, here I'm going to show an example in Java via JLink.

The following code is written in a Windows environment and it's not guaranteed to work on other platforms.

First, download the library and extract it. I extract it in C:\\;

Then, we have to change the Path variable to include the directory library that was extracted (why Path? Because Java System.loadLibrary was used to load the library and this variable is used to search for its dependencies):

SetEnvironment["Path"->Environment["Path"]<>";C:\\z3-4.12.2-x64-win\\bin\\"]

then:

Needs["JLink`"]

We have to reinstall Java to make sure it uses the updated environment variable:

ReinstallJava[]

Include the directory where the library was extracted:

AddToClassPath["C:\\z3-4.12.2-x64-win\\bin\\"];

Here I copied the optimizeExample with slight modification:

optimizeExample=ExternalFunction["Java","
import com.microsoft.z3.*;
public static String optimizeExample(Context ctx) 
    {
        System.out.println(\"Opt\");

        Optimize opt = ctx.mkOptimize();

        IntExpr xExp = ctx.mkIntConst(\"x\");
        IntExpr yExp = ctx.mkIntConst(\"y\");

        opt.Add(ctx.mkEq(ctx.mkAdd(xExp, yExp), ctx.mkInt(10)),
                ctx.mkGe(xExp, ctx.mkInt(0)),
                ctx.mkGe(yExp, ctx.mkInt(0)));

        Optimize.Handle mx = opt.MkMaximize(xExp);
        Optimize.Handle my = opt.MkMaximize(yExp);

        
        return opt.Check().toString()+\" , \"+mx.toString()+\" , \"+my.toString();
       
    }
"]

Now just create a new context and call the function:

JavaBlock[
 Module[{ctx = JavaNew["com.microsoft.z3.Context"]},
    optimizeExample[ctx]
    ]
]

(* Out: "SATISFIABLE , 10 , 0" *)

From here you can write your problem in Java (preferably in another IDE), and expose parameters to use in Mathematica.

Remember, there is an overhead for calling Java (here it was 0.006) and in the case of using this to solve larger problems, the overhead of passing values will be added.

$\endgroup$
2
  • 2
    $\begingroup$ If the library is in java, you should be able to do everything you need using JLink and Mathematica code - without writing any java code at all. $\endgroup$
    – Jason B.
    Commented Jul 31, 2023 at 19:01
  • 1
    $\begingroup$ @JasonB. Yes, you're right we can but coding with JLink is a little bit hard (and harder when you deal with ... syntax and arrays in Java). That's why I recommended writing it in an IDE with a better autocompletion and checks instead. $\endgroup$
    – Ben Izd
    Commented Aug 2, 2023 at 17:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.