程序验证(六):纳尔逊-欧朋算法(Nelson-Oppen Procedure)

2024-03-02 14:38

本文主要是介绍程序验证(六):纳尔逊-欧朋算法(Nelson-Oppen Procedure),希望对大家解决编程问题提供一定的参考价值,需要的开发者们随着小编来一起学习吧!

程序验证(六):纳尔逊-欧朋算法(Nelson-Oppen Procedure)

动机

截至目前,我们学习了一些一阶理论,每一个都是关于某一种数据类型
然而,现实中的公式并不是由单一的理论组成,如:
∀ i . 0 ≤ i ≤ n → a [ i ] ≤ a [ i + 1 ] \forall i.0\le i\le n\to a[i]\le a[i+1] i.0ina[i]a[i+1]
这个公式实际上包含了两个理论:等价与数组
我们需要找到一个方法,将复杂的一阶逻辑公式转化为简单的一阶逻辑公式

一些概念

复合理论

给定 T 1 , T 2 T_1,T_2 T1,T2,且 Σ 1 ∩ Σ 2 = { = } \Sigma_1\cap \Sigma_2 = \{=\} Σ1Σ2={=},那么复合理论 T 1 ∪ T 2 T_1\cup T_2 T1T2有:

  • 符号集: Σ 1 ∪ Σ 2 \Sigma_1 \cup \Sigma_2 Σ1Σ2
  • 公理集: A 1 ∪ A 2 A_1 \cup A_2 A1A2
    纳尔逊-欧朋(Nelson-Oppen)复合方法: T 1 ∪ T 2 T_1\cup T_2 T1T2是可判定的,如果 T 1 T_1 T1 T 2 T_2 T2均满足:
  • 是量词自由的合取的片段(Quantifier-free, conjunctive fragments)
  • 可判定的
  • 稳定无限的(stably-infinite)

稳定无限的理论

一个建立在符号集 Σ \Sigma Σ上的理论 T T T是稳定无限的,如果对于每个量词自由的公式 F F F,只要 F F F T T T-可满足的,存在一个解释,它的大小(cardinality)是无限的
例如这样的一个理论:

  • Σ = { a , b , = } \Sigma =\{a,b,=\} Σ={a,b,=}
  • 公理: ∀ x . x = a ∨ x = b \forall x.x=a\vee x=b x.x=ax=b
    这个理论不是稳定无限的,因为每个解释 ( D , I ) (D,I) (D,I)都有这样的性质: D D D包含至多两个元素,即 ∣ D ∣ ≤ 2 |D|\le 2 D2
    但是大多数我们关心的理论,即 T E , T A , T Z T_E,T_A,T_Z TE,TA,TZ等等,都是稳定无限的

纳尔逊-欧朋算法

概况

输入:由复合理论 T 1 ∪ T 2 T_1\cup T_2 T1T2得到的公式 F F F
输出:等价的公式 F 1 ∧ F 2 F_1\wedge F_2 F1F2,这里:

  • F 1 F_1 F1是一个 T 1 T_1 T1公式
  • F 2 F_2 F2是一个 T 2 T_2 T2公式
    这个算法的功能:
  • F F F净化为 F 1 F_1 F1 F 2 F_2 F2
  • F 1 F_1 F1 F 2 F_2 F2中共享的变量做等价变换

步骤1:变量抽象

理论

目标: F F F中所有的文字或者属于 T 1 T_1 T1,或者属于 T 2 T_2 T2,但不能是二者共有
方法:将以下两个转化方法不断使用,直到不能再用为止:

  • 对于任何一项 f ( … , t , … ) f(\dots ,t,\dots) f(,t,),满足 f ∈ Σ i f\in \Sigma_i fΣi t ∉ Σ i t\not\in \Sigma_i tΣi,将 t t t用一个新的(fresh)变量 w w w替换,并在最后合取上 t = w t=w t=w
  • 对于任一谓词 p ( … , t , … ) p(\dots ,t,\dots) p(,t,),满足 p ∈ Σ i p\in \Sigma_i pΣi t ∉ Σ i t\not\in \Sigma_i tΣi,将 t t t用一个新的(fresh)变量 w w w替换,并在最后合取上 t = w t=w t=w
    结束的时候,我们就可以把 F F F分为 F 1 F_1 F1 F 2 F_2 F2了。
