Loading [MathJax]/jax/output/SVG/jax.js
  • ISSN 0258-2724
  • CN 51-1277/U
  • EI Compendex
  • Scopus 收录
  • 全国中文核心期刊
  • 中国科技论文统计源期刊
  • 中国科学引文数据库来源期刊

多孔介质海床对单桩所受波浪力的影响分析

陈林雅 廖晨聪 段伦良 郑东生

曾国艳, 徐扬, 陈树伟, 姜世攀. 基于多属性决策的一阶逻辑子句选择方法[J]. 西南交通大学学报, 2025, 60(1): 185-193. doi: 10.3969/j.issn.0258-2724.20230023
引用本文: 陈林雅, 廖晨聪, 段伦良, 郑东生. 多孔介质海床对单桩所受波浪力的影响分析[J]. 西南交通大学学报, 2019, 54(2): 328-335. doi: 10.3969/j.issn.0258-2724.20170800
ZENG Guoyan, XU Yang, CHEN Shuwei, JIANG Shipan. First-Order Logic Clause Selection Method Based on Multi-criteria Decision Making[J]. Journal of Southwest Jiaotong University, 2025, 60(1): 185-193. doi: 10.3969/j.issn.0258-2724.20230023
Citation: CHEN Linya, LIAO Chencong, DUAN Lunliang, ZHENG Dongsheng. Influence of Porous Seabed Characteristics on Wave Forces Acting on Monopile[J]. Journal of Southwest Jiaotong University, 2019, 54(2): 328-335. doi: 10.3969/j.issn.0258-2724.20170800

多孔介质海床对单桩所受波浪力的影响分析

doi: 10.3969/j.issn.0258-2724.20170800
基金项目: 国家自然科学基金项目资助项目(41176073);中央高校基本科研业务费专项资金资助项目(2682017QY02)
详细信息
    作者简介:

    陈林雅(1990—),女,博士研究生,研究方向为桥梁基础流固土耦合动力学及长期服役安全控制,E-mail:chenlinya01@yeah.net

    通讯作者:

    郑东生(1964—),男,教授,博士,研究方向为波浪-海床-结构物相互作用理论,E-mail:dsjeng@home.swjtu.edu.cn

  • 中图分类号: V221.3

