Python 3でZ3-solver 'model is not available'例外が発生する

Question

SAT問題を解決するためにMicrosoftとPython 3のZ3-solverを使用することにしました。目的は長いモデル（最大50万のフィーチャーすべての可能な解決策を見つける。それらを見つけるために、私は最初の方程式に最初の方程式S1を加え、S1を除外したいと思います。 whileループを使ってやります。 フィーチャーモデルを分析したいので、SAT問題を解決することが重要です。

しかし、最初の方程式にsthを追加することに問題があります。 # Successfull...はz3types.Z3Exception: model is not availableエラーをスローした後、第1の符号化ライン

# Import statements 
import sys 
sys.path.insert(0,'/.../z3/bin') 
from z3 import *  # https://github.com/Z3Prover/z3/wiki 

def main(): 

    ''' 
    Solves after transformation a given boolean equation by using the Z3-Solver from Microsoft. 
    ''' 

    fd = dict() 
    fd['_r'] = Bool('_r') 
    fd['_r_1'] = Bool('_r_1') 

    equation = '''And(fd.get("_r"),Or(Not(fd.get("_r")),fd.get("_r_1")))''' 

    # Solve the equation 
    s = Solver() 
    exec('s.add(' + equation + ')') 
    s.check() 
    print(s.model()) 

    ################################### 
    # Successfull until here. 
    ################################### 

    s.add(Or(fd['_r'] != bool(s.model()[fd.get('_r')]))) 
    # s.add(Or(fd['_r'] != False)) 

    s.check() 
    print(s.model()) 


if __name__=='__main__': 
    main() 

：私は、最小限の例を共有します。だから私は単純にモデルにfalseを追加する上記の行を試してみました。それはうまく動作します。

ここに貼り付けられています。私はエラーを解決するのは簡単だと信じていますが、私は解決策を見ません。あなたは誰ですか？ありがとう！

Answer 1

モデルは、s.check（）が 'sat'を返した後にのみ使用可能になります。 ブール命題を{True、False}にマップし、 は一般に定数と関数を固定値にマップします。 モデルは、ソルバの式に追加された式を満たす解釈 を提供するという要件です。 私たちは 's.check（）'を呼び出す前にソルバーの状態が充足可能かどうかわかりません。

あなたが言いたいとします

制約を満たすモデルに FD [「_ R」]、その後、「_r」のモデルで真である場合という性質を持っていなければならないことを意味し

s.add(Or(fd['_r'] != bool(s.model()[fd.get('_r')]))) 

！= Trueで、モデルの '_r'がfalseの場合、 fd ['_ r']！= Falseです。これは、 fd ['_ r']！= '_r'と同じです。だから、その評価について何か と言うには、どのモデルでも '_r'を評価できるものであれば、 '_r'の値 に実際にアクセスする必要はありません。