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

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?

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?


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!

• So, what is your question? Nov 9, 2012 at 22:49
• Do you want the software to solve the algebra problems, or do you just want it to randomly generate questions that match a certain LaTeX format? Nov 9, 2012 at 23:16
• I need the software to solve algebra problems. I'm wondering what are my options in this regard. Nov 12, 2012 at 17:46
• The guys at mathematica.stackexchange.com are more than capable to help you Mathematica wise. Nov 12, 2012 at 17:49

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.

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