Influence of Porous Seabed Characteristics on Wave Forces Acting on Monopile

  • 摘要: 为研究多孔介质海床的波浪衰减作用及单桩所受波浪力的变化规律,采用修正RANS方程和Forchheimer饱和阻力模型控制多孔介质内部流体流动,运用流体体积法追踪自由液面,建立波浪-多孔介质海床-单桩相互作用三维数值分析模型. 首先,基于波浪与多孔介质海床相互作用过程,研究了多孔介质海床对波浪传播的衰减作用;其次,分析了相同波浪条件下多孔介质海床及刚性海床时单桩所受波浪力的数值变化,突出了考虑海床多孔特性的必要性;最后,采用单一变量控制法,进一步研究了单桩所受波浪力数值随海床多孔特性参数的变化规律. 研究结果表明,海床多孔特性对波浪传播具有明显的衰减作用;给定的波浪参数和多孔介质海床条件下,单桩所受波浪力最大值比刚性海床情况提高约35%,若忽略海床多孔特性结构物会因低估波浪力数值而造成安全隐患;另外,结构物所受波浪力与海床孔隙率、颗粒直径、海床厚度及双层海床分布厚度及每层孔隙率密切相关. 其中,波浪力最大值随着海床颗粒直径的增加而递减,随着孔隙率的增大先增加后降低,且孔隙率会影响波浪力随海床厚度变化的趋势.

     

  • 一阶逻辑是经典的逻辑理论,基于一阶逻辑的定理机器证明和自动推理是人工智能领域的重要研究课题. 1965年,Robinson[1]提出的归结原理是实现定理自动证明的工具之一,推动了自动推理的发展.自动定理证明器(ATP)通过输入被形式化为一阶逻辑的前提条件和结论,自动从前提条件推出结论. 研究ATP有重要的应用价值:一阶逻辑可以形式化研究软件验证[2]、数学定理证明[3]、信息安全的程序自动验证[4]等.

    因为一阶逻辑子句含有变元的函数项,所以搜索空间是无限的,这使得一阶逻辑定理的证明成为一个无限问题. 目前,ATP采用的推理规则主要有2类:一类是归结原理,每次有且仅有2个子句参与归结,只消去一组互补对文字,生成的归结式含有大量文字;另一类是2018年Xu等[5]提出的标准矛盾体分离(S-CS)规则,突破了静态二元归结的限制,允许多个子句动态参与演绎,生成大量单元子句. Xu等[6]同年分析了(S-CS)规则的优势,如动态性、协同性、鲁棒性等.

    根据上述提到的2类推理方法,ATP选择其中一种作为推理机制. 确定推理机制后,提高ATP的证明效率是关键. ATP选择子句集中的子句,按照推理规则进行推理,直至推出空子句,定理得证. 子句的选择是ATP必不可少的部分. 理论和实验表明,有些子句会多次参与演绎推理,而有些则未能参与. 因此,通过启发式策略选取合适的子句对提升ATP性能至关重要. 由于不同推理规则之间存在本质差异,针对基于不同推理规则的ATP,应采用不同的启发式策略.

    当前,针对ATP的启发式策略已有广泛研究. 例如,基于重写规则的E中多种项排序策略[7]、基于二元归结的Vampire中动态选择策略[8]. 基于S-CS规则的启发式策略包括子句演绎权重[9]、决策文字选择策略和矛盾体分离式策略[10]等. 这些子句选择策略通常通过设定策略优先级来决定子句参与演绎的顺序,优先级越高的策略对应的子句会优先被选择. 然而,这些策略有时需要多次比较子句优先级,才能选择出一个合适的子句,在一定程度上会影响对子句的评估.

    为解决该问题,本文提出一种新的子句选择框架,将多种策略选择子句视为多属性决策问题. 不同的子句选择策略反映了子句的不同属性特征,因此,每种策略对应不同的子句属性,为多属性决策(MCDM)方法综合评估子句提供了基础. 本文利用MCDM方法,根据多种子句属性值对各子句进行综合评估.

    目前,已有多种经典的MCDM方法,例如逼近理想解法(TOPSIS) [11]、VIKOR[12]和偏好顺序结构评估法(PROMETHEE) [13]等. 其中,PROMETHEE能在丢失很少属性信息情况下对候选子句进行部分或完全排序,因而在实际决策过程中较其他MCDM方法具有更高的灵活性. PROMETHEE的核心思想是通过正、负优先流以及净占优流对候选子句进行排序,其已扩展出多种形式[14],包括PROMEHTEE Ⅰ 、PROMETHEE Ⅱ 、PROMETHEE Ⅲ、PROMETHEE Ⅳ等. 其中,PROMETHEE Ⅱ能够对候选子句进行完全排序,且无需对子句属性值进行量纲化和规范化处理,从而避免了信息偏差. 因此,本文选择PROMETHEE Ⅱ对子句进行评估.

    本文采用MCDM方法评估子句有如下优点:1) MCDM基于子句的多种客观信息进行评估,有效避免了人为设定策略优先级的问题,一定程度上减少了为设置优先级而进行的大量实验测试. 2) MCDM已有成熟的研究,为多属性决策评估子句提供了理论依据,支持多种子句属性同时参与决策评估. 3) WCDM是一种高效的动态综合评估方法,能够反映子句的多种属性特征,通过组合策略进行评估,通常优于单一策略.

    本文基于S-CS规则的多个子句动态参与演绎的特性,在演绎过程中应用PROMETHEE Ⅱ方法对子句进行排序. 当子句属性值在演绎过程中发生更新时,子句排序也会相应更新. 对比实验结果表明,基于S-CS规则的PROMETHEE Ⅱ方法能有效提升ATP的性能.

    首先介绍本文涉及的一阶逻辑的相关概念[15].原子公式由谓词符号(如P)和项组成. 其中,变元(如x, y)、常元(如a)和函数符(如f)都是项. 原子公式A及其否定¬A称为文字,称A¬A为互补对. 若干个文字的析取称为子句,只有一个文字的子句称为单元子句. 若干个子句的合集称为子句集. 一个替换是形如{t1/y1,t2/y2,,tN/yN}的有限集合,其中,yJJ=1,2,,N为变量符号,N为变量个数, tJ为不同于yJ的项. 集合中yJ各不相同,称tJ为替换的分子,yJ为替换的分母.

    二元归结方法只允许(有互补对的) 2个子句参与归结,从而仅消去1组互补对文字;而矛盾体分离规则允许多个子句参与演绎,每次演绎可消去多组互补对,是二元归结方法的拓展.

    矛盾体分离规则[5]:设一阶逻辑子句集 S={C1,C2,,Cm}m为子句个数),子句 C1C2Cm之间不存在相同变元(若存在不同的子句有相同的变元,则需对变元更名),称由子句集S产生新子句的推理规则为标准矛盾体分离规则,简称S-CS规则.

    对于任意子句Ckk=1,2,,m),存在替换σk可以应用于子句Ckσk可以为空替换),使得Ck中相同的文字可以合并,得到子句Ckσk.Ckσk分为两部分子句(CkσkC+kσk),满足:

    1) Ckσk=CkσkC+kσk, CkσkC+kσk不含相同的文字,Ckσk不能为空,C+kσk可以为空.

    2) 对任意x1,x2,,xmmk=1Ckσkx1,x2,,xm中至少存在一个互补对文字,称mk=1Ckσk为标准矛盾体(S-SC).

    3) mk=1C+kσk=Csmσ(C1,C2,,Cm),其中,σ=mk=1σk,称Csmσ(C1,C2,,Cm)为矛盾体分离式(S-CSC).

    根据上述S-CS规则,演绎定义如下:

    定义1 矛盾体分离动态演绎[5]:设一阶逻辑子句集S={C1,C2,,Cm},对于任意的h{1,2,,ˉt}ˉt为演绎序列个数),当Φ1,Φ2,,Φˉt满足下列条件之一,则称Φ1,Φ2,,Φˉt为基于标准矛盾体分离的多元动态演绎序列,称该演绎为S-CS演绎:

    1)ΦhS.

    2) 存在 r1,r2,,rlh<h, 有矛盾体分离式Φh=Csrlhθh(Φr1,Φr2,,Φrlh). 其中,替换 θh=lhK=1σK,σKΦrK的变元替换,K=1,2,,lh.

    与二元归结演绎形成鲜明对比,S-CS演绎有以下显著的优势:

    1) 多元演绎. 多个子句协同参与演绎,通过分离矛盾体删除多个互补对,从而生成含有文字数较少的矛盾体分离式.

    2) 可控性. 矛盾体的大小和文字数均可控. 可限制S-CS规则生成的矛盾体分离式所含的文字数,如限制在6个文字以内. 当生成的子句不符合该限制时,将重新构造矛盾体,直到生成的子句满足文字数限制或产生空子句为止.

    3) 生成大量单元子句,S-CS规则有生成大量单元子句的能力. 如在矛盾体分离式的文字数不超过6个的限制下,通过实验分析发现,矛盾体分离式为单元子句的占比为90%左右.

    为更好地规划演绎搜索路径并节省计算资源,学者们提出了多种启发式策略[16-19] ,用于选择合适的子句和文字参与演绎推理. 子句选择策略主要依据不同的评估标准来选择最优子句进行推理,即从不同角度刻画子句特性,描述子句各种属性,根据选择方案确定当前推理过程中的最优子句. 目前,国际主流ATP采用的主要策略包括以下几种类型:

    1) 基于字符符号和“序”评估的策略[7,16]. 如基于重写规则的E中KBO (Knuth-Bendix order) 序方法对等词的有效处理[16]. 基于人为设定项的权重,KBO序是项重写的基础,可终止等词替换.

    2) 分层的子句选取策略. 如 GKC (graph knowledge core)中分层的子句选择策略[17]. 针对大知识库,GKC使用2层的子句选择方法,多个队列被用于选择子句,并赋予不同的优先级. 如第1层使用项总数排序和子句生成时间排序的队列,第2层使用4个队列.

    3) 基于二元归结的Vampire中动态调度策略[8,18]. Vampire实现了动态调用策略[18],给定策略优先级,优先使用最有可能成功的策略,如生成子句的文字数最小策略.

    由于上述ATP受推理机制的影响,在搜索空间中保留了大量含有较多文字数的归结式,所以上面的子句选择策略主要是为了避免搜索空间的迅速增长. 相比而言,基于S-CS规则的子句选择策略有明显不同. 针对S-CS规则的策略更倾向于全面的路径搜索,以充分发挥S-CS规则的动态演绎能力.

    基于子句的符号特征,提出以下子句选择策略:

    1) 子句的文字数:子句中包含的文字数目. 在演绎过程中,包含文字数较少的子句通常有更高的演绎推理效率. 因此,只含一个文字的单元子句必定参与演绎,其次选择文字数较少的非单元子句参与演绎.

    2) 子句函数项嵌套层数:子句的函数项嵌套层数越多,所涉及的替换越复杂,因此,选择函数项嵌套层数少的子句参与演绎,同时也控制生成的矛盾体分离式的函数项嵌套层数.

    3) 子句的负文字数:子句中包含的负文字数目. 在演绎过程中,包含负文字多的子句通常与结论密切相关,所以优先选择包含负文字多的子句参与演绎推理. 比如,最多只含一个正文字的Horn子句被优先选择. 特别地,优先选择只有负文字的负子句.

    4) 矛盾分离式的文字数:S-CSC包含的文字数目. 当矛盾体分离式为空子句时,ATP证明定理成功. 所以应该控制矛盾体分离式的文字数,如少于6个文字. 当矛盾体分离式的文字数不小于6个时,返回上一演绎步骤,重新选择子句构造矛盾体. 将生成的矛盾体分离式加入原始子句集,以构造新的子句集,直到演绎出空子句.

    在子句的使用次数方面,提出以下子句选择策略:

    1) 子句参与演绎的次数:每当子句参与一次演绎,其计数加 1,重复使用的子句会多次累计. 这一策略有效避免了演绎路径的局部最优和部分子句未参与推理的情况,确保路径搜索的全面性.

    2) 重复使用子句策略[19]:对子句集中的子句进行重复使用,并设置重复使用次数的阈值. 该策略确保充分使用子句的演绎能力,以搜索更多的演绎路径.

    本文根据S-CS规则的特点,为充分利用其优势,并体现 S-CS 演绎的以下特性:文字的可控性、子句的可重复性、协同性、灵活性、目标导向性,选取以下5种属性进行综合评估:子句的文字数、重复使用子句的次数、子句参与演绎的次数、子句函数项嵌套层数和子句的负文字数.

    MCDM方法中,确定属性权重主要有主观赋权法和客观赋权法2种方式. 属性权重对子句的最后排序影响较大,因此,为保证评估的客观性,选择客观赋权法更为合适. 常见的客观赋权方法包括标准离差法[20]、因子分析法[21]、熵权法[22]等. 其中,熵权法因应用广泛、计算和编程实现简单且精度较高而被广泛采用. 熵权法通过属性的离散程度直观地解释权重赋值,易与MCDM方法结合. 因此,本文采用熵权法确定属性权重. 其计算步骤如下:

    步骤1 给定1组候选子句SC={C1,C2,,Cm}和1组属性SG={G1,G2,,GM}M为属性个数). 其评价矩阵中的元素ciji=1,2,,m;j=1,2,,M是候选子句的各属性值.

    步骤2 将各属性的数据分类按式(1)进行归一化处理.

    dij={cijmincijmaxcijmincij,maxcijcijmaxcijmincij, (1)

    式中:dij为[0,1]之间的实数.

    若属性的属性值越大,对子句的评估表现越好,则该属性为正向属性;反之,为负向属性.

    步骤3 根据信息熵的定义,求各属性的熵. 第j个属性的熵值为

    ej=1lnmmi=1pijlnpij (2)

    式中:ej0pij=dij/mi=1dij;当pij=0时,定义pijlnpij=0.

    步骤4 传统计算第j个属性的熵权wj如式(3)所示.

    wj=(1ej)/Mj=1(1ej). (3)

    当各熵值ej趋于1且差异微小时,得到的熵权wj却差异很大. 因此,本文采用式(4)所示的改进熵权计算方法[23]确定属性权重.

    wj=1ej+0.1Mj=1(1ej)Mj=1[1ej+0.1Mj=1(1ej)] (4)

    式中:Mj=1wj=1.

    步骤1 根据式(4)可得每个属性的熵权wj.

    步骤2 计算每对候选子句在各属性下的差异值¯dj(Ci,Cˉr),如式(5)所示. 其中,ˉr{1,2,,m}.

    ¯dj(Ci,Cˉr)=gj(Ci)gj(Cˉr) (5)

    式中:gj(Ci)gj(Cˉr)分别为子句CiCˉr的第j个属性值.

    步骤3 选择合适的偏好函数. Brans等[14]提出6种含参数的偏好函数类型(V-shape、V-shape I、Level、U-shape、Usual 和Gaussian). 根据评估矩阵的信息,偏好函数选取V-shape,如式(6)所示,其中,参数q为每种属性的最大值. 因为不同的属性,其值域有明显差异,所以,不同的属性对应不同的参数. 本文同时也测试了其他参数以及其他类型的偏好函数,如Usual类型的偏好函数,研究发现式(6)的效果最好. 因此,选择式(6)作为本文的偏好函数.

    Pj(Ci,Cˉr)={0,¯dj(Ci,Cˉr)0,¯dj(Ci,Cˉr)/q,0<¯dj(Ci,Cˉr)q,1,¯dj(Ci,Cˉr)>q. (6)

    偏好函数Pj(Ci,Cˉr)表示在第j个属性上子句Ci优先于Cˉr的程度,取值范围为 [0,1].

    步骤4 定义并计算每一对候选子句的偏好指数,偏好指数π(Ci,Cˉr)表示在所有属性上,Ci超过Cˉr的偏好度. 对于任意的ˉri, π(Ci,Cˉr)的定义如式(7)所示,取值范围为 [0, 1].

    π(Ci,Cˉr)=Mj=1Pj(Ci,Cˉr)wj. (7)

    步骤5 定义和计算正负优先流.

    φ+(Ci)=1n1nˉr=1π(Ci,Cˉr), (8)
    φ(Ci)=1n1nˉr=1π(Cˉr,Ci) (9)

    正优先流φ+(Ci)表示Ci优于其他候选子句的程度;φ+(Ci)越大,子句越优. 负优先流φ(Ci)表示Ci劣于其他候选子句的程度;φ(Ci)越小,子句越优. φ+(Ci)φ(Ci)取值范围为[0, 1].

    步骤6 计算候选子句的净占优流.

    净占优流φ(Ci)表示子句的综合优先值,φ(Ci)越大,子句越优,φ(Ci)取值范围为[−1, 1],如式(10)所示.

    φ(Ci)=φ+(Ci)φ(Ci). (10)

    步骤7 对候选子句按净占优流的值从大到小进行排序.

    基于PROMETHEE Ⅱ方法的候选子句选择框架如图1所示. 本文只对5个属性进行评估,根据图1中的计算流程,得出候选子句的完全排序.

    图  1  基于 PROMETHEE Ⅱ的候选子句选择框架
    Figure  1.  Framework diagram for candidate clause selection based on PROMETHEE Ⅱ

    目前,基于S-CS规则研发了多个自动定理证明器,如MC-SCS (multi-clause synergized contradiction separation) [24]和CSE (contradiction separation extension)[25]等. 其中,CSE从2018年开始一直参加国际竞赛CADE (Conference on Automated Deduction) [25]. 为继续提高CSE的性能,本文将MCDM方法应用到CSE 1.5自动定理证明器,记作MCDM_CSE,其流程如图2所示.

    图  2  基于 PROMETHEE Ⅱ的 S-CS 算法流程
    Figure  2.  Flowchart of S-CS algorithm based on PROMETHEE Ⅱ

    将基于MCDM方法的S-CS演绎算法流程中选择的第一个参与矛盾体分离演绎的子句称为起步子句. 根据S-CS演绎时间决定是否使用新的PROMETHEE Ⅱ方法评估子句,如每隔20 s使用PROMETHEE Ⅱ方法评估子句.

    基于S-CS规则的PROMETHEE Ⅱ子句评估方法的主要优势如下:1) MCDM方法可组合多种子句属性,评估出当前演绎步骤中的最优子句. 相比优先级子句选择方法,MCDM方法更高效,对子句评估更灵活. 2) 可增加、删减、更换属性.属性的选取非常重要,所选属性的数量会直接影响评价矩阵,从而影响对子句的评估结果. 3) 克服主观因素对权重的影响. 采用熵权法客观确定属性权重,有效避免了人为因素的影响. 针对不同的子句集,其评价矩阵不同,因此相应属性权重也不同. 4) 使用多属性决策方法的次数可动态调整,可控性更强. 随着演绎过程中属性值的动态变化,更新评价矩阵,再动态使用多属性决策方法.

    本文对2022年国际竞赛CADE 中FOF (First-Order Form) 组的500个定理和TPTP-v8.1.0 (Thousands of Problems for Theorem Provers)[26]问题库中FOF格式的9091个定理以及最难的定理进行证明. TPTP问题库中每个定理对应一个rating值参数,代表定理的难度等级. 定理的难度等级是[0, 1]中的实数,rating = 0的定理能被所有自动定理证明器证明,rating = 1的定理目前不能被任何自动定理证明器证明. TPTP问题库也对每个定理进行了分类,如SET表示集合论定理,SWV表示软件验证类的定理. 为评估本文多属性决策方法的有效性,该方法被加入到Vampire 4.7[27]和Eprover (E 2.6)[28],自动定理证明器记作MCDM_V 和MCDM_E.

    实验硬件环境为3.4 GHz Inter (R) Core (TM) i7-6700处理器,11.1GB内存,操作系统为Ubuntu15.04 64位. 证明每个定理的时间为国际竞赛标准时间300 s. 本文所有的自动定理证明器在相同的测试环境下进行测试. Prover9[29] 和Otter[30]均可检查证明过程的正确性,而Prover9自动定理证明器是在Otter自动定理证明器基础上改进的,并一直参与国际竞赛,所以Prover9作为本实验S-CS演绎过程的验证工具.

    MCDM_CSE自动定理证明器证明的定理个数为2586个,比CSE 1.5多证明151个. 其中,CSR、GEO、SET、NUM、SEU、SWV、KRS、SWC和SYN这9类定理的证明数量均超过 100 个. 分析实验数据发现,除SYN以外,其他8类定理的证明个数在MCDM_CSE中均超过CSE 1.5,尤其是NUM多证明了38个. 因此,MCDM_CSE比CSE 1.5的性能更好. 特别地,CSR、GEO、SET、NUM、SEU这5类定理证明的个数均不低于200个.

    MCDM_CSE和CSE 1.5在不同难度等级下证明的定理数量对比如表1所示. 每个定理的证明时间均在300 s内,MCDM_CSE证明的数量比CSE 1.5多151个. 当rating值不低于0.1时,MCDM_CSE证明的定理数量均超过了CSE 1.5,表明MCDM_CSE的能力优于CSE 1.5.PROMETHEE Ⅱ方法能有效提升CSE 1.5的性能.

    表  1  MCDM_CSE和CSE 1.5在不同难度等级下证明的定理数量对比
    Table  1.  Comparison of the number of theorems proved by MCDM_CSE and CSE 1.5 at different difficulty levels
    难度等级 MCDM_CSE CSE 1.5
    [0, 0.10) 1061 1073
    [0.10,0.50) 1338 1212
    [0.50,0.60) 98 79
    [0.60,0.70) 43 39
    [0.70,0.80) 22 16
    [0.80,0.90) 13 11
    [0.90,1.00) 8 5
    1.00 3 0
    下载: 导出CSV 
    | 显示表格

    分析结果表明,多属性决策子句评估方法发挥了关键作用. 对于CSE 1.5不能证明的151个定理,多属性决策方法能缩短定理判定的总时间,使得这些定理能在300 s内被MCDM_CSE证明. 在证明定理效率方面,CSE 1.5的平均时间为26.19 s,而MCDM_CSE平均时间为25.24 s. 相比CSE 1.5, MCDM_CSE提高了1540个定理的证明效率.

    表2列出6个被MCDM_CSE证明但未被CSE 1.5证明的定理,这些定理的难度等级均大于 0.90,平均证明时间为132.34 s. 这表明 MCDM_CSE 对较难定理的证明具有良好表现. 尤其值得注意的是,其中有 3 个定理的难度等级为 1.00,目前尚无其他 ATP 能证明这些定理.

    表  2  MCDM_CSE证明难度大于0.90的定理所需的证明时长
    Table  2.  Time consumed by MCDM_CSE to prove theorems with difficulty greater than 0.90
    定理名称 难度等级 证明时间/s
    SEU413 + 2 0.92 26.81
    SWB088 + 1 0.97 137.78
    SWB090 + 1 0.97 126.04
    NUM736 + 4 1.00 65.49
    SYO625-1 1.00 219.51
    SYO587 + 1 1.00 218.41
    下载: 导出CSV 
    | 显示表格

    表3为MCDM_CSE已证明的2586个定理在国际知名自动定理证明器中的对比情况. Vampire 自 2002 年起一直是国际自动定理证明器竞赛 (FOF 组) 的冠军,E 多年稳居亚军或季军,而 Prover9 被广泛视为衡量 ATP 能力的基准自动定理证明器. 因此,本文选取这3个证明器作为比较对象. 结果显示,Vampire 4.7有5个定理不能证明, E 2.6有41个定理不能证明, Prover9有293个定理不能证明.

    表  3  对已证明定理(按难度等级)在国际知名自动定理证明器中证明数量的比较
    Table  3.  Comparison of the number of theorems (by difficulty level) proved by internationally known ATPs
    自动定理证
    明器
    难度等级
    [0,0.70) [0.70,0.80) [0.80,0.90) [0.90,1.00]
    MCDM_CSE 2540 22 13 11
    Vampire 4.7 2539 21 13 8
    E 2.6 2532 12 1 0
    Prover9 2264 13 8 8
    下载: 导出CSV 
    | 显示表格

    为进一步评估多属性决策方法的有效性,本文测试了2022年CADE竞赛的500个竞赛例,测试的自动定理证明器为MCDM_V、 MCDM_E、Vampire 4.7和E 2.6.

    表4为各自动定理证明器在2022年CADE竞赛的比较结果. MCDM_V 证明了462个定理,比Vampire 4.7多6个. MCDM_E证明了387个定理,比E 2.6多7个. 因此,本文的多属性决策评估子句的方法能有效地评估子句,能提高Vampire 4.7和E 2.6的能力. 在效率方面,MCDM_V证明462个定理的平均时间为15.30 s,比Vampire 4.7少0.80 s. MCDM_E证明387个定理的平均时间为27.40 s,比E 2.6少4.30 s. 实验表明,多属性决策评估子句方法能节省子句评估时间.

    表  4  2022年CADE竞赛的比较结果
    Table  4.  Comparative results on the CADE 2022 competition
    自动定理证明器 平均时间/s 证明个数/个
    MCDM_V 15.3 462
    Vampire 4.7 16.1 456
    MCDM_E 27.4 387
    E 2.6 31.7 380
    下载: 导出CSV 
    | 显示表格

    图3表示在300 s内每个自动定理证明器证明定理的实验结果,横轴表示证明的定理个数,纵轴表示证明定理所需的CPU时间. 从图3可以看出,在相同时间内(同一水平线),MCDM_E的曲线几乎在E 2.6的右边或与E 2.6重合,MCDM_V的曲线几乎在Vampire 4.7的右边或与Vampire 4.7重合. 并且通过分析实验数据发现,相比E 2.6,MCDM_E提高了证明79个定理的效率;相比Vampire 4.7, MCDM_V提高了28个定理的效率. 因此,多属性决策方法能提高自动定理证明器的能力和效率.

    图  3  不同ATP在2022年CADE竞赛的CPU时间比较
    Figure  3.  Comparison of CPU time of different ATPs for the CADE 2022 competition

    为削弱主观因素对子句评估的影响,通过充分利用多种子句属性信息对子句进行客观评估,本文提出一种用于动态综合评估子句的多属性决策方法.实验结果表明,本文提出的方法能提高自动定理证明器的性能,主要贡献如下:

    1) 本文提出一种新的子句选择方法,结合S-CS规则的特性,应用PROMETHEE Ⅱ方法得到子句的完全排序,从而选择最优的候选子句参与S-CS演绎.

    2) 针对PROMETHEE Ⅱ方法中属性权重的确定,采用熵权法(客观赋权法)计算属性权重,避免人为因素造成偏差.

    3) 将PROMETHEE Ⅱ方法应用到自动定理证明器CSE 1.5、Vampire 4.7和E 2.6中. 实验表明,该方法有效提高了证明器的性能,尤其在子句的选择方面发挥重要作用,能更精确地评估子句,有利于子句的选择.

    4) 针对多个属性值相同的子句,PROMETHEE Ⅱ方法可以进行完全排序,从而选择更适合的子句参与S-CS演绎,有效避免按照优先级对子句进行多次比较.

    综上所述,多属性决策子句评估方法均能提高CSE 1.5、Vampire 4.7和E 2.6的性能,但仍有一些不足之处可改进. 如可以按照TPTP库的定理类型进行评估,以及增加对文字的评估.

  • 图 1  桩基式海上风机

    Figure 1.  Pile foundation type offshore wind turbine

    图 2  波浪-多孔介质海床-单桩相互作用三维示意

    Figure 2.  3D sketch of wave-porous seabed-monopile- interactions

    图 3  多孔介质孔隙流动体积平均法示意

    Figure 3.  Sketch of pore volume average method forporous media

    图 4  海绵层消波原理

    Figure 4.  Wave attenuation of sponge layer

    图 5  网格划分及FAVOR显示图

    Figure 5.  Mesh generation and FAVOR display

    图 6  数值波剖面对比结果

    Figure 6.  Comparision of numerical wave profiles

    图 7  波浪沿多孔介质海床衰减数值结果与相应试验结果对比

    Figure 7.  Comparison of numerical results for wave dampingalong the porous seabed with the correspondingexperimental results

    图 8  单桩所受波浪力时程曲线

    Figure 8.  Time history curves of wave forces acting on monopile

    图 9  Fx,max随海床孔隙率的变化曲线

    Figure 9.  Variation curve of maximum wave force inthe x axis with seabed porosity

    图 10  Fx的时程曲线

    Figure 10.  Time history curves of wave force in the x axis

    图 11  Fx,max随多孔介质海床颗粒直径的变化曲线

    Figure 11.  Variation curve of maximum wave force in the x axis with partical size

    图 12  不同海床孔隙率条件下Fx,max随海床相对厚度的变化曲线

    Figure 12.  Variation curves of maximum wave force inthe x axis with seabed relative thickness with different seabed porosity

    图 13  不同双层海床孔隙率特性下Fx,max随海床厚度的变化曲线

    Figure 13.  Variation curves of maximum wave force in the x axis with seabed thickness with different porosity in two-layered seabed

  • 王伟, 杨敏. 海上风电机组地基基础: 设计理论与工程应用[M]. 北京: 中国建筑工业出版社, 2014: 1-20
    LOSADA I J, LARA J L, JESUS M D. Modeling the interaction of water waves with porous coastal structures[J]. Journal of Waterway,Port,Coastal,and Ocean Engineering, 2016, 142(6): 1-18.
    PUTNAM J A. Loss of wave energy due to percolation in a permeable sea bottom[J]. Transactions,American Geophysical Union, 1949, 30(3): 349-356. doi: 10.1029/TR030i003p00349
    LIU P F. Damping of water waves over porous bed[J]. Journal of the Hydraulics Division, 1973, 99: 2263-2271.
    SAVAGE R P, FAIRCHILD J C. Laboratory study of energy losses by bottom friction and percolation[J]. Beach Erosion Board,Corps of Engineers,Technical Memorandum, 1953, 31: 1-25.
    LIU P L F, DALRYMPLE R A. The damping of gravity waves due to percolation[J]. Coastal Engineering, 1984, 8(1): 33-49. doi: 10.1016/0378-3839(84)90021-8
    KARUNARATHNA S, LIN P Z. Numerical simulation of wave damping over porous seabeds[J]. Coastal Engineering, 2006, 53(10): 845-855. doi: 10.1016/j.coastaleng.2006.05.003
    MORISON J R, JOHNSON J W, SCHAAF S A. The force exerted by surface waves on piles[J]. Journal of Petroleum Technology, 1950, 2(5): 149-154. doi: 10.2118/950149-G
    MACCAMY R C, FUCHS R A. Wave forces on piles:a diffraction theory[J]. Beach Erosion Board, 1954, 69: 100-103.
    李世森,张伟,秦崇仁. 大直径圆筒结构上波浪力的数值模拟与实验研究[J]. 中国港湾建设,2003(2): 11-16. doi: 10.3969/j.issn.1003-3688.2003.02.004

    LI Shisen, ZHANG Wei, QIN Chongren. Numerical simulation and experimental study of wave force on large diameter cylindrical structure[J]. China Harbour Engineering, 2003(2): 11-16. doi: 10.3969/j.issn.1003-3688.2003.02.004
    祝兵,宋随弟,谭长建. 三维波浪作用下大直径圆柱绕流的数值模拟[J]. 西南交通大学学报,2012,47(2): 224-229.

    ZHU Bing, SONG Suidi, TAN Changjian. Numerical simulation for diffraction around large-diameter circular cylinder subjected to three-dimension wave[J]. Journal of Southwest Jiaotong University, 2012, 47(2): 224-229.
    张文娟,王媛,倪小东. Forchheimer型非达西渗流参数特征分析[J]. 水电能源科学,2014(1): 52-54,164.

    ZHANG Wenjuan, WANG Yuan, NI Xiaodong. Analysis of parameters characteristics of Forchheimer’s non-Darcy seepage[J]. Water Resources and Power, 2014(1): 52-54,164.
    BOUSSINESQ J. Theory of wave and swells propagated in long horizontal rectangular canal and imparting to the liquid contained in this canal[J]. Journal of Mathematiques Pures et Appliquees, 1872, 17(2): 55-108.
    RODI W. Turbulence models and their application in hydraulics: a state of the art review[M]. 3rd edition. Rotterdam: CRC Press, 1984: 26-33
    LAUNDER B E, SPALDING D B. The numerical computation of turbulence flows[J]. Computer Methods in Applied Mechanics and Engineering, 1974, 3(1): 269-289.
    CARMAN P C. Fluid flow through granular beds[J]. Transactions of the Institution of Chemical Engineering, 1937, 15(1): 150-167.
    DEAN R G. Relative validation of water wave theories[J]. Journal of the Waterways,Harbors and Coastal Engineering Division, 1970, 96(1): 105-119.
    FENTON J D. A fifth-order stokes theory for steady waves[J]. Journal of Waterway,Port,Coastal,and Ocean Engineering, 1985, 111(2): 216-234.
    ORLANSK I. A simple boundary condition for unbounded hyperbolic flows[J]. Journal of Computational Physics, 1976, 21(3): 251-269. doi: 10.1016/0021-9991(76)90023-1
    HIRT C W, NICHOLS B D. Volume of fluid (VOF) method for the dynamics of free boundaries[J]. Journal of Computational Physics, 1981, 39(1): 201-225. doi: 10.1016/0021-9991(81)90145-5
  • 加载中
图(13)
计量
  • 文章访问数:  500
  • HTML全文浏览量:  261
  • PDF下载量:  4
  • 被引次数: 0
出版历程
  • 收稿日期:  2017-11-10
  • 修回日期:  2018-04-03
  • 网络出版日期:  2018-04-03
  • 刊出日期:  2019-04-01

目录

/

返回文章
返回