Tableau with Holes: Clarifying NP-Completeness
Edgar Graham Daylight · Symmetry · 2025
In the context of defining NP-completeness, a tableau represents a hypothetical accepting computation path p of a nondeterministic polynomial time Turing machine N on an input w. The tableau is encoded by the propositional logic formula ψ, defined as ψ=ψcell∧ψrest. The component ψcell enforces the constraint that each cell in the tableau contains exactly one symbol, while ψrest incorporates constraints governing the step-by-step behavior of N on w. Intuitively, ψrest appears to pose a much greater challenge for satisfiability. This raises the question of whether the distinction between ψcell being a 3cnf formula, rather than a cheap 2cnf formula, actually matters. We show that if, hypothetically, ψrest can be succinctly represented as a Horn formula, then satisfying ψ can be achieved efficiently in Kf(n,k) steps, where N operates within O(nk) steps and both k and K are constants. Asymptotically, f(n,k)≈n23k. Our method has the potential for iterative application. Technically, we trim ψcell down to a 2cnf–Horn formula, whose satisfiability allows for empty cells, or “holes”, in the tableau. This modified tableau represents exponentially many paths of N on w, rather than a single accepting path p. While a tableau with holes conceptualizes the satisfiability of ψtrim—a trimmed-down version of ψ—it does not directly address the satisfiability of ψ. Therefore, we introduce an external user who efficiently employs backtracking to fill in specific holes, ultimately verifying the satisfiability of the original ψ.