Solving an uncomplete nonlinear system of equations with Z3

Question

I am trying to make a solver for nonlinear system of equations using the Z3 library in c++. It will exists with multiple equations and variables. Depending on previous steps in my software, it could be that some variables are unknown.

When too many variables are unknown and the system does not have a single solution, I want to be notified about this.

I made a simple fictional system of equations for testing that looks as follows:

Ax = 1
Ay = 1
Bx = 3
By = 2
Cx = 7
Cy = Ay + (By - Ay) / (Bx - Ax) * (Cx - Ax)

I wrote the following code to solve the system, in this example fairly easy:

context ctx;
expr Ax = ctx.real_const("Ax");
expr Ay = ctx.real_const("Ay");
expr Bx = ctx.real_const("Bx");
expr By = ctx.real_const("By");
expr Cx = ctx.real_const("Cx");
expr Cy = ctx.real_const("Cy");
solver s(ctx);

s.add(Ax == 1);
s.add(Ay == 1);
s.add(Bx == 3);
s.add(By == 2);
s.add(Cx == 7);
s.add(Cy == Ay + (By - Ay) / (Bx - Ax) * (Cx - Ax));


std::cout << s.check() << "\n";
model m = s.get_model();

auto CySolution = m.eval(Cy, true);

std::cout << CySolution << "\n";

As output I get the following:

sat
4.0

When for example "Ax" would be unknown, this can be simulated using following code:

context ctx;
expr Ax = ctx.real_const("Ax");
expr Ay = ctx.real_const("Ay");
expr Bx = ctx.real_const("Bx");
expr By = ctx.real_const("By");
expr Cx = ctx.real_const("Cx");
expr Cy = ctx.real_const("Cy");
solver s(ctx);

//s.add(Ax == 1);
s.add(Ay == 1);
s.add(Bx == 3);
s.add(By == 2);
s.add(Cx == 7);
s.add(Cy == Ay + (By - Ay) / (Bx - Ax) * (Cx - Ax));


std::cout << s.check() << "\n";
model m = s.get_model();

auto CySolution = m.eval(Cy, true);

std::cout << CySolution << "\n";

Now the output is:

sat
(/ 78.0 23.0)

I have tried detect when this system of equations give an implicit solution using functions as "expr.get_sort()" or "expr.is_real", but there is never a difference between the complete solution and the implicit one.

Now I have two questions:

How can I interpret "(/ 78.0 23.0)"?
Is there a proper way to detect if the solution is an implicit function or not?

Thanks in advance for any help!

score 1 · Accepted Answer · answered Sep 21 '22 at 14:45

(/ 78.0 23.0) simply means 78/23, i.e., approx. 3.39. Z3 prints real-values in this format since they are infinitely precise; as the fraction might require an unbounded number of digits in general.

Your question regarding "proper way to detect is an implicit function" is a bit ambiguous. I assume what you mean is if there's a unique solution? That is, if a variable's value is "forced" by all the other equations or not?

If that's the case, i.e., to check that a solution is unique, you'd essentially get the first solution, then assert the negation of that solution and ask if there's some other solution with this additional constraint: If the solver comes back unsat then you know the solution was unique. See many questions on stack-overflow regarding how to get multiple solutions from the solver.

Indeed, I want to check if the solution is unique or not. Also as you suggested, I found other questions that gives examples how to check for multiple solutions. Thanks! — TijsVP, Sep 22 '22 at 06:53

Solving an uncomplete nonlinear system of equations with Z3

1 Answers1