1
$\begingroup$

I need a way to solve linear and non-linear inequalities over the natural numbers. So equations like this should be solveable:

$\forall n, p, q \in \mathbb{N}. q \cdot (1 + n^p) \leq q$

From what I gather SMT solver should are a good choice for this. I'm not an expert on the area of SMT solvers so I would like guidance on what solver would be best suited for this task. Wikipedia lists many but it's not clear to me which one I should pick.

Any pointers are appreciated! This will be part of a larger program so I can't use online services.

$\endgroup$
6
  • $\begingroup$ wolframalpha.com is a great site that can solve many equations, and do many other things. I dunno if it can do what you specifically want to do with it, but i think its worth taking a look at it $\endgroup$
    – nir shahar
    Commented Jun 22, 2021 at 11:49
  • $\begingroup$ @nirshahar this will be part of a program. I can't rely on online services. $\endgroup$
    – John Smith
    Commented Jun 22, 2021 at 12:11
  • $\begingroup$ z3 is a well known SMT solver and supports non-linear arithmetic, but note that non-linear arithmetic are in general undecidable. $\endgroup$
    – tphilipp
    Commented Jun 22, 2021 at 14:22
  • 1
    $\begingroup$ Please don't delete and re-post closed questions; instead, edit them and then vote to re-open. My comment from before remains valid: Your question is too broad as it doesn't narrow down the set of constraints you want to deal with. "Linear and nonlinear constraints" includes all possible constraints. We can't guide you on picking a solver without more specific information about your requirements. $\endgroup$
    – D.W.
    Commented Jun 22, 2021 at 17:19
  • $\begingroup$ @D.W. It does include all possible constraints over the naturals. Why is that question invalid? I did edit my question. However the question remained closed with the request of either editing my question or reposting a new version. $\endgroup$
    – John Smith
    Commented Jun 22, 2021 at 17:40

1 Answer 1

2
$\begingroup$

You can't. There is no solver that can handle all constraints over the natural numbers and always finds a solution if one exists. The problem is undecidable, even without allowing variables in the exponent. (See, e.g., https://en.wikipedia.org/wiki/Hilbert%27s_tenth_problem.)

So, there is no one-size-fits-all solver.

For this reason, and for other reasons, instead many solvers target a particular class of constraints that they are good at: maybe it's linear constraints, or quadratic, or polynomial, or convex, or something else. So, figuring out how to narrow down the set of constraints you need to support and then looking for a solver tailored for those is generally a more useful approach than trying to find one solver that can handle everything.

You can try a general-purpose solver like Z3, but it is more focused on (fixed-length or bounded-length) bitvectors than (unlimited-length) natural numbers and integers, and I'm not optimistic about its ability to handle hard cases over the natural numbers. While it does have some support for nonlinear constraints, I think that support might be more focused on real numbers than on natural numbers; and in any case Z3's support for arithmetic is primarily focused on linear constraints. I'm especially pessimistic if you have a combination of nested quantifiers together with nonlinear constraints over the naturals. On the other hand, if you have an upper bound on the size of all variables than you can convert to bitvector arithmetic and you will be in a domain where Z3 might have a better chance.

As you can see, the specifics of the constraints matter a lot on what solver is most appropriate and on your chances of success.

$\endgroup$

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.