I recently did a seminar on decision procedures, and my talk was on Tarski's decision procedure for first-order real arithmetic.
Basically, the problem is that you have a formula with real variables and constants and the usual arithmetic operations like addition, subtraction, multiplication (division, too, if you want, but that doesn't make it any more powerful) and comparisons such as equality, inequality, greater/less than, greater/less than or equal and so on. And on top of that, you can have all of first-order logic, i.e. and, or, not and universal and existential quantifiers.
What you want is an algorithm that decides whether a given formula like that holds. Obviously, this is only interesting when you have quantifiers in there. For example, you could find out if some polynomial has a root (it turns out you can even find out how many), or whether it has positive roots or even whether it has global minima and maxima.
The decision procedure itself is a bit technical, so I will not go into detail here, but the central idea is the usage of Sturm chains. These are finite chains of polynomials that give information about the number and position of roots of a polynomial, and, in a slight modification, whether these roots fulfil give inequalities.
I have implemented this in Java for doule-precision floating point coefficients.
The basic process is this: the class Polynomial is an abstraction of a real polynomial with constant real coefficients that provides some convenience methods. A PolynomialSystem is a system of polynomial equations p(x)=0 and q(x)>0. If isSolvable() is called, the system does some simplifications to reduce itself to a system with one equation and several inequalities, then performs some case distinctions to rule out edge cases and finally, it computes a number of Sturm chains, evaluates their limits for infinity and applies a magical matrix to the result, and we get the number of solutions of the system.
The time is exponential with the number of inequalities, but it should be polynomial with the highest polynomial degree of the equations involved. Probably quadratic, but I didn't really think about that very much. It is not highly optimised or anything, but it works quite well as long as you don't put in too many inequality conditions.
I also included some bisection code to approximate these solutions up to a given precision. Giving a closed algebraic formula is not possible in the general case, as there exists no such formula for polynomials of a degree >4.
I might add some code for solving multivariate systems, too, but this requires the programme to perform complicated case distinctions dynamically, which is a bit tricky to do, and I would probably have to add some handling of arithmetic and logical expressions, which is a pain to code from scratch, so I don't know whether I'll do that any time soon.
Downloads
Sturm chain code (.tar.gz, 19.5 kB)
