链接：
Z3 定理证明者
picosat 与 pyhton 绑定
我使用 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
输出/结果
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"
您推荐什么作为将表示 CNF 中的公式的 Z3 变量（如代码示例中的变量“f”）转换为上述格式 picosat 用于表示 CNF 中的公式的简单解决方案？我真的尝试使用Z3的python API，但是文档不足以自己解决问题。
（请注意，上面的例子只是说明概念。变量C表示的公式将是动态生成的，并且过于复杂，无法直接被z3高效处理）