gpt4 book ai didi

python - Z3py:将 Z3 公式转换为 picosat 使用的子句

转载 作者:太空狗 更新时间:2023-10-30 01:15:41 25 4
gpt4 key购买 nike

链接:
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

输出/结果

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 高效处理)

最佳答案

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

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

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

关于python - Z3py:将 Z3 公式转换为 picosat 使用的子句,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/19551225/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com