Z3解算器拋出'模型不可用'python 3上的異常3

爲了解決SAT問題，我決定使用Microsoft和Python 3的Z3解算器。目標是獲取長模型（多達500,000個特徵）並找到所有可能的解決方案。要找到它們，我想將第一個解S1添加到初始方程中，並排除S1等等。我會用while循環來做。解決SAT問題對我來說很重要，因爲我想分析特徵模型。Z3解算器拋出'模型不可用'python 3上的異常3

但是我面臨着在初始方程中增加某些問題。我將分享一個最小的例子：

# 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()

第一編碼的線# Successfull...後拋出z3types.Z3Exception: model is not available錯誤。所以我嘗試了上面的一行，簡單地將false添加到模型中。這工作得很好。

我被困在這裏。我相信這個錯誤很容易解決，但我看不到解決方案。你們中的一個？謝謝！

來源

2016-09-14 So S

只有在s.check（）返回'sat'後，模型纔可用。該模型將布爾命題映射爲{True，False}並且通常將常量和函數映射爲固定值。要求是該模型提供的解釋滿足添加到求解器'的公式。我們不知道在我們稱之爲's.check（）'的之前求解器狀態是否可滿足。

假設你想說：

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

這意味着在滿足約束應該有屬性的模型，如果「_r」模式下爲真，那麼 FD [「_ R」] ！=真，如果模型下'_r'爲假，則 fd ['_ r']！= False。這相當於說 fd ['_ r']！='_r'。因此，在任何可能評估'_r'的模型中，訪問'_r'的值並不是真的必要，以便說出關於它的評估。

來源

2016-09-15 02:04:50

感謝您的回答。作爲一個例子，你已經清楚了我對這個問題的描述。感謝您解釋我的示例無法解決的原因。 –

Z3解算器拋出'模型不可用'python 3上的異常3

回答

相關問題