3 ms·

I’m curious: Has there been any research on optimization in the opposite direction? Start with the most naively implemented correct function—a giant switch/nest

I’m curious: Has there been any research on optimization in the opposite direction? Start with the most naively implemented correct function—a giant switch/nested if covering all possible inputs—and transform it piecewise in a correctness-preserving manner?

UncleMeat 3y ago
Mostly yes. There is a lot of research on taking arbitrary programs and distilling constraints and invariants out of them or doing various forms of function simplification.
boothby 3y ago
I've done this. In my experience it ends up stuck in local minima from which there are no obvious correctness-preserving improvements. Add Monte Carlo to escape valleys and this mode of exploration is still too timid to find anything close to optimal. When you find a truly optimal solution, you end up with the least satisfying proof of correctness: "Here's this this inscrutable formula; I verified that it produces the right output for all possible inputs."
retrac 3y ago
A similar problem comes up in digital design. Behaviour is often specified in terms of exhaustive truth tables, perhaps tables that were generated automatically, from a hardware description language. While such a table can be directly translated into a circuit, doing so in a naive fashion is potentially extremely non-optimal. Optimizing it is a hard problem. Everything has been tried, from exhaustive search (suitable only for small numbers of terms), to rule-based fuzzy backtracking searches, to in recent years, deep learning. But at least when I was in school a couple decades ago, the best known algorithm was still a person playing with the terms on graph paper, rearranging them until patterns emerged: https://en.wikipedia.org/wiki/Karnaugh_map https://en.wikipedia.org/wiki/Karnaugh_map As I understand it, there are recent advances in SAT solvers giving practical algorithms for much larger numbers of terms, but I'm much behind the state of the art at this point.

UncleMeat 3y ago

Mostly yes. There is a lot of research on taking arbitrary programs and distilling constraints and invariants out of them or doing various forms of function simplification.

boothby 3y ago

I've done this. In my experience it ends up stuck in local minima from which there are no obvious correctness-preserving improvements. Add Monte Carlo to escape valleys and this mode of exploration is still too timid to find anything close to optimal. When you find a truly optimal solution, you end up with the least satisfying proof of correctness: "Here's this this inscrutable formula; I verified that it produces the right output for all possible inputs."

retrac 3y ago

A similar problem comes up in digital design. Behaviour is often specified in terms of exhaustive truth tables, perhaps tables that were generated automatically, from a hardware description language. While such a table can be directly translated into a circuit, doing so in a naive fashion is potentially extremely non-optimal. Optimizing it is a hard problem. Everything has been tried, from exhaustive search (suitable only for small numbers of terms), to rule-based fuzzy backtracking searches, to in recent years, deep learning. But at least when I was in school a couple decades ago, the best known algorithm was still a person playing with the terms on graph paper, rearranging them until patterns emerged: https://en.wikipedia.org/wiki/Karnaugh_map https://en.wikipedia.org/wiki/Karnaugh_map As I understand it, there are recent advances in SAT solvers giving practical algorithms for much larger numbers of terms, but I'm much behind the state of the art at this point.