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.