我想在另一个模型中使用模型的输出(在我的情况下是sat和不饱和) . 这里,模型是对一组逻辑公式(在这种情况下为Z3表达式)中涉及的常量的令人满意的赋值 . 我的目标可以简要解释如下 .
我的问题可以详细描述如下:我有一个问题P,一组逻辑公式(表达式)对应于一些约束(C) . 在表达式中,一个(例如,Ai> 0)是我的目标 . 如果所有约束都是可满足的,则执行模型/形式化P返回sat . 注意,Ai = 0始终是可能的 . 现在,我想找到一组特定变量的赋值集对应于确保Ai> 0(对于任何i)不可能的约束(C) . 目前,我正在通过编写一个程序(在C#中)来解决这个问题,该程序开发了一个基于DFS的约束搜索算法(即约束值)并执行P以在“push / pop”的帮助下查看结果是否为false ” . 虽然我试图让搜索更好,但它对我帮助不大 . 对于大问题,这是非常低效的 . 如果我能用P创建另一个SMT程序(模型)来搜索这样一个可满足的集合,那就太好了 .
问题P的当前形式化(原始问题的短SMT LIB 2版本)如下:
(declare-fun th1 () Real)
(declare-fun th2 () Real)
(declare-fun th3 () Real)
(declare-fun th4 () Real)
(declare-fun th5 () Real)
(declare-fun l1 () Real)
(declare-fun l2 () Real)
(declare-fun l3 () Real)
(declare-fun l4 () Real)
(declare-fun l5 () Real)
(declare-fun l6 () Real)
(declare-fun l7 () Real)
(declare-fun p1 () Real)
(declare-fun p2 () Real)
(declare-fun p3 () Real)
(declare-fun p4 () Real)
(declare-fun p5 () Real)
(declare-fun sl1 () Int)
(declare-fun sl2 () Int)
(declare-fun sl3 () Int)
(declare-fun sl4 () Int)
(declare-fun sl5 () Int)
(declare-fun sl6 () Int)
(declare-fun sl7 () Int)
(declare-fun sp1 () Int)
(declare-fun sp2 () Int)
(declare-fun sp3 () Int)
(declare-fun sp4 () Int)
(declare-fun sp5 () Int)
(declare-fun a1 () Int)
(declare-fun a2 () Int)
(declare-fun a3 () Int)
(declare-fun a4 () Int)
(declare-fun a5 () Int)
(declare-fun na () Int)
(declare-fun ns () Int)
(declare-fun attack () Bool)
;;;; System
(assert (and (= l1 (* (- th2 th1) 17.0))
(= l2 (* (- th5 th1) 4.5))
(= l3 (* (- th3 th2) 5.05))
(= l4 (* (- th4 th2) 5.65))
(= l5 (* (- th5 th2) 5.75))
(= l6 (* (- th4 th3) 5.85))
(= l7 (* (- th5 th4) 23.75))
(= p1 (+ l1 l2))
(= p2 (+ l1 l3 l4 l5))
(= p3 (+ l3 l6))
(= p4 (+ l4 l6 l7))
(= p5 (+ l2 l5 l7))
)
)
;;;; Secured measurements
(assert (and (or (= sl1 0) (= sl1 1))
(or (= sl2 0) (= sl2 1))
(or (= sl3 0) (= sl3 1))
(or (= sl4 0) (= sl4 1))
(or (= sl5 0) (= sl5 1))
(or (= sl6 0) (= sl6 1))
(or (= sl7 0) (= sl7 1))
(or (= sp1 0) (= sp1 1))
(or (= sp2 0) (= sp2 1))
(or (= sp3 0) (= sp3 1))
(or (= sp4 0) (= sp4 1))
(or (= sp5 0) (= sp5 1))
)
)
(assert (and (=> (not (= l1 0.0)) (= sl1 0))
(=> (not (= l2 0.0)) (= sl2 0))
(=> (not (= l3 0.0)) (= sl3 0))
(=> (not (= l4 0.0)) (= sl4 0))
(=> (not (= l5 0.0)) (= sl5 0))
(=> (not (= l6 0.0)) (= sl6 0))
(=> (not (= l7 0.0)) (= sl7 0))
(=> (not (= p1 0.0)) (= sp1 0))
(=> (not (= p2 0.0)) (= sp2 0))
(=> (not (= p3 0.0)) (= sp3 0))
(=> (not (= p4 0.0)) (= sp4 0))
(=> (not (= p5 0.0)) (= sp5 0))
)
)
(assert (and (= sl1 1) (= sl2 1)))
;;;; Attacks
(assert (and (or (= a1 0) (= a1 1))
(or (= a2 0) (= a2 1))
(or (= a3 0) (= a3 1))
(or (= a4 0) (= a4 1))
(or (= a5 0) (= a5 1))
)
)
(assert (and
(= (not (= th1 0.0)) (= a1 1))
(= (not (= th2 0.0)) (= a2 1))
(= (not (= th3 0.0)) (= a3 1))
(= (not (= th4 0.0)) (= a4 1))
(= (not (= th5 0.0)) (= a5 1))
)
)
(assert (= th1 0.0)) // Base condition
(assert (= na (+ a1 a2 a3 a4 a5)))
(assert (=> attack (> na 1)))
;;;; Check for satisfiable model
(assert attack)
(check-sat)
(get-model)
(exit)
我想合成安全性测量(即,找到'sl'和'sp'项的赋值),以便在给定约束的情况下不存在攻击(即,na将为0),例如,如下:
(assert (= ns (+ sl1 sl2 sl3 sl4 sl5 sl6 sl7 sp1 sp2 sp3 sp4 sp5)))
(assert (<= ns 4))
在这种情况下,将声明断言(即'(断言(和(= sl1 1)(= sl2 1)))') . 目前,我开发了一个C#程序,它接受'sl'和'sp'的赋值,断言它们(assert(和(= sl1 1)(= sl2 1)...))',然后执行给定的程序看看是否有任何可能的攻击 . 当程序返回不满时我就完成了(即,na> 1是不可能的) . 有没有办法只使用SMT(Z3)解决问题?
2 回答
谢谢你清理问题 . 如果我已经理解了东西,你可以使用Z3搜索
sli
和spj
值,但是你不能仅使用SMT-LIB来执行此操作,需要使用API . 我们的想法是使用一个坐标检查中的模型(满足分配)作为未来检查中的约束,详见下面的答案:Z3: finding all satisfying models
Z3: Check if model is unique
(Z3Py) checking all solutions for equation
这是您在Python API中编码的示例(z3py链接:http://rise4fun.com/Z3Py/KHzm):
对所有常量和数字表示道歉,我刚刚使用了SMT-LIB脚本的最快翻译,但最后却变得相当繁琐,我会在任何地方使用迭代器 . 这会在
sli
和spj
常量上生成以下约束:如果我理解正确,那么你正在寻找(通用)量化 . 请原谅我的伪符号,但是你不是在寻找对以下自由变量(
config_params
)的令人满意的赋值吗?其中
()
符号仅表示约束所依赖的变量(集合) . 我很确定.Net API支持量词,因为它们在Java API中 .