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.
January 28, 2022