Thanks to Igor Pak for pointing out to us that NP-hardness of the
POSITIVE PLANAR 1-IN-3-SAT problem (Proposition 3.3) has apparently
been shown already by
P. Laroche,
Planar 1-in-3 satisfiability is NP-complete,
ASMICS Workshop on Tilings, Deuxiemes journees polyominos et pavages,
Ecole Normale Superieure de Lyon, 1992,
according to a reference in
C. Moore and J. M. Robson,
Hard tiling problems with simple tiles,
Discrete & Computational Geometry 26 (2001), pp. 573-590.