Entailment vs. Verification for Partial-assignment Satisfiability and Enumeration

要約

SAT関連の問題の多くの手順、特に満足のいく真実の割り当ての完全な列挙を必要とする人々の手順は、入力式を満たす（おそらく小さい）部分割り当ての検出に効率と有効性を依存しています。
驚くべきことに、文献の部分的な割り当てによる式満足度のユニークな普遍的な定義はないようです。
この論文では、部分的な割り当てによって満足の問題を深く分析し、この概念の曖昧さと微妙さについて旗を掲げ、それらの実際的な結果を調査します。
文献で暗黙的に使用される2つの代替概念、すなわち検証と含意を特定します。これは、CNF式に適用された場合に一致しますが、非CNFまたは実存的に定量化された式に適用される場合は異なり、補完的な特性を提示します。
前者は確認が容易であり、そのため、現在のほとんどの検索手順で暗黙的に使用されているが、後者はより良い理論的特性を持ち、列挙手順の効率と有効性を改善できることを示しています。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google