A question to the #P-complete proof of the permanent from Ben-Dor/Halevi In the paper of Ben-Dor/Halevi [1] it is given another proof that the permanent is
$\#P$-complete. In the later part of the paper, they show the reduction chain
\begin{equation}
\text{IntPerm} \propto \text{NoNegPerm} \propto \text{2PowersPerm} \propto \text{0/1-Perm}
\end{equation}
while the permanent value is preserved along the chain. Since the number of satiesfying assignments of a 3SAT formula $\Phi$ can be obtained from the permanent value, it is sufficient to compute the permanent of the final $0/1$-matrix. So far so good. 

However, it is well known that the permanent of a $0/1$-matrix $\text{A}$ is equal to the number of perfect matchings in the bipartite double cover $G$, i.e., the graph from the matrix $\begin{pmatrix} 0 &amp; \text{A} \\ 
\text{A}^t &amp; 0 \end{pmatrix}$. And this number can be computed efficiently if $G$ turns out to be planar (using Kastelyens algorithm). 

So in total this means, someone could compute the number of satiesfying assignments of a boolean formula $\Phi$ if the final graph $G$ is planar. 

Since the embedding of $G$ depends heavily on the formula $\Phi$, the hope is, that there exists certain formulas that lead more often into planar bipartite covers.
Does anyone know if it has ever been investigated how large the chances are that $G$ will be planar?

Since counting satiesfying solutions is $\#P$-complete, the graphs will be for sure almost always non-planar, but i can not find any hints regarding this topic.

[1] Amir Ben-Dor and Shai Halevi. Zero-one permanent is #p-complete, a simpler proof. In 2nd Israel Symposium on Theory of Computing Systems, pages 108-117, 1993. Natanya, Israel.
This topic has been extensively investigated in recent years under the name of Holographic Algorithms by researchers such as Valiant, Cai, Lu, Xia, Lipton, and others. Essentially all tractable cases of #CSP (counting constraint satisfaction problems) have been identified in terms of dichotomy theorems (FP vs. #P-complete). In particular, Matchgate computations have been identified as the specific class of counting problems that become tractable on planar graphs. See e.g. this link for further references.