举例

考虑 T E ∪ T Z T_E\cup T_Z TETZ公式 F F F:
F : 1 ≤ x ∧ x ≤ 2 ∧ f ( x ) ≠ f ( 1 ) ∧ f ( x ) ≠ f ( 2 ) F:1\le x\wedge x\le 2\wedge f(x)\ne f(1)\wedge f(x)\ne f(2) F:1xx2f(x)=f(1)f(x)=f(2)

  • T E T_E TE中的非逻辑符是哪些? f , = f,= f,=
  • T Z T_Z TZ中的非逻辑符是哪些? 1 , 2 , ≤ , = 1,2,\le,= 1,2,,=
  • 净化:用 f ( w 1 ) f(w_1) f(w1)代替 f ( 1 ) f(1) f(1),用 f ( w 2 ) f(w_2) f(w2)代替 f ( 2 ) f(2) f(2),加入 w 1 = 1 w_1=1 w1=1 w 2 = 2 w_2=2 w2=2,得到 1 ≤ x ∧ x ≤ 2 ∧ f ( x ) ≠ f ( w 1 ) ∧ f ( x ) ≠ f ( w 2 ) ∧ w 1 = 1 ∧ w 2 = 2 1\le x\wedge x\le 2\wedge f(x)\ne f(w_1)\wedge f(x)\ne f(w_2)\wedge w_1=1\wedge w_2=2 1xx2f(x)=f(w1)f(x)=f(w2)w1=1w2=2
  • F E : f ( x ) ≠ f ( w 1 ) ∧ f ( x ) ≠ f ( w 2 ) F_E:f(x)\ne f(w_1)\wedge f(x)\ne f(w_2) FE:f(x)=f(w1)f(x)=f(w2)
  • F Z : 1 ≤ x ∧ x ≤ 2 ∧ w 1 = 1 ∧ w 2 = 2 F_Z:1\le x\wedge x\le 2\wedge w_1 = 1\wedge w_2 = 2 FZ:1xx2w1=1w2=2

步骤2:猜测与检查(guess and check)

理论

给定 F 1 F_1 F1 F 2 F_2 F2,定义共享变量集 V V V:
V = f r e e ( F 1 ) ∩ f r e e ( F 2 ) V=free(F_1)\cap free(F_2) V=free(F1)free(F2)
E E E V V V上的一个等价关系,由 E E E生成的arrangement α ( V , E ) \alpha (V,E) α(V,E)即为:
α ( V , E ) : ⋀ u , v ∈ V . u E v u = v ∧ ⋀ u , v ∈ V . ¬ ( u E v ) u ¬ v \alpha (V,E): \bigwedge _{u,v\in V.uEv} u=v \wedge\bigwedge _{u,v\in V.\neg (uEv)} u\neg v α(V,E):u,vV.uEvu=vu,vV.¬(uEv)u¬v
公式 F = F 1 ∧ F 2 F=F_1 \wedge F_2 F=F1F2 ( T 1 ∪ T 2 ) (T_1\cup T_2) (T1T2)-可满足的当且仅当存在这样的 α ( V , E ) \alpha (V,E) α(V,E)使得:

  • F 1 ∧ α ( V , E ) F_1\wedge \alpha (V,E) F1α(V,E) T 1 T_1 T1-可满足的
  • F 2 ∧ α ( V , E ) F_2\wedge \alpha (V,E) F2α(V,E) T 2 T_2 T2-可满足的
举例

考虑之前的净化后的两个公式
共享变量: V = { w 1 , w 2 , x } V=\{w_1,w_2,x\} V={w1,w2,x}
猜测并检查 V V V上的等价关系:

  • { { w 1 } , { w 2 } , { x } } \{\{w_1\},\{w_2\},\{x\}\} {{w1},{w2},{x}}
  • { { w 1 , w 2 } , { x } } \{\{w_1,w_2\},\{x\}\} {{w1,w2},{x}}
  • { { w 1 } , { w 2 , x } } \{\{w_1\},\{w_2,x\}\} {{w1},{w2,x}}
  • { { w 2 } , { w 1 , x } } \{\{w_2\},\{w_1,x\}\} {{w2},{w1,x}}
  • { { w 1 , w 2 , x } } \{\{w_1,w_2,x\}\} {{w1,w2,x}}
