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.