发表机构
CRIL, U. Artois & CNRS（里尔计算机科学实验室，法国北部加来海峡大区大学与法国国家科学研究中心）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
研究如何通过预处理提高d-DNNF表示的查询效率，聚焦三项基本任务，指出多数现有预处理器不适用于此，而保持模型计数的预处理器可有效利用，经实验验证其预处理方法高效且能显著提升模型访问查询性能。
AI 中文摘要
本文研究旨在提高合取范式（CNF）表示的命题公式模型访问效率的预处理技术。聚焦均匀采样、直接模型访问和模型枚举三项基本任务。分析表明，多数不保持公式等价性的现有预处理器不适用于这些任务。相反，保持模型计数的预处理器可有效利用，前提是维护相关预处理信息。通过对多领域多样基准测试进行大量实验验证，结果表明预处理方法高效且稳健，将CNF公式编译为d-DNNF表示时，能显著提升模型访问查询性能。
英文摘要
In this paper, we investigate preprocessing techniques aimed at improving the efficiency of accessing models of propositional formulas represented in conjunctive normal form (CNF). We focus on three fundamental tasks: uniform sampling, direct model access, and model enumeration. Our analysis reveals that most state-of-the-art preprocessors, when they do not preserve formula equivalence, are generally unsuitable for these tasks. In contrast, we demonstrate that preprocessors which preserve model counts can be effectively leveraged, provided relevant preprocessing information is maintained. To validate our approach, we perform extensive experiments on a diverse suite of benchmarks from multiple domains. The experimental results show that our preprocessing methods are both efficient and robust, yielding significant performance improvements for model access queries when CNF formulas are compiled into d-DNNF representations.
DOI：10.1007/978-3-032-04590-4_9
