z3pyのいくつかのインプライズ条件でブール式を証明する

Question

私はZ3pyの使い方が新しく、私の割り当ては両方のソリューション（satとunsat）のカウンタの例を生成することです。
unsatソリューションの反例を生成する関数はありますか？

Answer 1

unsatは、与えられたアサーションを満たすモデルがないことを意味します。問題がsatの場合にのみモデルを抽出できます。だから、あなたの疑問に答えるために、unsatソリューションからモデルを作成することはできません。ただ存在しません。

典型的な方法は、証明しようとしている式のnegationをアサートすることです。その数式が充足可能ならば、元の数式は改ざん可能です。すなわち、そのための反例がある。おそらくあなたがしようとしているのでしょうか？つまり：式の否定が満足できるモデルを持つ場合、そのモデルは元の式の反例になります。これは、SMTソルバの上に構築されたほとんどの証明者が、証明しようとしているものの否定を返信することによって実現されます。unsat.証明者がモデルを返すと、反例になります。