z3 - SAT/SMT ソルバーでの変数の削除

Question

SMT/SAT の解法で、数式から無関係な変数を決定する手法はありますか? つまり、任意の値を持つことができ、式の充足可能性に影響を与えないものです。

Answer 1

式が文節の連言であり、それぞれがリテラルの選言である命題充足可能性の場合。例えば(A | B) & (!B | A) & (!A | B | A)

変数が式全体で正のリテラルまたは負のリテラルとしてのみ表示される場合、安全に削除でき、その変数が含まれる句を削除して、満たされたと見なすことができます。ただし、厳密な意味では、そのような変数の値は無関係ではありません。特定の式に対する満足のいく代入でこれらの節を満たすことができる唯一の変数である可能性があるからです。このような変数は純粋と呼ばれ、このフェーズは純粋なリテラル消去と呼ばれます。

純粋なリテラルの削除の前に、否定されていない変数と否定された変数を含む句が削除されるように、数式をクリーンアップする必要があります。これにより、一部の変数が純粋になる可能性があります。さらに、解決手順全体を通して、変数が純粋であると識別された場合は、それを削除する必要があります。

たとえば、節(!A | B | A)は自明に満たされます。A がどのような値を取っても、それは満たされます。

次に(A | B) & (!B | A) & (!A | B | A)->(A | B) & (!B | A)

現在、A は純粋であり、True に設定できるため、満足のいく代入が見つかります。決定を下す必要なく解決策が見つかったことに注意してください。単純に 2 つのルールを適用しました。