Beyond Complete Compilation: Task-semantic Images and the Complexity of Computing only What a Query can see
Abstract
Knowledge compilation transforms Boolean theories into reusable representations that support many downstream queries, but this generality can preserve distinctions a particular task will never observe. We introduce Task-Semantic Images (TSIs), the exact images of model sets under task-specified semantic maps, and develop a complexity theory for computing only the distinctions visible to a downstream computation. We prove an exact replacement theorem, an exponential separation between complete DNNF representation and compact task-semantic images, a proper-affine semantic-collapse theorem with polynomially closed composition, and a natural cardinality-image theorem for bipartite graph CNFs. We then prove the complementary Semantic-Resolution Barrier: polynomially many semantic states do not imply efficient realizability, because constrained minimum vertex cover remains NP-complete on bipartite graphs. This identifies three independent costs—image size, state realizability, and composition—that must all remain controlled for task-relative exact reasoning to be tractable. Reproducible experiments exhaustively verify finite affine and cardinality identities, compare exact finite OBDD state growth with TSI growth, and measure barrier-state behavior across generated instances. The Apache-2.0 software provides tests, a command-line interface, automated reproduction, and an interactive laboratory. The results establish a principled middle ground between complete reusable compilation and one-shot decision without implying a general polynomial-time breakthrough for SAT reasoning.
Fields of Study & Subjects
Graph Theory and Algorithms
Advanced Graph Neural Networks
Semantic Web and Ontologies
Publication details
- Journal / source
- SSRN Electronic Journal
- Publisher
- Elsevier BV
- Publication date
- 1 January 2026
- Language
- EN
- Document type
- Preprint