How do you most efficiently combine boolean functions with a large number of variables using AND, OR, and NOT? The most up-to-date work that I can find on this subject is about 20 years old (Efficient data structures for Boolean functions). Which search terms should I be using to explore this question?
I am starting from about 200 simple boolean functions. These are combined with each other using AND, OR, NOT, and XOR to give other boolean functions, which are then also combined using AND, OR, NOT, and XOR. The process repeats about 3000 times, until a final combination gives me a single boolean expression. I'm interested in that final expression.
Representing the functions as DNF or CNF makes certain operations (NOT and XOR) slow. Representing the functions as ROBDDs is an option - are there any drawbacks here? I'm not sure whether SMT solvers are useful here, because I am interested in the final equation rather than whether the equation is satisfiable. What else should I be looking at?