I think the example cheats a lot by assuming the solutions have to be positive integers. Is there a mechanism to tell the system "a and b are integers", and if so, could the system still solve the simultaneous equation?
About solving systems of simultaneous equations, I don't know if this particular solver can do it but many solvers can by using Gaussian Elimination from linear algebra.
This is basically logic programming. If you really want to do something like this, you are far better off just using a logic language like prolog and saving yourself the trouble.
The article is an introduction to Constraint Satisfaction Problems (CSP's). http://en.wikipedia.org/wiki/Constraint_satisfaction_problem
A very rudimentary demonstration of this: http://aispace.org/constraint/sample2.html
Norvig implemented a quick and dirty version of this for his sudoku solver: http://norvig.com/sudoku.html.
Note, while you eventually end up just telling a CSP what you want, there's a plethora of algorithms to solve these constraints.