Let $\phi$ be CNF formula with $n$ variables and $m$ clauses.I am looking for a reduction is $\phi$ satisfiable to a problemon a planar graph $G$ with as few vertices as possible.The majority of reductions I have seen use crossing gadget,which replaces edge crossing by a planar graph.So far the best reference is $|V(G)|=m^2$.The motivation is that the treewidth of planar graphsis at most $4.9 \sqrt{|V(G)|}$ and this gives subexponentialcomplexity for problems exponential in the treewidth likeIndependent Set.
Reduction SAT to a problem on a planar graph with as few vertices as possible
graph theory;sat;reductions