16

Allow solving for variables

under review

John Wiegley

By incorporating a free solver like Z3, one could imagine expressions such as:

solve for x in 0 = (x + 100) / 20

solve for x in 0 < (x + 100) / 20

Recent versions of Z3 support MaxSAT too, allowing for:

solve for min x in 0 < (x + 100) / 20

Multiple variables could be stated as:

solve for x, y in x + y = 100

When using MaxSAT on multiple variables, one can ask for the types of models desired, such as Pareto fronts, lexicographically, or each objective being optimized independently.

Once a solution is found, subsequent lines in the sheet would have access to variables

x

and y

whose values were discovered by the solver.