Tiling with bars and satisfaction of Boolean formulas (Q1922876): Difference between revisions

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.