On the construction of graphs with a planar bipartite double cover from boolean formulas and its application to counting satisfying solutions

We prove a theorem that describes necessary conditions for the gadgets (i.e., small subgraphs with certain properties) of G to allow a planar bipartite double cover G¨. For arbitrary 3CNF formulas and the known approaches to build G, our theorem shows that gadgets, which enable a planar bipartite double cover, do not exist. However, we show that for certain classes of boolean formulas, e.g., #5Pl-Rtw-2CNF, #7Pl-Rtw-2CNF and #3Forest-3CNF, such gadgets exist, hence these counting problems are in P. The results probably extended to other moduli p and perhaps further counting classes.