SATISFIABILITY OF CO-NESTED FORMULAS

As a notion dual to Knuth's nested formulas [4], we call a boolean for mula PHI = AND(i = 1)n c(i) in conjunctive normal form co-nested if it s clauses can be linearly ordered (say C = {c(i); i = 1, 2, ..., n}) s o that the graph G(PHI)cl = (X or C, {xc(i); x is-an-element-of c(i) o r inverted left perpendicular x is-an-element-of c(i)} or {c(i) c(i 1); i = 1, 2, ..., n}) allows a noncrossing drawing in the plane so th at the circle c1, c2, ..., c(n) bounds the outerface. Our main result is that maximum satisfiability of co-nested formulas can be decided in linear time.