The problem of determining whether a graph G can be realized as a unit-distance graph in $\mathbb{R}^2$ with integer-valued coordinates is NP-complete. We implement Eades and Whitesides' logic engine in this setting, and construct a graph that is realizable if and only if an arbitrary NA3SAT formula is satisfiable.

翻译：暂无翻译