Tossing Coins with an NP-Machine

In computational complexity, 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. In recent work, we reformulated a critical part of Ψ_rest as a compact Horn formula. In other work, we evaluated the cost of this reformulation, though our estimates were intentionally conservative. In this article, we provide a more rigorous analysis and derive a tighter upper bound on two enhanced variants of our original Filling Holes with Backtracking algorithm: the refined (rFHB) and the streamlined (sFHB) versions, each tasked with solving 3-SAT.