Z3py：将Z3公式转换为picosat使用的子句

Question

链接：具有Pyhton绑定的
Z3定理证明者
picosat

我已经使用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使用数字列表/数组，如以下示例所示（“ clauss1”：6表示变量P，-6表示“ not 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有效处理）

Answer 1

首先，我们应该将 Z3 公式转换为 CNF。下面的帖子解决了这个问题

• Z3 和 DIMACS 输出

要将 Z3 CNF 公式转换为 Dimacs，我们只需编写一个函数来遍历它并生成整数列表的列表。下面两篇文章描述了如何遍历Z3公式

• 代入 z3 公式中的函数符号
• 有没有办法通过 API 查询或访问 Z3 表达式的结构

最后，如果你需要从表达式到值的映射，你可以使用下面的方法

• Z3Python 中的散列表达式