The Quine-McCluskey algorithm merges disjunctors in a disjunction like $$ \lnot x_0 \land \lnot x_1 \land \lnot x_2 \land \lnot x_3 \lor\\ x_0 \land \lnot x_1 \land x_2 \land \lnot x_3 \lor\\ \lnot x_0 \land x_1 \land x_2 \land \lnot x_3 \lor\\ \lnot x_0 \land \lnot x_1 \land \lnot x_2 \land x_3 \lor\\ \lnot x_0 \land x_1 \land \lnot x_2 \land x_3 \lor\\ x_0 \land x_1 \land \lnot x_2 \land x_3 \lor\\ \lnot x_0 \land x_1 \land x_2 \land x_3 \lor\\ x_0 \land x_1 \land x_2 \land x_3 $$ into fewer disjunctors in an equivalent disjunction: $$ x_1 \land x_3 \lor\\ \lnot x_0 \land \lnot x_1 \land \lnot x_2 \lor\\ \lnot x_0 \land x_1 \land x_2 \lor\\ x_0 \land \lnot x_1 \land \lnot x_2 \land x_3 $$ by merging like this: $$x_0\land x_1\lor\lnot x_0\land x_1 \iff (x_0\lor\lnot x_0)\land x_1\iff x_1$$.
https://www.mathematik.uni-marburg.de/~thormae/lectures/ti1/code/qmc/ will generate test cases to taste.
Your task
Your task is to write a function transforming any disjunction into an equivalent disjunction of minimal disjunctor count.
The QMC algorithm imperative in the headline is a sloppy summary and a mere recommendation, no hard requirement.
You can encode the data any way fit, that is $$\lnot x_1 \land \lnot x_2 \land x_3$$ can become
- [3,0,0,1]
- [(1,0),(2,0),(3,1)]
- (14,8)
- …
This is code-golf. Shortest code wins.
