在本文中，我们探讨了旨在提高访问以合取范式（CNF）表示的命题公式模型的效率的预处理技术。我们专注于三项基本任务：均匀采样、直接模型访问和模型枚举。分析表明，许多最先进的预处理器在不保持公式等价性的情况下，通常不适合这些任务。相反，我们展示了保持模型计数的预处理器可以有效利用，只要保持相关的预处理信息。为了验证我们的方法，我们在多个领域的多样化基准上进行了广泛的实验。实验结果显示，我们的预处理方法在将 CNF 公式编译为 d-DNNF 表示时，能够显著提高模型访问查询的性能，且表现出高效性和鲁棒性。
博主点评： 本文提供了一种有效的预处理策略，为命题逻辑模型的高效查询奠定了基础，特别是在处理复杂的 CNF 表示时。通过保持模型计数，研究者们展示了如何在性能和准确性之间找到平衡，这对后续的研究和应用具有重要的启发意义。