Nested satisfiability (Q582905)

A special case of the satisfiability problem is shown to be solvable in linear time. This special case is essentially ''one-sided planar satisfiability'': It is means that the bipartite graph whose vertices are variables and clauses, and whose edges run from variables to the clauses containing the variables, can be represented in the plane without crossing edges, with all variables appearing in a straight line, and with all clauses on one side of that line. The linear-time algorithm assumes that such a representation has been given, and decides whether or not the clauses are satisfiable by dynamically replacing clauses by simpler clauses containing only two literals. (The running time needed to decide whether or not a given set of clauses has such a nested structure is not considered.)