效率问题

这个guess and check的时间复杂度是指数级的,所以不太实用,所以我们换个方法。

步骤2:等价推导(equality propagation)

凸理论(convex theory)

一个理论是凸的(convex),如果它对于每个变量自由的公式 F F F,都满足:

F ⇒ ⋁ i = 1 n u i = v i F\Rightarrow \bigvee ^n_{i=1} u_i =v_i Fi=1nui=vi

F ⇒ u i = v i f o r s o m e i ∈ { 1 , … , n } F\Rightarrow u_i = v_i~for~some~i\in\{1,\dots , n\} Fui=vi for some i{1,,n}
T Z , T A T_Z, T_A TZ,TA不是凸的,但是 T E , T Q T_E,T_Q TE,TQ是凸的。
举例: T Z T_Z TZ不是凸的
例如,考虑这样的量词自由的合取 Σ Z \Sigma_Z ΣZ-公式
F : 1 ≤ z ∧ z ≤ 2 ∧ u = 1 ∧ v = 2 F: 1\le z\wedge z\le 2\wedge u=1\wedge v=2 F:1zz2u=1v=2
那么
F ⇒ z = u ∨ z = v F\Rightarrow z=u\vee z=v Fz=uz=v
但是无法推出
F ⇒ z = u F\Rightarrow z=u Fz=u

F ⇒ z = v F\Rightarrow z=v Fz=v

等价推导

给定 F 1 F_1 F1 F 2 F_2 F2

  • T i ( i = 1 , 2 ) T_i (i=1,2) Ti(i=1,2)报告任何有关共享变量(包括 u u u, v v v)的新推出的等价关系
    • 如果 T i T_i Ti是凸的,令 u = v u=v u=v为新推出的等价关系
    • 如果 T i T_i Ti不是凸的,令 ⋁ i ( u i = v i ) \bigvee_i (u_i = v_i) i(ui=vi)为推出的等价关系的析取
  • 将新推出的等价关系存储到 E E E中( E E E是已经发现的等价关系的集合)
    • 如果 T i T_i Ti是凸的,将 u = v u=v u=v添加到 E E E
    • 如果 T i T_i Ti不是凸的,将搜索过程依据不同的析取 ⋁ i ( u i = v i ) \bigvee_i(u_i = v_i) i(ui=vi)分成不同的分支(通过在 E E E中添加相应的等价关系)
  • 对于每一个分支,将 E E E传播到另一个判定程序(也就是递归进行),重复以上步骤

算法返回:

  • s a t sat sat如果任一分支得到一个完整的arrangement
  • u n s a t unsat unsat如果所有的分支都推出矛盾
  • s a t sat sat如果所有的分支都不能发现新的等价关系
举例
1

考虑 Σ E ∪ Σ Q \Sigma_E\cup \Sigma_Q ΣEΣQ-公式:
F : f ( f ( x ) − f ( y ) ) ≠ f ( z ) ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ z F:f(f(x)-f(y))\ne f(z)\wedge x\le y\wedge y+z\le x\wedge 0\le z F:f(f(x)f(y))=f(z)xyy+zx0z
在第一步后, F F F被分为两个公式:

  • F E : f ( w ) ≠ f ( z ) ∧ u = f ( x ) ∧ v = f ( y ) F_E:f(w)\ne f(z)\wedge u=f(x)\wedge v=f(y) FE:f(w)=f(z)u=f(x)v=f(y)
  • F Q : x ≤ y ∧ y + z ≤ x ∧ 0 ≤ z ∧ w = u − v F_Q:x\le y\wedge y+z\le x\wedge 0\le z\wedge w=u-v FQ:xyy+zx0zw=uv
  • V = s h a r e d ( F E , F Q ) = { x , y , z , u , v , w } V=shared(F_E,F_Q)=\{x,y,z,u,v,w\} V=shared(FE,FQ)={x,y,z,u,v,w}

