automatic_reasoning_abt_sw:“关于软件的自动推理”课程中的最后一个项目67532(耶路撒冷希伯来大学)-源码

所需积分/C币:9 2021-02-16 02:56:42 66KB ZIP
6
收藏 收藏
举报

SAT解算器 :robot: 为了使用SAT求解器,您需要导入sat_solver.sat_engine ,然后调用其中定义了公式的函数solve_sat(formula) ,如下所示 原子命题应为'p'...'z'中的字母,并可选地后面跟数字序列。 例如:“ p”,“ y12”,“ z035”。 可以有“ T”和“ F”(分别为True和False)。 〜φ其中,φ是有效的命题公式。 '(φ&ψ)',其中φ和ψ均为有效命题公式。 '(φ|ψ)',其中φ和ψ均为有效命题公式。 '(φ->ψ)',其中φ和ψ均为有效的命题公式。 例子: from sat_solver.sat_engine import * formula = '(~p0|~pq<->(p2<->(p3->p4))))' print(solve_sat(formula)) SMT求解器 :ghost: 首先,您需要导入smt_solv

...展开详情
立即下载 身份认证VIP会员低至7折
一个资源只可评论一次,评论内容不能少于5个字
您会向同学/朋友/同事推荐我们的CSDN下载吗?
谢谢参与!您的真实评价是我们改进的动力~
  • 至尊王者

关注 私信
上传资源赚钱or赚积分
最新推荐
automatic_reasoning_abt_sw:“关于软件的自动推理”课程中的最后一个项目67532(耶路撒冷希伯来大学)-源码 9积分/C币 立即下载
1/0