Z3で2つの数独ソルバーを作成しました。1つは81の変数を使用し、もう1つはx座標とy座標をsquare [x] [y]の数値にマップする関数を使用します。代わりに配列を使用することもできると思います。
Z3変数のPython配列を持つこと、Z3配列を持つこと、またはZ3で関数を持つことの違いは何ですか？いつどちらを使うべきですか？
この質問に対する一般的に適用可能な答えはありません。通常、問題をモデル化する方法は複数あり、どれが実際に最適であるかは明確ではありません。原則として、コストのかかる理論間の推論を回避するため、1つの理論内に維持することは理にかなっています。つまり、ビットベクトルまたは（有界）整数に固執しますが、整数をビットベクトルに変換しようとしないでください（たとえば、このint2bv用語は基本的にZ3によって解釈されないものとして扱われます）。また、Z3で実装されたものよりも、配列の問題を解決するためのより良い解決策があることが知られているので、それらが本当に必要でない場合は、それらを排除するのに役立ちます。
この記事はインターネットから収集されたものであり、転載の際にはソースを示してください。
侵害の場合は、連絡してください[email protected]
コメントを追加