Processing math: 100%
  • 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]. 西南交通大学学报. doi: 10.3969/j.issn.0258-2724.20230584
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: JIANG Yuan, LIU Jinyang, HUI Yi, LIU Rui. Impact of Horizontal Ribs on Aerodynamic Characteristics of High-Rise Buildings[J]. Journal of Southwest Jiaotong University. doi: 10.3969/j.issn.0258-2724.20230584

水平肋板对高层建筑气动特性的影响研究

doi: 10.3969/j.issn.0258-2724.20230584
基金项目: 国家自然科学基金项目(52078087)
详细信息
    作者简介:

    蒋媛(1986—),女,高级工程师,研究方向为建筑风工程,E-mail:42239064@qq.com

    通讯作者:

    刘锦阳(1991—),男,讲师,博士,研究方向为建筑风工程,E-mail:2296454851@qq.com

  • 中图分类号: TU355

Impact of Horizontal Ribs on Aerodynamic Characteristics of High-Rise Buildings

  • 摘要:

    为分析高层建筑上外伸肋板的抗风工作机理,利用大涡模拟(LES)评估大气边界层来流下水平肋板对高层建筑的流场和风荷载的影响,对比不同类型水平肋板的抗风效果. 结果表明:水平肋板明显抑制了侧风面分离涡的形成,并拉长了尾涡;肋板会显著抑制建筑附近的竖向流,并在其附近诱导形成局部旋涡,最终导致近壁流动形式明显变化;流场的变化会影响风压分布和风荷载,水平肋板使建筑表面平均风压系数沿高度呈“之”字形分布,水平板明显降低侧壁面上平均和脉动风压,最大降幅分别约为20%和17%;对总荷载而言,水平肋板对平均阻力无明显影响,但能明显降低建筑上的脉动升力,最大降幅为27%;肋板的布置形式对气动特性的影响有明显差异,连续水平板通过改变近壁流、涡结构来影响风压分布和风荷载,而间隔水平板对风荷载的影响相对较弱.

     

  • 一阶逻辑是经典的逻辑理论,基于一阶逻辑的定理机器证明和自动推理是人工智能领域的重要研究课题. 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.  Sketch of models

    图 2  网格布局和计算域

    Figure 2.  Mesh configuration and computing domain

    图 3  风场特征

    Figure 3.  Wind field characteristics

    图 4  方柱压力分布及验证[22-23]

    Figure 4.  Pressure distribution on square column and verification

    图 5  不同高度处水平截面上的平均流线和平均流速

    Figure 5.  Mean streamlines and mean flow velocity on horizontal sections at different heights

    图 6  竖直截面上(y = 0D)的平均流线和平均流速

    Figure 6.  Mean streamlines and mean flow velocity on vertical sections (y = 0D

    图 7  迎风面中心线上风压分布

    Figure 7.  Distribution of wind pressure on windward centerline

    图 8  侧风面上风压分布

    Figure 8.  Distribution of wind pressure on sidewall

    图 9  模型表面平均风压分布

    Figure 9.  Mean wind pressure distribution on model surface

    表  1  肋板尺寸信息

    Table  1.   Dimension information of ribs

    模型编号 d/D/% b/D//% h/D//%
    1 6 50.0
    2 6 25.0
    3 6 12.5
    4 6 20 25.0
    5 6 60 25.0
    下载: 导出CSV

    表  2  网格信息

    Table  2.   Mesh information

    网格 最小网格 最大网格 数量/百万
    x/y z x/y z
    网格 1 1/62.5D 1/300D 0.6D 1D 3.7
    网格 2 1/125.0D 1/600D 0.6D 1D 7.2
    网格 3 1/250.0D 1/1200D 0.6D 1D 13.6
    下载: 导出CSV

    表  3  参考方柱LES结果及验证

    Table  3.   LES results of square column and verification

    方法 文献 Re/104 AR ¯Cd Cd1 Cl1 St
    LES 网格 1 5.5 4 1.220 0.09 0.330 0.100
    网格 2 5.5 4 1.147 0.10 0.300 0.096
    网格 3 5.5 4 1.156 0.11 0.310 0.094
    试验 文献 [22] 5.5 4 1.200 0.410 0.100
    文献 [23] 5.0 4 1.280 0.13 0.320 0.085
    文献 [24] 6.0 4 1.270 0.08 0.296 0.097
    文献 [25] 7.3 3 1.290 0.102
    文献 [11] 5.5 5 0.930 0.350 0.100
    文献 [10] 5.5 5 1.080
    下载: 导出CSV

    表  4  参考方柱和模型1~3的风荷载系数

    Table  4.   Wind load coefficients for square column and models 1–3

    名称 ¯Cd Cd1 Cl1
    方柱 1.147 0.100 0.300
    模型 1 0.146 0.102 0.232
    模型 2 0.149 0.102 0.219
    模型 3 0.145 0.101 0.218
    下载: 导出CSV

    表  5  模型2、4、5的风荷载

    Table  5.   Wind loads of models 2, 4, 5

    名称 ¯Cd Cd1 Cl1
    模型 2 1.149 0.102 0.219
    模型 4 1.156 0.106 0.229
    模型 5 1.153 0.103 0.261
    下载: 导出CSV
  • [1] 张正维,全涌,顾明,等. 锥度化方形截面高层建筑的气动力特性[J]. 西南交通大学学报,2014,49(5): 772-778. doi: 10.3969/j.issn.0258-2724.2014.05.005

    ZHANG Zhengwei, QUAN Yong, GU Ming, et al. Aerodynamic characteristics of tapered tall buildings with square section[J]. Journal of Southwest Jiaotong University, 2014, 49(5): 772-778. doi: 10.3969/j.issn.0258-2724.2014.05.005
    [2] 曾加东,李明水. 矩形断面高层建筑脉动风荷载频谱特性研究[J]. 西南交通大学学报,2017,52(1): 83-90. doi: 10.3969/j.issn.0258-2724.2017.01.012

    ZENG Jiadong, LI Mingshui. Experimental study of spectral characteristics of fluctuating wind loads on high-rise building with rectangular section[J]. Journal of Southwest Jiaotong University, 2017, 52(1): 83-90. doi: 10.3969/j.issn.0258-2724.2017.01.012
    [3] 黄东梅,何世青,朱学,等. 表面粗糙度对超高层建筑风荷载与风振响应的影响[J]. 湖南大学学报(自然科学版),2017,44(9): 41-51.

    HUANG Dongmei, HE Shiqing, ZHU Xue, et al. Influence of surface roughness on wind load and wind-induced response of super-tall building[J]. Journal of Hunan University (Natural Sciences), 2017, 44(9): 41-51.
    [4] MARUTA E, KANDA M, SATO J. Effects on surface roughness for wind pressure on glass and cladding of buildings[J]. Journal of Wind Engineering and Industrial Aerodynamics, 1998, 74/75/76: 651-663.
    [5] CHAND I, BHARGAVA P K, KRISHAK N L V. Effect of balconies on ventilation inducing aeromotive force on low-rise buildings[J]. Building and Environment, 1998, 33(6): 385-396. doi: 10.1016/S0360-1323(97)00054-1
    [6] ZHENG X, MONTAZERI H, BLOCKEN B. CFD analysis of the impact of geometrical characteristics of building balconies on near-façade wind flow and surface pressure[J]. Building and Environment, 2021, 200: 107904.1-107904.19.
    [7] MONTAZERI H, BLOCKEN B. CFD simulation of wind-induced pressure coefficients on buildings with and without balconies: validation and sensitivity analysis[J]. Building and Environment, 2013, 60: 137-149. doi: 10.1016/j.buildenv.2012.11.012
    [8] YUAN K, HUI Y, CHEN Z Q. Effects of facade appurtenances on the local pressure of high-rise building[J]. Journal of Wind Engineering and Industrial Aerodynamics, 2018, 178: 26-37. doi: 10.1016/j.jweia.2018.05.004
    [9] HUI Y, YUAN K, CHEN Z Q, et al. Characteristics of aerodynamic forces on high-rise buildings with various façade appurtenances[J]. Journal of Wind Engineering and Industrial Aerodynamics, 2019, 191: 76-90. doi: 10.1016/j.jweia.2019.06.002
    [10] CHENG X, HUANG G Q, YANG Q S, et al. Influence of architectural facades on wind pressures and aerodynamic forces of tall buildings[J]. Journal of Structural Engineering, 2021, 147(1): 04020303.1-04020303.14
    [11] YANG Q S, LIU Z H, HUI Y, et al. Modification of aerodynamic force characteristics on high-rise buildings with arrangement of vertical plates[J]. Journal of Wind Engineering and Industrial Aerodynamics, 2020, 200: 104155.1-104155.18.
    [12] AI Z T, MAK C M, NIU J L. Numerical investigation of wind-induced airflow and interunit dispersion characteristics in multistory residential buildings[J]. Indoor Air, 2013, 23(5): 417-429. doi: 10.1111/ina.12041
    [13] ZHENG X, MONTAZERI H, BLOCKEN B. CFD simulations of wind flow and mean surface pressure for buildings with balconies: comparison of RANS and LES[J]. Building and Environment, 2020, 173: 106747.1-106747.17.
    [14] KUMAR A, RAHUL P S, KUMAR S. Performance optimization of tall buildings subjected to wind—an Indian scenario[C]//Proceedings of the Eighth Asia-Pacific Conference on Wind Engineering. Singapore: Research Publishing Services, 2013: 817-826.
    [15] LIU J Y, HUI Y, YANG Q S, et al. Flow field investigation for aerodynamic effects of surface mounted ribs on square-sectioned high-rise buildings[J]. Journal of Wind Engineering and Industrial Aerodynamics, 2021, 211: 104551.1-104551.9.
    [16] LIU J Y, HUI Y, WANG J X, et al. LES study of windward-face-mounted-ribs’ effects on flow fields and aerodynamic forces on a square cylinder[J]. Building and Environment, 2021, 200: 107950.1-107950.14.
    [17] LIU J Y, HUI Y, LI S K, et al. Numerical studies on aerodynamic forces and flow control regimes of square cylinder with four surface ribs[J]. Computers & Fluids, 2022, 245: 105609.1-105609.13.
    [18] HUI Y, LIU J Y, WANG J X, et al. Effects of facade rib arrangement on aerodynamic characteristics and flow structure of a square cylinder[J]. Building and Environment, 2022, 214: 108924.1-108924.13.
    [19] LAM K, LIN Y F. Large eddy simulation of flow around wavy cylinders at a subcritical Reynolds number[J]. International Journal of Heat and Fluid Flow, 2008, 29(4): 1071-1088. doi: 10.1016/j.ijheatfluidflow.2008.01.006
    [20] YANG Q S, ZHOU T, YAN B W, et al. LES study of turbulent flow fields over hilly terrains—comparisons of inflow turbulence generation methods and SGS models[J]. Journal of Wind Engineering and Industrial Aerodynamics, 2020, 204: 104230.1-104230.22.
    [21] ABOSHOSHA H, ELSHAER A, BITSUAMLAK G T, et al. Consistent inflow turbulence generator for LES evaluation of wind-induced responses for tall buildings[J]. Journal of Wind Engineering and Industrial Aerodynamics, 2015, 142: 198-216. doi: 10.1016/j.jweia.2015.04.004
    [22] MARUYAMA Y, TAMURA T, OKUDA Y, et al. LES of fluctuating wind pressure on a 3D square cylinder for PIV-based inflow turbulence[J]. Journal of Wind Engineering and Industrial Aerodynamics, 2013, 122: 130-137. doi: 10.1016/j.jweia.2013.07.001
    [23] CAO Y, TAMURA T, KAWAI H. Investigation of wall pressures and surface flow patterns on a wall-mounted square cylinder using very high-resolution Cartesian mesh[J]. Journal of Wind Engineering and Industrial Aerodynamics, 2019, 188: 1-18. doi: 10.1016/j.jweia.2019.02.013
    [24] SAKAMOTO H, OIWAKE S. Fluctuating forces on a rectangular prism and a circular cylinder placed vertically in a turbulent boundary layer[J]. Journal of Fluids Engineering, 1984, 106(2): 160-166. doi: 10.1115/1.3243093
    [25] MCCLEAN J F, SUMNER D. An experimental investigation of aspect ratio and incidence angle effects for the flow around surface-mounted finite-height square prisms[J]. Journal of Fluids Engineering, 2014, 136(8): 081206.1-081206.10.
  • 加载中
图(9) / 表(5)
计量
  • 文章访问数:  115
  • HTML全文浏览量:  56
  • PDF下载量:  26
  • 被引次数: 0
出版历程
  • 收稿日期:  2023-11-02
  • 修回日期:  2024-01-07
  • 网络出版日期:  2024-10-31

目录

/

返回文章
返回