注意, T E T_E TE T Q T_{\mathbb{Q}} TQ都是凸理论
于是
在这里插入图片描述

2

考虑 T E ∪ T Z T_E\cup T_{\mathbb{Z}} TETZ-公式 F F F
F : 1 ≤ x ∧ x ≤ 2 ∧ f ( x ) ≠ f ( 1 ) ∧ f ( x ) ≠ f ( 2 ) F:1\le x\wedge x\le 2\wedge f(x)\ne f(1)\wedge f(x)\ne f(2) F:1xx2f(x)=f(1)f(x)=f(2)
在第一步后, F F F被分为两个公式:

  • F E : f ( x ) ≠ f ( w 1 ) ∧ f ( x ) ≠ f ( w 2 ) F_E:f(x)\ne f(w_1)\wedge f(x)\ne f(w_2) FE:f(x)=f(w1)f(x)=f(w2)
  • F Z : 1 ≤ x ∧ x ≤ 2 ∧ w 1 = 1 ∧ w 2 = 2 F_{\mathbb{Z}} :1\le x\wedge x\le 2\wedge w_1=1\wedge w_2=2 FZ:1xx2w1=1w2=2
  • V = s h a r e d ( F E , F Z ) = { w 1 , w 2 , x } V=shared(F_E,F_{\mathbb{Z}})=\{w_1,w_2,x\} V=shared(FE,FZ)={w1,w2,x}

注意, T E T_E TE是凸的, T Z T_{\mathbb{Z}} TZ不是
于是
在这里插入图片描述

3

考虑 T E ∪ T Z T_E\cup T_{\mathbb{Z}} TETZ-公式 F F F:
F : 1 ≤ x ∧ x ≤ 3 ∧ f ( x ) ≠ f ( 1 ) ∧ f ( x ) ≠ f ( 3 ) ∧ f ( 1 ) ≠ f ( 2 ) F: 1\le x\wedge x\le 3\wedge f(x)\ne f(1)\wedge f(x)\ne f(3)\wedge f(1)\ne f(2) F:1xx3f(x)=f(1)f(x)=f(3)f(1)=f(2)
在第一步后, F F F被分为两个公式:

  • F E : f ( x ) ≠ f ( w 1 ) ∧ f ( x ) ≠ f ( w 3 ) ∧ f ( w 1 ) ≠ f ( w 2 ) F_E:f(x)\ne f(w_1)\wedge f(x)\ne f(w_3)\wedge f(w_1)\ne f(w_2) FE:f(x)=f(w1)f(x)=f(w3)f(w1)=f(w2)
  • F Z : 1 ≤ x ∧ x ≤ 3 ∧ w 1 = 1 ∧ w 2 = 2 ∧ w 3 = 3 F_{\mathbb{Z}}:1\le x\wedge x\le 3\wedge w_1=1\wedge w_2=2\wedge w_3=3 FZ:1xx3w1=1w2=2w3=3
  • V = s h a r e d ( F E , F Z ) = { w 1 , w 2 , w 3 , x } V=shared(F_E,F_{\mathbb{Z}})=\{w_1,w_2,w_3,x\} V=shared(FE,FZ)={w1,w2,w3,x}

注意, T E T_E TE是凸的, T Z T_{\mathbb{Z}} TZ不是
于是
在这里插入图片描述

这篇关于程序验证(六):纳尔逊-欧朋算法(Nelson-Oppen Procedure)的文章就介绍到这儿,希望我们推荐的文章对编程师们有所帮助!



http://www.chinasem.cn/article/766453

相关文章

不懂推荐算法也能设计推荐系统

本文以商业化应用推荐为例,告诉我们不懂推荐算法的产品,也能从产品侧出发, 设计出一款不错的推荐系统。 相信很多新手产品,看到算法二字,多是懵圈的。 什么排序算法、最短路径等都是相对传统的算法(注:传统是指科班出身的产品都会接触过)。但对于推荐算法,多数产品对着网上搜到的资源,都会无从下手。特别当某些推荐算法 和 “AI”扯上关系后,更是加大了理解的难度。 但,不了解推荐算法,就无法做推荐系

康拓展开(hash算法中会用到)

