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.

翻译：判定图G是否能在$\mathbb{R}^2$中以整数值坐标实现为单位距离图的问题是NP完全的。我们在该场景下实现了Eades和Whitesides的逻辑引擎，并构造了一个图，其可实现的充要条件是任意NA3SAT公式可满足。