Nested satisfiability
Donald E. Knuth · arXiv (Cornell University) · 1990
A special case of the satisfiability problem, in which the clauses have a hierarchical structure, is shown to be solvable in linear time, assuming that the clauses have been represented in a convenient way.