Tiling with bars and satisfaction of Boolean formulas (Q1922876)

The paper considers plane figures made up from finitely many squares of the plane tessellation by unit squares. It is proved that the problem of tiling such a figure with horizontal or vertical bars of length 2 or 3 can be reduced in linear time (in the area of the figure) to the logic problem 3-SAT (3-satisfiability). In particular, this gives a linear algorithm which, given a figure \(F\), either exhibits a tiling of \(F\) or indicates that such a tiling cannot exist.