康拓展开是一个全排列到一个自然数的双射(也就是某个全排列与某个自然数一一对应) 公式: X=a[n]*(n-1)!+a[n-1]*(n-2)!+...+a[i]*(i-1)!+...+a[1]*0! 其中,a[i]为整数,并且0<=a[i]<i,1<=i<=n。(a[i]在不同应用中的含义不同); 典型应用: 计算当前排列在所有由小到大全排列中的顺序,也就是说求当前排列是第

csu 1446 Problem J Modified LCS (扩展欧几里得算法的简单应用)

这是一道扩展欧几里得算法的简单应用题,这题是在湖南多校训练赛中队友ac的一道题,在比赛之后请教了队友,然后自己把它a掉 这也是自己独自做扩展欧几里得算法的题目 题意:把题意转变下就变成了:求d1*x - d2*y = f2 - f1的解,很明显用exgcd来解 下面介绍一下exgcd的一些知识点:求ax + by = c的解 一、首先求ax + by = gcd(a,b)的解 这个

综合安防管理平台LntonAIServer视频监控汇聚抖动检测算法优势

LntonAIServer视频质量诊断功能中的抖动检测是一个专门针对视频稳定性进行分析的功能。抖动通常是指视频帧之间的不必要运动,这种运动可能是由于摄像机的移动、传输中的错误或编解码问题导致的。抖动检测对于确保视频内容的平滑性和观看体验至关重要。 优势 1. 提高图像质量 - 清晰度提升:减少抖动,提高图像的清晰度和细节表现力,使得监控画面更加真实可信。 - 细节增强:在低光条件下,抖

【数据结构】——原来排序算法搞懂这些就行,轻松拿捏

前言:快速排序的实现最重要的是找基准值,下面让我们来了解如何实现找基准值 基准值的注释:在快排的过程中,每一次我们要取一个元素作为枢纽值,以这个数字来将序列划分为两部分。 在此我们采用三数取中法,也就是取左端、中间、右端三个数,然后进行排序,将中间数作为枢纽值。 快速排序实现主框架: //快速排序 void QuickSort(int* arr, int left, int rig

poj 3974 and hdu 3068 最长回文串的O(n)解法(Manacher算法)

求一段字符串中的最长回文串。 因为数据量比较大,用原来的O(n^2)会爆。 小白上的O(n^2)解法代码:TLE啦~ #include<stdio.h>#include<string.h>const int Maxn = 1000000;char s[Maxn];int main(){char e[] = {"END"};while(scanf("%s", s) != EO

秋招最新大模型算法面试,熬夜都要肝完它

💥大家在面试大模型LLM这个板块的时候,不知道面试完会不会复盘、总结,做笔记的习惯,这份大模型算法岗面试八股笔记也帮助不少人拿到过offer ✨对于面试大模型算法工程师会有一定的帮助,都附有完整答案,熬夜也要看完,祝大家一臂之力 这份《大模型算法工程师面试题》已经上传CSDN,还有完整版的大模型 AI 学习资料,朋友们如果需要可以微信扫描下方CSDN官方认证二维码免费领取【保证100%免费

dp算法练习题【8】

不同二叉搜索树 96. 不同的二叉搜索树 给你一个整数 n ,求恰由 n 个节点组成且节点值从 1 到 n 互不相同的 二叉搜索树 有多少种?返回满足题意的二叉搜索树的种数。 示例 1: 输入:n = 3输出:5 示例 2: 输入:n = 1输出:1 class Solution {public int numTrees(int n) {int[] dp = new int

Codeforces Round #240 (Div. 2) E分治算法探究1

Codeforces Round #240 (Div. 2) E  http://codeforces.com/contest/415/problem/E 2^n个数,每次操作将其分成2^q份,对于每一份内部的数进行翻转(逆序),每次操作完后输出操作后新序列的逆序对数。 图一:  划分子问题。 图二: 分而治之,=>  合并 。 图三: 回溯:

最大公因数:欧几里得算法

简述         求两个数字 m和n 的最大公因数,假设r是m%n的余数,只要n不等于0,就一直执行 m=n,n=r 举例 以18和12为例 m n r18 % 12 = 612 % 6 = 06 0所以最大公因数为:6 代码实现 #include<iostream>using namespace std;/