Comment by retrac

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

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.