The SMTLIB package has been extended to support satisfiability queries on Boolean combinations of polynomial equations and inequalities.
Consider the following description of a set:
We can use first use SMTLIB[Satisfiable] to verify that a solution exists:
In this simple two-dimensional case, we can use plots[inequal] to visualize the solution space:
The new command SMTLIB[Satisfy] offers an efficient method of finding a concrete example for a point in the solution space:
To produce a satisfying point within the visual bounds of the plot above, we can simply augment our system with a bounding rectangle: