区分验证与蕴含，提升满足赋值枚举的效率与准确性
Entailment vs. Verification for Partial-assignment Satisfiability and Enumeration
- 提出验证与蕴含两种部分赋值满足判定方式
- 蕴含在非CNF公式中理论性能更优，可加速枚举
- 适合从事SAT求解与形式化验证的研究者参考
许多SAT相关问题的求解方法，尤其是需要完全枚举满足赋值的情况，依赖于对小规模部分赋值是否满足输入公式的检测。然而，文献中尚未就部分赋值如何满足公式达成统一定义。本文深入分析了这一概念的模糊性与细微差别，揭示其实际影响。识别出文献中隐含使用的两种不同概念：验证（verification）与蕴含（entailment）。二者在CNF公式下等价，但在非CNF或存在量词公式中则不同，且具有互补性质。尽管当前多数搜索过程因验证更易检查而默认使用，但蕴含具备更优的理论特性，能显著提升枚举过程的效率与有效性。
原文摘要 · Abstract (English)
Many procedures for SAT-related problems, in particular for those requiring the complete enumeration of satisfying truth assignments, rely their efficiency and effectiveness on the detection of (possibly small) partial assignments satisfying an input formula. Surprisingly, there seems to be no unique universally-agreed definition of formula satisfaction by a partial assignment in the literature. In this paper we analyze in deep the issue of satisfaction by partial assignments, raising a flag about some ambiguities and subtleties of this concept, and investigating their practical consequences. We identify two alternative notions that are implicitly used in the literature, namely verification and entailment, which coincide if applied to CNF formulas but differ and present complementary properties if applied to non-CNF or to existentially-quantified formulas. We show that, although the former is easier to check and as such is implicitly used by most current search procedures, the latter has better theoretical properties, and can improve the efficiency and effectiveness of enumeration procedures.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。