AI 中文总结
针对知识编译中离线编译成瓶颈的问题，提出dkc分布式知识编译器，利用Cube-and-Conquer策略划分搜索空间，还引入dreasoner分布式推理引擎，实验证明该分布式架构能有效扩展，可编译和查询复杂公式。
AI 中文摘要
知识编译（KC）是一种强大的范式，通过将命题公式转换为易于处理的目标语言（如确定性、可分解否定范式（d-DNNF））来实现高效推理。然而，随着实际问题实例复杂度增加，离线编译阶段成为显著计算瓶颈。分布式计算虽成功应用于模型计数，但扩展到知识编译有挑战。本文提出dkc，首个用于大规模决策-DNNF生成的分布式知识编译器，利用Cube-and-Conquer策略有效划分搜索空间。还引入dreasoner分布式推理引擎，能跨分布式d-DNNF结构执行核心推理任务。实验表明分布式架构有效扩展，能编译和查询复杂公式。
英文摘要
Knowledge Compilation (KC) is a powerful paradigm that enables efficient reasoning by transforming propositional formulas into tractable target languages, such as Deterministic, Decomposable Negation Normal Form (d-DNNF). However, as real-world problem instances grow in complexity, the offline compilation phase becomes a significant computational bottleneck, often exceeding the memory and temporal limits of single-node systems. While distributed computing has been successfully applied to model counting ($\#\mathsf{SAT}$), extending these techniques to knowledge compilation remains a challenge due to the difficulty of sharing partial circuit fragments across distributed nodes. In this paper, we propose dkc, the first distributed knowledge compiler designed for large-scale Decision-DNNF generation. Leveraging a Cube-and-Conquer strategy, dkc effectively partitions the search space into independent subproblems, mitigating the communication overhead typically associated with work-stealing architectures in circuit-based tasks. Recognizing that the utility of compilation lies in subsequent querying, we further introduce dreasoner, a distributed reasoning engine. dreasoner is capable of performing core inference tasks (including model counting, direct access, and uniform sampling) across a distributed d-DNNF structure, even under variable conditioning. Our experimental evaluation on benchmarks demonstrates that our distributed architecture scales effectively, enabling the compilation and querying of complex formulas that remain beyond the reach of state-of-the-art sequential compilers.
