python – Z3py:将Z3公式转换为picosat使用的子句
内容导读
互联网集市收集整理的这篇技术教程文章主要介绍了python – Z3py:将Z3公式转换为picosat使用的子句,小编现在分享给大家,供广大互联网技能从业者学习和参考。文章包含1870字,纯文字阅读大概需要3分钟。
内容图文
![python – Z3py:将Z3公式转换为picosat使用的子句](/upload/InfoBanner/zyjiaocheng/786/9528a8b3637a4e6daa4e22673ca0f7a3.jpg)
链接:
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公式
> 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
内容总结
以上是互联网集市为您收集整理的python – Z3py:将Z3公式转换为picosat使用的子句全部内容,希望文章能够帮你解决python – Z3py:将Z3公式转换为picosat使用的子句所遇到的程序开发问题。 如果觉得互联网集市技术教程内容还不错,欢迎将互联网集市网站推荐给程序员好友。
内容备注
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 gblab@vip.qq.com 举报,一经查实,本站将立刻删除。
内容手机端
扫描二维码推送至手机访问。