Z3py：轉換一個Z3公式由picosat使用條款

Question

LINKS：
Z3 theorem prover
picosat with pyhton bindings

我使用Z3作爲SAT解算器。對於較大的公式，似乎存在性能問題，這就是爲什麼我想檢查一下picosat是否是更快的選擇。 我的現有Python代碼生成Z3語法命題公式：

from z3 import * 

import pycosat 
from pycosat import solve, itersolve 

# 
#1 2 3 4 5 6 7 8 (variable names in picosat are numbers!) 
# 
C, G, M, P, R, S, SN, B = Bools('C G M P R S SN B') 
C = (And(*(S,Or(Not(S),P),Or(Not(P),S),Or(Not(P),B),Or(Not(C),P),Or(Not(G),P),Or(Not(M),P),Or(Not(R),P),Or(Not(SN),P),Or(Not(B),P),True,Not(False),Or(R,SN,B,G,M,C,True)))) 

# formula in Z3: 
f = simplify(C) 

print f 

OUTPUT/RESULT

And(S, 
    Or(Not(S), P), 
    Or(Not(P), S), 
    Or(Not(P), B), 

    Or(Not(C), P), 
    Or(Not(G), P), 
    Or(Not(M), P), 
    Or(Not(R), P), 
    Or(Not(SN), P), 
    Or(Not(B), P)) 

然而Picosat使用如在下面的例子中示出的列表/數字的陣列，（「clauses1 「：6表示變量P，-6表示」不是P「等）：

import pycosat 
from pycosat import solve, itersolve 
# 
# use pico sat 
# 
nvars = 8 
clauses =[ 
    [6], 
    [-6, 4], ## "Or(Not(S), P)" from OUPUT above 
    [-4, 6], 
    [-4, 8], 
    [-1, 4], 
    [-2, 4], 
    [-3, 4], 
    [-5, 4], 
    [-7, 4], 
    [-8, 4]] 

# 
# efficiently find all models of the formula 
# 
sols = list(itersolve(clauses, vars=nvars)) 
print "result:" 
print sols 
print "\n\n====\n" 

作爲簡體中文le解決方案將表示CNF中的公式的Z3變量（如代碼示例中的變量「f」）轉換爲picosat用於表示CNF中公式的前述格式？我真的試圖使用Z3的python API，但是這些文檔不足以自己解決問題。

（請注意上面的例子僅說明了概念。通過變量C表示的公式將被動態地生成的並且將是太複雜，無法通過Z3直接有效地處理）

Answer 1

首先，我們應該轉換Z3式進入CNF。以下崗位針對這個問題

• Z3 and DIMACS output

要轉換的Z3 CNF公式爲DIMACS，我們可以只寫穿越它的功能和產生的整數列表的列表。下面的兩個職位描述如何遍歷Z3公式

• Substituting function symbols in z3 formulas
• Is there a way of querying or accessing the structure of a Z3 expression via the API

最後，如果你需要從表達式值的地圖，你可以用下面的辦法

• Hashing expressions in Z3Python