{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T14:03:33Z","timestamp":1760623413708,"version":"build-2065373602"},"reference-count":11,"publisher":"MDPI AG","issue":"5","license":[{"start":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T00:00:00Z","timestamp":1745884800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Symmetry"],"abstract":"<jats:p>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 \u03c8, defined as \u03c8=\u03c8cell\u2227\u03c8rest. The component \u03c8cell enforces the constraint that each cell in the tableau contains exactly one symbol, while \u03c8rest incorporates constraints governing the step-by-step behavior of N on w. Intuitively, \u03c8rest appears to pose a much greater challenge for satisfiability. This raises the question of whether the distinction between \u03c8cell being a 3cnf formula, rather than a cheap 2cnf formula, actually matters. We show that if, hypothetically, \u03c8rest can be succinctly represented as a Horn formula, then satisfying \u03c8 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)\u2248n23k. Our method has the potential for iterative application. Technically, we trim \u03c8cell down to a 2cnf\u2013Horn formula, whose satisfiability allows for empty cells, or \u201choles\u201d, 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 \u03c8trim\u2014a trimmed-down version of \u03c8\u2014it does not directly address the satisfiability of \u03c8. Therefore, we introduce an external user who efficiently employs backtracking to fill in specific holes, ultimately verifying the satisfiability of the original \u03c8.<\/jats:p>","DOI":"10.3390\/sym17050677","type":"journal-article","created":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T11:35:13Z","timestamp":1746185713000},"page":"677","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Tableau with Holes: Clarifying NP-Completeness"],"prefix":"10.3390","volume":"17","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9815-3966","authenticated-orcid":false,"given":"Edgar Graham","family":"Daylight","sequence":"first","affiliation":[{"name":"a.k.a. Karel Van Oudheusden, Department of Computer Science, KU Leuven, Celestijnenlaan 200a, Box 2402, 3001 Leuven, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1968","published-online":{"date-parts":[[2025,4,29]]},"reference":[{"key":"ref_1","unstructured":"Sipser, M. (2006). Introduction to the Theory of Computation, Thomson Course Technology."},{"key":"ref_2","unstructured":"Papadimitriou, C. (1994). Computational Complexity, Addison Wesley Longman."},{"key":"ref_3","unstructured":"Hopcroft, J., Motwani, R., and Ullman, J. (2007). Introduction to Automata Theory, Languages, and Computation, Addison Wesley\/Pearson Education."},{"key":"ref_4","doi-asserted-by":"crossref","unstructured":"Aaronson, S. (2013). Quantum Computing since Democritus, Cambridge University Press.","DOI":"10.1017\/CBO9780511979309"},{"key":"ref_5","unstructured":"Cook, S. (1971, January 3\u20135). The Complexity of Theorem-Proving Procedures. Proceedings of the 3rd Annual ACM Symposium on Theory of Computing. Association for Computing Machinery, Shaker Heights, OH, USA."},{"key":"ref_6","unstructured":"Dean, W. (2016). Computational Complexity Theory. The Stanford Encyclopedia of Philosophy, The Metaphysics Research Lab."},{"key":"ref_7","unstructured":"Gr\u00e4del, E. (2009). Complexity Theory: WS 2009\/10, Mathematische Grundlagen der Informatik, RWTH Aachen."},{"key":"ref_8","unstructured":"Daylight, E. (2025, April 04). Capturing Nondeterminism with Accepting Observer Systems. To appear, Available online: https:\/\/dijkstrascry.com\/pnp."},{"key":"ref_9","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","article-title":"Linear-Time Algorithms for Testing the Satisfiability of Propositional Horn Formulae","volume":"1","author":"Dowling","year":"1984","journal-title":"J. Log. Program."},{"key":"ref_10","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1305\/ndjfl\/1093883561","article-title":"Acceptable notation","volume":"23","author":"Shapiro","year":"1982","journal-title":"Notre Dame J. Form. Log."},{"key":"ref_11","doi-asserted-by":"crossref","first-page":"1756","DOI":"10.1093\/comjnl\/bxr002","article-title":"Dijkstra\u2019s Rallying Cry for Generalization: The Advent of the Recursive Procedure, late 1950s\u2013early 1960s","volume":"54","author":"Daylight","year":"2011","journal-title":"Comput. J."}],"container-title":["Symmetry"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2073-8994\/17\/5\/677\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:24:11Z","timestamp":1760030651000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2073-8994\/17\/5\/677"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,29]]},"references-count":11,"journal-issue":{"issue":"5","published-online":{"date-parts":[[2025,5]]}},"alternative-id":["sym17050677"],"URL":"https:\/\/doi.org\/10.3390\/sym17050677","relation":{},"ISSN":["2073-8994"],"issn-type":[{"type":"electronic","value":"2073-8994"}],"subject":[],"published":{"date-parts":[[2025,4,29]]}}}