How to solve generic algebraic problem using solver/library programmatically? Matlab, Mathematica, Wolfram etc?

Question

I'm trying to build an algebra trainer for students. I want to construct a representative problem, define constraints and relationships on the parameters, and then generate a bunch of Latex formatted problems from the representation. As an example:

A specific question might be:

If y < 0 and (x+3)(y-5) = 0, what is x?

Answer (x = -3)

I would like to encode this as a Latex formatted problem like.

If $y<0$ and $(x+constant_1)(y+constant_2)=0$ what is the value of x?
Answer = -constant_1

And plug into my problem solver

constant_1 > 0, constant_1 < 60, constant_1 = INTEGER
constant_2 < 0, constant_2 > -60, constant_2 = INTEGER

Then it will randomly construct me pairs of (constant_1, constant_2) that I can feed into my Latex generator.

Obviously this is an extremely simple example with no real "solving" but hopefully it gets the point across.

Things I'm looking for ideally in priority order
* Solve algebra problems
* Definition of relationships relatively straight forward
* Rich support for latex formatting (not just writing encoded strings)

Thanks!

Answer 1

Here is a paper that does what I believe you are asking for.

Rohit Singh, Sumit Gulwani, Sriram Rajamani: Automatically Generating Algebra Problems. AAAI 2012

Answer 2

Depending on the theory you're interested in working in, it sounds like an SMT solver (e.g. e.g. Z3) will solve your problem. SMT solvers allow you to enter a set of constraints on your variables and tell you whether there are any solutions that satisfy all the constraints. If there are any solutions, it will give you one.

So for example, your sample problem corresponds to the following Z3 query:

(declare-fun x () Int)
(declare-fun y () Int)

(assert (< y 0))
(assert (=
         (*
           (+ x 3)
           (- y 5)
         )
         0))

(check-sat)
(get-model)
(exit)

to which Z3 gives the answer y = -5, x = -3. You can enumerate more solutions by adding the constraint that y != -5 or x != 3:

(declare-fun x () Int)
(declare-fun y () Int)

(assert (< y 0))
(assert (=
         (*
           (+ x 3)
           (- y 5)
         )
         0))
(assert (or
         (not (= y (- 5)))
         (not (= x (- 3)))
))

(check-sat)
(get-model)
(exit)

which gives x = -3, y = -13.