Algorithm to decide the universality / functional completeness of a set of logic gates?

Given a set of logic gates $G$, let $F_G$ denote the set of all formulas composed of gates from $G$. We say that $G$ is "universal for computation" or "functionally complete" if it forms a basis for all boolean functions, i.e., $$\forall n > 0, \forall f: \{ 0, 1 \}^n \rightarrow \{ 0, 1 \}, f \in F_G.$$ For example the following sets are universal: $$G = \{ \text{NAND} \},$$ $$G = \{ \text{OR}, \text{NOT} \}.$$

Is there an algorithm to decide whether a given set of boolean logic gates is universal? This algorithm must (in principle) yield the correct answer even if given a set of "large" gates, for example containing the boolean function on 100 bits that computes the AND of all bits.

I have been trying to automatically check the universality of several large gate sets. Even an inefficient algorithm would be enlightening.

The closest piece of literature I found is this paper, which seems to suggest that there is a brute-force way to check for some properties that are necessary for universality due to a theorem of Post's.

• I am puzzled--how does the paper you linked not immediately answer your question? – Eric Wofsey Aug 19 '18 at 19:59

Indeed, the paper you link describes two different simple algorithms. First, by Post's theorem, $G$ is functionally complete iff it satisfies the following conditions (here $n$ will always denote the arity of the chosen element $g\in G$):
• Some element $g\in G$ is not monotonic, meaning that there exists $x\in \{0,1\}^n$ and $y\in\{0,1\}^n$ obtained by changing a coordinate of $x$ from $0$ to $1$ such that $g(x)=1$ and $g(y)=0$.
• Some element $g\in G$ is not affine, meaning that there exist $x,y,z,w\in\{0,1\}^n$ such that $x+y=z+w$ but $g(x)+g(y)\neq g(z)+g(w)$ (where the addition is mod $2$).
• Some element $g\in G$ is not self-dual, meaning that there exists $x\in\{0,1\}^n$ such that $g(x')\neq g(x)'$ where $'$ denotes negation (swap $0$ and $1$).
• Some element $g\in G$ satisfies $g(1_n)=0$ (where $1_n$ denotes the $n$-tuple of all $1$s).
• Some element $g\in G$ satisfies $g(0_n)=1$ (where $0_n$ denotes the $n$-tuple of all $0$s).
Each of these conditions can just be checked by brute force for each element of $G$. Presumably if you want to actually apply this when $G$ has elements of large arity, though, you would want to try to find a more efficient way to test the first three conditions than brute force.
Alternatively, by the Corollary in the paper, $G$ is functionally complete iff NAND can be formed using at most $20$ gates of $G$. You can again just brute force through all possible combinations of $20$ or fewer gates and see if any of them compute NAND. This would presumably be much less efficient than using Post's theorem, though.