Detecting circuit that's similar in functionality and implementation Let $x=(x_1,\dots,x_n)$ be a vector of boolean variables.  Let $C,D$ be two boolean circuits on $x$.  Say that $C$ is similar to $D$ if:


$\Pr[C(x) \ne D(x)]$ is exponentially small, when $x$ is drawn uniformly at random from $\{0,1\}^n$ (in other words, they have almost-identical functionality); and,
$C,D$ differ in graph edit distance by a tiny amount (their edit distance is much smaller than the size of the circuit, say, $O(1)$ or some small constant), meaning that almost all of the gates and wires of $C$ match a corresponding gate and wire in $D$, with only a few gates added/deleted/changed.




My problem: I am given a circuit $C$, and I want to know whether there exists a circuit $D$ that is similar to $C$ but not identical to $C$ (i.e., where there exists $x$ such that $C(x)\ne D(x)$).

Can anyone suggest an algorithm to solve this problem?

If it helps, we can restrict attention to circuits $D$ that are smaller than the given circuit $C$ (i.e., we want to know whether there exists a circuit $D$ such that $D$ is smaller than $C$, $D$ is similar to $C$, and there exists $x$ such that $C(x)\ne D(x)$).

If it helps, you can additionally assume we are given known-good test cases $x^1,\dots,x^m,y^1,\dots,y^m$ such that $C(x^i)=y^i$ for all $i$, and we can further restrict attention to only circuits $D$ such that $D(x^i)=y^i$ for all $i$.



This arises from a practical application, so if you can't solve this problem, feel free to solve any variant or interesting special case.  For instance, feel free to instantiate any of the parameters or thresholds in any way that's convenient for you.  You can assume the circuits are not too large (polynomial sized, or something).  Feel free to replace graph edit distance by some other measure of near-match of implementation.  Also, in practice SAT solvers are often surprisingly effective on the structured circuits that arise in practice, so it's probably fine to invoke a SAT solver as a subroutine/oracle (at least, if you're invoking it on something like a SAT instance derived from a circuit like $C$).

Alternatively, lacking any algorithms, I would also be interested in the existence question: for an "average" circuit $C$, what's the probability that there exists some $D$ that meets all the criteria?  (I'm hoping this probability is very low, but I have no clue if that is the case.)



The practical application is to test whether a circuit $C$ might contain a malicious backdoor / hidden Easter egg.  The hypothesis of how such a thing might get inserted goes like this.  We start with a "golden" circuit $D$, that computes the desired functionality and has no hidden backdoor.  Then, the adversary makes a small change to $D$ to introduce the hidden backdoor, obtaining a modified circuit $C$.  The purpose of the backdoor is to change the function computed by $D$ in some way.  If $\Pr[C(x) \ne D(x)]$ is not too small, the change can plausibly be detected by random testing, so an adversary will probably try to keep $\Pr[C(x) \ne D(x)]$ very small.  Similarly, if $C$ differs from $D$ in too many places, this might be noticed by random inspection of the circuit, so an adversary will probably try to minimize the number of changes.  (And, there may be a test suite of $x^i,y^i$ pairs that represent instances of the desired functionality, so we know that whatever the "golden" circuit $D$ is, it satisfies $D(x^i)=y^i$ for all $i$.)  Ultimately, we are given the circuit $C$ (but not the "golden" circuit $D$), and we want to know whether $C$ might be a modified version of some $D$, where the modification was made to introduce a hidden backdoor of this sort.
This is only an extended comment that came to my mind immediately after reading the question:


suppose you have a 3SAT formula $\phi$ with $n$ variables $x_1,...,x_n$ and let $C$ be the corresponding circuit;
build a new circuit $C'$, adding $m = n^k$ variables $y_1, y_2, ...,y_{n^k}$, and enough gates to AND the $m$ new variables with the output of the original $C$ ($C' = \phi \land y_1 \land ... \land y_m$);
build a new circuit $D'$ from $C'$ that simply forces its output to 0 using an AND and NOT gate ($D' = C' \land \neg C'$)


If $\phi$ is not satisfiable then $D'$ and $C'$ are equivalent, otherwise they differ when the $x_i$ satisfy the formula AND all $y_i = 1$, but you can choose $m$ large enough to make the probability that $\bigwedge y_i =  1$ very small.

So if you have an efficient algorithm for your problem, you can afficiently solve the 3SAT instance.