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 & \text{A} \\ \text{A}^t & 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.